From cce0d9dcda71b1bb052ee430133ab48672c4c70b Mon Sep 17 00:00:00 2001 From: Canitas <112231952+Sequela02@users.noreply.github.com> Date: Thu, 12 Nov 2026 19:57:24 -0700 Subject: [PATCH 1/9] test: write stage 10's machine cases before their code AGENTS asks for a construct's conformance cases, faults included, before the compiler code that produces them. These fix what a machine's obligations are and in which order, what refutes an invariant (a trace from an init) and what is only not inductive, and what the checker must reject. Refs #82 --- conformance/README.md | 18 ++++++++++ .../cases/machine-dead-event-fault.accord | 33 +++++++++++++++++++ conformance/cases/machine-decide.accord | 25 ++++++++++++++ .../cases/machine-event-ensures.accord | 17 ++++++++++ conformance/cases/machine-fault.accord | 32 ++++++++++++++++++ conformance/cases/machine-helped.accord | 23 +++++++++++++ conformance/cases/machine-init-fault.accord | 31 +++++++++++++++++ .../cases/machine-init-missing-field.accord | 12 +++++++ .../cases/machine-invariant-call.accord | 17 ++++++++++ conformance/cases/machine-next-twice.accord | 11 +++++++ conformance/cases/machine-no-init.accord | 11 +++++++ conformance/cases/machine-observer.accord | 30 +++++++++++++++++ .../cases/machine-overflow-fault.accord | 18 ++++++++++ conformance/cases/machine-overflow.accord | 19 +++++++++++ conformance/cases/machine-param-field.accord | 11 +++++++ conformance/cases/machine-unhelped.accord | 22 +++++++++++++ .../cases/machine-unknown-field.accord | 11 +++++++ conformance/cases/machine.accord | 33 +++++++++++++++++++ 18 files changed, 374 insertions(+) create mode 100644 conformance/cases/machine-dead-event-fault.accord create mode 100644 conformance/cases/machine-decide.accord create mode 100644 conformance/cases/machine-event-ensures.accord create mode 100644 conformance/cases/machine-fault.accord create mode 100644 conformance/cases/machine-helped.accord create mode 100644 conformance/cases/machine-init-fault.accord create mode 100644 conformance/cases/machine-init-missing-field.accord create mode 100644 conformance/cases/machine-invariant-call.accord create mode 100644 conformance/cases/machine-next-twice.accord create mode 100644 conformance/cases/machine-no-init.accord create mode 100644 conformance/cases/machine-observer.accord create mode 100644 conformance/cases/machine-overflow-fault.accord create mode 100644 conformance/cases/machine-overflow.accord create mode 100644 conformance/cases/machine-param-field.accord create mode 100644 conformance/cases/machine-unhelped.accord create mode 100644 conformance/cases/machine-unknown-field.accord create mode 100644 conformance/cases/machine.accord diff --git a/conformance/README.md b/conformance/README.md index 3b5ee15..a7bfecc 100644 --- a/conformance/README.md +++ b/conformance/README.md @@ -22,6 +22,24 @@ listed after every obligation, in source order; `error` means the file must be rejected before any obligation is generated. A case named `x-fault` or `x--fault` plants a fault in the correct case `x`, and must be refuted or fail. +A machine's obligations come in source order with its functions': + +- for each `init`, in order: that some input is allowed, when it has a + `requires`; that its state meets every invariant and helper invariant; + then its arithmetic and decision tables, as a function's; +- for each event, in order: that it preserves every invariant and helper + invariant; that it is allowed in some state an `init` reaches; then its + arithmetic and decision tables, as a function's, each assuming the + invariants and helper invariants; +- its observers, as functions. + +An invariant is refuted only by a trace from an `init`, which the explorer +finds and the interpreter replays. Where the solvers refute an obligation +from a state no trace reaches, its outcome is `not_inductive`. An event is +allowed in a reachable state when the explorer reaches one where its +`requires` holds. A machine's `example` is listed as `passed` or `failed` +with the other examples. + `cargo test --test conformance` runs every case through both solvers. It needs Z3 and cvc5: on the `PATH` as `z3` and `cvc5`, or named by the `ACCORD_Z3` and `ACCORD_CVC5` environment variables. Without them the diff --git a/conformance/cases/machine-dead-event-fault.accord b/conformance/cases/machine-dead-event-fault.accord new file mode 100644 index 0000000..9c50382 --- /dev/null +++ b/conformance/cases/machine-dead-event-fault.accord @@ -0,0 +1,33 @@ +// expect: proved, proved, proved, proved, proved, proved, refuted +// `reset` needs more presses than the invariant allows, so no state the +// machine reaches allows it: the solvers prove that none does. +enum Light { Off, On } + +machine Switch { + state { + light: Light, + presses: i32, + } + + init start() { + next { light: Off, presses: 0 } + } + + event press() + requires presses < 100 + { + if light == Off { + next { light: On, presses: presses + 1 } + } else { + next { light: Off, presses: presses + 1 } + } + } + + event reset() + requires presses > 100 + { + next { light: Off, presses: 0 } + } + + invariant pressed: presses >= 0 and presses <= 100 +} diff --git a/conformance/cases/machine-decide.accord b/conformance/cases/machine-decide.accord new file mode 100644 index 0000000..9a9babe --- /dev/null +++ b/conformance/cases/machine-decide.accord @@ -0,0 +1,25 @@ +// expect: proved, proved, proved, proved, proved, proved, proved, proved +// An event whose body is a decision table: every state the invariant allows +// reaches a row, each row can be the first to hold, and each row's addition +// stays within `i32`. +enum Light { Off, On } + +machine Switch { + state { + light: Light, + presses: i32, + } + + init start() { + next { light: Off, presses: 0 } + } + + event press() + requires presses < 100 + decide { + | light == Off => next { light: On, presses: presses + 1 } + | otherwise => next { light: Off, presses: presses + 1 } + } + + invariant pressed: presses >= 0 and presses <= 100 +} diff --git a/conformance/cases/machine-event-ensures.accord b/conformance/cases/machine-event-ensures.accord new file mode 100644 index 0000000..8751078 --- /dev/null +++ b/conformance/cases/machine-event-ensures.accord @@ -0,0 +1,17 @@ +// expect: error +// An event takes `intent` and `requires` only: it has no result to ensure. +machine Switch { + state { + presses: i32, + } + + init start() { + next { presses: 0 } + } + + event press() + ensures presses >= 0 + { + next { presses: presses + 1 } + } +} diff --git a/conformance/cases/machine-fault.accord b/conformance/cases/machine-fault.accord new file mode 100644 index 0000000..b1bae6e --- /dev/null +++ b/conformance/cases/machine-fault.accord @@ -0,0 +1,32 @@ +// expect: proved, refuted, proved, proved, proved, passed +// `press` is allowed at 100 presses, so a run of 101 presses breaks the +// invariant. +enum Light { Off, On } + +machine Switch { + state { + light: Light, + presses: i32, + } + + init start() { + next { light: Off, presses: 0 } + } + + event press() + requires presses <= 100 + { + if light == Off { + next { light: On, presses: presses + 1 } + } else { + next { light: Off, presses: presses + 1 } + } + } + + invariant pressed: presses >= 0 and presses <= 100 +} + +example Switch + start() + press() + gives light == On and presses == 1 diff --git a/conformance/cases/machine-helped.accord b/conformance/cases/machine-helped.accord new file mode 100644 index 0000000..69d06fe --- /dev/null +++ b/conformance/cases/machine-helped.accord @@ -0,0 +1,23 @@ +// expect: proved, proved, proved, proved, proved +// The machine of `machine-unhelped.accord`, with the helper invariant that `y` +// moves with `x`: the invariant is now proved inductive. +machine Pair { + state { + x: i32, + y: i32, + } + + init start() { + next { x: 0, y: 0 } + } + + event step() + requires x < 3 + { + next { x: x + 1, y: y + 1 } + } + + invariant y_bounded: y <= 3 + + helper invariant together: x == y +} diff --git a/conformance/cases/machine-init-fault.accord b/conformance/cases/machine-init-fault.accord new file mode 100644 index 0000000..d8aaf99 --- /dev/null +++ b/conformance/cases/machine-init-fault.accord @@ -0,0 +1,31 @@ +// expect: proved, refuted, proved, proved, proved, proved +// `broken` starts past the bound the invariant sets, so the run that is only +// `broken()` breaks it. +enum Light { Off, On } + +machine Switch { + state { + light: Light, + presses: i32, + } + + init start() { + next { light: Off, presses: 0 } + } + + init broken() { + next { light: Off, presses: 101 } + } + + event press() + requires presses < 100 + { + if light == Off { + next { light: On, presses: presses + 1 } + } else { + next { light: Off, presses: presses + 1 } + } + } + + invariant pressed: presses >= 0 and presses <= 100 +} diff --git a/conformance/cases/machine-init-missing-field.accord b/conformance/cases/machine-init-missing-field.accord new file mode 100644 index 0000000..900a291 --- /dev/null +++ b/conformance/cases/machine-init-missing-field.accord @@ -0,0 +1,12 @@ +// expect: error +// An `init` must give every field a value: `start` leaves `presses` out. +machine Switch { + state { + on: Bool, + presses: i32, + } + + init start() { + next { on: false } + } +} diff --git a/conformance/cases/machine-invariant-call.accord b/conformance/cases/machine-invariant-call.accord new file mode 100644 index 0000000..3698848 --- /dev/null +++ b/conformance/cases/machine-invariant-call.accord @@ -0,0 +1,17 @@ +// expect: error +// An invariant is a specification, and no specification can call a function. +machine Switch { + state { + presses: i32, + } + + init start() { + next { presses: 0 } + } + + fn many() -> Bool { + presses > 10 + } + + invariant few: not many() +} diff --git a/conformance/cases/machine-next-twice.accord b/conformance/cases/machine-next-twice.accord new file mode 100644 index 0000000..5695eaa --- /dev/null +++ b/conformance/cases/machine-next-twice.accord @@ -0,0 +1,11 @@ +// expect: error +// A `next` gives each field one value. +machine Switch { + state { + presses: i32, + } + + init start() { + next { presses: 0, presses: 1 } + } +} diff --git a/conformance/cases/machine-no-init.accord b/conformance/cases/machine-no-init.accord new file mode 100644 index 0000000..993a3b2 --- /dev/null +++ b/conformance/cases/machine-no-init.accord @@ -0,0 +1,11 @@ +// expect: error +// A machine needs a way to start. +machine Switch { + state { + presses: i32, + } + + event press() { + next { presses: presses + 1 } + } +} diff --git a/conformance/cases/machine-observer.accord b/conformance/cases/machine-observer.accord new file mode 100644 index 0000000..b4f8ccd --- /dev/null +++ b/conformance/cases/machine-observer.accord @@ -0,0 +1,30 @@ +// expect: proved, proved, proved, proved, proved, proved +// `press` asks the observer `at_limit` whether to count, and knows its answer +// only through its contract. The observer's own `ensures` is proved too. +machine Counter { + state { + presses: i32, + } + + init start() { + next { presses: 0 } + } + + event press() { + if at_limit() { + next { } + } else { + next { presses: presses + 1 } + } + } + + /// Whether another press would pass the limit. + fn at_limit() -> Bool + ensures result implies presses == 100 + ensures presses == 100 implies result + { + presses == 100 + } + + invariant pressed: presses >= 0 and presses <= 100 +} diff --git a/conformance/cases/machine-overflow-fault.accord b/conformance/cases/machine-overflow-fault.accord new file mode 100644 index 0000000..f595af7 --- /dev/null +++ b/conformance/cases/machine-overflow-fault.accord @@ -0,0 +1,18 @@ +// expect: proved, proved, proved, refuted +// Without its `requires`, the third increment overflows `i32`. +machine Counter { + state { + count: i32, + } + + init near_top() { + next { count: 2147483645 } + } + + event increment() + { + next { count: count + 1 } + } + + invariant non_negative: count >= 0 +} diff --git a/conformance/cases/machine-overflow.accord b/conformance/cases/machine-overflow.accord new file mode 100644 index 0000000..b22a8b5 --- /dev/null +++ b/conformance/cases/machine-overflow.accord @@ -0,0 +1,19 @@ +// expect: proved, proved, proved, proved +// A counter that starts near the top of `i32` and stops below it. +machine Counter { + state { + count: i32, + } + + init near_top() { + next { count: 2147483645 } + } + + event increment() + requires count < 2147483647 + { + next { count: count + 1 } + } + + invariant non_negative: count >= 0 +} diff --git a/conformance/cases/machine-param-field.accord b/conformance/cases/machine-param-field.accord new file mode 100644 index 0000000..76121bf --- /dev/null +++ b/conformance/cases/machine-param-field.accord @@ -0,0 +1,11 @@ +// expect: error +// A parameter can't share a field's name. +machine Switch { + state { + presses: i32, + } + + init start(presses: i32) { + next { presses: presses } + } +} diff --git a/conformance/cases/machine-unhelped.accord b/conformance/cases/machine-unhelped.accord new file mode 100644 index 0000000..22aec2e --- /dev/null +++ b/conformance/cases/machine-unhelped.accord @@ -0,0 +1,22 @@ +// expect: proved, not_inductive, proved, proved, proved +// `y` never passes 3, since it moves with `x`, but the invariant alone doesn't +// say so: from `y == 3` and `x < 3`, which no run reaches, `step` breaks it. +// That is not a failure of the machine: a helper invariant settles it. +machine Pair { + state { + x: i32, + y: i32, + } + + init start() { + next { x: 0, y: 0 } + } + + event step() + requires x < 3 + { + next { x: x + 1, y: y + 1 } + } + + invariant y_bounded: y <= 3 +} diff --git a/conformance/cases/machine-unknown-field.accord b/conformance/cases/machine-unknown-field.accord new file mode 100644 index 0000000..f859b39 --- /dev/null +++ b/conformance/cases/machine-unknown-field.accord @@ -0,0 +1,11 @@ +// expect: error +// A `next` can only give values to the fields the state declares. +machine Switch { + state { + presses: i32, + } + + init start() { + next { presses: 0, count: 0 } + } +} diff --git a/conformance/cases/machine.accord b/conformance/cases/machine.accord new file mode 100644 index 0000000..267fbf8 --- /dev/null +++ b/conformance/cases/machine.accord @@ -0,0 +1,33 @@ +// expect: proved, proved, proved, proved, proved, passed +// A switch that counts its presses. The invariant holds of the state `start` +// gives and after each `press`, `press` is allowed in the state `start` +// gives, and each addition stays within `i32`. +enum Light { Off, On } + +machine Switch { + state { + light: Light, + presses: i32, + } + + init start() { + next { light: Off, presses: 0 } + } + + event press() + requires presses < 100 + { + if light == Off { + next { light: On, presses: presses + 1 } + } else { + next { light: Off, presses: presses + 1 } + } + } + + invariant pressed: presses >= 0 and presses <= 100 +} + +example Switch + start() + press() + gives light == On and presses == 1 From 10e8be501e6b2bfe6d5f6737f3d39912b51590fb Mon Sep 17 00:00:00 2001 From: Canitas <112231952+Sequela02@users.noreply.github.com> Date: Thu, 12 Nov 2026 20:25:30 -0700 Subject: [PATCH 2/9] feat: check machines with the solvers and an explorer A machine is desugared into functions of its state, so its inits, events and observers reuse the obligation machinery: the invariants are assumed of the state an event or observer reads and claimed of the state an init or event ends in. Z3 and cvc5 prove each obligation. An invariant or arithmetic obligation the solvers refute from a state is refuted only by a run from an init that a breadth-first explorer finds and the interpreter runs again; otherwise it is not_inductive, with the solvers' state, a standing of incomplete and ACC0015. An event is allowed in a reachable state only by such a run. What exploration covered is an annotation on the obligation, never an outcome. The receipt becomes version 4. `accord build` refuses a machine. `count` is a name again outside a quantifier, since machines have fields by it. Refs #82 --- crates/accord/src/check.rs | 48 ++- crates/accord/src/check/calls.rs | 9 + crates/accord/src/check/expr.rs | 4 + crates/accord/src/check/machine.rs | 329 +++++++++++++++ crates/accord/src/diagnostic.rs | 8 +- crates/accord/src/diff/strength.rs | 4 +- crates/accord/src/evidence.rs | 36 +- crates/accord/src/evidence/machine.rs | 351 ++++++++++++++++ crates/accord/src/evidence/standing.rs | 7 +- crates/accord/src/explore.rs | 451 +++++++++++++++++++++ crates/accord/src/identity.rs | 149 +++---- crates/accord/src/identity/normalize.rs | 5 + crates/accord/src/identity/source.rs | 5 + crates/accord/src/interpret.rs | 63 ++- crates/accord/src/interpret/eval.rs | 6 + crates/accord/src/interpret/machine.rs | 92 +++++ crates/accord/src/interpret/replay.rs | 15 +- crates/accord/src/interpret/value.rs | 2 +- crates/accord/src/ledger.rs | 7 +- crates/accord/src/lib.rs | 90 +++- crates/accord/src/mutation/mutants.rs | 3 + crates/accord/src/obligation.rs | 53 ++- crates/accord/src/obligation/claims.rs | 6 + crates/accord/src/obligation/lists.rs | 1 + crates/accord/src/obligation/operations.rs | 8 +- crates/accord/src/obligation/smt.rs | 98 ++++- crates/accord/src/openness.rs | 3 +- crates/accord/src/receipt.rs | 2 +- crates/accord/src/receipt/diagnostics.rs | 1 + crates/accord/src/receipt/json.rs | 58 ++- crates/accord/src/receipt/review.rs | 23 +- crates/accord/src/receipt/text.rs | 51 ++- crates/accord/src/syntax.rs | 73 ++++ crates/accord/src/syntax/declarations.rs | 65 ++- crates/accord/src/syntax/expr.rs | 6 +- crates/accord/src/syntax/machines.rs | 197 +++++++++ crates/accord/src/syntax/parser.rs | 17 +- crates/accord/src/typescript.rs | 10 + crates/accord/src/typescript/expr.rs | 1 + crates/accord/tests/cli.rs | 2 +- crates/accord/tests/conformance.rs | 1 + crates/accord/tests/diagnostics.rs | 2 +- crates/accord/tests/machines.rs | 123 ++++++ 43 files changed, 2317 insertions(+), 168 deletions(-) create mode 100644 crates/accord/src/check/machine.rs create mode 100644 crates/accord/src/evidence/machine.rs create mode 100644 crates/accord/src/explore.rs create mode 100644 crates/accord/src/interpret/machine.rs create mode 100644 crates/accord/src/syntax/machines.rs create mode 100644 crates/accord/tests/machines.rs diff --git a/crates/accord/src/check.rs b/crates/accord/src/check.rs index ca12964..25b8d99 100644 --- a/crates/accord/src/check.rs +++ b/crates/accord/src/check.rs @@ -6,6 +6,7 @@ mod calls; mod example; mod expr; mod lists; +mod machine; mod operators; use calls::{Signature, check_recursion, ordered}; @@ -116,6 +117,7 @@ pub(crate) fn check(program: &mut Program, files: &[String]) -> Result<(), Diagn name: f.name.clone(), params: f.params.clone(), ret: f.ret.clone(), + state: Vec::new(), }) .collect(); for function in &mut program.functions { @@ -130,23 +132,38 @@ pub(crate) fn check(program: &mut Program, files: &[String]) -> Result<(), Diagn .map_or(0, |f| f.file); d.in_file(&name(file)) })?; + for (index, machine) in program.machines.iter().enumerate() { + if program.machines[..index] + .iter() + .any(|other| other.name == machine.name) + || program.functions.iter().any(|f| f.name == machine.name) + { + return Err(Diagnostic::new( + machine.line, + format!("`{}` is declared more than once", machine.name), + ) + .in_file(&name(machine.file))); + } + } + for machine in &mut program.machines { + let file = name(machine.file); + machine::check(enums, &signatures, &program.functions, machine) + .map_err(|d| d.in_file(&file))?; + } let functions = &program.functions; for example in &mut program.examples { let file = name(example.file); example::check(enums, functions, example).map_err(|d| d.in_file(&file))?; } + for run in &mut program.machine_examples { + let file = name(run.file); + machine::check_run(enums, &program.machines, run).map_err(|d| d.in_file(&file))?; + } Ok(()) } -fn check_function( - enums: &[Enum], - signatures: &[Signature], - function: &mut Function, -) -> Result<(), Diagnostic> { - for (_, ty) in &function.params { - check_type(enums, ty, function.line)?; - } - check_type(enums, &function.ret, function.line)?; +/// Checks each clause of `function` against its parameters. +fn check_clauses(enums: &[Enum], function: &mut Function) -> Result<(), Diagnostic> { for clause in &mut function.clauses { let scope = Scope { enums, @@ -164,6 +181,19 @@ fn check_function( )); } } + Ok(()) +} + +fn check_function( + enums: &[Enum], + signatures: &[Signature], + function: &mut Function, +) -> Result<(), Diagnostic> { + for (_, ty) in &function.params { + check_type(enums, ty, function.line)?; + } + check_type(enums, &function.ret, function.line)?; + check_clauses(enums, function)?; let scope = Scope { enums, params: &function.params, diff --git a/crates/accord/src/check/calls.rs b/crates/accord/src/check/calls.rs index 40153b6..d8dfdc8 100644 --- a/crates/accord/src/check/calls.rs +++ b/crates/accord/src/check/calls.rs @@ -7,10 +7,15 @@ use crate::Diagnostic; use crate::syntax::{Body, Expr, Function, Program, Type}; /// What a call needs to know about the function it calls. +#[derive(Clone)] pub(super) struct Signature { pub name: String, + /// The parameters a call gives. pub params: Vec<(String, Type)>, pub ret: Type, + /// The machine fields an observer reads, which a call passes on as its + /// first arguments; empty for a function. + pub state: Vec<(String, Type)>, } impl Scope<'_> { @@ -36,6 +41,9 @@ impl Scope<'_> { return Err(Diagnostic::new(line, format!("unknown function `{name}`"))); }; let ordered = ordered(name, &callee.params, std::mem::take(args), line)?; + for (field, _) in &callee.state { + args.push((Some(field.clone()), Expr::Name(field.clone(), line))); + } for ((param, ty), mut expr) in callee.params.iter().zip(ordered) { self.value( &mut expr, @@ -123,6 +131,7 @@ pub(crate) fn callees(expr: &Expr, out: &mut Vec) { callees(condition, out); } Expr::Length(list, _) => callees(list, out), + Expr::Next(fields, _) => fields.iter().for_each(|(_, value)| callees(value, out)), Expr::Index(list, index, _) => { callees(list, out); callees(index, out); diff --git a/crates/accord/src/check/expr.rs b/crates/accord/src/check/expr.rs index 12e852e..032d116 100644 --- a/crates/accord/src/check/expr.rs +++ b/crates/accord/src/check/expr.rs @@ -198,6 +198,10 @@ impl Scope<'_> { self.quantified(*quantifier, name, range, condition, *line) } Expr::Length(list, line) => self.length(list, *line), + Expr::Next(_, line) => Err(Diagnostic::new( + *line, + "`next` can only end an init or an event", + )), Expr::Index(list, index, site) => self.index(list, index, site.line), Expr::If(condition, then, otherwise) => { self.condition(condition)?; diff --git a/crates/accord/src/check/machine.rs b/crates/accord/src/check/machine.rs new file mode 100644 index 0000000..5b2e9e4 --- /dev/null +++ b/crates/accord/src/check/machine.rs @@ -0,0 +1,329 @@ +//! A machine's state, inits, events, observers and invariants, and the runs +//! its examples give. Checking desugars a machine into functions: each member +//! takes the machine's fields as its first parameters and carries the +//! invariants as clauses, and each `next` gives every field, in order. + +use super::calls::{Signature, check_recursion, ordered}; +use super::expr::Scope; +use super::{check_clauses, check_function, check_type, type_name}; +use crate::Diagnostic; +use crate::syntax::{ + Body, Enum, Expr, Function, Machine, MachineExample, Member, Program, Role, Type, +}; + +/// Checks `machine` against the program's `enums` and `functions`, whose +/// signatures are `globals`, and desugars it. +pub(super) fn check( + enums: &[Enum], + globals: &[Signature], + functions: &[Function], + machine: &mut Machine, +) -> Result<(), Diagnostic> { + let state = machine.state.clone(); + check_state(enums, machine)?; + if machine.inits.is_empty() { + return Err(Diagnostic::new( + machine.line, + format!("`{}` needs an `init`: a way to start", machine.name), + )); + } + check_names(machine, functions)?; + for member in machine + .inits + .iter() + .chain(&machine.events) + .chain(&machine.observers) + { + for (param, ty) in &member.params { + check_type(enums, ty, member.line)?; + if param == "next" || state.iter().any(|(field, _)| field == param) { + return Err(Diagnostic::new( + member.line, + format!("a parameter can't be named `{param}`: it is a field or `next`"), + )); + } + } + } + let mut signatures = globals.to_vec(); + signatures.extend(machine.observers.iter().map(|observer| Signature { + name: observer.name.clone(), + params: observer.params.clone(), + ret: observer.ret.clone(), + state: state.clone(), + })); + for init in &mut machine.inits { + // An init doesn't read the state: its fields are placeholders, added + // once its body is checked. + check_clauses(enums, init)?; + check_body(enums, globals, init, &state)?; + with_state(init, &state); + } + for event in &mut machine.events { + with_state(event, &state); + check_clauses(enums, event)?; + check_body(enums, &signatures, event, &state)?; + } + for observer in &mut machine.observers { + with_state(observer, &state); + check_function(enums, &signatures, observer)?; + } + check_recursion(&Program { + enums: Vec::new(), + functions: functions + .iter() + .chain(&machine.observers) + .cloned() + .collect(), + machines: Vec::new(), + examples: Vec::new(), + machine_examples: Vec::new(), + })?; + for invariant in &mut machine.invariants { + let scope = Scope { + enums, + params: &state, + result: None, + spec: true, + functions: None, + indexing: false, + bound: false, + }; + scope.condition(&mut invariant.expr)?; + } + let invariants = machine.invariants.clone(); + for member in machine + .inits + .iter_mut() + .chain(&mut machine.events) + .chain(&mut machine.observers) + { + member.clauses.extend(invariants.iter().cloned()); + } + Ok(()) +} + +fn check_state(enums: &[Enum], machine: &Machine) -> Result<(), Diagnostic> { + for (index, (field, ty)) in machine.state.iter().enumerate() { + check_type(enums, ty, machine.line)?; + if !matches!(ty, Type::Bool | Type::Int(_) | Type::Enum(_)) { + return Err(Diagnostic::new( + machine.line, + format!( + "`{field}` is a `{}`: a state holds fixed-width integers, enums and `Bool`s", + type_name(ty) + ), + )); + } + if field == "next" { + return Err(Diagnostic::new( + machine.line, + "a field can't be named `next`", + )); + } + if machine.state[..index] + .iter() + .any(|(other, _)| other == field) + { + return Err(Diagnostic::new( + machine.line, + format!("`{field}` is a field twice"), + )); + } + } + Ok(()) +} + +/// Every init, event and observer has a name of its own, and an observer +/// isn't named like a function it could be mistaken for. +fn check_names(machine: &Machine, functions: &[Function]) -> Result<(), Diagnostic> { + let members: Vec<&Function> = machine.members().collect(); + for (index, member) in members.iter().enumerate() { + let observer = member.machine.is_some_and(|m| m.role == Role::Observer); + if members[..index] + .iter() + .any(|other| other.name == member.name) + || (observer && functions.iter().any(|f| f.name == member.name)) + { + return Err(Diagnostic::new( + member.line, + format!("`{}` is declared more than once", member.name), + )); + } + } + Ok(()) +} + +/// Puts the machine's fields before `member`'s own parameters. +fn with_state(member: &mut Function, state: &[(String, Type)]) { + let mut params = state.to_vec(); + params.append(&mut member.params); + member.params = params; + if let Some(machine) = &mut member.machine { + *machine = Member { + role: machine.role, + state: state.len(), + }; + } +} + +/// Checks an init's or event's body, which ends in `next` through `if` or a +/// decision table. An init's scope has no fields. +fn check_body( + enums: &[Enum], + signatures: &[Signature], + member: &mut Function, + state: &[(String, Type)], +) -> Result<(), Diagnostic> { + let init = member.machine.is_some_and(|m| m.role == Role::Init); + let scope = Scope { + enums, + params: &member.params, + result: None, + spec: false, + functions: Some(signatures), + indexing: true, + bound: false, + }; + let name = member.name.clone(); + match &mut member.body { + Body::Expr(body) => step(&scope, state, init.then_some(&name), body), + Body::Decide(rows, _) => { + for row in rows { + if let Some(condition) = &mut row.condition { + scope.condition(condition)?; + } + step(&scope, state, init.then_some(&name), &mut row.result)?; + } + Ok(()) + } + } +} + +/// Checks the `if`s and the `next` that end in a body, and gives each `next` +/// every field. An init (`init` names it) must give each field; an event +/// keeps the value of any it leaves out. +fn step( + scope: &Scope, + state: &[(String, Type)], + init: Option<&String>, + expr: &mut Expr, +) -> Result<(), Diagnostic> { + match expr { + Expr::If(condition, then, otherwise) => { + scope.condition(condition)?; + step(scope, state, init, then)?; + step(scope, state, init, otherwise) + } + Expr::Next(fields, line) => { + let line = *line; + let mut values: Vec> = state.iter().map(|_| None).collect(); + for (name, value) in std::mem::take(fields) { + let Some(index) = state.iter().position(|(field, _)| *field == name) else { + return Err(Diagnostic::new( + line, + format!("`{name}` isn't a field of the state"), + )); + }; + if values[index].replace(value).is_some() { + return Err(Diagnostic::new( + line, + format!("`next` gives `{name}` twice"), + )); + } + } + for (value, (field, ty)) in values.into_iter().zip(state) { + let mut value = match (value, init) { + (Some(value), _) => value, + (None, Some(init)) => { + return Err(Diagnostic::new( + line, + format!("`{init}` leaves `{field}` out: an init gives every field"), + )); + } + (None, None) => Expr::Name(field.clone(), line), + }; + scope.value( + &mut value, + ty, + &format!("`{field}` needs a `{}`", type_name(ty)), + )?; + fields.push((field.clone(), value)); + } + Ok(()) + } + other => Err(Diagnostic::new( + other.line(), + "an init or event ends in `next { … }`", + )), + } +} + +/// Checks an example's run of `machine`: an init, then events, each with +/// arguments put in the order of its parameters, and the condition it gives. +pub(super) fn check_run( + enums: &[Enum], + machines: &[Machine], + run: &mut MachineExample, +) -> Result<(), Diagnostic> { + let Some(machine) = machines.iter().find(|m| m.name == run.machine) else { + return Err(Diagnostic::new( + run.line, + format!("unknown machine `{}`", run.machine), + )); + }; + if run.steps.is_empty() { + return Err(Diagnostic::new( + run.line, + "an example runs an init, then events", + )); + } + let constants = Scope { + enums, + params: &[], + result: None, + spec: false, + functions: None, + indexing: false, + bound: false, + }; + for (index, step) in run.steps.iter_mut().enumerate() { + let line = step.line(); + let Expr::Call(name, args, _) = step else { + return Err(Diagnostic::new( + line, + "each step is an init's or an event's call", + )); + }; + let (pool, kind) = if index == 0 { + (&machine.inits, "an init") + } else { + (&machine.events, "an event") + }; + let Some(member) = pool.iter().find(|f| f.name == *name) else { + return Err(Diagnostic::new( + line, + format!("`{name}` isn't {kind} of `{}`", machine.name), + )); + }; + let own = &member.params[machine.state.len()..]; + let given = ordered(name, own, std::mem::take(args), line)?; + for ((param, ty), mut expr) in own.iter().zip(given) { + constants.value( + &mut expr, + ty, + &format!("`{param}` needs a `{}`", type_name(ty)), + )?; + args.push((Some(param.clone()), expr)); + } + } + let scope = Scope { + enums, + params: &machine.state, + result: None, + spec: true, + functions: None, + indexing: false, + bound: false, + }; + scope.condition(&mut run.gives) +} diff --git a/crates/accord/src/diagnostic.rs b/crates/accord/src/diagnostic.rs index bea4c9c..0c68157 100644 --- a/crates/accord/src/diagnostic.rs +++ b/crates/accord/src/diagnostic.rs @@ -33,11 +33,14 @@ pub enum DiagnosticCode { /// A function calls one that isn't verified, whose contract its proofs /// assume. UnverifiedCallee, + /// A machine's obligation fails from a state that meets every invariant + /// and helper invariant, and no run from an init was found to reach it. + NotInductive, } impl DiagnosticCode { /// The entire allocated catalog, including conditions with no current source producer. - pub const ALL: [Self; 14] = [ + pub const ALL: [Self; 15] = [ Self::SourceRejected, Self::ObligationRefuted, Self::ObligationUndecided, @@ -52,6 +55,7 @@ impl DiagnosticCode { Self::NoEvidence, Self::WeakCalleeContract, Self::UnverifiedCallee, + Self::NotInductive, ]; /// The permanent machine identifier, independent of severity and wording. @@ -71,6 +75,7 @@ impl DiagnosticCode { Self::NoEvidence => "ACC0012", Self::WeakCalleeContract => "ACC0013", Self::UnverifiedCallee => "ACC0014", + Self::NotInductive => "ACC0015", } } @@ -88,6 +93,7 @@ impl DiagnosticCode { Self::NoEvidence => "add_checks", Self::WeakCalleeContract => "strengthen_callee_contract", Self::UnverifiedCallee => "verify_callee", + Self::NotInductive => "add_helper_invariant", } } } diff --git a/crates/accord/src/diff/strength.rs b/crates/accord/src/diff/strength.rs index de67d1d..24ca3d3 100644 --- a/crates/accord/src/diff/strength.rs +++ b/crates/accord/src/diff/strength.rs @@ -65,7 +65,7 @@ pub(super) fn at_least_as_strong( evidence: crate::Refutation::Counterexample(inputs), } => return Ok(Some(Loosening::Rejects(unit.source_inputs(&inputs)))), Outcome::Undecided { reason } | Outcome::Unsupported { reason } => return Err(reason), - Outcome::Refuted { .. } | Outcome::WeakCallee { .. } => { + Outcome::Refuted { .. } | Outcome::WeakCallee { .. } | Outcome::NotInductive { .. } => { return Err("no counterexample".to_string()); } } @@ -117,7 +117,7 @@ pub(super) fn at_least_as_strong( Ok(Some(Loosening::Allows(unit.source_inputs(&inputs), result))) } Outcome::Undecided { reason } | Outcome::Unsupported { reason } => Err(reason), - Outcome::Refuted { .. } | Outcome::WeakCallee { .. } => { + Outcome::Refuted { .. } | Outcome::WeakCallee { .. } | Outcome::NotInductive { .. } => { Err("no counterexample".to_string()) } } diff --git a/crates/accord/src/evidence.rs b/crates/accord/src/evidence.rs index 476e78a..fb173ba 100644 --- a/crates/accord/src/evidence.rs +++ b/crates/accord/src/evidence.rs @@ -1,13 +1,15 @@ //! Everything one check establishes: each obligation's outcome, each //! example's run, and the standing they add up to. +mod machine; mod standing; use standing::{file_standing, standing_of}; use crate::{ - Definition, Determinacy, ExampleRun, Inputs, ObligationKind, Outcome, Refutation, Report, Run, - Solvers, Standing, Verdict, identity, interpret, mutation, obligation, openness, syntax, + Definition, DefinitionKind, Determinacy, ExampleRun, Inputs, ObligationKind, Outcome, + Refutation, Report, Run, Solvers, Standing, Verdict, identity, interpret, mutation, obligation, + openness, syntax, }; /// What the solvers established about `o`, in source terms: a model's call @@ -71,12 +73,19 @@ pub(crate) fn report( let file_of = |file: usize| names.get(file).cloned(); let all_units = identity::units(program); let targeted = |unit: &identity::Unit| target.is_none_or(|t| unit.source.file == t); + let machines: Vec<_> = program + .machines + .iter() + .filter(|machine| target.is_none_or(|t| machine.file == t)) + .map(|machine| (machine, machine::check(program, machine, solvers))) + .collect(); let needed: Vec = all_units .iter() .filter(|unit| targeted(unit)) .flat_map(|unit| { std::iter::once(unit.source.name.clone()).chain(unit.callees.iter().cloned()) }) + .chain(machines.iter().flat_map(|(_, c)| c.callees.iter().cloned())) .collect(); let units: Vec<_> = all_units .into_iter() @@ -100,6 +109,8 @@ pub(crate) fn report( obligation::Claim::InRange { .. } => ObligationKind::Overflow, obligation::Claim::Requires { .. } => ObligationKind::Precondition, obligation::Claim::InBounds { .. } => ObligationKind::Bounds, + obligation::Claim::Invariants => ObligationKind::Invariant, + obligation::Claim::Allowed => ObligationKind::Allowed, }, outcome: outcome_of(unit, &o, outcome), function: unit.source.name.clone(), @@ -108,6 +119,7 @@ pub(crate) fn report( reused, clause: o.clause, line: o.line, + exploration: None, }); } } @@ -171,11 +183,12 @@ pub(crate) fn report( standing = Standing::Incomplete; } Definition { + kind: DefinitionKind::Function, name: unit.source.name.clone(), intent: unit.source.intent.clone(), line: unit.source.line, params: unit.source.params.clone(), - result_type: unit.source.ret.clone(), + result_type: Some(unit.source.ret.clone()), specification: unit .source .clauses @@ -212,6 +225,23 @@ pub(crate) fn report( .filter(|d| reported(&d.function)) .collect(); let units: Vec<_> = units.into_iter().filter(|unit| targeted(unit)).collect(); + let (mut definitions, mut verdicts, mut examples) = (definitions, verdicts, examples); + for (machine, checked) in machines { + let mut definition = checked.definition; + definition.file = file_of(machine.file); + definition.unverified_callees = checked + .callees + .into_iter() + .filter(|name| standing_of_name(name) != Standing::Verified) + .collect(); + definition.standing = standing_of(checked.verdicts.iter(), checked.runs.iter(), None); + if definition.standing == Standing::Verified && !definition.unverified_callees.is_empty() { + definition.standing = Standing::Incomplete; + } + definitions.push(definition); + verdicts.extend(checked.verdicts); + examples.extend(checked.runs); + } let standing = file_standing(&definitions); let strength = if solvers.mutates() { let proved_units: Vec<_> = units diff --git a/crates/accord/src/evidence/machine.rs b/crates/accord/src/evidence/machine.rs new file mode 100644 index 0000000..17659b5 --- /dev/null +++ b/crates/accord/src/evidence/machine.rs @@ -0,0 +1,351 @@ +//! A machine's evidence. Its inits, events and observers are checked as +//! functions that read the machine's state, with its invariants assumed. +//! The solvers decide each obligation; where one is refuted from a state, +//! the explorer decides whether a run from an init reaches it. The machine +//! is proved only by the solvers, and refuted only by a replayed run. + +use super::outcome_of; +use crate::explore::{self, Exploration as Explored, Member, Step, Trace}; +use crate::interpret; +use crate::obligation::{self, Claim, Obligation}; +use crate::syntax::{Machine, Program, Role}; +use crate::{ + Definition, DefinitionKind, ExampleRun, Exploration, Inputs, ObligationKind, Outcome, + Refutation, Run, Solvers, Standing, TraceStep, Verdict, identity, syntax, +}; + +/// What checking a machine established, short of its standing. +pub(super) struct Checked { + pub verdicts: Vec, + pub runs: Vec, + pub definition: Definition, + /// The functions of the program, not of the machine, that its members call. + pub callees: Vec, +} + +/// The program as the machine's members see it: its functions, and the +/// machine's observers as functions known by their contracts, without the +/// invariants they assume. +fn callee_view(program: &Program, machine: &Machine) -> Program { + let mut functions = program.functions.clone(); + for observer in &machine.observers { + let mut callee = observer.clone(); + callee + .clauses + .retain(|c| c.kind != syntax::ClauseKind::Invariant); + functions.push(callee); + } + Program { + enums: program.enums.clone(), + functions, + machines: Vec::new(), + examples: Vec::new(), + machine_examples: Vec::new(), + } +} + +/// A run as steps in source terms: each call with its arguments, and the +/// state it leaves. +fn steps(units: &[identity::Unit], trace: &Trace, last: bool) -> Vec { + let step = |step: &Step| { + let unit = &units[step.member]; + let function = unit.source; + let state = function.machine.map_or(0, |m| m.state); + let own = &function.params[state..]; + let args: Vec = own + .iter() + .zip(&step.args) + .map(|((name, _), value)| { + if own.len() == 1 { + unit.source_of(value) + } else { + format!("{name}: {}", unit.source_of(value)) + } + }) + .collect(); + TraceStep { + call: format!("{}({})", function.name, args.join(", ")), + state: step.state.as_ref().map(|values| { + function.params[..state] + .iter() + .zip(values) + .map(|((name, _), value)| (name.clone(), unit.source_of(value))) + .collect() + }), + } + }; + trace + .path + .iter() + .chain(last.then_some(&trace.last)) + .map(step) + .collect() +} + +/// The arguments of `step`, as inputs in source terms. +fn arguments(unit: &identity::Unit, step: &Step) -> Inputs { + let function = unit.source; + let state = function.machine.map_or(0, |m| m.state); + function.params[state..] + .iter() + .zip(&step.args) + .map(|((name, _), value)| (name.clone(), unit.source_of(value))) + .collect() +} + +/// Without the placeholders an init has for the state it doesn't read. +fn own_only(unit: &identity::Unit, inputs: Inputs) -> Inputs { + let state = unit.source.machine.map_or(0, |m| m.state); + let fields: Vec<&String> = unit.source.params[..state].iter().map(|(n, _)| n).collect(); + inputs + .into_iter() + .filter(|(name, _)| !fields.contains(&name)) + .collect() +} + +fn unreached(explored: &Explored) -> String { + format!( + "no run from an init was found to a state that allows it: {} states explored, {}", + explored.states, + if explored.complete { + "every one of them" + } else { + "but not every state, or every way to move from one, could be" + } + ) +} + +/// What deciding a machine's obligations draws on. +struct Context<'a> { + units: &'a [identity::Unit<'a>], + members: &'a [Member<'a>], + explored: &'a Explored, + solvers: &'a Solvers, +} + +impl Context<'_> { + fn note(&self, trace: Option>) -> Option { + Some(Exploration { + states: self.explored.states, + complete: self.explored.complete, + trace, + }) + } + + /// The outcome of the obligation `ob`, the `o`th of member `m`, whether it + /// came from the ledger, and what exploring the states covered if it + /// was consulted. + fn decide(&self, m: usize, o: usize, ob: &Obligation) -> (Outcome, bool, Option) { + let unit = &self.units[m]; + let role = unit.source.machine.map_or(Role::Observer, |x| x.role); + let allowed = matches!(ob.claim, Claim::Allowed); + if role == Role::Event + && allowed + && let Some(trace) = self + .explored + .allowed + .get(&m) + .filter(|trace| explore::confirms(self.members, m, None, trace)) + { + let proved = Outcome::Proved { + witness: Some(arguments(unit, &trace.last)), + }; + return ( + proved, + false, + self.note(Some(steps(self.units, trace, true))), + ); + } + let (outcome, reused) = self.solvers.decide_calls( + &ob.script, + &unit.callee_bodies, + &ob.params, + ob.polarity, + |model| interpret::replay(ob, model), + ); + // An init that breaks an invariant is a run of one step. + let started = match (&ob.claim, &outcome) { + ( + Claim::Invariants, + Outcome::Refuted { + evidence: Refutation::Counterexample(model), + }, + ) if role == Role::Init => explore::start(self.members, m, model), + _ => None, + }; + let outcome = outcome_of(unit, ob, outcome); + if let Some(last) = started { + let trace = Trace { + path: Vec::new(), + last, + }; + let refuted = Outcome::Refuted { + evidence: Refutation::Trace(steps(self.units, &trace, true)), + }; + return (refuted, reused, None); + } + let from_state = + role != Role::Init && !allowed && ob.polarity == obligation::Polarity::Universal; + let failure = self + .explored + .failures + .get(&(m, o)) + .filter(|trace| from_state && explore::confirms(self.members, m, Some(ob), trace)); + // A run that breaks it refutes it, whatever else the solvers say; + // if they proved it, they proved it from the contract of a function + // the run calls, or something is wrong. + if let Some(trace) = failure { + let outcome = match outcome { + Outcome::Proved { .. } => Outcome::Undecided { + reason: "the solvers proved it, but a run from an init breaks it".to_string(), + }, + _ => Outcome::Refuted { + evidence: Refutation::Trace(steps(self.units, trace, true)), + }, + }; + return (outcome, reused, self.note(None)); + } + let outcome = match (role, outcome) { + (Role::Event, Outcome::Proved { .. }) if allowed => Outcome::Undecided { + reason: unreached(self.explored), + }, + (Role::Init, Outcome::Proved { witness: Some(w) }) => Outcome::Proved { + witness: Some(own_only(unit, w)), + }, + ( + Role::Init, + Outcome::Refuted { + evidence: Refutation::Counterexample(inputs), + }, + ) => Outcome::Refuted { + evidence: Refutation::Counterexample(own_only(unit, inputs)), + }, + ( + _, + Outcome::Refuted { + evidence: Refutation::Counterexample(inputs), + }, + ) if from_state => Outcome::NotInductive { inputs }, + (_, other) => other, + }; + let consulted = + role == Role::Event && allowed || matches!(outcome, Outcome::NotInductive { .. }); + ( + outcome, + reused, + consulted.then(|| self.note(None)).flatten(), + ) + } +} + +/// Checks `machine`: every obligation of its members and each of its +/// examples. +pub(super) fn check(program: &Program, machine: &Machine, solvers: &Solvers) -> Checked { + let view = callee_view(program, machine); + let units: Vec = machine + .members() + .map(|member| identity::unit(&view, member)) + .collect(); + let obligations: Vec> = units + .iter() + .map(|unit| obligation::unit_obligations(&unit.program)) + .collect(); + let members: Vec = units + .iter() + .zip(&obligations) + .map(|(unit, obligations)| Member { unit, obligations }) + .collect(); + let explored = explore::explore(&members); + let hash = identity::hash( + &units + .iter() + .map(|unit| unit.hash.as_str()) + .collect::>() + .join(" "), + ); + let context = Context { + units: &units, + members: &members, + explored: &explored, + solvers, + }; + let mut verdicts = Vec::new(); + for (m, obligations) in obligations.iter().enumerate() { + for (o, ob) in obligations.iter().enumerate() { + let (outcome, reused, exploration) = context.decide(m, o, ob); + verdicts.push(Verdict { + kind: match ob.claim { + Claim::Ensures(_) => ObligationKind::Postcondition, + Claim::Covered => ObligationKind::Coverage, + Claim::Reaches(_) => ObligationKind::RowReachability, + Claim::InRange { .. } => ObligationKind::Overflow, + Claim::Requires { .. } => ObligationKind::Precondition, + Claim::InBounds { .. } => ObligationKind::Bounds, + Claim::Invariants => ObligationKind::Invariant, + Claim::Allowed => ObligationKind::Allowed, + }, + outcome, + function: machine.name.clone(), + key: identity::hash(&ob.script), + definition: hash.clone(), + reused, + clause: ob.clause.clone(), + line: ob.line, + exploration, + }); + } + } + let functions: Vec<&str> = machine.observers.iter().map(|f| f.name.as_str()).collect(); + let mut callees: Vec = Vec::new(); + for name in units.iter().flat_map(|unit| unit.callees.iter()) { + if !functions.contains(&name.as_str()) && !callees.contains(name) { + callees.push(name.clone()); + } + } + let runs = program + .machine_examples + .iter() + .filter(|example| example.machine == machine.name) + .map(|example| ExampleRun { + function: machine.name.clone(), + text: example.text.clone(), + line: example.line, + run: match interpret::run_machine(example, machine, &view.functions) { + Ok(()) => Run::Passed, + Err(reason) => Run::Failed { reason }, + }, + }) + .collect(); + let mut enums: Vec<(String, Vec)> = Vec::new(); + for unit in &units { + for e in unit.source_enums() { + if !enums.contains(&e) { + enums.push(e); + } + } + } + let definition = Definition { + kind: DefinitionKind::Machine, + name: machine.name.clone(), + intent: machine.intent.clone(), + line: machine.line, + params: machine.state.clone(), + result_type: None, + specification: machine + .invariants + .iter() + .map(|c| (c.line, c.text.clone())) + .collect(), + enums, + file: None, + hash, + standing: Standing::Unverified, + unverified_callees: Vec::new(), + }; + Checked { + verdicts, + runs, + definition, + callees, + } +} diff --git a/crates/accord/src/evidence/standing.rs b/crates/accord/src/evidence/standing.rs index d1c5412..8abea73 100644 --- a/crates/accord/src/evidence/standing.rs +++ b/crates/accord/src/evidence/standing.rs @@ -23,7 +23,8 @@ pub(super) fn standing_of<'a>( Outcome::Refuted { .. } => failed = true, Outcome::Undecided { .. } | Outcome::Unsupported { .. } - | Outcome::WeakCallee { .. } => open = true, + | Outcome::WeakCallee { .. } + | Outcome::NotInductive { .. } => open = true, } } for example in examples { @@ -69,6 +70,7 @@ mod tests { key: String::new(), definition: String::new(), reused: false, + exploration: None, } } @@ -125,10 +127,11 @@ mod tests { let definitions: Vec = standings .iter() .map(|&standing| Definition { + kind: crate::DefinitionKind::Function, intent: None, line: 1, params: Vec::new(), - result_type: crate::Type::Bool, + result_type: Some(crate::Type::Bool), specification: Vec::new(), enums: Vec::new(), name: "f".to_string(), diff --git a/crates/accord/src/explore.rs b/crates/accord/src/explore.rs new file mode 100644 index 0000000..ce735e9 --- /dev/null +++ b/crates/accord/src/explore.rs @@ -0,0 +1,451 @@ +//! Exploring a machine's reachable states, breadth first from every init, so +//! that the traces it finds are the shortest. +//! +//! A trace is what refutes an invariant, or an arithmetic operation, in a +//! state the solvers only reach from outside the machine, and what shows an +//! event is allowed in a state the machine reaches. The explorer runs the +//! machine with the interpreter, in code, and every trace is run again from its +//! init before it is believed ([`replay`]). +//! +//! A parameter is enumerated only when its values are finite and known: +//! `Bool`, an enum, or an integer whose `requires` lists its values or bounds +//! it by literals to at most [`MAX_DOMAIN`] values. An init or event with any +//! other parameter isn't explored, and exploration is then incomplete, as it +//! is when it reaches [`MAX_STATES`] states or runs [`MAX_STEPS`] steps. + +use std::collections::{HashMap, VecDeque}; + +use crate::identity::Unit; +use crate::interpret::{self, Value}; +use crate::obligation::{Claim, Obligation, Polarity}; +use crate::syntax::{ClauseKind, Expr, Function, Op, Role, Type, Width}; + +/// The most states the explorer keeps. +const MAX_STATES: usize = 100_000; +/// The most times it runs an init, an event or an observer. +const MAX_STEPS: usize = 2_000_000; +/// The most values it enumerates for one integer parameter. +const MAX_DOMAIN: i128 = 1024; + +/// An init, event or observer, normalized, with its obligations. +pub(crate) struct Member<'a> { + pub unit: &'a Unit<'a>, + pub obligations: &'a [Obligation<'a>], +} + +impl Member<'_> { + /// The normalized function, the first of the unit's. + pub fn function(&self) -> &Function { + &self.unit.program.functions[0] + } + + fn role(&self) -> Role { + self.function() + .machine + .map_or(Role::Observer, |member| member.role) + } + + /// The names and values of the member's own parameters. + fn own(&self, args: &[Value]) -> Vec<(String, Value)> { + let function = self.function(); + let skip = function.machine.map_or(0, |m| m.state); + function.params[skip..] + .iter() + .map(|(name, _)| name.clone()) + .zip(args.iter().cloned()) + .collect() + } + + /// The values the member runs on in `state`: its fields, then `args`. + pub fn names(&self, state: Option<&[Value]>, args: &[Value]) -> Vec<(String, Value)> { + let mut names = state.map_or_else(Vec::new, |s| interpret::fields(self.function(), s)); + names.extend(self.own(args)); + names + } + + /// The state the member ends in, when it is run in code. + pub fn run(&self, state: Option<&[Value]>, args: &[Value]) -> Result, String> { + interpret::transition( + self.function(), + &self.names(state, args), + &self.unit.program.functions, + ) + } +} + +/// One step of a run: an init or event, its arguments, and the state it +/// leaves, where it leaves one. +#[derive(Clone)] +pub(crate) struct Step { + pub member: usize, + pub args: Vec, + pub state: Option>, +} + +/// A run to a state, and what is done in that state: an event or observer, +/// with its arguments. +pub(crate) struct Trace { + pub path: Vec, + pub last: Step, +} + +/// What exploring a machine found. +pub(crate) struct Exploration { + /// The states reached. + pub states: usize, + /// Whether every state, and every way to move from it, was visited. + pub complete: bool, + /// For a member's obligation, by their positions, the shortest trace to a + /// state where the obligation fails. + pub failures: HashMap<(usize, usize), Trace>, + /// For an event, by its position, the shortest trace to a state where its + /// `requires` hold, with the arguments that make them. + pub allowed: HashMap, +} + +struct Node { + state: Vec, + via: (Option, usize, Vec), +} + +fn path(nodes: &[Node], mut at: usize) -> Vec { + let mut steps = Vec::new(); + loop { + let node = &nodes[at]; + steps.push(Step { + member: node.via.1, + args: node.via.2.clone(), + state: Some(node.state.clone()), + }); + match node.via.0 { + Some(parent) => at = parent, + None => break, + } + } + steps.reverse(); + steps +} + +/// The literal an expression is, if it is one. +fn literal(expr: &Expr) -> Option { + match expr { + Expr::Int(n, _) => Some(*n), + Expr::Neg(inner, _) => literal(inner).map(|n| -n), + _ => None, + } +} + +fn is(expr: &Expr, name: &str) -> bool { + matches!(expr, Expr::Name(n, _) if n == name) +} + +/// The values a condition lists for `name`: equalities to literals, joined by +/// `or`, or membership in a list of literals. +fn listed(name: &str, condition: &Expr) -> Option> { + match condition { + Expr::Binary(Op::Or, left, right) => { + let mut values = listed(name, left)?; + values.extend(listed(name, right)?); + Some(values) + } + Expr::Binary(Op::Eq, left, right) if is(left, name) => literal(right).map(|n| vec![n]), + Expr::Binary(Op::Eq, left, right) if is(right, name) => literal(left).map(|n| vec![n]), + Expr::Binary(Op::In, element, list) if is(element, name) => match &**list { + Expr::List(items, ..) => items.iter().map(literal).collect(), + _ => None, + }, + _ => None, + } +} + +fn conjuncts<'a>(condition: &'a Expr, out: &mut Vec<&'a Expr>) { + match condition { + Expr::Binary(Op::And, left, right) => { + conjuncts(left, out); + conjuncts(right, out); + } + other => out.push(other), + } +} + +/// The operator that reads the same with its sides swapped. +fn flipped(op: Op) -> Option { + Some(match op { + Op::Lt => Op::Gt, + Op::Le => Op::Ge, + Op::Gt => Op::Lt, + Op::Ge => Op::Le, + _ => return None, + }) +} + +/// The values of an integer parameter that its `requires` pin down: those it +/// lists, or the range its literal bounds give, if that holds at most +/// [`MAX_DOMAIN`] values. +fn integers(name: &str, width: Width, requires: &[&Expr]) -> Option> { + let (mut low, mut high): (Option, Option) = (None, None); + let mut set: Option> = None; + let mut conditions = Vec::new(); + requires.iter().for_each(|r| conjuncts(r, &mut conditions)); + for condition in conditions { + if let Some(values) = listed(name, condition) { + set = Some(match set { + Some(old) => old.into_iter().filter(|v| values.contains(v)).collect(), + None => values, + }); + continue; + } + let Expr::Binary(op, left, right) = condition else { + continue; + }; + let bound = if is(left, name) { + literal(right).map(|n| (*op, n)) + } else if is(right, name) { + literal(left).and_then(|n| flipped(*op).map(|op| (op, n))) + } else { + None + }; + match bound { + Some((Op::Ge, n)) => low = Some(low.map_or(n, |l| l.max(n))), + Some((Op::Gt, n)) => low = Some(low.map_or(n + 1, |l| l.max(n + 1))), + Some((Op::Le, n)) => high = Some(high.map_or(n, |h| h.min(n))), + Some((Op::Lt, n)) => high = Some(high.map_or(n - 1, |h| h.min(n - 1))), + _ => {} + } + } + let (low, high) = (low.unwrap_or(width.min()), high.unwrap_or(width.max())); + let mut values: Vec = match (set, low > width.min() || high < width.max()) { + (Some(set), _) => set + .into_iter() + .filter(|v| (low..=high).contains(v)) + .collect(), + (None, true) if high.saturating_sub(low) < MAX_DOMAIN => (low..=high).collect(), + _ => return None, + }; + values.sort_unstable(); + values.dedup(); + Some(values.into_iter().map(Value::Int).collect()) +} + +/// Every combination of arguments the member is explored with, when the +/// values of each of its own parameters are known. +fn instances(member: &Member) -> Option>> { + let function = member.function(); + let skip = function.machine.map_or(0, |m| m.state); + let requires: Vec<&Expr> = function + .clauses + .iter() + .filter(|c| c.kind == ClauseKind::Requires) + .map(|c| &c.expr) + .collect(); + let mut combinations: Vec> = vec![Vec::new()]; + for (name, ty) in &function.params[skip..] { + let domain = match ty { + Type::Bool => vec![Value::Bool(false), Value::Bool(true)], + Type::Enum(owner) => { + let e = member + .unit + .program + .enums + .iter() + .find(|e| e.name == *owner)?; + e.variants + .iter() + .map(|v| Value::Variant(owner.clone(), v.clone())) + .collect() + } + Type::Int(width) => integers(name, *width, &requires)?, + Type::Text | Type::List(_) => return None, + }; + if combinations.len().checked_mul(domain.len())? > MAX_STEPS { + return None; + } + combinations = combinations + .into_iter() + .flat_map(|prefix| { + domain.iter().map(move |value| { + let mut args = prefix.clone(); + args.push(value.clone()); + args + }) + }) + .collect(); + } + Some(combinations) +} + +/// Whether the member's `requires` hold on `names`. +fn admits(member: &Member, names: &[(String, Value)]) -> bool { + matches!( + interpret::broken_requires(member.function(), names), + Ok(None) + ) +} + +/// Explores the states `members` reach: its inits, events and observers, in +/// that order. +pub(crate) fn explore(members: &[Member]) -> Exploration { + let domains: Vec>>> = members.iter().map(instances).collect(); + let mut complete = members + .iter() + .zip(&domains) + .all(|(member, domain)| member.role() == Role::Observer || domain.is_some()); + let mut nodes: Vec = Vec::new(); + let mut seen: HashMap, usize> = HashMap::new(); + let mut found = Exploration { + states: 0, + complete: false, + failures: HashMap::new(), + allowed: HashMap::new(), + }; + let mut steps = 0usize; + let mut add = |nodes: &mut Vec, state: Vec, via, complete: &mut bool| { + if seen.contains_key(&state) { + return; + } + if nodes.len() >= MAX_STATES { + *complete = false; + return; + } + seen.insert(state.clone(), nodes.len()); + nodes.push(Node { state, via }); + }; + for (m, member) in members.iter().enumerate() { + let (Role::Init, Some(instances)) = (member.role(), &domains[m]) else { + continue; + }; + for args in instances { + steps += 1; + if let Ok(state) = member.run(None, args) { + add(&mut nodes, state, (None, m, args.clone()), &mut complete); + } + } + } + let mut queue: VecDeque = (0..nodes.len()).collect(); + 'states: while let Some(at) = queue.pop_front() { + let state = nodes[at].state.clone(); + for (m, member) in members.iter().enumerate() { + let role = member.role(); + let (Role::Event | Role::Observer, Some(instances)) = (role, &domains[m]) else { + continue; + }; + let meets = matches!( + interpret::broken_invariant(member.function(), &state), + Ok(None) + ); + for args in instances { + if steps >= MAX_STEPS { + complete = false; + break 'states; + } + steps += 1; + let names = member.names(Some(&state), args); + if !admits(member, &names) { + continue; + } + let next = (role == Role::Event) + .then(|| member.run(Some(&state), args).ok()) + .flatten(); + let here = Step { + member: m, + args: args.clone(), + state: next.clone(), + }; + if role == Role::Event { + found.allowed.entry(m).or_insert_with(|| Trace { + path: path(&nodes, at), + last: here.clone(), + }); + } + if meets { + for (o, obligation) in member.obligations.iter().enumerate() { + if obligation.polarity == Polarity::Universal + && obligation.bound.is_empty() + && !matches!(obligation.claim, Claim::Allowed) + && !found.failures.contains_key(&(m, o)) + && matches!(interpret::fails(obligation, &names), Ok(true)) + { + found.failures.insert( + (m, o), + Trace { + path: path(&nodes, at), + last: here.clone(), + }, + ); + } + } + } + if let Some(next) = next { + let before = nodes.len(); + add(&mut nodes, next, (Some(at), m, args.clone()), &mut complete); + if nodes.len() > before { + queue.push_back(nodes.len() - 1); + } + } + } + } + } + found.states = nodes.len(); + found.complete = complete; + found +} + +/// The run that is only the init `m` called with the arguments a solver's +/// `model` gives it, provided the model admits them. +pub(crate) fn start(members: &[Member], m: usize, model: &[(String, String)]) -> Option { + let member = &members[m]; + let function = member.function(); + let names = interpret::admitted(function, &model.to_vec()).ok()?; + let args: Vec = names[function.machine?.state..] + .iter() + .map(|(_, value)| value.clone()) + .collect(); + let state = member.run(None, &args).ok(); + Some(Step { + member: m, + args, + state, + }) +} + +/// Whether `trace`, run again from its init, reaches a state where the +/// member `m`'s `requires` hold on the trace's arguments and, for +/// `obligation`, where the state meets the invariants and the obligation +/// fails. +pub(crate) fn confirms( + members: &[Member], + m: usize, + obligation: Option<&Obligation>, + trace: &Trace, +) -> bool { + let Ok(state) = replay(members, &trace.path) else { + return false; + }; + let member = &members[m]; + let names = member.names(Some(&state), &trace.last.args); + admits(member, &names) + && obligation.is_none_or(|obligation| { + matches!( + interpret::broken_invariant(member.function(), &state), + Ok(None) + ) && matches!(interpret::fails(obligation, &names), Ok(true)) + }) +} + +/// Runs `path` again from its init, and gives the state it ends in, or why it +/// doesn't end in the states it claims. +pub(crate) fn replay(members: &[Member], path: &[Step]) -> Result, String> { + let mut state: Option> = None; + for step in path { + let member = &members[step.member]; + if (member.role() == Role::Init) != state.is_none() { + return Err("a run starts with an init and goes on with events".to_string()); + } + let next = member.run(state.as_deref(), &step.args)?; + if step.state.as_ref() != Some(&next) { + return Err("the run doesn't reach the state it claims".to_string()); + } + state = Some(next); + } + state.ok_or_else(|| "the run is empty".to_string()) +} diff --git a/crates/accord/src/identity.rs b/crates/accord/src/identity.rs index 2df130d..e8c1484 100644 --- a/crates/accord/src/identity.rs +++ b/crates/accord/src/identity.rs @@ -61,80 +61,87 @@ pub(crate) fn units(program: &Program) -> Vec> { program .functions .iter() - .map(|source| { - let mut renamer = Renamer { - program, - enums: Vec::new(), - functions: Vec::new(), - }; - let mut function = renamer.contract(source); - renamer.body(&mut function, &source.params); - // The direct callees' contracts, then every callee's body: the - // enums found before the bodies are the ones a script declares. - let direct = renamer.functions.len(); - let mut callees: Vec = (0..direct) - .map(|index| { - let callee = renamer.functions[index]; - let mut normalized = renamer.contract(callee); - normalized.name = format!("f{index}"); - normalized - }) - .collect(); - let visible = renamer.enums.len(); - let mut index = 0; - while index < renamer.functions.len() { - let callee = renamer.functions[index]; - if index >= callees.len() { - let mut normalized = renamer.contract(callee); - normalized.name = format!("f{index}"); - callees.push(normalized); - } - renamer.body(&mut callees[index], &callee.params); - index += 1; - } - let enums: Vec = renamer.enums[..visible] - .iter() - .enumerate() - .map(|(index, e)| enumeration(index, e)) - .collect(); - let mut text = String::from("(fn"); - for e in &enums { - text += &format!(" (enum {} {})", e.name, e.variants.len()); - } - text += &canonical(&function, true); - for callee in &callees[..direct] { - text += &format!(" (callee {}{})", callee.name, canonical(callee, false)); - } - let hash = hash(&(text + ")")); - let callee_names = renamer.functions.iter().map(|f| f.name.clone()).collect(); - let callee_bodies = if callees.is_empty() { - String::new() - } else { - self::hash( - &callees - .iter() - .map(|c| format!("(callee {}{})", c.name, canonical(c, true))) - .collect::(), - ) - }; - let mut functions = vec![function]; - functions.extend(callees); - Unit { - program: Program { - enums, - functions, - examples: Vec::new(), - }, - source, - enums: renamer.enums, - callees: callee_names, - callee_bodies, - hash, - } - }) + .map(|source| unit(program, source)) .collect() } +/// `source` normalized, with the functions of `program` it calls. `source` +/// needn't be among them: a machine's function is analysed with its +/// invariants, and called without them. +pub(crate) fn unit<'a>(program: &'a Program, source: &'a Function) -> Unit<'a> { + let mut renamer = Renamer { + program, + enums: Vec::new(), + functions: Vec::new(), + }; + let mut function = renamer.contract(source); + renamer.body(&mut function, &source.params); + // The direct callees' contracts, then every callee's body: the + // enums found before the bodies are the ones a script declares. + let direct = renamer.functions.len(); + let mut callees: Vec = (0..direct) + .map(|index| { + let callee = renamer.functions[index]; + let mut normalized = renamer.contract(callee); + normalized.name = format!("f{index}"); + normalized + }) + .collect(); + let visible = renamer.enums.len(); + let mut index = 0; + while index < renamer.functions.len() { + let callee = renamer.functions[index]; + if index >= callees.len() { + let mut normalized = renamer.contract(callee); + normalized.name = format!("f{index}"); + callees.push(normalized); + } + renamer.body(&mut callees[index], &callee.params); + index += 1; + } + let enums: Vec = renamer.enums[..visible] + .iter() + .enumerate() + .map(|(index, e)| enumeration(index, e)) + .collect(); + let mut text = String::from("(fn"); + for e in &enums { + text += &format!(" (enum {} {})", e.name, e.variants.len()); + } + text += &canonical(&function, true); + for callee in &callees[..direct] { + text += &format!(" (callee {}{})", callee.name, canonical(callee, false)); + } + let hash = hash(&(text + ")")); + let callee_names = renamer.functions.iter().map(|f| f.name.clone()).collect(); + let callee_bodies = if callees.is_empty() { + String::new() + } else { + self::hash( + &callees + .iter() + .map(|c| format!("(callee {}{})", c.name, canonical(c, true))) + .collect::(), + ) + }; + let mut functions = vec![function]; + functions.extend(callees); + Unit { + program: Program { + enums, + functions, + machines: Vec::new(), + examples: Vec::new(), + machine_examples: Vec::new(), + }, + source, + enums: renamer.enums, + callees: callee_names, + callee_bodies, + hash, + } +} + #[cfg(test)] mod tests { use super::{hash, units}; diff --git a/crates/accord/src/identity/normalize.rs b/crates/accord/src/identity/normalize.rs index c15bcca..d6cf763 100644 --- a/crates/accord/src/identity/normalize.rs +++ b/crates/accord/src/identity/normalize.rs @@ -105,6 +105,11 @@ impl<'a> Renamer<'a> { self.expr(condition, &inner); } Expr::Length(list, _) => self.expr(list, params), + Expr::Next(fields, _) => { + for (_, value) in fields { + self.expr(value, params); + } + } Expr::Index(list, index, _) => { self.expr(list, params); self.expr(index, params); diff --git a/crates/accord/src/identity/source.rs b/crates/accord/src/identity/source.rs index 713f6b7..9d11163 100644 --- a/crates/accord/src/identity/source.rs +++ b/crates/accord/src/identity/source.rs @@ -38,6 +38,11 @@ impl Unit<'_> { .collect() } + /// A value of the normalized function in source terms. + pub fn source_of(&self, value: &Value) -> String { + self.source_value_tree(value.clone()).source() + } + /// A normalized value, such as `E0.v1`, in source terms. pub fn source_value(&self, value: &str) -> String { self.program.functions.first().map_or_else( diff --git a/crates/accord/src/interpret.rs b/crates/accord/src/interpret.rs index 9360d63..39dae07 100644 --- a/crates/accord/src/interpret.rs +++ b/crates/accord/src/interpret.rs @@ -12,27 +12,26 @@ //! being weaker than its body. mod eval; +mod machine; mod replay; mod value; use eval::{Env, Mode, body}; -pub(crate) use replay::{Replay, replay}; +pub(crate) use machine::{broken_invariant, fields, run as run_machine, transition}; +pub(crate) use replay::{Replay, fails, replay}; pub(crate) use value::{Value, read}; use crate::Inputs; -use crate::syntax::{ClauseKind, Example, Function}; +use crate::syntax::{ClauseKind, Example, Function, Role}; -/// The first `requires` that doesn't hold, as written. -pub(crate) fn broken_requires( +/// The first clause of `kind` that doesn't hold, as written. +pub(crate) fn broken( function: &Function, names: &[(String, Value)], + kind: ClauseKind, ) -> Result, String> { let env = Env::plain(names, None, Mode::Math); - for clause in function - .clauses - .iter() - .filter(|c| c.kind == ClauseKind::Requires) - { + for clause in function.clauses.iter().filter(|c| c.kind == kind) { if !env.boolean(&clause.expr)? { return Ok(Some(clause.text.clone())); } @@ -40,6 +39,34 @@ pub(crate) fn broken_requires( Ok(None) } +/// The first `requires` that doesn't hold, as written. +pub(crate) fn broken_requires( + function: &Function, + names: &[(String, Value)], +) -> Result, String> { + broken(function, names, ClauseKind::Requires) +} + +/// Runs `function` in code on `names`: its value, provided its `requires` +/// hold and nothing overflows. +pub(crate) fn execute( + function: &Function, + names: &[(String, Value)], + functions: &[Function], +) -> Result { + if let Some(clause) = broken_requires(function, names)? { + return Err(format!("the call breaks `{clause}`")); + } + let env = Env { + names, + result: None, + mode: Mode::Code, + functions, + assumed: None, + }; + body(function, &env) +} + /// Runs an example: `Ok` when the call gives the expected result, otherwise /// why it doesn't. `functions` are those its function may call. pub(crate) fn run( @@ -53,17 +80,7 @@ pub(crate) fn run( .iter() .map(|(label, expr)| Ok((label.clone().unwrap_or_default(), constants.eval(expr)?))) .collect::, String>>()?; - if let Some(clause) = broken_requires(function, &names)? { - return Err(format!("the call breaks `{clause}`")); - } - let env = Env { - names: &names, - result: None, - mode: Mode::Code, - functions, - assumed: None, - }; - let got = body(function, &env)?; + let got = execute(function, &names, functions)?; let want = constants.eval(&example.expected)?; if got == want { Ok(()) @@ -92,6 +109,12 @@ pub(crate) fn admitted(function: &Function, inputs: &Inputs) -> Result { self.quantified(*quantifier, name, range, condition) } Expr::Length(list, _) => Ok(Value::Int(self.list(list)?.len() as i128)), + // The state a transition ends in, as its fields' values in order. + Expr::Next(fields, _) => fields + .iter() + .map(|(_, value)| self.eval(value)) + .collect::>() + .map(Value::List), Expr::Index(list, index, site) => { let items = self.list(list)?; usize::try_from(self.int(index)?) diff --git a/crates/accord/src/interpret/machine.rs b/crates/accord/src/interpret/machine.rs new file mode 100644 index 0000000..00c553a --- /dev/null +++ b/crates/accord/src/interpret/machine.rs @@ -0,0 +1,92 @@ +//! Running a machine: an init or an event in code, the invariants of a state, +//! and an example's run. + +use super::eval::{Env, Mode}; +use super::{Names, Value, broken, execute}; +use crate::syntax::{ClauseKind, Expr, Function, Machine, MachineExample}; + +/// The state `member` ends in, as the value of each field in order, when run +/// in code on `names`: its own parameters, and for an event the state. +pub(crate) fn transition( + member: &Function, + names: &Names, + functions: &[Function], +) -> Result, String> { + match execute(member, names, functions)? { + Value::List(state) => Ok(state), + _ => Err("a transition ends in a state".to_string()), + } +} + +/// The fields of `member`'s machine, each with its value in `state`. +pub(crate) fn fields(member: &Function, state: &[Value]) -> Names { + let count = member.machine.map_or(0, |m| m.state); + member.params[..count] + .iter() + .map(|(name, _)| name.clone()) + .zip(state.iter().cloned()) + .collect() +} + +/// The first invariant, or helper invariant, that `state` breaks, as written. +pub(crate) fn broken_invariant( + member: &Function, + state: &[Value], +) -> Result, String> { + broken(member, &fields(member, state), ClauseKind::Invariant) +} + +/// Runs an example: its init, then its events, each in code, then whether the +/// condition it gives holds of the state it ends in. +pub(crate) fn run( + example: &MachineExample, + machine: &Machine, + functions: &[Function], +) -> Result<(), String> { + let constants = Env::plain(&[], None, Mode::Code); + let mut state: Option> = None; + for (index, step) in example.steps.iter().enumerate() { + let Expr::Call(name, args, site) = step else { + return Err("a step is a call".to_string()); + }; + let pool = if index == 0 { + &machine.inits + } else { + &machine.events + }; + let member = pool + .iter() + .find(|f| f.name == *name) + .ok_or(format!("`{name}` isn't a step of `{}`", machine.name))?; + let mut names = match &state { + Some(state) => fields(member, state), + None => Vec::new(), + }; + for (label, arg) in args { + names.push((label.clone().unwrap_or_default(), constants.eval(arg)?)); + } + state = Some( + transition(member, &names, functions) + .map_err(|why| format!("`{}`: {why}", site.text))?, + ); + } + let state = state.ok_or("the example runs nothing")?; + let names: Names = machine + .state + .iter() + .map(|(field, _)| field.clone()) + .zip(state) + .collect(); + if Env::plain(&names, None, Mode::Math).boolean(&example.gives)? { + Ok(()) + } else { + let after: Vec = names + .iter() + .map(|(field, value)| format!("{field} = {}", value.source())) + .collect(); + Err(format!( + "it doesn't hold after the run: {}", + after.join(", ") + )) + } +} diff --git a/crates/accord/src/interpret/replay.rs b/crates/accord/src/interpret/replay.rs index b9da1c3..21f0ed1 100644 --- a/crates/accord/src/interpret/replay.rs +++ b/crates/accord/src/interpret/replay.rs @@ -2,7 +2,7 @@ //! the solver's word alone. use super::eval::{Env, Mode, body, first_row}; -use super::{Names, Value, admitted, broken_requires, read}; +use super::{Names, Value, admitted, broken_invariant, broken_requires, read}; use crate::Inputs; use crate::obligation::{Claim, Guard, Obligation, term}; use crate::syntax::{Expr, Range}; @@ -35,6 +35,13 @@ fn reproduces( assumed, }; Ok(match &obligation.claim { + Claim::Allowed => true, + Claim::Invariants => { + let Value::List(next) = body(function, &env)? else { + return Err("a transition ends in a state".to_string()); + }; + broken_invariant(function, &next)?.is_some() + } Claim::Ensures(clause) => { let result = body(function, &env)?; let with_result = Env { @@ -91,6 +98,12 @@ fn reproduces( }) } +/// Whether `obligation`'s universal claim fails on `names`, which give a value +/// to every parameter of its function, with each call running. +pub(crate) fn fails(obligation: &Obligation, names: &Names) -> Result { + reproduces(obligation, names, None) +} + /// Whether every guard holds, each evaluated whatever the others give. fn runs(env: &Env, guards: &[Guard]) -> Result { let mut runs = true; diff --git a/crates/accord/src/interpret/value.rs b/crates/accord/src/interpret/value.rs index d7a5d3f..bcf8b7c 100644 --- a/crates/accord/src/interpret/value.rs +++ b/crates/accord/src/interpret/value.rs @@ -2,7 +2,7 @@ use crate::syntax::Type; -#[derive(Clone, Debug, PartialEq)] +#[derive(Clone, Debug, PartialEq, Eq, Hash)] pub(crate) enum Value { Bool(bool), Int(i128), diff --git a/crates/accord/src/ledger.rs b/crates/accord/src/ledger.rs index 6215a71..525074a 100644 --- a/crates/accord/src/ledger.rs +++ b/crates/accord/src/ledger.rs @@ -109,7 +109,12 @@ fn to_json(outcome: &Outcome) -> Option { evidence: Refutation::NoSuchInput, } => json!({ "refuted": null }), Outcome::WeakCallee { inputs, .. } => json!({ "weak_callee": inputs_to_json(inputs) }), - Outcome::Undecided { .. } | Outcome::Unsupported { .. } => return None, + Outcome::Undecided { .. } + | Outcome::Unsupported { .. } + | Outcome::NotInductive { .. } + | Outcome::Refuted { + evidence: Refutation::Trace(_), + } => return None, }) } diff --git a/crates/accord/src/lib.rs b/crates/accord/src/lib.rs index 125d2e8..dcb9fd0 100644 --- a/crates/accord/src/lib.rs +++ b/crates/accord/src/lib.rs @@ -6,6 +6,7 @@ mod check; mod diagnostic; pub mod diff; mod evidence; +mod explore; mod identity; mod interpret; mod ledger; @@ -96,6 +97,15 @@ pub enum Outcome { /// Each call as written, with the result the counterexample gives it. calls: Inputs, }, + /// Not proved from the invariants alone, though the machine may be right: + /// the solvers' counterexample starts in a state that meets every + /// invariant and helper invariant, and no run from an init was found to + /// reach it. A helper invariant can settle it. + NotInductive { + /// The state the counterexample starts in, and the parameters of the + /// step it takes. + inputs: Inputs, + }, } /// What shows that an obligation fails. @@ -105,6 +115,32 @@ pub enum Refutation { Counterexample(Inputs), /// It needs some input, and both solvers proved that none exists. NoSuchInput, + /// A run of a machine from an init that the interpreter replays, ending + /// at the step that fails. + Trace(Vec), +} + +/// One step of a run of a machine. +#[derive(Clone, Debug, PartialEq)] +pub struct TraceStep { + /// The init or event as called, such as `start()` or `set(level: 3)`. + pub call: String, + /// The fields after the step; `None` for a step that doesn't end in a + /// state, such as one whose arithmetic overflows. + pub state: Option, +} + +/// What exploring a machine's reachable states covered. It is trusted, not +/// proved, and never an outcome. +#[derive(Clone, Debug, PartialEq)] +pub struct Exploration { + /// How many states were reached. + pub states: usize, + /// Whether every state, and every way to move from it, was visited. + pub complete: bool, + /// For an event proved allowed: a run to a state where it is, ending at + /// the event. + pub trace: Option>, } /// The property an obligation checks, independent of its wording. @@ -122,6 +158,12 @@ pub enum ObligationKind { Precondition, /// An index is within its list. Bounds, + /// A machine's init or event leaves it in a state that meets every + /// invariant and helper invariant. + Invariant, + /// A machine's init has an input its `requires` admits, or its event is + /// allowed in a state the machine reaches. + Allowed, } impl ObligationKind { @@ -134,6 +176,8 @@ impl ObligationKind { Self::Overflow => "overflow", Self::Precondition => "precondition", Self::Bounds => "bounds", + Self::Invariant => "invariant", + Self::Allowed => "allowed", } } } @@ -158,6 +202,9 @@ pub struct Verdict { pub definition: String, /// Whether the outcome came from the ledger rather than the solvers. pub reused: bool, + /// For an obligation about a machine's reachable states: what exploring + /// them covered. + pub exploration: Option, } /// Whether an example gave its result when run. @@ -200,20 +247,43 @@ pub enum Standing { Unverified, } -/// One function's identity, unchecked intent, and standing. +/// What a definition is. +#[derive(Clone, Copy, Debug, PartialEq)] +pub enum DefinitionKind { + /// A function. + Function, + /// A machine. + Machine, +} + +impl DefinitionKind { + /// The kind's name, as the receipt writes it. + pub fn name(self) -> &'static str { + match self { + Self::Function => "function", + Self::Machine => "machine", + } + } +} + +/// One function's or machine's identity, unchecked intent, and standing. #[derive(Clone, Debug, PartialEq)] pub struct Definition { - /// The function's name. + /// Whether it is a function or a machine. + pub kind: DefinitionKind, + /// The function's or machine's name. pub name: String, /// Its declared purpose in unchecked natural language, when present. pub intent: Option, /// The declaration's 1-based line. pub line: usize, - /// Parameter names and types, in declaration order. + /// Parameter names and types, in declaration order; for a machine, its + /// state's fields. pub params: Vec<(String, Type)>, - /// The result's type. - pub result_type: Type, - /// Source lines and text of every specification clause, including requires. + /// The result's type; a machine has none. + pub result_type: Option, + /// Source lines and text of every specification clause, including + /// requires; for a machine, its invariants and helper invariants. pub specification: Vec<(usize, String)>, /// Enums used by this function, with their source variants. pub enums: Vec<(String, Vec)>, @@ -283,16 +353,24 @@ fn program_of(files: &[(String, String)]) -> Result<(syntax::Program, Vec Option { mutate_expr(range.list_mut(), n).or_else(|| mutate_expr(condition, n)) } Expr::Length(list, _) => mutate_expr(list, n), + Expr::Next(fields, _) => fields + .iter_mut() + .find_map(|(_, value)| mutate_expr(value, n)), Expr::Index(list, index, _) => mutate_expr(list, n).or_else(|| mutate_expr(index, n)), Expr::Bool(_) | Expr::Text(..) | Expr::Name(..) | Expr::Variant(..) => None, } diff --git a/crates/accord/src/obligation.rs b/crates/accord/src/obligation.rs index 6d89a40..7f28886 100644 --- a/crates/accord/src/obligation.rs +++ b/crates/accord/src/obligation.rs @@ -21,7 +21,7 @@ //! `ensures`. An operation inside a quantifier's condition is about every //! index the quantifier ranges over: its script asks for one where it fails. -use crate::syntax::{Body, ClauseKind, Expr, Function, Program}; +use crate::syntax::{Body, ClauseKind, Expr, Function, Program, Role}; mod calls; mod claims; @@ -38,7 +38,7 @@ pub(crate) use operations::Guard; use operations::{Operation, assumption, body_operations, for_some, guard_term, spec_indexes}; pub(crate) use scripts::{mutant_scripts, open_script}; pub(crate) use smt::{all, datatypes, ending, in_range, sort, term}; -use smt::{prelude, value}; +use smt::{meets_invariants, prelude, value}; /// Whether an obligation is about every input or about some input. #[derive(Clone, Copy, Debug, PartialEq)] @@ -140,6 +140,55 @@ fn obligations_of<'a>( None => format!("(and (= result {body}) {claim})"), }; let mut out = Vec::new(); + if let Some(member) = function.machine.filter(|m| m.role != Role::Observer) { + let name = &function.name; + let allowed = |clause: String| { + obligation( + &clause, + function.line, + Polarity::Existential, + Claim::Allowed, + "", + &[], + &[], + "true".to_string(), + ) + }; + let init = member.role == Role::Init; + if init + && function + .clauses + .iter() + .any(|c| c.kind == ClauseKind::Requires) + { + out.push(allowed(format!("`{name}` is allowed for some input"))); + } + let fails = format!("(not {})", meets_invariants(function)); + out.push(obligation( + &if init { + format!( + "`{name}` starts in a state that meets every invariant and helper invariant" + ) + } else { + format!("`{name}` preserves every invariant and helper invariant") + }, + function.line, + Polarity::Universal, + Claim::Invariants, + "", + &every, + &[], + match &covered { + Some(covered) => format!("(and {covered} {fails})"), + None => fails, + }, + )); + if !init { + out.push(allowed(format!( + "`{name}` is allowed in some state an init reaches" + ))); + } + } let ensures = function .clauses .iter() diff --git a/crates/accord/src/obligation/claims.rs b/crates/accord/src/obligation/claims.rs index 7243f02..a5c556c 100644 --- a/crates/accord/src/obligation/claims.rs +++ b/crates/accord/src/obligation/claims.rs @@ -10,6 +10,12 @@ use crate::syntax::{Expr, Program, Width}; pub(crate) enum Claim<'a> { /// The `ensures` holds of the body's value. Ensures(&'a Expr), + /// The state a machine's init or event ends in meets every invariant and + /// helper invariant. + Invariants, + /// A machine's init has some input its `requires` admits, or its event + /// is allowed in some state that meets the invariants. + Allowed, /// Some row of the decision table matches. Covered, /// The row at this index is the first that matches. diff --git a/crates/accord/src/obligation/lists.rs b/crates/accord/src/obligation/lists.rs index 1c2d19b..6827c6a 100644 --- a/crates/accord/src/obligation/lists.rs +++ b/crates/accord/src/obligation/lists.rs @@ -106,6 +106,7 @@ fn walk<'a>(expr: &'a Expr, bound: &[&'a Expr], visit: &mut impl FnMut(&'a Expr, each(otherwise); } Expr::List(items, ..) => items.iter().for_each(each), + Expr::Next(fields, _) => fields.iter().for_each(|(_, value)| each(value)), Expr::Call(_, args, _) => args.iter().for_each(|(_, arg)| each(arg)), Expr::Bool(_) | Expr::Int(..) | Expr::Text(..) | Expr::Name(..) | Expr::Variant(..) => {} } diff --git a/crates/accord/src/obligation/operations.rs b/crates/accord/src/obligation/operations.rs index fe1df02..f5dd7cb 100644 --- a/crates/accord/src/obligation/operations.rs +++ b/crates/accord/src/obligation/operations.rs @@ -56,6 +56,7 @@ fn operations<'a>( Expr::Neg(inner, _) | Expr::Not(inner) | Expr::Length(inner, _) => each(inner, out), Expr::Call(_, args, _) => args.iter().for_each(|(_, arg)| each(arg, out)), Expr::List(items, ..) => items.iter().for_each(|item| each(item, out)), + Expr::Next(fields, _) => fields.iter().for_each(|(_, value)| each(value, out)), Expr::If(condition, then, otherwise) => { each(condition, out); let guard = |holds| Guard { @@ -128,7 +129,12 @@ pub(super) fn spec_indexes<'a>( Expr::Call(_, args, _) => args .iter() .for_each(|(_, a)| spec_indexes(a, guards, bound, out)), - Expr::Bool(_) | Expr::Int(..) | Expr::Text(..) | Expr::Name(..) | Expr::Variant(..) => {} + Expr::Bool(_) + | Expr::Int(..) + | Expr::Text(..) + | Expr::Name(..) + | Expr::Variant(..) + | Expr::Next(..) => {} } if matches!(expr, Expr::Index(..)) { out.push(Operation { diff --git a/crates/accord/src/obligation/smt.rs b/crates/accord/src/obligation/smt.rs index 9f4412c..660668f 100644 --- a/crates/accord/src/obligation/smt.rs +++ b/crates/accord/src/obligation/smt.rs @@ -3,7 +3,7 @@ use super::calls::apply; use super::lists::{MAX_LENGTH, contains, quantified}; -use crate::syntax::{Arith, Body, ClauseKind, Expr, Function, Op, Program, Row, Type, Width}; +use crate::syntax::{Arith, Body, ClauseKind, Expr, Function, Op, Program, Role, Row, Type, Width}; pub(crate) fn sort(ty: &Type) -> String { match ty { @@ -74,6 +74,16 @@ pub(crate) fn term(expr: &Expr) -> String { } Expr::Length(list, _) => format!("(seq.len {})", term(list)), Expr::Index(list, index, _) => format!("(seq.nth {} {})", term(list), term(index)), + // Identity reads a `next` as one term; a script reads it field by + // field (`meets_invariants`). + Expr::Next(values, _) => format!( + "(next {})", + values + .iter() + .map(|(_, value)| term(value)) + .collect::>() + .join(" ") + ), } } /// A text as an SMT-LIB string literal. SMT-LIB reads `\u{...}` in a @@ -143,11 +153,13 @@ pub(crate) fn prelude(function: &Function, datatypes: &str) -> String { _ => {} } } - for clause in function - .clauses - .iter() - .filter(|c| c.kind == ClauseKind::Requires) - { + // An init has no state before it, so no invariant to assume. + let reads_state = function.machine.is_none_or(|m| m.role != Role::Init); + for clause in function.clauses.iter().filter(|c| match c.kind { + ClauseKind::Requires => true, + ClauseKind::Invariant => reads_state, + ClauseKind::Ensures | ClauseKind::Open => false, + }) { prelude += &format!("(assert {})\n", term(&clause.expr)); } prelude @@ -165,15 +177,87 @@ pub(crate) fn ending(names: &[String]) -> String { } /// A body's value as a term, and for a decision table the condition that some /// row matches. +/// An init or event has no value to speak of: its `next` is read field by +/// field. pub(crate) fn value(function: &Function) -> (String, Option) { + let transition = function.machine.is_some_and(|m| m.role != Role::Observer); match &function.body { + Body::Expr(_) if transition => (String::new(), None), Body::Expr(body) => (term(body), None), Body::Decide(rows, _) => ( - decide_term(rows), + if transition { + String::new() + } else { + decide_term(rows) + }, Some(all("or", rows.iter().map(condition).collect(), "false")), ), } } + +/// The terms of the fields of the state an init or event ends in, in order: +/// the field's value in the branch or row that runs. +fn next_terms(function: &Function) -> Vec { + let count = function.machine.map_or(0, |m| m.state); + (0..count) + .map(|field| match &function.body { + Body::Expr(body) => next_term(body, field), + Body::Decide(rows, _) => { + let Some((last, earlier)) = rows.split_last() else { + return String::new(); + }; + earlier + .iter() + .rev() + .fold(next_term(&last.result, field), |rest, row| { + format!( + "(ite {} {} {rest})", + condition(row), + next_term(&row.result, field) + ) + }) + } + }) + .collect() +} + +fn next_term(expr: &Expr, field: usize) -> String { + match expr { + Expr::If(c, then, otherwise) => format!( + "(ite {} {} {})", + term(c), + next_term(then, field), + next_term(otherwise, field) + ), + Expr::Next(values, _) => term(&values[field].1), + _ => unreachable!("`check` ends every init and event in a `next`"), + } +} + +/// That the state an init or event ends in meets every invariant and helper +/// invariant: they hold of the fields as `next` gives them. +pub(crate) fn meets_invariants(function: &Function) -> String { + let count = function.machine.map_or(0, |m| m.state); + let invariants = all( + "and", + function + .clauses + .iter() + .filter(|c| c.kind == ClauseKind::Invariant) + .map(|c| term(&c.expr)) + .collect(), + "true", + ); + if count == 0 { + return invariants; + } + let bindings: Vec = function.params[..count] + .iter() + .zip(next_terms(function)) + .map(|((field, _), next)| format!("({field} {next})")) + .collect(); + format!("(let ({}) {invariants})", bindings.join(" ")) +} /// The SMT-LIB declarations of a program's enums. pub(crate) fn datatypes(program: &Program) -> String { program diff --git a/crates/accord/src/openness.rs b/crates/accord/src/openness.rs index d923684..d980287 100644 --- a/crates/accord/src/openness.rs +++ b/crates/accord/src/openness.rs @@ -115,7 +115,8 @@ fn search(unit: &Unit, solvers: &Solvers) -> Option { } Outcome::Proved { witness: None } | Outcome::Refuted { .. } - | Outcome::WeakCallee { .. } => Openness::Undecided { + | Outcome::WeakCallee { .. } + | Outcome::NotInductive { .. } => Openness::Undecided { reason: "the search gave no witness".to_string(), }, }; diff --git a/crates/accord/src/receipt.rs b/crates/accord/src/receipt.rs index 83d0bbe..7ab8e0b 100644 --- a/crates/accord/src/receipt.rs +++ b/crates/accord/src/receipt.rs @@ -13,7 +13,7 @@ pub use text::text; use crate::Standing; /// The receipt schema's version. -pub const VERSION: u32 = 3; +pub const VERSION: u32 = 4; impl Standing { /// The standing's name, as the receipt writes it. diff --git a/crates/accord/src/receipt/diagnostics.rs b/crates/accord/src/receipt/diagnostics.rs index d52c88b..a082987 100644 --- a/crates/accord/src/receipt/diagnostics.rs +++ b/crates/accord/src/receipt/diagnostics.rs @@ -28,6 +28,7 @@ pub(super) fn findings(report: &Report) -> Vec { Outcome::Undecided { .. } => Some(C::ObligationUndecided), Outcome::Unsupported { .. } => Some(C::ObligationUnsupported), Outcome::WeakCallee { .. } => Some(C::WeakCalleeContract), + Outcome::NotInductive { .. } => Some(C::NotInductive), }; if let Some(code) = code { add( diff --git a/crates/accord/src/receipt/json.rs b/crates/accord/src/receipt/json.rs index 66487e5..472a53b 100644 --- a/crates/accord/src/receipt/json.rs +++ b/crates/accord/src/receipt/json.rs @@ -1,8 +1,8 @@ //! Structured projection of the same review record as terminal text. use super::{VERSION, review}; use crate::{ - Definition, ExampleRun, Inputs, Openness, Outcome, Refutation, Report, Run, Strength, Type, - Verdict, + Definition, ExampleRun, Inputs, Openness, Outcome, Refutation, Report, Run, Strength, + TraceStep, Type, Verdict, }; use serde_json::{Value, json}; @@ -64,10 +64,26 @@ fn inputs_json(inputs: &Inputs, definition: &Definition) -> Value { .collect() } +fn trace_json(steps: &[TraceStep], definition: &Definition) -> Value { + steps + .iter() + .map(|step| { + json!({ + "call": step.call, + "state": step.state.as_ref().map(|state| inputs_json(state, definition)), + }) + }) + .collect() +} + fn verdict_json(verdict: &Verdict, definition: &Definition) -> Value { + let existential = matches!( + verdict.kind, + crate::ObligationKind::RowReachability | crate::ObligationKind::Allowed + ); let mut out = json!({ "kind": verdict.kind.name(), - "polarity": if verdict.kind == crate::ObligationKind::RowReachability { "existential" } else { "universal" }, + "polarity": if existential { "existential" } else { "universal" }, "clause": verdict.clause, "line": verdict.line, "key": verdict.key, @@ -87,6 +103,13 @@ fn verdict_json(verdict: &Verdict, definition: &Definition) -> Value { Outcome::Refuted { evidence: Refutation::NoSuchInput, } => json!({ "outcome": "refuted", "no_such_input": true }), + Outcome::Refuted { + evidence: Refutation::Trace(steps), + } => json!({ "outcome": "refuted", "trace": trace_json(steps, definition) }), + Outcome::NotInductive { inputs } => json!({ + "outcome": "not_inductive", + "counterexample": inputs_json(inputs, definition), + }), Outcome::Undecided { reason } => json!({ "outcome": "undecided", "reason": reason }), Outcome::Unsupported { reason } => json!({ "outcome": "unsupported", "reason": reason }), Outcome::WeakCallee { inputs, calls } => json!({ @@ -101,6 +124,15 @@ fn verdict_json(verdict: &Verdict, definition: &Definition) -> Value { if let (Some(out), Some(fields)) = (out.as_object_mut(), fields.as_object()) { out.extend(fields.clone()); } + if let Some(exploration) = &verdict.exploration { + out["exploration"] = json!({ + "states": exploration.states, + "complete": exploration.complete, + }); + if let Some(trace) = &exploration.trace { + out["exploration"]["trace"] = trace_json(trace, definition); + } + } out } @@ -116,6 +148,14 @@ fn example_json(example: &ExampleRun) -> Value { } } +/// `source` read as the definition's result type, which a function has. +fn result_typed(source: &str, definition: &Definition) -> Value { + definition + .result_type + .as_ref() + .map_or(Value::Null, |ty| typed(source, ty)) +} + fn openness_json(openness: &Openness, definition: &Definition) -> Value { match openness { Openness::Determined => json!({ "determined": true }), @@ -126,8 +166,8 @@ fn openness_json(openness: &Openness, definition: &Definition) -> Value { } => json!({ "open": { "inputs": inputs_json(inputs, definition), - "results": [typed(&results.0, &definition.result_type), typed(&results.1, &definition.result_type)], - "implementation": typed(code, &definition.result_type), + "results": [result_typed(&results.0, definition), result_typed(&results.1, definition)], + "implementation": result_typed(code, definition), } }), Openness::Undecided { reason } => json!({ "undecided": reason }), @@ -147,8 +187,8 @@ fn strength_json(strength: &Strength, definition: &Definition) -> Value { .map(|s| json!({ "change": s.change, "inputs": inputs_json(&s.inputs, definition), - "original": typed(&s.original, &definition.result_type), - "mutant": typed(&s.mutant, &definition.result_type), + "original": result_typed(&s.original, definition), + "mutant": result_typed(&s.mutant, definition), })) .collect::>(), }) @@ -178,14 +218,14 @@ pub(super) fn definition_json(report: &Report, definition: &Definition) -> Value "signature": review::signature(definition), "line": definition.line, "parameters": definition.params.iter().map(|(name, ty)| json!({"name": name, "type": type_json(ty)})).collect::>(), - "result_type": type_json(&definition.result_type), + "result_type": definition.result_type.as_ref().map(type_json), "types": definition.enums.iter().map(|(name, variants)| json!({"name": name, "variants": variants})).collect::>(), "specification": definition.specification.iter().map(|(line, text)| json!({"line": line, "text": text})).collect::>(), "not_proved": review::limits(report, definition).into_iter().map(|(kind, message)| json!({"kind": kind, "message": message})).collect::>(), "name": definition.name, "intent": definition.intent, "file": definition.file, - "kind": "function", + "kind": definition.kind.name(), "hash": definition.hash, "standing": definition.standing.name(), "unverified_callees": definition.unverified_callees, diff --git a/crates/accord/src/receipt/review.rs b/crates/accord/src/receipt/review.rs index ddf19f2..7469bc4 100644 --- a/crates/accord/src/receipt/review.rs +++ b/crates/accord/src/receipt/review.rs @@ -2,13 +2,16 @@ use crate::{Definition, Openness, Outcome, Report, Run}; pub(super) fn signature(d: &Definition) -> String { + let Some(result_type) = &d.result_type else { + return format!("machine {}", d.name); + }; let params = d .params .iter() .map(|(name, ty)| format!("{name}: {}", ty.name())) .collect::>() .join(", "); - format!("fn {}({params}) -> {}", d.name, d.result_type.name()) + format!("fn {}({params}) -> {}", d.name, result_type.name()) } pub(super) fn limits(report: &Report, d: &Definition) -> Vec<(&'static str, &'static str)> { @@ -70,6 +73,21 @@ pub(super) fn limits(report: &Report, d: &Definition) -> Vec<(&'static str, &'st "It calls a function that isn't verified; its own proofs assume that function's contract.", )); } + if verdicts + .iter() + .any(|v| matches!(v.outcome, Outcome::NotInductive { .. })) + { + out.push(( + "not_inductive_obligation", + "At least one obligation was not proved because a state that meets every invariant and helper invariant leaves them, though no run from an init was found to reach it; a helper invariant may settle it.", + )); + } + if verdicts.iter().any(|v| v.exploration.is_some()) { + out.push(( + "exploration", + "Exploring a machine's reachable states runs the interpreter over finitely many states and arguments; what it covers is trusted, and it proves nothing.", + )); + } if verdicts .iter() .any(|v| matches!(v.outcome, Outcome::Unsupported { .. })) @@ -98,6 +116,9 @@ pub(super) fn limits(report: &Report, d: &Definition) -> Vec<(&'static str, &'st { out.push(("admitted_domain", "Guarantees apply only to inputs meeting requires; no behavior is promised for excluded inputs.")); } + if d.result_type.is_none() { + return out; + } match report.openness.iter().find(|o| o.function == d.name) { None => out.push(("no_postcondition", "No ensures was declared; no postcondition or open-case search establishes the intended result.")), Some(o) => { diff --git a/crates/accord/src/receipt/text.rs b/crates/accord/src/receipt/text.rs index 70e189f..7e1b563 100644 --- a/crates/accord/src/receipt/text.rs +++ b/crates/accord/src/receipt/text.rs @@ -3,7 +3,8 @@ use super::{diagnostics, json, review}; use crate::{ - Determinacy, ExampleRun, Inputs, Openness, Outcome, Refutation, Report, Run, Strength, Verdict, + Determinacy, ExampleRun, Inputs, Openness, Outcome, Refutation, Report, Run, Strength, + TraceStep, Verdict, }; fn values(inputs: &Inputs) -> String { @@ -17,7 +18,45 @@ fn values(inputs: &Inputs) -> String { .join(", ") } +/// A run, one step to a line. +fn trace_text(steps: &[TraceStep]) -> String { + steps + .iter() + .map(|step| match &step.state { + Some(state) => format!(" {} leaves {}", step.call, values(state)), + None => format!(" {} fails here", step.call), + }) + .collect::>() + .join("\n") +} + +/// What exploring the reachable states covered, for an obligation that +/// consulted it. +fn exploration_text(verdict: &Verdict) -> Option { + let exploration = verdict.exploration.as_ref()?; + let mut line = format!( + " explored {} states, {} (trusted, not proved)", + exploration.states, + if exploration.complete { + "all of them" + } else { + "not all" + } + ); + if let Some(trace) = &exploration.trace { + line = format!("{line}\n{}", trace_text(trace)); + } + Some(line) +} + fn verdict_text(verdict: &Verdict) -> String { + match exploration_text(verdict) { + Some(note) => format!("{}\n{note}", outcome_text(verdict)), + None => outcome_text(verdict), + } +} + +fn outcome_text(verdict: &Verdict) -> String { let reused = if verdict.reused { " [reused]" } else { "" }; let clause = if verdict.kind == crate::ObligationKind::RowReachability { "some admitted input reaches this row first (existential)" @@ -45,6 +84,13 @@ fn verdict_text(verdict: &Verdict) -> String { Outcome::Refuted { evidence: Refutation::NoSuchInput, } => format!("refuted {place}\n no input reaches it"), + Outcome::Refuted { + evidence: Refutation::Trace(steps), + } => format!("refuted {place}\n{}", trace_text(steps)), + Outcome::NotInductive { inputs } => format!( + "not inductive {place}\n not proved from the invariants alone: from {}, which no run from an init was found to reach; a helper invariant may settle it", + values(inputs) + ), Outcome::Undecided { reason } => format!("undecided {place}\n {reason}"), Outcome::Unsupported { reason } => { format!("unsupported {place}\n {reason}") @@ -149,7 +195,8 @@ pub fn text(report: &Report) -> String { .as_ref() .map_or(String::new(), |f| format!(" ({f})")); lines.push(format!( - "function {}{file}", + "{:<13}{}{file}", + definition.kind.name(), review::signature(definition) )); let metadata = json::definition_json(report, definition); diff --git a/crates/accord/src/syntax.rs b/crates/accord/src/syntax.rs index 7af4ff5..6d5a0c6 100644 --- a/crates/accord/src/syntax.rs +++ b/crates/accord/src/syntax.rs @@ -5,6 +5,7 @@ mod declarations; mod expr; +mod machines; mod parser; mod token; @@ -133,6 +134,10 @@ pub(crate) enum Expr { Length(Box, usize), /// `list[index]`, and where it is. Index(Box, Box, Site), + /// `next { field: value, ... }`, the state an init or event ends in, and + /// its line. Only a machine's init or event ends in one; once checked, it + /// gives every field of the state, in the state's order. + Next(Vec<(String, Expr)>, usize), } impl Expr { @@ -146,6 +151,7 @@ impl Expr { | Expr::Text(_, line) | Expr::List(_, _, line) | Expr::Quantified(.., line) + | Expr::Next(_, line) | Expr::Length(_, line) => *line, Expr::Arith(.., site) | Expr::Neg(_, site) @@ -207,6 +213,10 @@ pub(crate) enum ClauseKind { Ensures, /// `open when`: inputs for which any result the contract allows is fine. Open, + /// A machine's invariant or helper invariant. An event or observer + /// assumes it of the state it reads; an init or event must meet it in + /// the state it ends in. + Invariant, } #[derive(Clone, Debug)] @@ -233,6 +243,27 @@ pub(crate) enum Body { Decide(Vec, usize), } +/// What a function is to the machine that declares it. +#[derive(Clone, Copy, Debug, PartialEq)] +pub(crate) enum Role { + /// A way to start. Its body ends in a `next`; it doesn't read the state. + Init, + /// A transition. Its body ends in a `next`. + Event, + /// A pure function of the state. + Observer, +} + +/// A function that belongs to a machine. Once checked, its first `state` +/// parameters are the machine's fields, in order, and its invariants are +/// clauses. An init's fields are placeholders: it doesn't read them. An init +/// or event's `ret` is a placeholder too: its value is its `next`. +#[derive(Clone, Copy, Debug, PartialEq)] +pub(crate) struct Member { + pub role: Role, + pub state: usize, +} + #[derive(Clone, Debug)] pub(crate) struct Function { pub name: String, @@ -246,6 +277,46 @@ pub(crate) struct Function { pub ret: Type, pub clauses: Vec, pub body: Body, + pub machine: Option, +} + +/// A state, the ways it starts, the events that move it, and what must hold +/// in every state it reaches. +#[derive(Clone, Debug)] +pub(crate) struct Machine { + pub name: String, + pub public: bool, + pub intent: Option, + pub line: usize, + pub file: usize, + pub state: Vec<(String, Type)>, + pub inits: Vec, + pub events: Vec, + pub observers: Vec, + /// Each invariant and helper invariant, as written. + pub invariants: Vec, +} + +impl Machine { + /// Inits, then events, then observers: the order of the machine's + /// obligations. + pub fn members(&self) -> impl Iterator { + self.inits.iter().chain(&self.events).chain(&self.observers) + } +} + +/// `example Machine`, then an init and events one per line, then +/// `gives condition`: a run and the condition that must hold after it. +#[derive(Clone, Debug)] +pub(crate) struct MachineExample { + pub machine: String, + pub file: usize, + /// Each step as a call, which the checker puts in the order of the + /// parameters, each labelled. + pub steps: Vec, + pub gives: Expr, + pub text: String, + pub line: usize, } #[derive(Clone, Debug)] @@ -294,5 +365,7 @@ pub(crate) struct Example { pub(crate) struct Program { pub enums: Vec, pub functions: Vec, + pub machines: Vec, pub examples: Vec, + pub machine_examples: Vec, } diff --git a/crates/accord/src/syntax/declarations.rs b/crates/accord/src/syntax/declarations.rs index d9cef02..7e768ab 100644 --- a/crates/accord/src/syntax/declarations.rs +++ b/crates/accord/src/syntax/declarations.rs @@ -7,7 +7,7 @@ use super::{Body, Clause, ClauseKind, Enum, Example, Function, Row, Type, Width} use crate::Diagnostic; impl Parser<'_> { - fn ty(&mut self) -> Result { + pub(super) fn ty(&mut self) -> Result { let name = self.name()?; Ok(match name.as_str() { "Bool" => Type::Bool, @@ -61,10 +61,8 @@ impl Parser<'_> { }) } - pub(super) fn function(&mut self) -> Result { - let line = self.line(); - self.expect_word("fn")?; - let name = self.name()?; + /// `(name: Type, ...)`. + pub(super) fn parameters(&mut self) -> Result, Diagnostic> { self.expect_sym("(")?; let mut params = Vec::new(); while !self.at_sym(")") { @@ -76,22 +74,28 @@ impl Parser<'_> { } } self.expect_sym(")")?; - self.expect_sym("->")?; - let ret = self.ty()?; - let intent = if self.at_word("intent") { - self.pos += 1; - match self.peek().cloned() { - Some(Token::Str(text)) => { - self.pos += 1; - Some(text) - } - _ => return self.error("expected the intent as a string"), + Ok(params) + } + + /// An `intent "..."` clause, where there is one. + pub(super) fn intent(&mut self) -> Result, Diagnostic> { + if !self.at_word("intent") { + return Ok(None); + } + self.pos += 1; + match self.peek().cloned() { + Some(Token::Str(text)) => { + self.pos += 1; + Ok(Some(text)) } - } else { - None - }; + _ => self.error("expected the intent as a string"), + } + } + + /// Every clause that starts with one of `words`, in order. + pub(super) fn clauses(&mut self, words: &[&str]) -> Result, Diagnostic> { let mut clauses = Vec::new(); - while self.at_word("requires") || self.at_word("ensures") || self.at_word("open") { + while words.iter().any(|word| self.at_word(word)) { let kind = if self.at_word("requires") { ClauseKind::Requires } else if self.at_word("ensures") { @@ -112,8 +116,20 @@ impl Parser<'_> { line, }); } + Ok(clauses) + } + + pub(super) fn function(&mut self) -> Result { + let line = self.line(); + self.expect_word("fn")?; + let name = self.name()?; + let params = self.parameters()?; + self.expect_sym("->")?; + let ret = self.ty()?; + let intent = self.intent()?; + let clauses = self.clauses(&["requires", "ensures", "open"])?; let body = if self.at_word("decide") { - self.decide()? + self.decide(Self::expr)? } else { self.expect_sym("{")?; let body = self.expr()?; @@ -130,6 +146,7 @@ impl Parser<'_> { ret, clauses, body, + machine: None, }) } @@ -183,7 +200,11 @@ impl Parser<'_> { Ok(args) } - fn decide(&mut self) -> Result { + /// A decision table whose rows give what `result` parses. + pub(super) fn decide( + &mut self, + result: fn(&mut Self) -> Result, + ) -> Result { let line = self.line(); self.expect_word("decide")?; self.expect_sym("{")?; @@ -203,7 +224,7 @@ impl Parser<'_> { self.expect_sym("=>")?; rows.push(Row { condition, - result: self.expr()?, + result: result(self)?, text, line: row_line, }); diff --git a/crates/accord/src/syntax/expr.rs b/crates/accord/src/syntax/expr.rs index fad0365..d10c102 100644 --- a/crates/accord/src/syntax/expr.rs +++ b/crates/accord/src/syntax/expr.rs @@ -149,8 +149,12 @@ impl Parser<'_> { } fn atom(&mut self) -> Result { + // `count` is a name too, so a quantifier is a word followed by + // `name in`. + let binds = + matches!(self.tokens.get(self.pos + 2), Some((Token::Word(w), ..)) if w == "in"); for quantifier in [Quantifier::All, Quantifier::Any, Quantifier::Count] { - if self.at_word(quantifier.name()) { + if self.at_word(quantifier.name()) && binds { return self.quantified(quantifier); } } diff --git a/crates/accord/src/syntax/machines.rs b/crates/accord/src/syntax/machines.rs new file mode 100644 index 0000000..a5def3f --- /dev/null +++ b/crates/accord/src/syntax/machines.rs @@ -0,0 +1,197 @@ +//! Machines: a state, inits, events, observers and invariants, and the run +//! an example gives. + +use super::parser::Parser; +use super::{ + Body, Clause, ClauseKind, Expr, Function, Machine, MachineExample, Member, Role, Type, +}; +use crate::Diagnostic; + +impl Parser<'_> { + pub(super) fn machine(&mut self) -> Result { + let line = self.line(); + self.expect_word("machine")?; + let name = self.name()?; + self.expect_sym("{")?; + let intent = self.intent()?; + let mut machine = Machine { + name, + public: false, + intent, + line, + file: 0, + state: Vec::new(), + inits: Vec::new(), + events: Vec::new(), + observers: Vec::new(), + invariants: Vec::new(), + }; + let mut stated = false; + while !self.at_sym("}") { + if self.at_word("state") { + if stated { + return self.error("a machine has one `state`"); + } + stated = true; + machine.state = self.state()?; + } else if self.at_word("init") { + machine.inits.push(self.transition(Role::Init)?); + } else if self.at_word("event") { + machine.events.push(self.transition(Role::Event)?); + } else if self.at_word("fn") { + let mut observer = self.function()?; + observer.machine = Some(Member { + role: Role::Observer, + state: 0, + }); + machine.observers.push(observer); + } else if self.at_word("invariant") || self.at_word("helper") { + machine.invariants.push(self.invariant()?); + } else { + return self.error( + "expected `state`, `init`, `event`, `fn`, `invariant` or `helper invariant`", + ); + } + } + self.expect_sym("}")?; + if !stated { + return Err(Diagnostic::new( + line, + format!("`{}` has no `state`", machine.name), + )); + } + Ok(machine) + } + + /// `state { field: Type, ... }`. + fn state(&mut self) -> Result, Diagnostic> { + self.expect_word("state")?; + self.expect_sym("{")?; + let mut fields = Vec::new(); + while !self.at_sym("}") { + let field = self.name()?; + self.expect_sym(":")?; + fields.push((field, self.ty()?)); + if !self.at_sym("}") { + self.expect_sym(",")?; + } + } + self.expect_sym("}")?; + Ok(fields) + } + + /// An init or event: its name and parameters, `intent` and `requires`, + /// and a body that ends in `next`. + fn transition(&mut self, role: Role) -> Result { + let line = self.line(); + self.pos += 1; + let name = self.name()?; + let params = self.parameters()?; + let intent = self.intent()?; + let clauses = self.clauses(&["requires"])?; + if self.at_word("ensures") || self.at_word("open") { + return self.error("an init or event takes `intent` and `requires` only"); + } + let body = if self.at_word("decide") { + self.decide(Self::step)? + } else { + self.expect_sym("{")?; + let body = self.step()?; + self.expect_sym("}")?; + Body::Expr(body) + }; + Ok(Function { + name, + public: false, + intent, + line, + file: 0, + params, + ret: Type::Bool, + clauses, + body, + machine: Some(Member { role, state: 0 }), + }) + } + + /// `next { ... }`, or an `if` and its `else` that each end in one. + pub(super) fn step(&mut self) -> Result { + if self.at_word("if") { + self.pos += 1; + let condition = self.expr()?; + self.expect_sym("{")?; + let then = self.step()?; + self.expect_sym("}")?; + self.expect_word("else")?; + self.expect_sym("{")?; + let otherwise = self.step()?; + self.expect_sym("}")?; + return Ok(Expr::If( + Box::new(condition), + Box::new(then), + Box::new(otherwise), + )); + } + if !self.at_word("next") { + return self.error("expected `next { … }` or an `if` that ends in one"); + } + let line = self.line(); + self.pos += 1; + self.expect_sym("{")?; + let mut fields = Vec::new(); + while !self.at_sym("}") { + let field = self.name()?; + self.expect_sym(":")?; + fields.push((field, self.expr()?)); + if !self.at_sym("}") { + self.expect_sym(",")?; + } + } + self.expect_sym("}")?; + Ok(Expr::Next(fields, line)) + } + + /// `invariant name: condition` or `helper invariant name: condition`. + fn invariant(&mut self) -> Result { + let (text, line) = self.rest_of_line(); + if self.at_word("helper") { + self.pos += 1; + } + self.expect_word("invariant")?; + self.name()?; + self.expect_sym(":")?; + Ok(Clause { + kind: ClauseKind::Invariant, + expr: self.expr()?, + text, + line, + }) + } + + /// `example Machine`, its steps one per line, then `gives condition`. + pub(super) fn machine_example(&mut self) -> Result { + let (_, line) = self.rest_of_line(); + self.expect_word("example")?; + let machine = self.name()?; + let mut steps = Vec::new(); + while !self.at_word("gives") { + steps.push(self.expr()?); + } + self.pos += 1; + let gives = self.expr()?; + let last = self.tokens[self.pos - 1].1; + let text = self.source[line - 1..last] + .iter() + .map(|l| l.trim()) + .collect::>() + .join(" "); + Ok(MachineExample { + machine, + file: 0, + steps, + gives, + text, + line, + }) + } +} diff --git a/crates/accord/src/syntax/parser.rs b/crates/accord/src/syntax/parser.rs index c649f23..cfd5de7 100644 --- a/crates/accord/src/syntax/parser.rs +++ b/crates/accord/src/syntax/parser.rs @@ -134,7 +134,6 @@ pub(super) fn is_keyword(word: &str) -> bool { | "result" | "all" | "any" - | "count" | "length" | "indices" ) @@ -150,7 +149,9 @@ pub(crate) fn parse(source: &str) -> Result { let mut program = Program { enums: Vec::new(), functions: Vec::new(), + machines: Vec::new(), examples: Vec::new(), + machine_examples: Vec::new(), }; while parser.peek().is_some() { // Within a folder every file sees every declaration; `pub` decides @@ -161,8 +162,20 @@ pub(crate) fn parse(source: &str) -> Result { } if parser.at_word("enum") { program.enums.push(parser.enumeration()?); + } else if parser.at_word("machine") { + let mut machine = parser.machine()?; + machine.public = public; + program.machines.push(machine); } else if parser.at_word("example") { - program.examples.push(parser.example()?); + // `example f(…) == v` calls a function; `example M` runs a machine. + if matches!( + parser.tokens.get(parser.pos + 2), + Some((Token::Sym("("), ..)) + ) { + program.examples.push(parser.example()?); + } else { + program.machine_examples.push(parser.machine_example()?); + } } else { let mut function = parser.function()?; function.public = public; diff --git a/crates/accord/src/typescript.rs b/crates/accord/src/typescript.rs index 8113b9e..791b0cf 100644 --- a/crates/accord/src/typescript.rs +++ b/crates/accord/src/typescript.rs @@ -60,6 +60,16 @@ fn proved(report: &Report) -> bool { /// names the functions that have one. pub fn build(files: &[(String, String)], solvers: &Solvers) -> Result { let (program, names) = crate::program_of(files)?; + if let Some(machine) = program.machines.first() { + return Err(Diagnostic::new( + machine.line, + format!( + "`{}` is a machine: machines aren't written as TypeScript yet", + machine.name + ), + ) + .in_file(&names[machine.file])); + } let report = crate::report(&program, None, &names, solvers); let modules = proved(&report).then(|| { modules(&program, &names, &report.openness) diff --git a/crates/accord/src/typescript/expr.rs b/crates/accord/src/typescript/expr.rs index ef2160e..3eb908a 100644 --- a/crates/accord/src/typescript/expr.rs +++ b/crates/accord/src/typescript/expr.rs @@ -162,6 +162,7 @@ impl Scope<'_> { } Expr::Length(list, _) => self.length(list), Expr::Index(list, index, _) => self.index(list, index), + Expr::Next(..) => unreachable!("`build` refuses a program with a machine"), } } diff --git a/crates/accord/tests/cli.rs b/crates/accord/tests/cli.rs index 3c4f22b..ff3af1e 100644 --- a/crates/accord/tests/cli.rs +++ b/crates/accord/tests/cli.rs @@ -69,7 +69,7 @@ fn check_json_writes_the_versioned_receipt() { ); let receipt: serde_json::Value = serde_json::from_slice(&output.stdout).expect("the receipt is JSON"); - assert_eq!(receipt["receipt"], 3); + assert_eq!(receipt["receipt"], 4); assert_eq!(receipt["standing"], "failed"); let larger = &receipt["definitions"][0]; assert_eq!(larger["name"], "larger"); diff --git a/crates/accord/tests/conformance.rs b/crates/accord/tests/conformance.rs index 2a2f2b8..be67a33 100644 --- a/crates/accord/tests/conformance.rs +++ b/crates/accord/tests/conformance.rs @@ -72,6 +72,7 @@ fn kind(outcome: &Outcome) -> &'static str { Outcome::Undecided { .. } => "undecided", Outcome::Unsupported { .. } => "unsupported", Outcome::WeakCallee { .. } => "weak_callee", + Outcome::NotInductive { .. } => "not_inductive", } } diff --git a/crates/accord/tests/diagnostics.rs b/crates/accord/tests/diagnostics.rs index eeeaa69..316e73e 100644 --- a/crates/accord/tests/diagnostics.rs +++ b/crates/accord/tests/diagnostics.rs @@ -49,7 +49,7 @@ fn json_rejection_and_missing_prerequisites_are_structured_without_a_proof() { assert_eq!(output.status.code(), Some(4)); let j: serde_json::Value = serde_json::from_slice(&output.stdout).expect("structured error on stdout"); - assert_eq!(j["receipt"], 3); + assert_eq!(j["receipt"], 4); assert_eq!(j["status"], status); assert!(j["standing"].is_null()); assert!(j["definitions"].as_array().unwrap().is_empty()); diff --git a/crates/accord/tests/machines.rs b/crates/accord/tests/machines.rs new file mode 100644 index 0000000..b63d152 --- /dev/null +++ b/crates/accord/tests/machines.rs @@ -0,0 +1,123 @@ +//! What the conformance cases leave open about machines: how events with +//! parameters and calls are explored, what an exploration that cannot finish +//! says, and what the receipt and `build` do with a machine. + +use accord::{Outcome, Refutation, Report, Solvers, build, receipt, verify}; + +const DIAL: &str = "enum Mode { Idle, Busy } + +machine Dial { + state { + level: i32, + mode: Mode, + } + + init start(initial: i32) + requires initial >= 0 and initial <= 2 + { + next { level: initial, mode: Idle } + } + + event set(to: i32, flag: Bool) + requires to >= 0 and to <= 12 + { + if flag { + next { level: to, mode: Busy } + } else { + next { level: to } + } + } + + invariant bounded: level <= 10 +} +"; + +fn report(source: &str) -> Report { + let solvers = Solvers::from_env().expect("Z3 and cvc5 are available"); + verify(source, &solvers).expect("the machine is accepted") +} + +fn clauses_of(report: &Report) -> Vec<(&str, &Outcome)> { + report + .verdicts + .iter() + .map(|v| (v.clause.as_str(), &v.outcome)) + .collect() +} + +#[test] +fn an_event_with_parameters_is_refuted_by_the_shortest_run() { + let report = report(DIAL); + let preserves = report + .verdicts + .iter() + .find(|v| v.clause.contains("`set` preserves")) + .expect("the event preserves its invariants"); + let Outcome::Refuted { + evidence: Refutation::Trace(steps), + } = &preserves.outcome + else { + panic!("not refuted by a run: {:?}", preserves.outcome); + }; + let calls: Vec<&str> = steps.iter().map(|s| s.call.as_str()).collect(); + assert_eq!(calls, ["start(0)", "set(to: 11, flag: false)"]); + let exploration = preserves.exploration.as_ref().expect("annotated"); + assert!(exploration.complete); + assert_eq!(exploration.states, 26); +} + +#[test] +fn a_parameter_without_known_values_leaves_exploration_incomplete() { + let source = DIAL.replace("requires to >= 0 and to <= 12", "requires to >= 0"); + let report = report(&source); + let allowed = report + .verdicts + .iter() + .find(|v| v.clause.contains("`set` is allowed")) + .expect("the event is allowed somewhere"); + assert!( + matches!(allowed.outcome, Outcome::Undecided { .. }), + "the solvers' state is not a run: {:?}", + clauses_of(&report) + ); + let exploration = allowed.exploration.as_ref().expect("annotated"); + assert!(!exploration.complete); +} + +#[test] +fn the_receipt_names_the_outcome_and_the_exploration() { + let source = "machine Pair { + state { x: i32, y: i32 } + init start() { next { x: 0, y: 0 } } + event step() requires x < 3 { next { x: x + 1, y: y + 1 } } + invariant y_bounded: y <= 3 +} +"; + let report = report(source); + let json: serde_json::Value = + serde_json::from_str(&receipt::json(&report, "pair")).expect("JSON"); + assert_eq!(json["receipt"], 4); + let definition = &json["definitions"][0]; + assert_eq!(definition["kind"], "machine"); + let stuck = definition["obligations"] + .as_array() + .expect("obligations") + .iter() + .find(|o| o["outcome"] == "not_inductive") + .expect("one obligation is not inductive"); + assert_eq!(stuck["kind"], "invariant"); + assert_eq!(stuck["exploration"]["complete"], true); + assert_eq!(json["diagnostics"][0]["code"], "ACC0015"); + assert_eq!(json["diagnostics"][0]["action"], "add_helper_invariant"); + assert_eq!(json["standing"], "incomplete"); +} + +#[test] +fn a_machine_is_not_written_as_typescript() { + let solvers = Solvers::from_env().expect("Z3 and cvc5 are available"); + let files = [("dial.accord".to_string(), DIAL.to_string())]; + let Err(refusal) = build(&files, &solvers) else { + panic!("a machine was built"); + }; + assert!(refusal.message.contains("machine"), "{}", refusal.message); +} From 6038e67da9a9b8583ca5a646a5449b6eb622834e Mon Sep 17 00:00:00 2001 From: Canitas <112231952+Sequela02@users.noreply.github.com> Date: Thu, 12 Nov 2026 20:25:30 -0700 Subject: [PATCH 3/9] docs: describe how machines are checked The receipt gains the not_inductive outcome, traces, the exploration annotation and ACC0015, and the concepts name them. Machines are checked now, though not yet written as TypeScript. Refs #82 --- docs/concepts.md | 18 +++++++++-- docs/design/syntax.md | 5 +-- docs/receipt.md | 71 +++++++++++++++++++++++++++++++++---------- 3 files changed, 73 insertions(+), 21 deletions(-) diff --git a/docs/concepts.md b/docs/concepts.md index 529115f..7edd460 100644 --- a/docs/concepts.md +++ b/docs/concepts.md @@ -64,7 +64,9 @@ never records acceptance; that stays with the person. by a **witness**, an input for which it holds, reported in source terms; - **refuted:** the solvers found a **counterexample**, concrete inputs on which it fails, reported in source terms; or, for an existential - obligation, both proved that no input exists; + obligation, both proved that no input exists; or, for a machine's + invariant or arithmetic, a **trace**, a run from an init that the + interpreter replays; - **undecided:** no proof and no counterexample, with a reason: a timeout, an unknown answer, or the solvers disagreeing (which is also raised as an alarm); @@ -75,7 +77,17 @@ never records acceptance; that stays with the person. a call takes a result its callee's contract allows and its body never gives. The interpreter tells the two apart by replaying the counterexample twice, once running every call and once giving each call - the solvers' value. + the solvers' value; + - **not inductive:** an obligation of a machine that the solvers refuted + from a state that meets every invariant and helper invariant, though no + run from an init was found to reach that state. The machine may be right: + a helper invariant can settle it. It is reported with the state and the + step's parameters, never as a failure. +- **Exploration** of a machine: a breadth-first search of the states its + inits and events reach, run by the interpreter. It finds the traces that + refute an obligation and the states that show an event is allowed. What it + covered, the states reached and whether every one was, is recorded on the + obligation; it is trusted, never an outcome, and proves nothing. - **Example run:** passed or failed. - **Strength** of a contract: small, plausible mistakes are planted in the body (mutants), and each is **caught** (the contract rules it out), @@ -127,7 +139,7 @@ weaker one count without a person. | --- | --- | | **failed** | An obligation is refuted or an example failed | | **verified** | Every obligation is proved, every example passed, all evidence is current, no open case remains and every assumption is approved | -| **incomplete** | Nothing failed, but something keeps it from verified: an undecided, unsupported or weak-callee obligation, stale evidence, an open case, an unapproved assumption, or a function it calls that isn't verified | +| **incomplete** | Nothing failed, but something keeps it from verified: an undecided, unsupported, weak-callee or not-inductive obligation, stale evidence, an open case, an unapproved assumption, or a function it calls that isn't verified | | **unverified** | No current evidence | A call is proved through its callee's contract, never its body, so a diff --git a/docs/design/syntax.md b/docs/design/syntax.md index e159ab2..c6a86de 100644 --- a/docs/design/syntax.md +++ b/docs/design/syntax.md @@ -178,8 +178,9 @@ Blocks are expressions: the last expression is the block's value. There is no ## 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 +Accepted for stage 10 ([#82](https://github.com/sequelcore/accord/issues/82)). +`accord check` checks a machine; `accord build` doesn't write it as +TypeScript 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 diff --git a/docs/receipt.md b/docs/receipt.md index 798cc77..874587a 100644 --- a/docs/receipt.md +++ b/docs/receipt.md @@ -1,6 +1,6 @@ # The receipt and review view -**Status: version 3, unstable until the first release.** `accord check ` produces a per-function terminal review view. Add `--json` for the same facts as a structured record with stable diagnostic codes. Both report only checks actually performed; neither records human approval. @@ -48,35 +48,34 @@ they are not failed proof attempts. In text mode pre-check errors go to stderr with an ACC code. A crash, interrupted command, empty output, or unreadable JSON must never be accepted as verified. -## JSON version 3 +## JSON version 4 Object keys have no fixed order; arrays keep source order. This replaces receipt -version 2, which had no calls between functions; there is no legacy-format -switch. `accord diff` retains its separately +version 3, which had no machines; there is no legacy-format switch. `accord diff` retains its separately versioned [comparison format](diff.md). | Field | Meaning | | --- | --- | -| `receipt` | Schema version, now 3 | +| `receipt` | Schema version, now 4 | | `accord` | Compiler package version | | `file` | Input path as passed to check | | `status` | checked, rejected, or unavailable | | `standing` | verified, failed, incomplete, unverified; null before a check exists | -| `definitions[]` | Each checked function, in source order | +| `definitions[]` | Each checked function or machine: functions in source order, then machines | | `diagnostics[]` | Conditions requiring attention, pointing to canonical evidence | Each definition has these fields: | Field | Meaning | | --- | --- | -| `name`, `kind` | Function name and function kind | +| `name`, `kind` | Name, and `function` or `machine` | | `file`, `line` | Source file within a folder, or null for a single file; 1-based declaration line | | `signature` | Function name, labeled parameters, and result type; no body | -| `parameters[]` | Parameter name and structured type | -| `result_type` | Structured result type | +| `parameters[]` | Parameter name and structured type; a machine's are its state's fields | +| `result_type` | Structured result type; null for a machine | | `types[]` | Used enums, each with name and source variants | | `intent` | Unchecked declared purpose, or null | -| `specification[]` | Each source clause, with text and 1-based line | +| `specification[]` | Each source clause, with text and 1-based line; a machine's are its invariants and helper invariants, the helpers written `helper invariant` | | `hash` | SHA-256 of normalized checked semantics; names and intent do not affect it | | `review_hash` | SHA-256 of this definition's review facts, excluding cache-use markers | | `standing` | The function's standing: verified only when every function it calls, directly or not, is verified too | @@ -88,11 +87,13 @@ Each definition has these fields: | `not_proved[]` | Limits, each with a stable kind and explanatory message | An obligation carries `kind` (postcondition, coverage, row_reachability, -overflow, precondition: a call meets its callee's `requires`, or bounds: an -index is within its list), `polarity` -(existential for row reachability, otherwise universal), `clause`, `line`, -`key`, `reused`, and `outcome`. Its key hashes the exact normalized SMT-LIB -script. Outcomes are proved, refuted, undecided, unsupported, or weak_callee. +overflow, precondition: a call meets its callee's `requires`, bounds: an +index is within its list, invariant: a machine's init or event leaves a state +that meets every invariant and helper invariant, or allowed), `polarity` +(existential for row reachability and allowed, otherwise universal), `clause`, +`line`, `key`, `reused`, and `outcome`. Its key hashes the exact normalized +SMT-LIB script. Outcomes are proved, refuted, undecided, unsupported, +weak_callee, or not_inductive. Proved existential checks carry `witness`; refuted universal checks carry `counterexample`; refuted existential checks carry `no_such_input: true`. Undecided and unsupported outcomes carry a human explanation in `reason`. @@ -102,6 +103,41 @@ each call in `calls[]` (the call as written, and the `value` the counterexample gives it) takes a result its callee's contract allows and its body never gives. Strengthening that contract can settle it; it makes standing incomplete, not failed. + +### Machines + +A machine is one definition. Its obligations come in this order: for each init, +that some input is allowed (when it has a `requires`) and that the state it +gives meets every invariant and helper invariant, then its arithmetic and +decision tables; for each event, that it preserves every invariant and helper +invariant and that it is allowed in some state an init reaches, then its +arithmetic and decision tables, each assuming the invariants; then the +observers, as functions. They are checked as functions of the state, so the +solvers prove them inductively, and their counterexamples start in any state +that meets the invariants. + +- An invariant or an arithmetic obligation is refuted only by a **trace**: a + `trace[]` of steps, each with the `call` (`start()`, `set(to: 3)`), and the + `state` it leaves as typed fields, or null for a step that doesn't end in a + state, as one that overflows. The explorer finds the trace, shortest first, + and the interpreter runs it again from its init before it is reported. An + init that breaks an invariant is a trace of one step. +- Where the solvers refute such an obligation from a state and no trace + reaches it, the outcome is `not_inductive`, with the `counterexample`: that + state and the step's parameters. It makes standing incomplete, not failed, + and its diagnostic is ACC0015. A helper invariant can settle it. +- An event is allowed in a reachable state when the explorer reaches one where + its `requires` hold. The outcome is then proved, with the `exploration`'s + `trace` ending in the event. It is refuted when both solvers prove that no + state that meets the invariants allows it. Otherwise it is undecided. + +An obligation that consulted the explorer carries `exploration`: `states`, the +number reached, and `complete`, whether every state and every way to move from +it was visited. It is trusted, not proved, and never an outcome. An init or +event is explored only if each parameter has finitely many known values: a +`Bool`, an enum, or an integer whose `requires` list its values or give it +literal bounds spanning at most 1024 values. Otherwise exploration is +incomplete. It also stops at 100,000 states and 2,000,000 steps. An agent routes undecided checks as unresolved regardless of that prose; ACC0003 does not promise that a timeout retry will succeed. @@ -189,6 +225,7 @@ there is no source location. Lines are 1-based; columns are not invented. | ACC0012 | No checked evidence for a function or program | add_checks | | ACC0013 | Obligation not proved because a callee's contract allows results its body never gives | strengthen_callee_contract | | ACC0014 | A function calls one that isn't verified | verify_callee | +| ACC0015 | A machine's obligation fails from a state no run from an init was found to reach | add_helper_invariant | Numbers identify conditions, never source lines, hashes, or particular solvers. They are never reassigned. Prose may change. ACC0004 supports the public Outcome @@ -205,7 +242,9 @@ is not proof of anything. Human acceptance remains a separate decision. ## Cache and freshness -The ledger in `.accord/` caches only proved, refuted and weak_callee outcomes, +The ledger in `.accord/` caches only proved, refuted and weak_callee outcomes +(a machine's trace and not_inductive outcomes are made again from the solvers' +answer and the exploration), keyed by the normalized script and compiler/solver builds. A script holds a callee's contract, never its body; an outcome resting on a replayed model, which runs the body, is also keyed by every callee's body. An unreadable or nonmatching entry From 5749af8eda9e31d37a41413a6963c021e5298485 Mon Sep 17 00:00:00 2001 From: Canitas <112231952+Sequela02@users.noreply.github.com> Date: Thu, 12 Nov 2026 20:31:09 -0700 Subject: [PATCH 4/9] refactor: keep count a keyword and rename the cases' field Making `count` an ordinary name changed the whole language for two cases. Those two cases' field is now `value`, since `count` is a quantifier keyword. No expected outcome changed. Refs #82 --- conformance/cases/machine-overflow-fault.accord | 8 ++++---- conformance/cases/machine-overflow.accord | 10 +++++----- crates/accord/src/syntax/expr.rs | 6 +----- crates/accord/src/syntax/parser.rs | 1 + 4 files changed, 11 insertions(+), 14 deletions(-) diff --git a/conformance/cases/machine-overflow-fault.accord b/conformance/cases/machine-overflow-fault.accord index f595af7..6bec224 100644 --- a/conformance/cases/machine-overflow-fault.accord +++ b/conformance/cases/machine-overflow-fault.accord @@ -2,17 +2,17 @@ // Without its `requires`, the third increment overflows `i32`. machine Counter { state { - count: i32, + value: i32, } init near_top() { - next { count: 2147483645 } + next { value: 2147483645 } } event increment() { - next { count: count + 1 } + next { value: value + 1 } } - invariant non_negative: count >= 0 + invariant non_negative: value >= 0 } diff --git a/conformance/cases/machine-overflow.accord b/conformance/cases/machine-overflow.accord index b22a8b5..bae5d9d 100644 --- a/conformance/cases/machine-overflow.accord +++ b/conformance/cases/machine-overflow.accord @@ -2,18 +2,18 @@ // A counter that starts near the top of `i32` and stops below it. machine Counter { state { - count: i32, + value: i32, } init near_top() { - next { count: 2147483645 } + next { value: 2147483645 } } event increment() - requires count < 2147483647 + requires value < 2147483647 { - next { count: count + 1 } + next { value: value + 1 } } - invariant non_negative: count >= 0 + invariant non_negative: value >= 0 } diff --git a/crates/accord/src/syntax/expr.rs b/crates/accord/src/syntax/expr.rs index d10c102..fad0365 100644 --- a/crates/accord/src/syntax/expr.rs +++ b/crates/accord/src/syntax/expr.rs @@ -149,12 +149,8 @@ impl Parser<'_> { } fn atom(&mut self) -> Result { - // `count` is a name too, so a quantifier is a word followed by - // `name in`. - let binds = - matches!(self.tokens.get(self.pos + 2), Some((Token::Word(w), ..)) if w == "in"); for quantifier in [Quantifier::All, Quantifier::Any, Quantifier::Count] { - if self.at_word(quantifier.name()) && binds { + if self.at_word(quantifier.name()) { return self.quantified(quantifier); } } diff --git a/crates/accord/src/syntax/parser.rs b/crates/accord/src/syntax/parser.rs index cfd5de7..09c747e 100644 --- a/crates/accord/src/syntax/parser.rs +++ b/crates/accord/src/syntax/parser.rs @@ -134,6 +134,7 @@ pub(super) fn is_keyword(word: &str) -> bool { | "result" | "all" | "any" + | "count" | "length" | "indices" ) From 6dce23ecd0ae3003cb55f27fc66dce11325e7f78 Mon Sep 17 00:00:00 2001 From: Canitas <112231952+Sequela02@users.noreply.github.com> Date: Thu, 12 Nov 2026 20:31:10 -0700 Subject: [PATCH 5/9] feat: report helper invariants as support and type every input A helper invariant is marked in the checked program and reported as support beside the specification, in JSON and text; it is assumed and proved as an invariant is. Each machine obligation also carries the parameters its inputs name, so a not_inductive state or an event witness types the event's and init's parameters too. Refs #82 --- crates/accord/src/evidence.rs | 2 + crates/accord/src/evidence/machine.rs | 8 +++ crates/accord/src/evidence/standing.rs | 2 + crates/accord/src/lib.rs | 7 +++ crates/accord/src/receipt/json.rs | 24 +++++---- crates/accord/src/receipt/text.rs | 3 ++ crates/accord/src/syntax.rs | 3 ++ crates/accord/src/syntax/declarations.rs | 1 + crates/accord/src/syntax/machines.rs | 4 +- crates/accord/tests/machines.rs | 67 ++++++++++++++++++++++++ docs/receipt.md | 5 +- 11 files changed, 114 insertions(+), 12 deletions(-) diff --git a/crates/accord/src/evidence.rs b/crates/accord/src/evidence.rs index fb173ba..60fa2e8 100644 --- a/crates/accord/src/evidence.rs +++ b/crates/accord/src/evidence.rs @@ -120,6 +120,7 @@ pub(crate) fn report( clause: o.clause, line: o.line, exploration: None, + parameters: Vec::new(), }); } } @@ -184,6 +185,7 @@ pub(crate) fn report( } Definition { kind: DefinitionKind::Function, + support: Vec::new(), name: unit.source.name.clone(), intent: unit.source.intent.clone(), line: unit.source.line, diff --git a/crates/accord/src/evidence/machine.rs b/crates/accord/src/evidence/machine.rs index 17659b5..0da8e1f 100644 --- a/crates/accord/src/evidence/machine.rs +++ b/crates/accord/src/evidence/machine.rs @@ -292,6 +292,7 @@ pub(super) fn check(program: &Program, machine: &Machine, solvers: &Solvers) -> clause: ob.clause.clone(), line: ob.line, exploration, + parameters: units[m].source.params.clone(), }); } } @@ -334,6 +335,13 @@ pub(super) fn check(program: &Program, machine: &Machine, solvers: &Solvers) -> specification: machine .invariants .iter() + .filter(|c| !c.helper) + .map(|c| (c.line, c.text.clone())) + .collect(), + support: machine + .invariants + .iter() + .filter(|c| c.helper) .map(|c| (c.line, c.text.clone())) .collect(), enums, diff --git a/crates/accord/src/evidence/standing.rs b/crates/accord/src/evidence/standing.rs index 8abea73..b5872e7 100644 --- a/crates/accord/src/evidence/standing.rs +++ b/crates/accord/src/evidence/standing.rs @@ -71,6 +71,7 @@ mod tests { definition: String::new(), reused: false, exploration: None, + parameters: Vec::new(), } } @@ -128,6 +129,7 @@ mod tests { .iter() .map(|&standing| Definition { kind: crate::DefinitionKind::Function, + support: Vec::new(), intent: None, line: 1, params: Vec::new(), diff --git a/crates/accord/src/lib.rs b/crates/accord/src/lib.rs index dcb9fd0..7bd06bf 100644 --- a/crates/accord/src/lib.rs +++ b/crates/accord/src/lib.rs @@ -205,6 +205,10 @@ pub struct Verdict { /// For an obligation about a machine's reachable states: what exploring /// them covered. pub exploration: Option, + /// The parameters the inputs of its outcome name, for an obligation of a + /// machine's init, event or observer; empty for a function's, whose + /// parameters are the definition's. + pub parameters: Vec<(String, Type)>, } /// Whether an example gave its result when run. @@ -287,6 +291,9 @@ pub struct Definition { pub specification: Vec<(usize, String)>, /// Enums used by this function, with their source variants. pub enums: Vec<(String, Vec)>, + /// For a machine, its helper invariants: support for proving its + /// invariants, not claims. Empty for a function. + pub support: Vec<(usize, String)>, /// The file it's declared in, when a folder was checked. pub file: Option, /// The hash of the normalized function. diff --git a/crates/accord/src/receipt/json.rs b/crates/accord/src/receipt/json.rs index 472a53b..a133da1 100644 --- a/crates/accord/src/receipt/json.rs +++ b/crates/accord/src/receipt/json.rs @@ -50,11 +50,11 @@ fn typed(source: &str, ty: &Type) -> Value { } } -fn inputs_json(inputs: &Inputs, definition: &Definition) -> Value { +fn inputs_json(inputs: &Inputs, params: &[(String, Type)]) -> Value { inputs .iter() .map(|(name, value)| { - let mut out = match definition.params.iter().find(|(n, _)| n == name) { + let mut out = match params.iter().find(|(n, _)| n == name) { Some((_, ty)) => typed(value, ty), None => json!({"source": value, "valid": false, "value": null}), }; @@ -70,7 +70,7 @@ fn trace_json(steps: &[TraceStep], definition: &Definition) -> Value { .map(|step| { json!({ "call": step.call, - "state": step.state.as_ref().map(|state| inputs_json(state, definition)), + "state": step.state.as_ref().map(|state| inputs_json(state, &definition.params)), }) }) .collect() @@ -89,17 +89,22 @@ fn verdict_json(verdict: &Verdict, definition: &Definition) -> Value { "key": verdict.key, "reused": verdict.reused, }); + let params = if verdict.parameters.is_empty() { + &definition.params + } else { + &verdict.parameters + }; let fields = match &verdict.outcome { Outcome::Proved { witness } => { let mut fields = json!({ "outcome": "proved" }); if let Some(inputs) = witness { - fields["witness"] = inputs_json(inputs, definition); + fields["witness"] = inputs_json(inputs, params); } fields } Outcome::Refuted { evidence: Refutation::Counterexample(inputs), - } => json!({ "outcome": "refuted", "counterexample": inputs_json(inputs, definition) }), + } => json!({ "outcome": "refuted", "counterexample": inputs_json(inputs, params) }), Outcome::Refuted { evidence: Refutation::NoSuchInput, } => json!({ "outcome": "refuted", "no_such_input": true }), @@ -108,13 +113,13 @@ fn verdict_json(verdict: &Verdict, definition: &Definition) -> Value { } => json!({ "outcome": "refuted", "trace": trace_json(steps, definition) }), Outcome::NotInductive { inputs } => json!({ "outcome": "not_inductive", - "counterexample": inputs_json(inputs, definition), + "counterexample": inputs_json(inputs, params), }), Outcome::Undecided { reason } => json!({ "outcome": "undecided", "reason": reason }), Outcome::Unsupported { reason } => json!({ "outcome": "unsupported", "reason": reason }), Outcome::WeakCallee { inputs, calls } => json!({ "outcome": "weak_callee", - "counterexample": inputs_json(inputs, definition), + "counterexample": inputs_json(inputs, params), "calls": calls .iter() .map(|(call, value)| json!({ "call": call, "value": value })) @@ -165,7 +170,7 @@ fn openness_json(openness: &Openness, definition: &Definition) -> Value { code, } => json!({ "open": { - "inputs": inputs_json(inputs, definition), + "inputs": inputs_json(inputs, &definition.params), "results": [result_typed(&results.0, definition), result_typed(&results.1, definition)], "implementation": result_typed(code, definition), } @@ -186,7 +191,7 @@ fn strength_json(strength: &Strength, definition: &Definition) -> Value { .iter() .map(|s| json!({ "change": s.change, - "inputs": inputs_json(&s.inputs, definition), + "inputs": inputs_json(&s.inputs, &definition.params), "original": result_typed(&s.original, definition), "mutant": result_typed(&s.mutant, definition), })) @@ -220,6 +225,7 @@ pub(super) fn definition_json(report: &Report, definition: &Definition) -> Value "parameters": definition.params.iter().map(|(name, ty)| json!({"name": name, "type": type_json(ty)})).collect::>(), "result_type": definition.result_type.as_ref().map(type_json), "types": definition.enums.iter().map(|(name, variants)| json!({"name": name, "variants": variants})).collect::>(), + "support": definition.support.iter().map(|(line, text)| json!({"line": line, "text": text})).collect::>(), "specification": definition.specification.iter().map(|(line, text)| json!({"line": line, "text": text})).collect::>(), "not_proved": review::limits(report, definition).into_iter().map(|(kind, message)| json!({"kind": kind, "message": message})).collect::>(), "name": definition.name, diff --git a/crates/accord/src/receipt/text.rs b/crates/accord/src/receipt/text.rs index 7e1b563..6c64862 100644 --- a/crates/accord/src/receipt/text.rs +++ b/crates/accord/src/receipt/text.rs @@ -217,6 +217,9 @@ pub fn text(report: &Report) -> String { ), None => format!("intent {}{file}: not declared", definition.name), }); + for (line, clause) in &definition.support { + lines.push(format!("support line {line}: {clause}")); + } if definition.specification.is_empty() { lines.push("specification none declared".to_string()); } diff --git a/crates/accord/src/syntax.rs b/crates/accord/src/syntax.rs index 6d5a0c6..098c760 100644 --- a/crates/accord/src/syntax.rs +++ b/crates/accord/src/syntax.rs @@ -222,6 +222,9 @@ pub(crate) enum ClauseKind { #[derive(Clone, Debug)] pub(crate) struct Clause { pub kind: ClauseKind, + /// A helper invariant: assumed and proved as an invariant is, but support + /// for proving the others rather than a claim. + pub helper: bool, pub expr: Expr, pub text: String, pub line: usize, diff --git a/crates/accord/src/syntax/declarations.rs b/crates/accord/src/syntax/declarations.rs index 7e768ab..0ae0225 100644 --- a/crates/accord/src/syntax/declarations.rs +++ b/crates/accord/src/syntax/declarations.rs @@ -111,6 +111,7 @@ impl Parser<'_> { let expr = self.expr()?; clauses.push(Clause { kind, + helper: false, expr, text, line, diff --git a/crates/accord/src/syntax/machines.rs b/crates/accord/src/syntax/machines.rs index a5def3f..9c7610b 100644 --- a/crates/accord/src/syntax/machines.rs +++ b/crates/accord/src/syntax/machines.rs @@ -154,7 +154,8 @@ impl Parser<'_> { /// `invariant name: condition` or `helper invariant name: condition`. fn invariant(&mut self) -> Result { let (text, line) = self.rest_of_line(); - if self.at_word("helper") { + let helper = self.at_word("helper"); + if helper { self.pos += 1; } self.expect_word("invariant")?; @@ -162,6 +163,7 @@ impl Parser<'_> { self.expect_sym(":")?; Ok(Clause { kind: ClauseKind::Invariant, + helper, expr: self.expr()?, text, line, diff --git a/crates/accord/tests/machines.rs b/crates/accord/tests/machines.rs index b63d152..c35e0aa 100644 --- a/crates/accord/tests/machines.rs +++ b/crates/accord/tests/machines.rs @@ -121,3 +121,70 @@ fn a_machine_is_not_written_as_typescript() { }; assert!(refusal.message.contains("machine"), "{}", refusal.message); } + +const STEPPED: &str = "machine Pair { + state { x: i32, y: i32 } + init start() { next { x: 0, y: 0 } } + event bump(by: i32) + requires x < 3 and by >= 1 and by <= 1 + { + next { x: x + by, y: y + by } + } + invariant y_bounded: y <= 3 +} +"; + +#[test] +fn every_input_a_receipt_names_is_typed() { + let json: serde_json::Value = + serde_json::from_str(&receipt::json(&report(STEPPED), "pair")).expect("JSON"); + let stuck = json["definitions"][0]["obligations"] + .as_array() + .expect("obligations") + .iter() + .find(|o| o["outcome"] == "not_inductive") + .expect("one obligation is not inductive"); + let names: Vec<&str> = stuck["counterexample"] + .as_array() + .expect("inputs") + .iter() + .map(|input| { + assert_eq!(input["valid"], true, "{input}"); + input["name"].as_str().expect("a name") + }) + .collect(); + assert!( + names.contains(&"by"), + "the event's parameter is named: {names:?}" + ); + let allowed = json["definitions"][0]["obligations"] + .as_array() + .expect("obligations") + .iter() + .find(|o| o["kind"] == "allowed" && o["outcome"] == "proved") + .expect("the event is allowed"); + assert_eq!(allowed["witness"][0]["name"], "by"); + assert_eq!(allowed["witness"][0]["valid"], true); +} + +#[test] +fn a_helper_invariant_is_support_not_a_claim() { + let source = STEPPED.replace( + " invariant y_bounded", + " helper invariant together: x == y + invariant y_bounded", + ); + let report = report(&source); + let json: serde_json::Value = + serde_json::from_str(&receipt::json(&report, "pair")).expect("JSON"); + let machine = &json["definitions"][0]; + assert_eq!(machine["specification"].as_array().map(Vec::len), Some(1)); + assert_eq!(machine["support"].as_array().map(Vec::len), Some(1)); + assert!( + machine["support"][0]["text"] + .as_str() + .is_some_and(|t| t.starts_with("helper invariant")) + ); + assert!(receipt::text(&report).contains("support line")); + assert_eq!(machine["standing"], "verified"); +} diff --git a/docs/receipt.md b/docs/receipt.md index 874587a..2b6f8f6 100644 --- a/docs/receipt.md +++ b/docs/receipt.md @@ -75,7 +75,8 @@ Each definition has these fields: | `result_type` | Structured result type; null for a machine | | `types[]` | Used enums, each with name and source variants | | `intent` | Unchecked declared purpose, or null | -| `specification[]` | Each source clause, with text and 1-based line; a machine's are its invariants and helper invariants, the helpers written `helper invariant` | +| `specification[]` | Each source clause, with text and 1-based line; a machine's are its invariants | +| `support[]` | A machine's helper invariants, each with text and line: support for proving its invariants, not claims. Both are assumed and proved alike; empty for a function | | `hash` | SHA-256 of normalized checked semantics; names and intent do not affect it | | `review_hash` | SHA-256 of this definition's review facts, excluding cache-use markers | | `standing` | The function's standing: verified only when every function it calls, directly or not, is verified too | @@ -146,7 +147,7 @@ failed. Passing an example proves no universal property. ### Typed witness values -Inputs in witnesses, counterexamples, open cases, and mutants have a parameter +Inputs in witnesses, counterexamples, open cases, and mutants (a machine's state fields and the parameters of the init or event) have a parameter `name`, structured `type`, decoded `value`, exact `source` spelling, and `valid`. Result values use the same shape without name. Types are: From cbddd1bed4280f38d044fc960627609a55f37419 Mon Sep 17 00:00:00 2001 From: Canitas <112231952+Sequela02@users.noreply.github.com> Date: Thu, 12 Nov 2026 20:45:50 -0700 Subject: [PATCH 6/9] test: write machine cases for the review's findings A review found an argument outside its type proving an event allowed, an overflowing step refuting an invariant it never broke, and two invariants sharing a name. These cases fix the intended outcomes before the code changes: each failure is reported once, by its own obligation, and no run uses a value its type can't hold. Refs #82 --- .../cases/machine-init-overflow-fault.accord | 17 +++++++++++++++ .../cases/machine-invariant-twice.accord | 16 ++++++++++++++ .../cases/machine-overflow-step-fault.accord | 21 +++++++++++++++++++ .../cases/machine-wide-argument-fault.accord | 20 ++++++++++++++++++ 4 files changed, 74 insertions(+) create mode 100644 conformance/cases/machine-init-overflow-fault.accord create mode 100644 conformance/cases/machine-invariant-twice.accord create mode 100644 conformance/cases/machine-overflow-step-fault.accord create mode 100644 conformance/cases/machine-wide-argument-fault.accord diff --git a/conformance/cases/machine-init-overflow-fault.accord b/conformance/cases/machine-init-overflow-fault.accord new file mode 100644 index 0000000..145a309 --- /dev/null +++ b/conformance/cases/machine-init-overflow-fault.accord @@ -0,0 +1,17 @@ +// expect: proved, proved, refuted +// `start(2147483647)` overflows in its own addition; the invariant is proved +// assuming the addition stays in range, and the addition's obligation is +// refuted by that run. +machine Counter { + state { + value: i32, + } + + init start(from: i32) + requires from >= 0 + { + next { value: from + 1 } + } + + invariant positive: value > 0 +} diff --git a/conformance/cases/machine-invariant-twice.accord b/conformance/cases/machine-invariant-twice.accord new file mode 100644 index 0000000..582fa19 --- /dev/null +++ b/conformance/cases/machine-invariant-twice.accord @@ -0,0 +1,16 @@ +// expect: error +// Invariants are named so a run can say which one it breaks: two can't +// share a name. +machine Switch { + state { + presses: i32, + } + + init start() { + next { presses: 0 } + } + + invariant bounded: presses >= 0 + + invariant bounded: presses <= 100 +} diff --git a/conformance/cases/machine-overflow-step-fault.accord b/conformance/cases/machine-overflow-step-fault.accord new file mode 100644 index 0000000..366230e --- /dev/null +++ b/conformance/cases/machine-overflow-step-fault.accord @@ -0,0 +1,21 @@ +// expect: proved, proved, proved, refuted +// `increment` overflows from the state `start` gives. That is a failure of +// the addition, and only the addition's obligation reports it: an event's +// invariants are proved assuming its arithmetic stays in range, since that +// is an obligation of its own. +machine Counter { + state { + value: i32, + } + + init start() { + next { value: 2147483647 } + } + + event increment() + { + next { value: value + 1 } + } + + invariant capped: value <= 2147483647 +} diff --git a/conformance/cases/machine-wide-argument-fault.accord b/conformance/cases/machine-wide-argument-fault.accord new file mode 100644 index 0000000..7b9531e --- /dev/null +++ b/conformance/cases/machine-wide-argument-fault.accord @@ -0,0 +1,20 @@ +// expect: proved, proved, refuted +// `set` asks for an argument no `i32` holds, so no state allows it: the +// solvers prove that none does, and no run can use a value outside `i32`. +machine Gauge { + state { + level: i32, + } + + init start() { + next { level: 0 } + } + + event set(reading: i32) + requires reading >= 3000000000 and reading <= 3000000010 + { + next { level: 1 } + } + + invariant low: level < 100 +} From 20240a7c2352d95e1d0e13d0b390ae4271418775 Mon Sep 17 00:00:00 2001 From: Canitas <112231952+Sequela02@users.noreply.github.com> Date: Thu, 12 Nov 2026 20:49:06 -0700 Subject: [PATCH 7/9] fix: keep machine runs and proofs inside their types Arguments the explorer enumerates, and that a run may carry, are now within their parameter's type. An init's or event's invariants are proved, and a run breaks them, only where its arithmetic stays within its type; that failure belongs to the arithmetic obligation alone. `accord diff` refuses a machine, a machine's hash covers each member's role and whether an invariant is a helper, invariant names are unique, and an outcome the explorer changed no longer says it was reused. Refs #82 --- crates/accord/src/diff.rs | 6 ++++++ crates/accord/src/evidence/machine.rs | 10 ++++++++-- crates/accord/src/explore.rs | 14 ++++++++++++-- crates/accord/src/identity/normalize.rs | 6 +++++- crates/accord/src/interpret/replay.rs | 13 ++++++++++--- crates/accord/src/obligation.rs | 10 ++++++++-- crates/accord/src/obligation/operations.rs | 14 +++++++++++++- crates/accord/src/syntax/machines.rs | 21 ++++++++++++++++----- crates/accord/tests/diff.rs | 21 +++++++++++++++++++++ crates/accord/tests/machines.rs | 20 ++++++++++++++++++++ 10 files changed, 119 insertions(+), 16 deletions(-) diff --git a/crates/accord/src/diff.rs b/crates/accord/src/diff.rs index e4fcc72..0b5d814 100644 --- a/crates/accord/src/diff.rs +++ b/crates/accord/src/diff.rs @@ -134,6 +134,12 @@ fn compare(old: &Unit, new: &Unit, solvers: &Solvers) -> Change { fn parse(source: &str, side: Side) -> Result { let mut program = syntax::parse(source).map_err(|d| (side, d))?; check::check(&mut program, &[]).map_err(|d| (side, d))?; + if let Some(machine) = program.machines.first() { + return Err(( + side, + Diagnostic::new(machine.line, "machines aren't compared yet"), + )); + } Ok(program) } diff --git a/crates/accord/src/evidence/machine.rs b/crates/accord/src/evidence/machine.rs index 0da8e1f..967f42b 100644 --- a/crates/accord/src/evidence/machine.rs +++ b/crates/accord/src/evidence/machine.rs @@ -182,7 +182,7 @@ impl Context<'_> { let refuted = Outcome::Refuted { evidence: Refutation::Trace(steps(self.units, &trace, true)), }; - return (refuted, reused, None); + return (refuted, false, None); } let from_state = role != Role::Init && !allowed && ob.polarity == obligation::Polarity::Universal; @@ -203,7 +203,7 @@ impl Context<'_> { evidence: Refutation::Trace(steps(self.units, trace, true)), }, }; - return (outcome, reused, self.note(None)); + return (outcome, false, self.note(None)); } let outcome = match (role, outcome) { (Role::Event, Outcome::Proved { .. }) if allowed => Outcome::Undecided { @@ -230,6 +230,12 @@ impl Context<'_> { }; let consulted = role == Role::Event && allowed || matches!(outcome, Outcome::NotInductive { .. }); + // What the explorer turned into another outcome isn't the ledger's. + let reused = reused + && !matches!( + outcome, + Outcome::NotInductive { .. } | Outcome::Undecided { .. } + ); ( outcome, reused, diff --git a/crates/accord/src/explore.rs b/crates/accord/src/explore.rs index ce735e9..6fe749d 100644 --- a/crates/accord/src/explore.rs +++ b/crates/accord/src/explore.rs @@ -65,6 +65,15 @@ impl Member<'_> { /// The state the member ends in, when it is run in code. pub fn run(&self, state: Option<&[Value]>, args: &[Value]) -> Result, String> { + let function = self.function(); + let skip = function.machine.map_or(0, |m| m.state); + for ((name, ty), arg) in function.params[skip..].iter().zip(args) { + if let (Type::Int(width), Value::Int(n)) = (ty, arg) + && !(width.min()..=width.max()).contains(n) + { + return Err(format!("`{name}` is {n}, which is outside its type")); + } + } interpret::transition( self.function(), &self.names(state, args), @@ -213,7 +222,8 @@ fn integers(name: &str, width: Width, requires: &[&Expr]) -> Option> _ => {} } } - let (low, high) = (low.unwrap_or(width.min()), high.unwrap_or(width.max())); + let low = low.map_or(width.min(), |l| l.max(width.min())); + let high = high.map_or(width.max(), |h| h.min(width.max())); let mut values: Vec = match (set, low > width.min() || high < width.max()) { (Some(set), _) => set .into_iter() @@ -400,7 +410,7 @@ pub(crate) fn start(members: &[Member], m: usize, model: &[(String, String)]) -> .iter() .map(|(_, value)| value.clone()) .collect(); - let state = member.run(None, &args).ok(); + let state = Some(member.run(None, &args).ok()?); Some(Step { member: m, args, diff --git a/crates/accord/src/identity/normalize.rs b/crates/accord/src/identity/normalize.rs index d6cf763..adf607e 100644 --- a/crates/accord/src/identity/normalize.rs +++ b/crates/accord/src/identity/normalize.rs @@ -159,11 +159,15 @@ pub(super) fn canonical(function: &Function, with_body: bool) -> String { out += &format!(" (param {ty:?})"); } out += &format!(" (returns {:?})", function.ret); + if let Some(member) = function.machine { + out += &format!(" (member {:?})", member.role); + } for clause in &function.clauses { if with_body || clause.kind != ClauseKind::Open { out += &format!( - " ({:?} {})", + " ({:?}{} {})", clause.kind, + if clause.helper { " helper" } else { "" }, crate::obligation::term(&clause.expr) ); } diff --git a/crates/accord/src/interpret/replay.rs b/crates/accord/src/interpret/replay.rs index 21f0ed1..a132e78 100644 --- a/crates/accord/src/interpret/replay.rs +++ b/crates/accord/src/interpret/replay.rs @@ -37,10 +37,17 @@ fn reproduces( Ok(match &obligation.claim { Claim::Allowed => true, Claim::Invariants => { - let Value::List(next) = body(function, &env)? else { - return Err("a transition ends in a state".to_string()); + // A step whose arithmetic leaves its type ends in no state; its + // own obligation reports that. + let code = Env { + mode: Mode::Code, + ..env }; - broken_invariant(function, &next)?.is_some() + match body(function, &code) { + Ok(Value::List(next)) => broken_invariant(function, &next)?.is_some(), + Ok(_) => return Err("a transition ends in a state".to_string()), + Err(_) => false, + } } Claim::Ensures(clause) => { let result = body(function, &env)?; diff --git a/crates/accord/src/obligation.rs b/crates/accord/src/obligation.rs index 7f28886..dcc415c 100644 --- a/crates/accord/src/obligation.rs +++ b/crates/accord/src/obligation.rs @@ -35,7 +35,9 @@ pub(crate) use claims::Claim; use claims::claim_of; use lists::list_facts; pub(crate) use operations::Guard; -use operations::{Operation, assumption, body_operations, for_some, guard_term, spec_indexes}; +use operations::{ + Operation, assumption, body_operations, for_some, guard_term, range_assumption, spec_indexes, +}; pub(crate) use scripts::{mutant_scripts, open_script}; pub(crate) use smt::{all, datatypes, ending, in_range, sort, term}; use smt::{meets_invariants, prelude, value}; @@ -163,6 +165,10 @@ fn obligations_of<'a>( { out.push(allowed(format!("`{name}` is allowed for some input"))); } + // The arithmetic that makes the next state stays within its type: an + // obligation of its own, assumed here as a call's `requires` is. + let mut fits = every.clone(); + fits.extend(ops.iter().filter_map(range_assumption)); let fails = format!("(not {})", meets_invariants(function)); out.push(obligation( &if init { @@ -176,7 +182,7 @@ fn obligations_of<'a>( Polarity::Universal, Claim::Invariants, "", - &every, + &fits, &[], match &covered { Some(covered) => format!("(and {covered} {fails})"), diff --git a/crates/accord/src/obligation/operations.rs b/crates/accord/src/obligation/operations.rs index f5dd7cb..d41e60e 100644 --- a/crates/accord/src/obligation/operations.rs +++ b/crates/accord/src/obligation/operations.rs @@ -4,7 +4,7 @@ use super::calls::{has_requires, requires_of}; use super::lists::{at_index, in_bounds, index_name}; -use super::smt::{all, term}; +use super::smt::{all, in_range, term}; use crate::syntax::{Body, Expr, Function, Op, Program}; /// A condition that must have a given value for code to run; `None` is a @@ -180,6 +180,18 @@ pub(super) fn for_every(bound: &[&Expr], claim: String) -> String { } out } +/// That where `op` runs, an arithmetic operation stays within its type; `None` +/// for any other operation. +pub(super) fn range_assumption(op: &Operation) -> Option { + let (Expr::Arith(.., site) | Expr::Neg(_, site)) = op.expr else { + return None; + }; + let width = site.width?; + let guards = all("and", op.guards.iter().map(guard_term).collect(), "true"); + let holds = format!("(=> {guards} {})", in_range(&term(op.expr), width)); + Some(for_every(&op.bound, holds)) +} + /// That where `op` runs, its callee's `requires` holds; `None` for an /// operation that isn't a call to a function with a `requires`. pub(super) fn assumption(program: &Program, op: &Operation) -> Option { diff --git a/crates/accord/src/syntax/machines.rs b/crates/accord/src/syntax/machines.rs index 9c7610b..4bfce74 100644 --- a/crates/accord/src/syntax/machines.rs +++ b/crates/accord/src/syntax/machines.rs @@ -27,6 +27,7 @@ impl Parser<'_> { invariants: Vec::new(), }; let mut stated = false; + let mut names: Vec = Vec::new(); while !self.at_sym("}") { if self.at_word("state") { if stated { @@ -46,7 +47,16 @@ impl Parser<'_> { }); machine.observers.push(observer); } else if self.at_word("invariant") || self.at_word("helper") { - machine.invariants.push(self.invariant()?); + let line = self.line(); + let (name, invariant) = self.invariant()?; + if names.contains(&name) { + return Err(Diagnostic::new( + line, + format!("`{name}` names two invariants of `{}`", machine.name), + )); + } + names.push(name); + machine.invariants.push(invariant); } else { return self.error( "expected `state`, `init`, `event`, `fn`, `invariant` or `helper invariant`", @@ -152,22 +162,23 @@ impl Parser<'_> { } /// `invariant name: condition` or `helper invariant name: condition`. - fn invariant(&mut self) -> Result { + fn invariant(&mut self) -> Result<(String, Clause), Diagnostic> { let (text, line) = self.rest_of_line(); let helper = self.at_word("helper"); if helper { self.pos += 1; } self.expect_word("invariant")?; - self.name()?; + let name = self.name()?; self.expect_sym(":")?; - Ok(Clause { + let clause = Clause { kind: ClauseKind::Invariant, helper, expr: self.expr()?, text, line, - }) + }; + Ok((name, clause)) } /// `example Machine`, its steps one per line, then `gives condition`. diff --git a/crates/accord/tests/diff.rs b/crates/accord/tests/diff.rs index 48d9417..2d168ac 100644 --- a/crates/accord/tests/diff.rs +++ b/crates/accord/tests/diff.rs @@ -159,3 +159,24 @@ fn a_dropped_property_of_the_ported_rule_is_caught() { ); assert_ne!(result, "ProofOutcome.TimedOut"); } + +#[test] +fn a_machine_on_either_side_is_refused() { + let solvers = + Solvers::from_env().expect("Z3 and cvc5 are available (see conformance/README.md)"); + let machine = "machine Switch { + state { presses: i32 } + init start() { next { presses: 0 } } + invariant bounded: presses >= 0 +} +"; + let Err((side, refusal)) = diff(ADD, machine, &solvers) else { + panic!("a machine was compared"); + }; + assert_eq!(side, accord::diff::Side::New); + assert!(refusal.message.contains("machines aren't compared yet")); + let Err((side, _)) = diff(machine, ADD, &solvers) else { + panic!("a machine was compared"); + }; + assert_eq!(side, accord::diff::Side::Old); +} diff --git a/crates/accord/tests/machines.rs b/crates/accord/tests/machines.rs index c35e0aa..1d7e132 100644 --- a/crates/accord/tests/machines.rs +++ b/crates/accord/tests/machines.rs @@ -188,3 +188,23 @@ fn a_helper_invariant_is_support_not_a_claim() { assert!(receipt::text(&report).contains("support line")); assert_eq!(machine["standing"], "verified"); } + +#[test] +fn a_machine_s_hash_covers_roles_and_helpers() { + let hash = |source: &str| report(source).definitions[0].hash.clone(); + let base = "machine M { + state { x: i32 } + init a() { next { x: 0 } } + event b() { next { x: 0 } } + invariant i: x >= 0 +} +"; + let second_init = base.replace("event b()", "init b()"); + let helper = base.replace(" invariant i", " helper invariant i"); + assert_ne!(hash(base), hash(&second_init)); + assert_ne!(hash(base), hash(&helper)); + assert_eq!( + hash(base), + hash(&base.replace("invariant i", "invariant j")) + ); +} From affab8d032bf49298bd201a398a6dc22561a664f Mon Sep 17 00:00:00 2001 From: Canitas <112231952+Sequela02@users.noreply.github.com> Date: Thu, 12 Nov 2026 21:00:42 -0700 Subject: [PATCH 8/9] fix: accept receipt 4 in the E2 materials and regenerate them The review materials check the receipt contract they read, and receipt 4 adds machine outcomes and a support list. For functions it changes only the review hash, so the cards and stage 7 packets differ in that line alone; regenerated with materials.py --write. Refs #82 --- .../e2-human-review/cards/review/R01.md | 2 +- .../e2-human-review/cards/review/R02.md | 2 +- .../e2-human-review/cards/review/R03.md | 2 +- .../e2-human-review/cards/review/R04.md | 2 +- .../e2-human-review/cards/review/R05.md | 2 +- .../e2-human-review/cards/review/R06.md | 2 +- .../e2-human-review/cards/review/R07.md | 2 +- .../e2-human-review/cards/review/R08.md | 2 +- .../e2-human-review/cards/review/R09.md | 2 +- .../e2-human-review/cards/review/R10.md | 2 +- .../e2-human-review/cards/review/R11.md | 2 +- .../e2-human-review/cards/review/R12.md | 2 +- .../e2-human-review/material-hashes.json | 30 +++++++++---------- docs/design/e2-human-review/materials.py | 2 +- docs/design/stage-7-review/cedar-packet.md | 8 ++--- docs/design/stage-7-review/gate-packet.md | 10 +++---- 16 files changed, 37 insertions(+), 37 deletions(-) diff --git a/docs/design/e2-human-review/cards/review/R01.md b/docs/design/e2-human-review/cards/review/R01.md index 489bffb..865c1ef 100644 --- a/docs/design/e2-human-review/cards/review/R01.md +++ b/docs/design/e2-human-review/cards/review/R01.md @@ -15,7 +15,7 @@ cannot reveal a defect, say not_observable. After the task, rate confidence ```text function fn gate_verdict(outcome: ProofOutcome, failure: Text, sent: List) -> GateVerdict -review_hash fdfd284e0a7491734d591a7781c17f19012b7eb2113bf722899de42d24832993 +review_hash 2461b8a438b074b7c1ee513e893247fcdfb04762875063555fe47045977dcbc5 type enum ProofOutcome { Passed, Failed, Vacuous, TimedOut, Cancelled, NotStarted } type enum GateVerdict { Proved, SendBack, NoProgress, Operator } intent gate_verdict (unchecked): Accept a passed proof; send a failed or vacuous proof back once per failure; identify repetition as no progress; ask the operator about interrupted or unstarted work. diff --git a/docs/design/e2-human-review/cards/review/R02.md b/docs/design/e2-human-review/cards/review/R02.md index 3f49b93..4ed8cd2 100644 --- a/docs/design/e2-human-review/cards/review/R02.md +++ b/docs/design/e2-human-review/cards/review/R02.md @@ -15,7 +15,7 @@ cannot reveal a defect, say not_observable. After the task, rate confidence ```text function fn gate_verdict(outcome: ProofOutcome, failure: Text, sent: List) -> GateVerdict -review_hash 3d732dfde5a9edd9a5335b9e1c89f09eab07358827eb1d8dca5e9a3cb9d74a89 +review_hash 917d611f031dbb0e8408def000f04afa0d99c5cc2ff8e6b1806d20f03d607715 type enum ProofOutcome { Passed, Failed, Vacuous, TimedOut, Cancelled, NotStarted } type enum GateVerdict { Proved, SendBack, NoProgress, Operator } intent gate_verdict (unchecked): Accept a passed proof; send a failed or vacuous proof back once per failure; identify repetition as no progress; ask the operator about interrupted or unstarted work. diff --git a/docs/design/e2-human-review/cards/review/R03.md b/docs/design/e2-human-review/cards/review/R03.md index ac2e9f9..cccee88 100644 --- a/docs/design/e2-human-review/cards/review/R03.md +++ b/docs/design/e2-human-review/cards/review/R03.md @@ -15,7 +15,7 @@ cannot reveal a defect, say not_observable. After the task, rate confidence ```text function fn gate_verdict(outcome: ProofOutcome, failure: Text, sent: List) -> GateVerdict -review_hash 326b51bc0df1d2f2fda0d7373ccb580cd82ffc6800a8a8848613488a6058da03 +review_hash 92fd60db96b323486f37c897aeb42667ef6710bae90e814cdb000b87c028ca38 type enum ProofOutcome { Passed, Failed, Vacuous, TimedOut, Cancelled, NotStarted } type enum GateVerdict { Proved, SendBack, NoProgress, Operator } intent gate_verdict (unchecked): Accept a passed proof; send a failed or vacuous proof back once per failure; identify repetition as no progress; ask the operator about interrupted or unstarted work. diff --git a/docs/design/e2-human-review/cards/review/R04.md b/docs/design/e2-human-review/cards/review/R04.md index 877668b..f24eef4 100644 --- a/docs/design/e2-human-review/cards/review/R04.md +++ b/docs/design/e2-human-review/cards/review/R04.md @@ -15,7 +15,7 @@ cannot reveal a defect, say not_observable. After the task, rate confidence ```text function fn gate_verdict(outcome: ProofOutcome, failure: Text, sent: List) -> GateVerdict -review_hash 7caa071502e2299c4256d9d3ee243d323b756f4f858c1b78f03f2f2b79a1c36e +review_hash f488b60f0eedda042f91e9a3bd149049b215e197b477d5987a6ad103a21b6afc type enum ProofOutcome { Passed, Failed, Vacuous, TimedOut, Cancelled, NotStarted } type enum GateVerdict { Proved, SendBack, NoProgress, Operator } intent gate_verdict (unchecked): Accept a passed proof; send a failed or vacuous proof back once per failure; identify repetition as no progress; ask the operator about interrupted or unstarted work. diff --git a/docs/design/e2-human-review/cards/review/R05.md b/docs/design/e2-human-review/cards/review/R05.md index aa2c6d4..acd2f9b 100644 --- a/docs/design/e2-human-review/cards/review/R05.md +++ b/docs/design/e2-human-review/cards/review/R05.md @@ -15,7 +15,7 @@ cannot reveal a defect, say not_observable. After the task, rate confidence ```text function fn gate_verdict(outcome: ProofOutcome, failure: Text, sent: List) -> GateVerdict -review_hash e405bb7be465f43f5332e4aee22485c6bec15a4b8a51141cb66f432375b27313 +review_hash e13f2d598f251750476bc54d1a88bb9bc91f364dbfdec4136f74fac7fdd92ae2 type enum ProofOutcome { Passed, Failed, Vacuous, TimedOut, Cancelled, NotStarted } type enum GateVerdict { Proved, SendBack, NoProgress, Operator } intent gate_verdict (unchecked): Accept a passed proof; send a failed or vacuous proof back once per failure; identify repetition as no progress; ask the operator about interrupted or unstarted work. diff --git a/docs/design/e2-human-review/cards/review/R06.md b/docs/design/e2-human-review/cards/review/R06.md index f11477a..ea93130 100644 --- a/docs/design/e2-human-review/cards/review/R06.md +++ b/docs/design/e2-human-review/cards/review/R06.md @@ -15,7 +15,7 @@ cannot reveal a defect, say not_observable. After the task, rate confidence ```text function fn gate_verdict(outcome: ProofOutcome, failure: Text, sent: List) -> GateVerdict -review_hash f876bf84bb543b220fb65ffd31894711dd72734a1362ec1d05fbca2332f57d5f +review_hash 8e5749f40db9010a0d4f3091e42076158a5bf09a6ef724fcd2552fbd2e8e4deb type enum ProofOutcome { Passed, Failed, Vacuous, TimedOut, Cancelled, NotStarted } type enum GateVerdict { Proved, SendBack, NoProgress, Operator } intent gate_verdict (unchecked): Accept a passed proof; send a failed or vacuous proof back once per failure; identify repetition as no progress; ask the operator about interrupted or unstarted work. diff --git a/docs/design/e2-human-review/cards/review/R07.md b/docs/design/e2-human-review/cards/review/R07.md index ab80fa3..0fbde27 100644 --- a/docs/design/e2-human-review/cards/review/R07.md +++ b/docs/design/e2-human-review/cards/review/R07.md @@ -22,7 +22,7 @@ see the retained [notice](../../../../../conformance/programs/cedar/NOTICE). ```text function fn partial_decision(satisfied_forbid: Bool, satisfied_permit: Bool, residual_permit: Bool, residual_forbid: Bool) -> PartialDecision -review_hash d66fe63f854832c9c261c0f770f5ba51f6b5b0813ea6d92a274bbc907a4b7c8a +review_hash 35aba8f24b4c178020592559fb1eed7d6fea416a4c92d4e584c33980d309837d type enum PartialDecision { Deny, Allow, Unknown } intent partial_decision (unchecked): Deny on a satisfied forbid or no possible permit; allow on a satisfied permit with no possible forbid; otherwise keep the decision unknown. specification line 15: ensures result == Deny implies satisfied_forbid or (not satisfied_permit and not residual_permit) diff --git a/docs/design/e2-human-review/cards/review/R08.md b/docs/design/e2-human-review/cards/review/R08.md index a5f7b40..d3bd027 100644 --- a/docs/design/e2-human-review/cards/review/R08.md +++ b/docs/design/e2-human-review/cards/review/R08.md @@ -22,7 +22,7 @@ see the retained [notice](../../../../../conformance/programs/cedar/NOTICE). ```text function fn partial_decision(satisfied_forbid: Bool, satisfied_permit: Bool, residual_permit: Bool, residual_forbid: Bool) -> PartialDecision -review_hash 4e1f8cf867a538b87b3a1a8a968eef9694dbfdb15bfccaaf9fb56137913f91e7 +review_hash f8ec174a35d8991437b8fc0938a7459f914d5aa33e90962c81d83526fcd9243e type enum PartialDecision { Deny, Allow, Unknown } intent partial_decision (unchecked): Deny on a satisfied forbid or no possible permit; allow on a satisfied permit with no possible forbid; otherwise keep the decision unknown. specification line 15: ensures result == Deny implies satisfied_forbid or (not satisfied_permit and not residual_permit) diff --git a/docs/design/e2-human-review/cards/review/R09.md b/docs/design/e2-human-review/cards/review/R09.md index 47aea59..e36b208 100644 --- a/docs/design/e2-human-review/cards/review/R09.md +++ b/docs/design/e2-human-review/cards/review/R09.md @@ -22,7 +22,7 @@ see the retained [notice](../../../../../conformance/programs/cedar/NOTICE). ```text function fn partial_decision(satisfied_forbid: Bool, satisfied_permit: Bool, residual_permit: Bool, residual_forbid: Bool) -> PartialDecision -review_hash 8c6e9f8c9ee82c2d0b229555d675a57f657c111216d42939a9394ea24d2b393d +review_hash cbfad03521d50cfcf9d8723275a2a7e73369e23f1e8eb5f61a3cf9832543a4e0 type enum PartialDecision { Deny, Allow, Unknown } intent partial_decision (unchecked): Deny on a satisfied forbid or no possible permit; allow on a satisfied permit with no possible forbid; otherwise keep the decision unknown. specification line 15: ensures result == Deny implies satisfied_forbid or (not satisfied_permit and not residual_permit) diff --git a/docs/design/e2-human-review/cards/review/R10.md b/docs/design/e2-human-review/cards/review/R10.md index fc5fd3e..b24512c 100644 --- a/docs/design/e2-human-review/cards/review/R10.md +++ b/docs/design/e2-human-review/cards/review/R10.md @@ -22,7 +22,7 @@ see the retained [notice](../../../../../conformance/programs/cedar/NOTICE). ```text function fn partial_decision(satisfied_forbid: Bool, satisfied_permit: Bool, residual_permit: Bool, residual_forbid: Bool) -> PartialDecision -review_hash 2aadfaa65e2d2af8c473a7786b474f9f8cc2c3dec122e4697711f1f7ec0daa64 +review_hash 23f2ebd5cdac908cca6debe686e9731fcff4a76f62d8a2a00bca76c34f6c1967 type enum PartialDecision { Deny, Allow, Unknown } intent partial_decision (unchecked): Deny on a satisfied forbid or no possible permit; allow on a satisfied permit with no possible forbid; otherwise keep the decision unknown. specification line 15: ensures result == Deny implies satisfied_forbid or (not satisfied_permit and not residual_permit) diff --git a/docs/design/e2-human-review/cards/review/R11.md b/docs/design/e2-human-review/cards/review/R11.md index b4dc635..8d287ca 100644 --- a/docs/design/e2-human-review/cards/review/R11.md +++ b/docs/design/e2-human-review/cards/review/R11.md @@ -22,7 +22,7 @@ see the retained [notice](../../../../../conformance/programs/cedar/NOTICE). ```text function fn partial_decision(satisfied_forbid: Bool, satisfied_permit: Bool, residual_permit: Bool, residual_forbid: Bool) -> PartialDecision -review_hash be785a9e01c46c7984c7ef50b1d45ed2b649344098a4bf67c9bd0e944a94dc71 +review_hash 950499771600f3245868a062ec63ea8a5114461cc9756ee6b20a027fa2fbf9bc type enum PartialDecision { Deny, Allow, Unknown } intent partial_decision (unchecked): Deny on a satisfied forbid or no possible permit; allow on a satisfied permit with no possible forbid; otherwise keep the decision unknown. specification line 15: requires satisfied_forbid or not satisfied_permit or not residual_forbid diff --git a/docs/design/e2-human-review/cards/review/R12.md b/docs/design/e2-human-review/cards/review/R12.md index c388099..ce198bc 100644 --- a/docs/design/e2-human-review/cards/review/R12.md +++ b/docs/design/e2-human-review/cards/review/R12.md @@ -22,7 +22,7 @@ see the retained [notice](../../../../../conformance/programs/cedar/NOTICE). ```text function fn partial_decision(satisfied_forbid: Bool, satisfied_permit: Bool, residual_permit: Bool, residual_forbid: Bool) -> PartialDecision -review_hash 627d8ed60741ff6d3142115f46d9539fdb96f2af72e982d6a9804f143b3b00cb +review_hash 909aef8f80e31953705108c9ed74be0df80ff5ecd5d60df7337a969c12361c6f type enum PartialDecision { Deny, Allow, Unknown } intent partial_decision (unchecked): Deny on a satisfied forbid or no possible permit; allow on a satisfied permit with no possible forbid; otherwise keep the decision unknown. specification line 15: ensures result == Deny implies satisfied_forbid or (not satisfied_permit and not residual_permit) diff --git a/docs/design/e2-human-review/material-hashes.json b/docs/design/e2-human-review/material-hashes.json index b0d6b4f..f83c939 100644 --- a/docs/design/e2-human-review/material-hashes.json +++ b/docs/design/e2-human-review/material-hashes.json @@ -1,6 +1,6 @@ { - "../stage-7-review/cedar-packet.md": "4a0652aa102f95daaa98aab859176442e7e4c91813eadaa008c45bcd516d6cad", - "../stage-7-review/gate-packet.md": "a1b138c200ff8b9abe9af7a3c8d31561439dbdc4e33ebab58cd23dec9f39de08", + "../stage-7-review/cedar-packet.md": "18617ebf09f10f08518f9e84810dbbd311b359237aafcc67a93d3eb516f515e0", + "../stage-7-review/gate-packet.md": "bdfe413109be5209cfc8e2563f8f875602a826177b83c3c6013db7669109d60f", "README.md": "df813d2abf5ddc8f7b56c971735e35866e19c1e0eff70329843a5f28afc87188", "allocation.csv": "bbf1978a19f09aba46adb2ac271379d89a5314a90c37d0ec69a61f285a80c28a", "answer-key.json": "75f3b6b74078aa34c199d1a2919ecc89ca7779ec1021e08372b8e773319821c2", @@ -16,18 +16,18 @@ "cards/code/R10.md": "0015e28a8137338529eb91d9916cf5381de50d338dbb6a879f3970a116aa903a", "cards/code/R11.md": "cbbc641cb67fb59cdf060fb2d65197ba988df62ed3284910d3b8f5c0466e492e", "cards/code/R12.md": "a0696adceadb9dccf05e51350051937ac77553879f3008f3963e7805b6c2dc4f", - "cards/review/R01.md": "2656ff2ea9667a5b462c4e19b71123dcb80631a3a32c0dc0fdd0cbe1c6143cba", - "cards/review/R02.md": "fbb9ad2c1a02dac2a4391593a30c1a7cf7f97f160ab476e915972cb628e2c70a", - "cards/review/R03.md": "4a31c14069639227f98bfb5ac242aa66f81a14d3e2db16676a7a9e85372afb09", - "cards/review/R04.md": "7e76182a1b1918d3e642ff60c98af03d5315ab43a9fdc1ce3e889208f6eb2853", - "cards/review/R05.md": "b3a14e13474f3b96e5efc213dba5857546913f4cb04049885ea3d82ae92a93c3", - "cards/review/R06.md": "4311b233684baa64e14432e3adc63453358bd1477be11e79e73ffd139b61b100", - "cards/review/R07.md": "5cb1775d7452a5af23b7137f7e24cec752601b0d1c45724e10c4f47075f009b0", - "cards/review/R08.md": "ca9dfeb01f0ee57b9e65bef32442a7020b0b2e85fb41823dc2ca7cb3944f3b6a", - "cards/review/R09.md": "81a4da13603c228fc4a95d4b1765b357d39aa11a15552140352891a0a4420f88", - "cards/review/R10.md": "ce13b625de4144ceb5b445ae5d28518b7836012f0309516f7be6d1445053ebbf", - "cards/review/R11.md": "eab4f9de3740874cee8cd667bfb2066a3ff000aec254f7445d95ea766c36f4c5", - "cards/review/R12.md": "c6f23d456154bce5cb6fba06cc91691c2b4a251a390985e15c76e97f0b364c51", + "cards/review/R01.md": "75278b8a4458d41b795a15089e38242628be172d51e30c89fc37246a552c6d8b", + "cards/review/R02.md": "df4c1d48609000ddbbaca96dfc729751c31bcf3c32252776209e57d0aecea5ba", + "cards/review/R03.md": "4ed35ab3b7eba67a87e1d91f61ad49648315df4a428fc0645fa0683234f74310", + "cards/review/R04.md": "5b80da4aba86a1b5b58ee42936ed678b28c01644b2a121feb5f35f3168c08ed8", + "cards/review/R05.md": "1f785ae4b262ff79495168257d1c9db09f2d9bf5bc5bda23453282f7da1a0df5", + "cards/review/R06.md": "194952078e9455cef7841ae84dd6522a70d2e8e68e635c0a2e7fc92d19a0b232", + "cards/review/R07.md": "fd5a3d674fae27b4a1594e69e2a5ca1ce675d72ab8c5105bbd8ec8c63a9a9348", + "cards/review/R08.md": "71ab9b7a13adee9c63c9808b030568f50996a8b848d135e3a1af5d0a5ea17453", + "cards/review/R09.md": "0df200dbbb389506630907306c35d271874b1bf85c1e35e6b9590c3671cc0047", + "cards/review/R10.md": "2c1ad83718e0d28934fc4d41cf5d3fbf8ccebfe052e2cc74fdb76b9cfc252ce4", + "cards/review/R11.md": "9864b6f72f211d2e68efd47fc37d01b0a39c20980f02b0df75f9c7ee38af1cd8", + "cards/review/R12.md": "b8634d2b8cc50147a197815864d9a994ece42c9755c1eed527d4cf7fbfd83489", "cards/specification/R01.md": "6f1c3ca283c7166a8115548fa43ee193d1578ca2ce40ee8e79545ae7dc257884", "cards/specification/R02.md": "6efc5b2a71bec9e40c64c6718548d275c41299b51a10bde7dcf27dab91e672d4", "cards/specification/R03.md": "5c80708ba02b31901784578dacd240cdec8869071f4ecdba2772dca78aa47e31", @@ -52,7 +52,7 @@ "corpus/R10.accord": "f5a8a9bb2aa5979107e4ea8f8e69b9dde2040d42104aa199332f64e48c89b778", "corpus/R11.accord": "3a0af93be2e7685cd8cd4701df21fdfc135610377c033951fb38f3dfb76524c6", "corpus/R12.accord": "c907371e24d6474d4d970e53b1fb0dcfb336dbc1845b9746ec8f344d861c4832", - "materials.py": "66d7fde27bf640630c601c07f34b910a9f5100e0d3941613f6d8bc3688425ff0", + "materials.py": "5166bf10f86e53756959714493b133ebb974b50d831e2fc8d9369a935e8686bd", "score.py": "cb0cc7c3b43fbdda746bc2aa9273fdd46140b4c6ec5cc61756bf3955830b25c0", "test_materials.py": "9b942a3fd9070bc105590683c065c516a0f1aacd578c5d0ecd5bb588db415b43", "test_score.py": "821dfd3b9469f73362a9236d2e4478317b24bd0e9f3fbead1e436cf9a93454c6" diff --git a/docs/design/e2-human-review/materials.py b/docs/design/e2-human-review/materials.py index 68b4c1b..5d65455 100644 --- a/docs/design/e2-human-review/materials.py +++ b/docs/design/e2-human-review/materials.py @@ -76,7 +76,7 @@ def check(binary, path): def validate_wire(report): - assert report["receipt"] == 3 and report["status"] == "checked", "unknown receipt contract" + assert report["receipt"] == 4 and report["status"] == "checked", "unknown receipt contract" for finding in report["diagnostics"]: assert finding["code"] in KNOWN_CODES, "unknown diagnostic code" assert report_pointer(report, finding["evidence"]) is not None diff --git a/docs/design/stage-7-review/cedar-packet.md b/docs/design/stage-7-review/cedar-packet.md index 8813f4b..eefcc4e 100644 --- a/docs/design/stage-7-review/cedar-packet.md +++ b/docs/design/stage-7-review/cedar-packet.md @@ -21,7 +21,7 @@ see the retained [notice](../../../conformance/programs/cedar/NOTICE). ```text function fn partial_decision(satisfied_forbid: Bool, satisfied_permit: Bool, residual_permit: Bool, residual_forbid: Bool) -> PartialDecision (partial-decision.accord) -review_hash f92c4f8f341c7109abc0d2edcdd42e85612146acefdf4304009015eaefc21524 +review_hash 06da101b3c338f0b2b1784ddd17ea155b9a4456d288f8a9805352a0cdbaf9b16 type enum PartialDecision { Deny, Allow, Unknown } intent partial_decision (partial-decision.accord) (unchecked): Deny on a satisfied forbid or no possible permit; allow on a satisfied permit with no possible forbid; otherwise keep the decision unknown. specification line 21: ensures result == Deny implies satisfied_forbid or (not satisfied_permit and not residual_permit) @@ -73,7 +73,7 @@ not_proved trusted_components: The parser, obligation generator, solvers, and not_proved mutation_sample: Only the reported finite sample of mutants was checked; contract adequacy is not proved. standing partial_decision (partial-decision.accord): verified function fn some_policy(effects: List, evaluations: List, effect: Effect, evaluation: Evaluation) -> Bool (policy-set.accord) -review_hash 78c42516fa1c4f4227b6bf67acaf7984771baa4c2bd5b82f0f02d788581aef48 +review_hash 0a3c4d258ad1d1064740079cf6f398272927e445edb3dedb1d4d702aba1545ae type enum Effect { Permit, Forbid } type enum Evaluation { Satisfied, NotSatisfied, Residual, Error } intent some_policy (policy-set.accord) (unchecked): Some policy with this effect evaluated to this result. @@ -98,7 +98,7 @@ not_proved admitted_domain: Guarantees apply only to inputs meeting requires; not_proved mutation_sample: Only the reported finite sample of mutants was checked; contract adequacy is not proved. standing some_policy (policy-set.accord): verified function fn partial_authorization(effects: List, evaluations: List) -> PartialDecision (policy-set.accord) -review_hash 8b4555fe76c23ef271ef357e8b7c55873f8eaba5bf7cbe3cb760bbf17095483d +review_hash 6541b4f751804a2c6ed9b06a892c27f03d41dbe864c8bd9795c60ce16c86e44c type enum Effect { Permit, Forbid } type enum Evaluation { Satisfied, NotSatisfied, Residual, Error } type enum PartialDecision { Deny, Allow, Unknown } @@ -147,7 +147,7 @@ not_proved admitted_domain: Guarantees apply only to inputs meeting requires; not_proved mutation_sample: Only the reported finite sample of mutants was checked; contract adequacy is not proved. standing partial_authorization (policy-set.accord): verified function fn is_authorized(effects: List, evaluations: List) -> Decision (policy-set.accord) -review_hash ae601e0acac29091dfce90213c371028cff96a666872cb9db8a67607c12c0b83 +review_hash 42bbbdd28ded7d48de17dfce6b82bd340c2342bf26440431e4975a1fe48f1510 type enum Effect { Permit, Forbid } type enum Evaluation { Satisfied, NotSatisfied, Residual, Error } type enum Decision { Allow, Deny } diff --git a/docs/design/stage-7-review/gate-packet.md b/docs/design/stage-7-review/gate-packet.md index c9552c3..20f4acb 100644 --- a/docs/design/stage-7-review/gate-packet.md +++ b/docs/design/stage-7-review/gate-packet.md @@ -17,7 +17,7 @@ program. Interaction: run the check and read its output. ```text function fn verification_required(changed: Bool, selected: Bool) -> Bool (gate-rule.accord) -review_hash 15e099c16280f33e77a4f2affd540a37559db8ae8beab8810edd1c8e62ec5c22 +review_hash 64ca67bdcea411dd153954ca9d7103ee83275143cc0418973c6b9b79f0b75ce1 intent verification_required (gate-rule.accord) (unchecked): Require verification after changed files or a selected design check. specification line 15: ensures result implies changed or selected specification line 16: ensures changed or selected implies result @@ -35,7 +35,7 @@ not_proved trusted_components: The parser, obligation generator, solvers, and not_proved mutation_sample: Only the reported finite sample of mutants was checked; contract adequacy is not proved. standing verification_required (gate-rule.accord): verified function fn tool_may_change_files(tool_name: Text, native_question: Bool, read_only: Bool) -> Bool (gate-rule.accord) -review_hash 471c5723a3aa7ff71a0b38acc6cbe66caf07f4c6c3640ae129111c083a8276ff +review_hash fea37f38e3dfd24d836d4855da5e1a3d865e23f2e8c2212493736f0c41983cc2 intent tool_may_change_files (gate-rule.accord) (unchecked): A started tool may change files unless it asks a native question, runs read-only, or is a trusted reader. specification line 24: ensures result implies not native_question and not read_only and not tool_name in ["read", "grep", "find", "ls", "update_tasks"] specification line 25: ensures not native_question and not read_only and not tool_name in ["read", "grep", "find", "ls", "update_tasks"] implies result @@ -52,7 +52,7 @@ not_proved trusted_components: The parser, obligation generator, solvers, and not_proved mutation_sample: Only the reported finite sample of mutants was checked; contract adequacy is not proved. standing tool_may_change_files (gate-rule.accord): verified function fn gate_verdict(outcome: ProofOutcome, failure: Text, sent: List) -> GateVerdict (gate-rule.accord) -review_hash f8b165984fbb9b1098890ef2750fef518aa567fc76dc1b0744db53c639dab040 +review_hash a849f2b1cbf2e06e44fbecaa391d2b2f566f7a265c7127325e40268bef911cd0 type enum ProofOutcome { Passed, Failed, Vacuous, TimedOut, Cancelled, NotStarted } type enum GateVerdict { Proved, SendBack, NoProgress, Operator } intent gate_verdict (gate-rule.accord) (unchecked): Accept a passed proof; send a failed or vacuous proof back once per failure; identify repetition as no progress; ask the operator about interrupted or unstarted work. @@ -97,7 +97,7 @@ not_proved list_assumptions: Every list is assumed to hold at most 4,294,967,2 not_proved mutation_sample: Only the reported finite sample of mutants was checked; contract adequacy is not proved. standing gate_verdict (gate-rule.accord): verified function fn command_verdict(outcome: ProofOutcome, failure: Text, sent: List, preexisting: Bool) -> GateVerdict (gate-rule.accord) -review_hash b817b9d7a08bd57e1e650a25298bfeadebe2f9acff622013d8f6685a1800d201 +review_hash 10298f85224a3905432b4faf4aa1bc194e2fc2a3da1adc4a0115dcca069a6fec type enum ProofOutcome { Passed, Failed, Vacuous, TimedOut, Cancelled, NotStarted } type enum GateVerdict { Proved, SendBack, NoProgress, Operator } intent command_verdict (gate-rule.accord) (unchecked): Treat an already present command failure as the operator's; otherwise accept passed proofs, send failures back once, and identify interrupted work or repetition. @@ -130,7 +130,7 @@ not_proved list_assumptions: Every list is assumed to hold at most 4,294,967,2 not_proved mutation_sample: Only the reported finite sample of mutants was checked; contract adequacy is not proved. standing command_verdict (gate-rule.accord): verified function fn keeps_working(verdicts: List) -> Bool (gate-rule.accord) -review_hash 33aa0944bb9a5f98fb05a3dec2dcb98aa1519361328c878b5abfddf9f027552a +review_hash 2da9f32342249cf57df44942fdb782f83bae335e8257fbc4ba9c3cf2ae3b1bf1 type enum GateVerdict { Proved, SendBack, NoProgress, Operator } intent keeps_working (gate-rule.accord) (unchecked): Continue while at least one verdict requests another attempt. specification line 65: ensures result implies SendBack in verdicts From 7047726d1f8db299fbf242c7622d0c975144092c Mon Sep 17 00:00:00 2001 From: Canitas <112231952+Sequela02@users.noreply.github.com> Date: Thu, 12 Nov 2026 21:05:36 -0700 Subject: [PATCH 9/9] fix: test the E2 wire contract against receipt 4 The wire test's known report still named receipt 3, which the contract now rejects; a stale bytecode cache hid it locally. Refs #82 --- docs/design/e2-human-review/material-hashes.json | 2 +- docs/design/e2-human-review/test_materials.py | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/design/e2-human-review/material-hashes.json b/docs/design/e2-human-review/material-hashes.json index f83c939..3db1432 100644 --- a/docs/design/e2-human-review/material-hashes.json +++ b/docs/design/e2-human-review/material-hashes.json @@ -54,6 +54,6 @@ "corpus/R12.accord": "c907371e24d6474d4d970e53b1fb0dcfb336dbc1845b9746ec8f344d861c4832", "materials.py": "5166bf10f86e53756959714493b133ebb974b50d831e2fc8d9369a935e8686bd", "score.py": "cb0cc7c3b43fbdda746bc2aa9273fdd46140b4c6ec5cc61756bf3955830b25c0", - "test_materials.py": "9b942a3fd9070bc105590683c065c516a0f1aacd578c5d0ecd5bb588db415b43", + "test_materials.py": "9c2c41f90278b3685b4d4480b5b87f23bdc58de4ad5561583cce5eadcb14a27c", "test_score.py": "821dfd3b9469f73362a9236d2e4478317b24bd0e9f3fbead1e436cf9a93454c6" } diff --git a/docs/design/e2-human-review/test_materials.py b/docs/design/e2-human-review/test_materials.py index d932eef..efeaee3 100644 --- a/docs/design/e2-human-review/test_materials.py +++ b/docs/design/e2-human-review/test_materials.py @@ -6,7 +6,7 @@ class WireTests(unittest.TestCase): def setUp(self): - self.report = dict(receipt=3, status="checked", definitions=[], diagnostics=[dict(code="ACC0012", evidence="/definitions")]) + self.report = dict(receipt=4, status="checked", definitions=[], diagnostics=[dict(code="ACC0012", evidence="/definitions")]) def test_known_wire_contract_has_resolvable_evidence(self): materials.validate_wire(self.report)