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.