From 56e18c8b4df7a6ec651c632278f7c485023fc3b1 Mon Sep 17 00:00:00 2001 From: Canitas <112231952+Sequela02@users.noreply.github.com> Date: Thu, 12 Nov 2026 19:43:50 -0700 Subject: [PATCH] docs: settle how a machine's events state the next state Stage 10 needs a syntax for machines before its conformance cases. A probe gave twenty-four readers the same machine in three forms: one update per line was read as updating in order by seven of eight, while next { field: value } was read as Accord means it by all eight. Record the machine syntax with that form, the probe behind it, and that the boundary checks helper invariants, which event overflow proofs assume. Refs #82 --- ROADMAP.md | 3 +- docs/design/native-code-constraints.md | 2 +- .../2026-11-12-machine-updates/README.md | 132 ++++++++++++++++++ .../2026-11-12-machine-updates/prompt.txt | 20 +++ .../2026-11-12-machine-updates/replies.md | 61 ++++++++ .../2026-11-12-machine-updates/rewrite-A.txt | 4 + .../2026-11-12-machine-updates/rewrite-B.txt | 6 + .../2026-11-12-machine-updates/rewrite-C.txt | 4 + .../2026-11-12-machine-updates/variants/A.txt | 91 ++++++++++++ .../2026-11-12-machine-updates/variants/B.txt | 101 ++++++++++++++ .../2026-11-12-machine-updates/variants/C.txt | 91 ++++++++++++ docs/design/syntax.md | 93 ++++++++++++ 12 files changed, 606 insertions(+), 2 deletions(-) create mode 100644 docs/design/probes/2026-11-12-machine-updates/README.md create mode 100644 docs/design/probes/2026-11-12-machine-updates/prompt.txt create mode 100644 docs/design/probes/2026-11-12-machine-updates/replies.md create mode 100644 docs/design/probes/2026-11-12-machine-updates/rewrite-A.txt create mode 100644 docs/design/probes/2026-11-12-machine-updates/rewrite-B.txt create mode 100644 docs/design/probes/2026-11-12-machine-updates/rewrite-C.txt create mode 100644 docs/design/probes/2026-11-12-machine-updates/variants/A.txt create mode 100644 docs/design/probes/2026-11-12-machine-updates/variants/B.txt create mode 100644 docs/design/probes/2026-11-12-machine-updates/variants/C.txt diff --git a/ROADMAP.md b/ROADMAP.md index ce11077..b606ce5 100644 --- a/ROADMAP.md +++ b/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. diff --git a/docs/design/native-code-constraints.md b/docs/design/native-code-constraints.md index 5187477..cb84e1d 100644 --- a/docs/design/native-code-constraints.md +++ b/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 diff --git a/docs/design/probes/2026-11-12-machine-updates/README.md b/docs/design/probes/2026-11-12-machine-updates/README.md new file mode 100644 index 0000000..5694860 --- /dev/null +++ b/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. diff --git a/docs/design/probes/2026-11-12-machine-updates/prompt.txt b/docs/design/probes/2026-11-12-machine-updates/prompt.txt new file mode 100644 index 0000000..5817539 --- /dev/null +++ b/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. diff --git a/docs/design/probes/2026-11-12-machine-updates/replies.md b/docs/design/probes/2026-11-12-machine-updates/replies.md new file mode 100644 index 0000000..71ae415 --- /dev/null +++ b/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)." diff --git a/docs/design/probes/2026-11-12-machine-updates/rewrite-A.txt b/docs/design/probes/2026-11-12-machine-updates/rewrite-A.txt new file mode 100644 index 0000000..4c3dbfb --- /dev/null +++ b/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 } + } diff --git a/docs/design/probes/2026-11-12-machine-updates/rewrite-B.txt b/docs/design/probes/2026-11-12-machine-updates/rewrite-B.txt new file mode 100644 index 0000000..49dc8e6 --- /dev/null +++ b/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 }, + } + } diff --git a/docs/design/probes/2026-11-12-machine-updates/rewrite-C.txt b/docs/design/probes/2026-11-12-machine-updates/rewrite-C.txt new file mode 100644 index 0000000..742288f --- /dev/null +++ b/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 } + } diff --git a/docs/design/probes/2026-11-12-machine-updates/variants/A.txt b/docs/design/probes/2026-11-12-machine-updates/variants/A.txt new file mode 100644 index 0000000..19d4957 --- /dev/null +++ b/docs/design/probes/2026-11-12-machine-updates/variants/A.txt @@ -0,0 +1,91 @@ +/// Where a retried model call stands. +enum RetryPhase { Failed, Waiting, Calling, Ended } + +/// A failed model call, retried within a budget and a time window. +machine ProviderRetry { + intent "Retry a failed model call at most three times within its window, wait before each retry, and never call again after cancellation." + + state { + phase: RetryPhase, + time: i32, + due: i32, + retries: i32, + calls: i32, + stopped: Bool, + calls_at_stop: i32, + terminal: Bool, + last_start: i32, + last_due: i32, + } + + init start(is_terminal: Bool) { + phase = Failed + time = 0 + due = 0 + retries = 0 + calls = 1 + stopped = false + calls_at_stop = 0 + terminal = is_terminal + last_start = 0 + last_due = 0 + } + + event schedule(delay: i32) + requires phase == Failed + requires delay == 1 or delay == 60 or delay == 121 + { + if not terminal and not stopped and retries < 3 and time + delay < 120 { + phase = Waiting + due = time + delay + retries = retries + 1 + } else { + phase = Ended + } + } + + event advance(to: i32) + requires phase == Waiting and time < 120 + requires (to == due or to == 120) and to >= time + { + time = to + } + + event cancel() + requires not stopped and phase != Ended + { + stopped = true + calls_at_stop = calls + } + + event start_call() + requires phase == Waiting and time >= due and time < 120 and not stopped + { + phase = Calling + calls = calls + 1 + last_start = time + last_due = due + } + + event failure(is_terminal: Bool) + requires phase == Calling + { + phase = Failed + terminal = is_terminal + } + + event success() + requires phase == Calling + { + phase = Ended + } + + invariant bounds: retries <= 3 and calls <= 4 and last_start < 120 + invariant cancel_stops_calls: stopped implies calls == calls_at_stop + invariant wait_respected: last_start >= last_due + + helper invariant calls_follow_retries: calls <= retries + 1 + helper invariant waiting_before_call: phase == Waiting implies calls <= retries + helper invariant time_in_window: time <= 120 + helper invariant due_in_window: due <= 120 +} diff --git a/docs/design/probes/2026-11-12-machine-updates/variants/B.txt b/docs/design/probes/2026-11-12-machine-updates/variants/B.txt new file mode 100644 index 0000000..3eb6f99 --- /dev/null +++ b/docs/design/probes/2026-11-12-machine-updates/variants/B.txt @@ -0,0 +1,101 @@ +/// Where a retried model call stands. +enum RetryPhase { Failed, Waiting, Calling, Ended } + +/// A failed model call, retried within a budget and a time window. +machine ProviderRetry { + intent "Retry a failed model call at most three times within its window, wait before each retry, and never call again after cancellation." + + state { + phase: RetryPhase, + time: i32, + due: i32, + retries: i32, + calls: i32, + stopped: Bool, + calls_at_stop: i32, + terminal: Bool, + last_start: i32, + last_due: i32, + } + + init start(is_terminal: Bool) { + { + phase: Failed, + time: 0, + due: 0, + retries: 0, + calls: 1, + stopped: false, + calls_at_stop: 0, + terminal: is_terminal, + last_start: 0, + last_due: 0, + } + } + + event schedule(delay: i32) + requires phase == Failed + requires delay == 1 or delay == 60 or delay == 121 + { + if not terminal and not stopped and retries < 3 and time + delay < 120 { + next { + phase: Waiting, + due: time + delay, + retries: retries + 1, + } + } else { + next { phase: Ended } + } + } + + event advance(to: i32) + requires phase == Waiting and time < 120 + requires (to == due or to == 120) and to >= time + { + next { time: to } + } + + event cancel() + requires not stopped and phase != Ended + { + next { + stopped: true, + calls_at_stop: calls, + } + } + + event start_call() + requires phase == Waiting and time >= due and time < 120 and not stopped + { + next { + phase: Calling, + calls: calls + 1, + last_start: time, + last_due: due, + } + } + + event failure(is_terminal: Bool) + requires phase == Calling + { + next { + phase: Failed, + terminal: is_terminal, + } + } + + event success() + requires phase == Calling + { + next { phase: Ended } + } + + invariant bounds: retries <= 3 and calls <= 4 and last_start < 120 + invariant cancel_stops_calls: stopped implies calls == calls_at_stop + invariant wait_respected: last_start >= last_due + + helper invariant calls_follow_retries: calls <= retries + 1 + helper invariant waiting_before_call: phase == Waiting implies calls <= retries + helper invariant time_in_window: time <= 120 + helper invariant due_in_window: due <= 120 +} diff --git a/docs/design/probes/2026-11-12-machine-updates/variants/C.txt b/docs/design/probes/2026-11-12-machine-updates/variants/C.txt new file mode 100644 index 0000000..1f943e8 --- /dev/null +++ b/docs/design/probes/2026-11-12-machine-updates/variants/C.txt @@ -0,0 +1,91 @@ +/// Where a retried model call stands. +enum RetryPhase { Failed, Waiting, Calling, Ended } + +/// A failed model call, retried within a budget and a time window. +machine ProviderRetry { + intent "Retry a failed model call at most three times within its window, wait before each retry, and never call again after cancellation." + + state { + phase: RetryPhase, + time: i32, + due: i32, + retries: i32, + calls: i32, + stopped: Bool, + calls_at_stop: i32, + terminal: Bool, + last_start: i32, + last_due: i32, + } + + init start(is_terminal: Bool) { + phase = Failed + time = 0 + due = 0 + retries = 0 + calls = 1 + stopped = false + calls_at_stop = 0 + terminal = is_terminal + last_start = 0 + last_due = 0 + } + + event schedule(delay: i32) + requires phase == Failed + requires delay == 1 or delay == 60 or delay == 121 + { + if not terminal and not stopped and retries < 3 and time + delay < 120 { + phase' = Waiting + due' = time + delay + retries' = retries + 1 + } else { + phase' = Ended + } + } + + event advance(to: i32) + requires phase == Waiting and time < 120 + requires (to == due or to == 120) and to >= time + { + time' = to + } + + event cancel() + requires not stopped and phase != Ended + { + stopped' = true + calls_at_stop' = calls + } + + event start_call() + requires phase == Waiting and time >= due and time < 120 and not stopped + { + phase' = Calling + calls' = calls + 1 + last_start' = time + last_due' = due + } + + event failure(is_terminal: Bool) + requires phase == Calling + { + phase' = Failed + terminal' = is_terminal + } + + event success() + requires phase == Calling + { + phase' = Ended + } + + invariant bounds: retries <= 3 and calls <= 4 and last_start < 120 + invariant cancel_stops_calls: stopped implies calls == calls_at_stop + invariant wait_respected: last_start >= last_due + + helper invariant calls_follow_retries: calls <= retries + 1 + helper invariant waiting_before_call: phase == Waiting implies calls <= retries + helper invariant time_in_window: time <= 120 + helper invariant due_in_window: due <= 120 +} diff --git a/docs/design/syntax.md b/docs/design/syntax.md index 7a56d7c..e159ab2 100644 --- a/docs/design/syntax.md +++ b/docs/design/syntax.md @@ -176,6 +176,88 @@ leaves its callers' proofs current; changing its contract doesn't. Blocks are expressions: the last expression is the block's value. There is no `return`: an early exit is a decision table. +## Machines + +Accepted for stage 10 ([#82](https://github.com/sequelcore/accord/issues/82)) +and not compiled yet. A machine is a state, the ways it starts, the events +that move it, and what must hold in every state it reaches: + +```accord +/// A failed model call, retried within a budget and a time window. +pub machine ProviderRetry { + intent "Retry a failed model call at most three times within its window, and never call again after cancellation." + + state { + phase: RetryPhase, + retries: i32, + calls: i32, + stopped: Bool, + calls_at_stop: i32, + } + + init start() { + next { + phase: Failed, + retries: 0, + calls: 1, + stopped: false, + calls_at_stop: 0, + } + } + + event schedule() + requires phase == Failed + decide { + | not stopped and retries < 3 => next { phase: Waiting, retries: retries + 1 } + | otherwise => next { phase: Ended } + } + + event start_call() + requires phase == Waiting and not stopped + { + next { phase: Calling, calls: calls + 1 } + } + + event cancel() + requires not stopped + { + next { stopped: true, calls_at_stop: calls } + } + + invariant cancel_stops_calls: stopped implies calls == calls_at_stop + + helper invariant calls_follow_retries: calls <= retries + 1 +} +``` + +| Form | Meaning | +| --- | --- | +| `machine Name { … }` | A `state`, at least one `init`, its events, observers, invariants and helper invariants. `pub` exports it to TypeScript. Its `intent` is about the machine | +| `state { field: Type, … }` | The fields: fixed-width integers, enums and `Bool`s | +| `init name(params) clauses body` | A way to start. Its `next { … }` lists every field | +| `event name(params) clauses body` | A transition. Its `requires` say when it is allowed and which parameters it takes | +| `next { field: value, … }` | The state after the event. A field it doesn't list keeps its value, and every expression in an `init` or event, conditions and observer calls included, reads the state before it. `next { }` changes nothing | +| `fn name(params) -> Type` inside a machine | An observer: a pure function of the state, with the usual clauses. Events and observers can call it; an invariant can't, as no specification can call a function | +| `invariant name: condition` | A claim about every reachable state: proved inductive with the helper invariants, or refuted by a trace from an `init` | +| `helper invariant name: condition` | A condition proved with the invariants so they can be proved inductive. The receipt reports it as support, not as a claim, and the boundary checks it like an invariant | + +- An `init` or event takes `intent` and `requires` only; it has no `result`. + Its body is a block that ends in `next { … }`, through `if`, which always + has an `else`, or a decision table whose rows give `next { … }`. +- A parameter can't share a field's name, and `next` is reserved, so no + field or parameter can use it. +- Each event is proved to be allowed in some reachable state, as each row of a + decision table is proved reachable. +- A machine's example names it, its events one per line, and what holds after: + + ```accord + example ProviderRetry + start() + schedule() + start_call() + gives phase == Calling and calls == 2 + ``` + ## Files and folders A file is a program on its own. A folder is one program too: every `.accord` @@ -221,3 +303,14 @@ Accepted on 2026-11-08 ([#27](https://github.com/sequelcore/accord/issues/27)): it, for the same reason `intent` is a clause. An open case it doesn't cover makes the function incomplete, not failed: whether a freedom is intended is a person's decision. + +Accepted on 2026-11-12 ([#82](https://github.com/sequelcore/accord/issues/82)): + +7. **An event states its next state as `next { field: value }`**, and every + expression in it reads the state before the event. In a + [probe](probes/2026-11-12-machine-updates/README.md), every reader read + that form so, while seven readers of eight read `field = value`, one + update per line, as updating in order, and one read `field' = value` so. + A program that reads a field after setting it means, in `next { … }`, + what its readers expect. `helper invariant` keeps what supports a proof + apart from what the machine claims, and every reader told the two apart.