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-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-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-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-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..6bec224 --- /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 { + value: i32, + } + + init near_top() { + next { value: 2147483645 } + } + + event increment() + { + next { value: value + 1 } + } + + invariant non_negative: value >= 0 +} 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-overflow.accord b/conformance/cases/machine-overflow.accord new file mode 100644 index 0000000..bae5d9d --- /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 { + value: i32, + } + + init near_top() { + next { value: 2147483645 } + } + + event increment() + requires value < 2147483647 + { + next { value: value + 1 } + } + + invariant non_negative: value >= 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-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 +} 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 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.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/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..60fa2e8 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,8 @@ pub(crate) fn report( reused, clause: o.clause, line: o.line, + exploration: None, + parameters: Vec::new(), }); } } @@ -171,11 +184,13 @@ pub(crate) fn report( standing = Standing::Incomplete; } Definition { + kind: DefinitionKind::Function, + support: Vec::new(), 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 +227,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..967f42b --- /dev/null +++ b/crates/accord/src/evidence/machine.rs @@ -0,0 +1,365 @@ +//! 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, false, 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, false, 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 { .. }); + // What the explorer turned into another outcome isn't the ledger's. + let reused = reused + && !matches!( + outcome, + Outcome::NotInductive { .. } | Outcome::Undecided { .. } + ); + ( + 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, + parameters: units[m].source.params.clone(), + }); + } + } + 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() + .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, + 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..b5872e7 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,8 @@ mod tests { key: String::new(), definition: String::new(), reused: false, + exploration: None, + parameters: Vec::new(), } } @@ -125,10 +128,12 @@ mod tests { let definitions: Vec = standings .iter() .map(|&standing| Definition { + kind: crate::DefinitionKind::Function, + support: Vec::new(), 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..6fe749d --- /dev/null +++ b/crates/accord/src/explore.rs @@ -0,0 +1,461 @@ +//! 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> { + 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), + &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 = 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() + .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 = Some(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..adf607e 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); @@ -154,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/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..a132e78 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,20 @@ fn reproduces( assumed, }; Ok(match &obligation.claim { + Claim::Allowed => true, + Claim::Invariants => { + // A step whose arithmetic leaves its type ends in no state; its + // own obligation reports that. + let code = Env { + mode: Mode::Code, + ..env + }; + 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)?; let with_result = Env { @@ -91,6 +105,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..7bd06bf 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,13 @@ 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, + /// 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. @@ -200,23 +251,49 @@ 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)>, + /// 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. @@ -283,16 +360,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..dcc415c 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; @@ -35,10 +35,12 @@ 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::{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 +142,59 @@ 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"))); + } + // 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 { + 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, + "", + &fits, + &[], + 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..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 @@ -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 { @@ -174,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/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..a133da1 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}; @@ -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}), }; @@ -64,34 +64,62 @@ 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.params)), + }) + }) + .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, "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 }), + 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, 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 })) @@ -101,6 +129,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 +153,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 }), @@ -125,9 +170,9 @@ fn openness_json(openness: &Openness, definition: &Definition) -> Value { code, } => 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), + "inputs": inputs_json(inputs, &definition.params), + "results": [result_typed(&results.0, definition), result_typed(&results.1, definition)], + "implementation": result_typed(code, definition), } }), Openness::Undecided { reason } => json!({ "undecided": reason }), @@ -146,9 +191,9 @@ fn strength_json(strength: &Strength, definition: &Definition) -> Value { .iter() .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), + "inputs": inputs_json(&s.inputs, &definition.params), + "original": result_typed(&s.original, definition), + "mutant": result_typed(&s.mutant, definition), })) .collect::>(), }) @@ -178,14 +223,15 @@ 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::>(), + "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, "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..6c64862 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); @@ -170,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 7af4ff5..098c760 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,11 +213,18 @@ 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)] 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, @@ -233,6 +246,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 +280,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 +368,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..0ae0225 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") { @@ -107,13 +111,26 @@ impl Parser<'_> { let expr = self.expr()?; clauses.push(Clause { kind, + helper: false, expr, text, 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 +147,7 @@ impl Parser<'_> { ret, clauses, body, + machine: None, }) } @@ -183,7 +201,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 +225,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/machines.rs b/crates/accord/src/syntax/machines.rs new file mode 100644 index 0000000..4bfce74 --- /dev/null +++ b/crates/accord/src/syntax/machines.rs @@ -0,0 +1,210 @@ +//! 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; + let mut names: Vec = Vec::new(); + 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") { + 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`", + ); + } + } + 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<(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")?; + let name = self.name()?; + self.expect_sym(":")?; + 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`. + 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..09c747e 100644 --- a/crates/accord/src/syntax/parser.rs +++ b/crates/accord/src/syntax/parser.rs @@ -150,7 +150,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 +163,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/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 new file mode 100644 index 0000000..1d7e132 --- /dev/null +++ b/crates/accord/tests/machines.rs @@ -0,0 +1,210 @@ +//! 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); +} + +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"); +} + +#[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")) + ); +} 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/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..3db1432 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,8 +52,8 @@ "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_materials.py": "9c2c41f90278b3685b4d4480b5b87f23bdc58de4ad5561583cce5eadcb14a27c", "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/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) 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 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..2b6f8f6 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,35 @@ 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 | +| `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 | @@ -88,11 +88,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 +104,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. @@ -110,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: @@ -189,6 +226,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 +243,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