docs: settle how a machine's events state the next state

ROADMAP.md

@@ -30,7 +30,8 @@ Taken on 2026-11-12:
     them in one step. Exploring every reachable state, or exploring within a
     bound, is recorded on the unproved obligation and is never an outcome.
   - **`accord build`** writes a machine only when its invariants are
-    proved. The boundary checks a state's types and its invariants.
+    proved. The boundary checks a state's types and its invariants,
+    helper invariants included.
   - **opossum is ported faithfully.** Its breaker closes on any success
     while half-open. Its threshold is compared exactly, and fractional
     thresholds are rejected. The invariants proved are the ones #82 names.

docs/design/native-code-constraints.md

@@ -170,7 +170,7 @@ before the stage that first depends on it. Rows are in dependency order.
 | 7 | Proving calls: callers rely on the callee's contract, not its body | Enforced: at each call, the callee's `requires` is an obligation and its `ensures` an assumption; recursion is rejected (`conformance/cases/call*.accord`) | 1, 2, 4 | Calls between functions | The cost of proofs, separate compilation, inlining |
 | 8 | Normalization and hashing | Enforced. A machine's fields and events are normalized by position, as parameters and variants are (stage 10, approved) | 1 | Any change to the normal form | Every stored hash and piece of evidence |
 | 9 | An identity for a specification apart from its implementation | Partly enforced: a caller's proofs bind to a hash of the callee's contract, so a change to the callee's body alone leaves them current (`identity.rs` tests). How approval binds is undecided | 7, 8 | Several implementations of one specification | How approval and evidence bind |
