# §9 · Durability semantics

> **Status: DRAFT.** The classification, its lattice, and where the compiler places a durable step are probed —
> the first two through `osy model --json`, the third read from the resolver that performs the lowering. What a
> **crash** actually does is runtime behaviour and is **UNVERIFIED here**; §9.7 names the guards.

§11.1 and §11.2 both refuse a C# construct "because a call can suspend and resume in a different process". This
section is that claim, stated properly. It is the reason the language has no `out` parameter and no `async`.

## 9.1 The premise

**Normative.** A call MUST NOT assume that the process which began it is the process which finishes it.

Everything below follows from that one sentence. An Osy# call may suspend — for a timer, for a human, for a child
workflow — and resume later, elsewhere. So the stack frame is not a durable place: nothing may be written back into
it (§11.1), and nothing may be scheduled against it (§11.2).

⭐ **The interesting consequence is that a re-run is normal, not exceptional.** A continuation-based engine replays
nothing wholesale, but it does re-execute in two places: a statement is replayed after an in-process sub-call
returns, and a statement that suspended is re-entered on resume. So "what does it cost to run this leaf twice" is a
question the engine must be able to ask of every leaf in the program — which is what §9.2 is.

## 9.2 The durability classification

Every leaf the language provides carries one of three values.

| value | a re-run… | so it is |
|---|---|---|
| **Deterministic** | reproduces its value, and nothing escaped | free — never recorded |
| **Nondeterministic** | yields a *different* value, but nothing left the platform | memoized on the per-statement node memo |
| **External** | is a **second real-world effect** — a second charge, a second enqueue | given its own durable step |

*Source: `StdlibDurability`, `Platform.Core/Dsl/OsySharp/Stdlib/OsySharpStdlib.cs`.*

**Normative.** The three values form a **total order** — `Deterministic < Nondeterministic < External` — and the
durability of a construct MUST be the maximum over its parts. That is what makes the classification usable as a
lattice over whole programs rather than only over the leaves it was defined on.

⚠ **`External` is about *whose* system rolls back, not about I/O.** A commit to the application's own database is
`Nondeterministic`: the platform owns the transaction. `File.WriteAllText` is `External`: the filesystem does not
roll back because a later segment failed.

## 9.3 Asking a program what it costs

**Normative.** An implementation MUST report the classification, and MUST report a witness for it.

⚑ **Probed 2026-08-27.** For a function whose body is `Security.RandomId()` and then `File.WriteAllText(path, id)` —
a `Nondeterministic` leaf written *first* and an `External` leaf written *second* — `osy model --json` reports:

```
Archive   direct: External   durabilityVia = File.WriteAllText
Wrapper   direct: Deterministic          via = (none)
          trans : External   durabilityVia = Archive → File.WriteAllText
```

Three separable facts, each of which a reader would plausibly guess wrong:

1. **The lattice wins over source order.** `External` is reported although the nondeterministic call is written
   first. The value is a max, not a last-writer.
2. **`durabilityVia` is a path, not a name.** Through a call graph it reads `Archive → File.WriteAllText` — the
   route by which a plain-looking call reaches an egress. This is the field that makes the classification
   *actionable* rather than merely present.
3. **`effects` and `transitive` are different answers and both are given.** `Wrapper` calls nothing but `Archive`:
   it is `Deterministic` **directly** and `External` **transitively**. A reader who consults only one of them will
   be wrong about half the functions in any real program.

## 9.4 Where a durable step goes — the leaf, never the function

**Normative.** An implementation MUST place the exactly-once boundary at the **egress leaf**, not at the enclosing
function.

⭐ **This is the load-bearing design decision of the whole section.** If `Notify(u)` makes external calls A and then
B, and the whole of `Notify` is one coarse step, a crash between A and B re-runs A on resume — a double send. Each
egress is therefore its own step, and the deterministic orchestration between them re-runs freely, being a pure
function of the memoized results.

**It is automatic.** The resolver wraps every `External` leaf in a durable step during lowering. An author writes
`Http.Get(url)` and gets exactly-once without naming it. `Workflow.Once("key", …)` remains available for a step the
author wants to name or key, and an already-stepped leaf is not wrapped twice.

⚠ **So the transitive lattice of §9.3 does not decide anything.** It is an *author-facing* signal — "this
plain-looking call reaches an egress". Step placement is a purely **local** decision at each leaf. Reading the
lattice as the mechanism gets the model backwards, and is the likeliest misreading of this section.

**A nondeterministic leaf gets no step, deliberately.** `DateTime.UtcNow` and `Guid.NewGuid` ride the per-statement
node memo, which already serialises into the continuation. Giving each one its own out-of-band database write would
be a real cost for a guarantee they already hold. Only egress — where the second execution reaches *someone else's*
system — earns one.

⚑ **An unclassified target defaults to `External`.** A leaf missing from the durability table is treated as egress,
so an omission over-protects rather than under-protects. *Informative:* the platform has been bitten by the
resulting symptom more than once, which is itself the argument for the default being this way round.

## 9.5 A step wraps one thing

```osy probe=accepts
int Charge(int amount) { return Workflow.Once("charge", () => amount * 2); }
```

```osy probe=refuses RESOLVE_ERROR
int Charge(int amount) { return Workflow.Once("charge", () => { var a = amount; return a; }); }
```

A step body is an **expression**. Statements go in a function, which the step then calls.

⚠ *Informative, and honest about a rough edge:* the refusal above is real and stable, but its diagnostic explains
itself in terms of **query** lambdas ("a block can't lower to SQL in a query predicate") because block-bodied
lambdas are refused language-wide from one site. At a durable-step call site that reason is not the applicable one.
The refusal is right; the explanation is aimed elsewhere. Recorded as a §12 diagnostics concern.

## 9.6 `await` means *park*

Restating §11.2 from this side, because it only makes sense here: `await Workflow.Run(…)` does not yield a thread.
It **parks the run durably** — possibly for days — and resumes it in whatever process next picks it up. The keyword
is reused because the English reading is right; the mechanism is this engine, not a task scheduler.

## 9.7 What this section does NOT establish

**UNVERIFIED, deliberately.** Every claim above is about what the compiler *classifies* and *lowers*. None of it
establishes what a crash does. Specifically unproven here:

- that a step's result survives a process restart and is not re-executed on resume;
- that a memoized nondeterministic value is the *same* value after resume;
- that a durable step commits out-of-band, so a crash before the enclosing segment commits still finds it.

Those need runtime tests. The guards that exist are `AutoDurableLoweringTests` (the leaf-level wrap),
`WorkflowOnceDurableStepTests` and `WorkflowStepMemoIdentityTests` (memo identity across a resume),
`DurableFunctionRunnerTests` (resume itself), and `FunctionEffectsDurabilityTests` with
`OsySharpStdlibDurabilityTests` (the classification and its rollup). **A future revision MUST cite which of them
proves which of the three claims above, or drop the claim.**

---

**Next:** §8 Security as a language rule — the other declaration-time rule, and the one with the most surface.
Not started.