-| 10 | The boundary contract: what is checked and which error a failed check returns | Decided: [types, ranges and each `requires`](../typescript.md#the-boundary), with `TypeError` or `RangeError`. A machine's state crosses as an object of its fields in `camelCase`, checked for types, ranges and every invariant; each event is an exported function from the state and its parameters to the next state, and each observer one from the state (stage 10, approved) | 1, 5, 6 | Stage 8's first published output | A public interface, once others call it |
+| 10 | The boundary contract: what is checked and which error a failed check returns | Decided: [types, ranges and each `requires`](../typescript.md#the-boundary), with `TypeError` or `RangeError`. A machine's state crosses as an object of its fields in `camelCase`, checked for types, ranges and every invariant, helper invariants included; each event is an exported function from the state and its parameters to the next state, and each observer one from the state (stage 10, approved) | 1, 5, 6 | Stage 8's first published output | A public interface, once others call it |
 
 ## Keep these optimizations possible
 

docs/design/probes/2026-11-12-machine-updates/README.md

@@ -0,0 +1,132 @@
+# Probe: how a machine's updates are written (2026-11-12)
+
+An informal probe to guide stage 10's syntax for updates in `machine`
+events ([#82](https://github.com/sequelcore/accord/issues/82)). Its
+questions, answer key and decision rule were written before any run. It is
+not a registered experiment: it has no pass mark, and its result guides the
+design without counting as evidence that the syntax is understood.
+
+## Question
+
+Do readers who have never seen Accord predict a machine's next state
+correctly, and which reading does each way of writing an update suggest:
+that a later expression in the same event sees the old value, or the new
+one?
+
+## Method
+
+Tesota's ProviderRetry model as an Accord machine, written in three versions
+([`variants/`](variants)), identical except for how an event states the next
+value of a field:
+
+| Version | Form |
+| --- | --- |
+| A | `phase = Waiting`, one update per line |
+| B | `next { phase: Waiting, retries: retries + 1 }` |
+| C | `phase' = Waiting`, the primed form of TLA+ and Quint |
+
+In all three a field an event doesn't name keeps its value, and an `init`
+lists every field (as `phase = Failed` in A and C, as a field list in B).
+Question 3 gives a rewrite of `schedule` in each version's own notation
+([`rewrite-A.txt`](rewrite-A.txt), [`rewrite-B.txt`](rewrite-B.txt),
+[`rewrite-C.txt`](rewrite-C.txt)) that reads `retries` after setting it.
+
+Each version goes to each reader once, in a new conversation, with
+[the prompt](prompt.txt) as the only message, its `{code}` filled with the
+version and its `{rewrite}` with that version's rewrite. Readers: Claude models
+(Haiku, Sonnet, Opus, Fable) in fresh contexts with no repository access,
+and, if run, the five public chat models stage 9 used (ChatGPT, Grok,
+DeepSeek, Qwen, Gemini).
+
+## Answer key
+
+1. `phase` Calling, `calls` 2, `retries` 1, `time` 1, `last_start` 1,
+   `last_due` 1.
+2. `phase` Ended, `due` 0, `retries` 0: `0 + 121 < 120` is false, and the
+   fields the `else` branch doesn't name keep their values.
+3. In every version, every expression in an event sees the state before
+   the event, so the condition reads `retries == 2` and the phase is
+   **Waiting**. In version A, Accord rejects this rewrite, since it reads a
+   field the event already set. The reply is scored by the reading it
+   commits to: Ended (the update already took effect), Waiting (the old
+   value), or the ambiguity pointed out.
+4. `phase` (to Failed) and `terminal` (to true); every other field keeps
+   its value.
+5. Both must hold in every reachable state; helper invariants exist so the
+   other invariants can be proved, and aren't claims of their own.
+6. No: `schedule` returns the next state and leaves `state` unchanged.
+
+Questions 7 and 8 are recorded, not scored.
+
+## What would change the decision
+
+Written before the runs:
+
+- A is replaced by C's labelled spelling, or by B, if A is answered wrongly
+  on question 1, 2 or 4 where B or C is answered rightly, or if A's replies
+  say on question 6 that `state` changes where B's and C's don't.
+- If A's replies answer question 3 with Ended where B's or C's answer
+  Waiting, the rule and its diagnostic are required for A; that alone
+  doesn't replace A.
+- `helper invariant` is renamed if question 5 is missed.
+- If every version is answered at the ceiling, A is kept, as stage 9 kept
+  its shorter form.
+
+## Result
+
+Twenty-four replies ([`replies.md`](replies.md)): Haiku, Sonnet, Opus and
+Fable through fresh agents told to use no tools, and ChatGPT, Grok, DeepSeek
+and Gemini through their public chat interfaces, each in a conversation with
+no memory of earlier ones. Qwen wasn't run: the browser extension had no
+permission on its site.
+
+Questions 1, 2, 4 and 5 were answered as the key gives in all 24 replies,
+helper invariants by inference ("scaffolding for the proof"). On question 6,
+23 replies said `state` doesn't change; ChatGPT, on A, said it can't be
+determined. Confidence was 4 or 5 in every reply that gave one.
+
+Question 3:
+
+| Reader | A | B | C |
+| --- | --- | --- | --- |
+| Haiku | Ended | Waiting | Waiting |
+| Sonnet | Ended | Waiting, after first writing Ended | Waiting |
+| Opus | Ended | Waiting | Waiting |
+| Fable | Ended | Waiting | Waiting |
+| ChatGPT | Ended | Waiting | Waiting |
+| Grok | Waiting, reasoned from the value after the increment | Waiting | Ended |
+| DeepSeek | Ended | Waiting | Waiting |
+| Gemini | Ended | Waiting | Waiting |
+
+- **A is read sequentially.** Seven replies answered Ended, and the eighth
+  reasoned from the incremented value before misapplying `>=`.
+- **B is read as the state before the event** in all eight. Several replies
+  named the rule they assumed: "every expression in `next` reads the state
+  from before the event."
+- **C is read as the old value** in seven of eight; Grok read the prime
+  sequentially.
+- **What was hardest**, across versions: what `helper` means, what happens
+  when a `requires` fails, and in B and C whether the new or the old state is
+  read.
+
+## Decision
+
+The rule written before the runs keeps A, with the rejection of a read after
+a set and its diagnostic required. The maintainers chose B instead: it was
+the only form that every reader read as Accord means it, and with A every
+author, person or agent, would write order-dependent updates by instinct and
+meet the diagnostic. B's costs are that `next` is a reserved word, so no
+parameter or field can use it, and that `next { field: value }` looks like a
+record before records exist; stage 11 decides records on their own.
+`helper invariant` is kept. Accepted as
+[decision 7](../../syntax.md#decisions).
+
+## Limits
+
+- One run per reader and version; the public interfaces' model versions and
+  settings weren't recorded, so the run can't be repeated exactly.
+- Grok searched the web on C ("9 fuentes") despite the instruction, and
+  DeepSeek showed a reasoning step with its "deep thinking" option apparently
+  off.
+- The prompt stated none of the semantics, on purpose, so it measures a
+  first reading, not a reading after the reference. No person was asked.

docs/design/probes/2026-11-12-machine-updates/prompt.txt

@@ -0,0 +1,20 @@
+Below is code in a programming language you have probably never seen. Don't search the web or look anything up; answer only from reading it.
+
+{code}
+
+The machine compiles to a TypeScript module with one exported function per init and per event: `start(isTerminal)` returns a state, and each event takes a state and the event's parameters, for example `schedule(state, 1)`.
+
+1. Start with start(is_terminal: false), then apply schedule(delay: 1), advance(to: 1) and start_call(), in that order. What are phase, calls, retries, time, last_start and last_due afterwards?
+2. Start with start(is_terminal: false), then apply schedule(delay: 121). What are phase, due and retries afterwards?
+3. A colleague rewrites the body of schedule as:
+
+{rewrite}
+
+   If retries is 2 before this event runs, which phase results?
+4. Which fields does failure(is_terminal: true) change, and which keep their value?
+5. What is the difference between an invariant and a helper invariant?
+6. In TypeScript, after `const after = schedule(state, 1)`, does `state` change?
+7. How confident are you in your answers, from 1 (a guess) to 5 (certain)?
+8. Which part was hardest to read, and why?
+
+Answer each question separately and briefly.

docs/design/probes/2026-11-12-machine-updates/replies.md

@@ -0,0 +1,61 @@
+# Replies, 2026-11-12
+
+## Claude models
+
+Twelve replies: four Claude models (Haiku, Sonnet, Opus, Fable), each in a
+fresh context with no repository, given one version's message and told to
+use no tools. Questions 1, 2 and 4 were answered as the key gives in all
+twelve, so only questions 3, 5, 6, 7 and 8 are quoted, condensed.
+
+### A: `field = expression`
+
+- **Haiku.** 3: "the rewritten body makes retries 3, so `retries >= 3` holds and phase becomes Ended." 5: inferred, supporting properties. 6: "Probably not." 7: 5 on 1 to 4, 3 on 5 and 6. 8: the guard of `schedule`.
+- **Sonnet.** 3: "Ended. retries becomes 3, and 3 >= 3 sends it to Ended." 5: supporting fact for the main invariants. 6: "No." 7: 4. 8: helper invariants, and whether delay 121 is meant to be valid.
+- **Opus.** 3: "Ended. retries becomes 3, and 3 >= 3 is true." 5: "scaffolding for the proof". 6: "Probably not." 7: 5 on 1 to 4, 3 on 5 and 6. 8: helper invariants; what a failed `requires` does.
+- **Fable.** 3: "Ended. retries becomes 3 first, and the `if` then reads the updated value. This assumes statements run in order and see earlier assignments, which the text does not state." 5: auxiliary, not a promise. 6: "Most likely no." 7: 4. 8: helper invariants; a failed `requires`.
+
+### B: `next { field: expression }`
+
+- **Haiku.** 3: "phase = Waiting. This assumes the if reads retries before the event … If it read the updated value (3), the result would be Ended." 5: supporting. 6: "No." 7: about 4. 8: whether `next` reads the old or the new state.
+- **Sonnet.** 3: "Ended. The rewritten body compares retries (2) with 3, and 2 >= 3 is false, so the result is Waiting. (Correction: phase = Waiting, not Ended.)" 5: inductive strengthening. 6: "No." 7: 4. 8: that unlisted fields keep their values.
+- **Opus.** 3: "Waiting. I am assuming every expression in a `next` block reads the state from before the event." 5: makes the main invariants provable. 6: "No." 7: 4. 8: whether omitted fields keep values and expressions read the old state.
+- **Fable.** 3: "Waiting. I assume every expression in `next` reads the state from before the event … If fields were assigned in order … the answer would be Ended, but I think that is unlikely." 5: auxiliary. 6: "No." 7: 4. 8: the two unstated rules of `next`.
+
+### C: `field' = expression`
+
+- **Haiku.** 3: "Waiting. With retries = 2, retries' becomes 3 and the test 2 >= 3 is false." 5: supporting. 6: "Probably not." 7: 4 on 1 to 4, 3 on 5 and 6. 8: helper invariants and mutation.
+- **Sonnet.** 3: "with retries=2 the test retries>=3 is false, so phase=Waiting (and retries becomes 3)." 5: auxiliary. 6: "No." 7: 4. 8: primed semantics; helper invariants.
+- **Opus.** 3: "Waiting. I read unprimed `retries` as the value before the event." 5: extra fact for the proof. 6: "No." 7: 4. 8: whether unprimed names read the old state; helper; mutation.
+- **Fable.** 3: "Waiting. I read the unprimed `retries` in the condition as the value before the event (2) … the answer flips (Waiting versus Ended) depending on it." 5: auxiliary. 6: "No, as far as I can infer." 7: 4. 8: the primed assignments in the rewrite; helper.
+
+## Public chat models
+
+Each in a new conversation, through the owner's browser, with the version's message as the only input. Condensed; questions 1, 2 and 4 are noted only where they differ from the key.
+
+### ChatGPT (temporary chat: no memory or custom instructions; reasoning effort "High")
+
+- **A.** 1, 2, 4 as the key. 3: "Phase = Ended. The rewrite increments retries from 2 to 3, then checks retries >= 3, which is true." 5: helpers "establish supporting properties used to prove those guarantees." 6: "This cannot be determined from the snippet alone." 7: 4. 8: question 6, mutable or immutable state.
+- **B.** 1, 2, 4 as the key. 3: "Resulting phase: Waiting. Assuming expressions inside next evaluate against the original state." 5: helpers "used to help prove the main invariants." 6: "No, assuming immutable transition semantics." 7: 4. 8: question 3, "whether expressions within a next block read the original state or intermediate updates. I inferred simultaneous assignment semantics."
+- **C.** 1, 2, 4 as the key. 3: "Phase = Waiting. The condition checks retries >= 3 using its pre-event value of 2, even though retries' becomes 3." 5: helpers "assist verification." 6: "No. Assuming the generated functions use immutable state transitions." 7: 4.
+
+### Grok (private chat: not in history, not used for training; mode "Fast")
+
+- **A.** 1, 2, 4 as the key. 3: "phase = Waiting (retries becomes 3, but the rewritten if only ends when retries >= 3 after the increment, so it still sets Waiting)": it reads the condition after the increment and then misapplies `>=`, so the answer contradicts its own reasoning. 5: helper "used only to help prove the real invariants." 6: "No." 7: 5. 8: "the order of the increment vs. the phase decision" in question 3, and helper invariants.
+- **B.** 1, 2, 4 as the key. 3: "Waiting (the if uses the pre-increment value of retries)." 5: "auxiliary properties that assist in proving the main ones." 6: "No; state is unchanged." 7: 5. 8: the `schedule` conditional.
+- **C.** 1, 2, 4 as the key. 3: "Ended (the assignment retries' = retries + 1 makes the subsequent test see 3)." 5: "auxiliary/derived property used to help establish the main ones." 6: "No." 7: 5. 8: "the precise evaluation timing of the rewritten schedule body." The reply shows "9 fuentes": Grok searched the web despite the instruction not to.
+
+### DeepSeek (no memory between chats; "Pensamiento Profundo" and "Búsqueda inteligente" left as found, though the reply shows a reasoning step; the paste became an attachment and was turned back into text with "Pegar original")
+
+- **A.** 1, 2, 4 as the key. 3: "Ended — retries becomes 3, so retries >= 3 is true." 5: helper "used to support checking/proving the main invariants, not the primary exported contract." 6: "No." 7: 4. 8: helper invariants.
+- **B.** 1, 2, 4 as the key. 3: "phase = Waiting. Assuming next { ... } evaluates its field expressions against the pre-event state." 5: "an auxiliary lemma used to help prove/check the main invariants." 6: "No." 7: not given. 8: question 3, "whether next field expressions are evaluated simultaneously against the old state or sequentially."
+- **C.** 1, 2, 4 as the key. 3: "the if retries >= 3 test uses the old retries, so it is false. Result: phase = Waiting and retries becomes 3." 5: "likely used to support proofs/checking rather than as a primary public invariant." 6: "No." 7 and 8 not read.
+
+### Qwen
+
+Not run: the browser extension has no permission on `chat.qwen.ai`.
+
+### Gemini (signed out, so no history or memory)
+
+- **A.** 1, 2, 4 as the key. 3: "Phase: Ended (since retries becomes 2 + 1 = 3, making retries >= 3 true)." 5: "auxiliary lemmas or intermediate properties used by a verification engine." 6: "No." 7: 5. 8: the compound condition in `schedule`.
+- **B.** 3: "phase: Waiting. (Because the condition retries >= 3 evaluates using the pre-update value of retries, which is 2)." 4 as the key. 6: "No … (pure/immutable update pattern)."
+- **C.** 1, 2, 4 as the key. 3: "Waiting (because retries in the if condition refers to the current/unprimed value of 2, making 2 >= 3 false)." 5: "auxiliary internal properties (often used as inductive lemmas for verification)."

docs/design/probes/2026-11-12-machine-updates/rewrite-A.txt

@@ -0,0 +1,4 @@
+    {
+        retries = retries + 1
+        if retries >= 3 { phase = Ended } else { phase = Waiting }
+    }

docs/design/probes/2026-11-12-machine-updates/rewrite-B.txt

@@ -0,0 +1,6 @@
+    {
+        next {
+            retries: retries + 1,
+            phase: if retries >= 3 { Ended } else { Waiting },
+        }
+    }

docs/design/probes/2026-11-12-machine-updates/rewrite-C.txt

@@ -0,0 +1,4 @@
+    {
+        retries' = retries + 1
+        if retries >= 3 { phase' = Ended } else { phase' = Waiting }
+    }