feat: compound boolean asserts in invariants (#101)#134
Merged
Conversation
Extend the invariant assertion language with `&&`, `||`, parentheses,
and `!` negation, so safety properties can span multiple boolean gates
in a single expression (e.g. `migrations_ok && typecheck_ok && unit_tests_ok`).
Previously invariants could only check single-field assertions, forcing
authors to replicate the condition as per-transition guards — which catch
illegal transitions but not illegal states reached by any other path.
Changes:
- `temper-spec/assert_parser`: rewrite as recursive-descent tokenizer +
parser; add `ParsedAssert::BoolRequired{var,expect}`, `And`, `Or`.
- `temper-runtime/sim_handler` + `sim_actor_system`: add matching
`SpecAssert::BoolRequired/And/Or` variants with recursive evaluation;
add `SimActorHandler::bool_field(var)` accessor.
- `temper-server/entity_actor/sim_handler`: map new `ParsedAssert`
variants; expose booleans via the trait method.
- `temper-verify`: add `InvariantKind::And/Or`, update `BoolRequired`
to carry `expect`, factor evaluators into recursive helpers across
proptest_gen, simulation, stateright_impl, and smt. Compound
expressions referencing undeclared booleans fall back to Unverifiable
so model checking continues to behave safely.
- SMT induction for `And` is sound via per-part check; `Or` defers to
runtime/simulation (joint encoding out of scope for this PR).
26 parser tests + 3 compound invariant tests pass. Full workspace
`cargo build` is clean; temper-spec/temper-runtime/temper-server/
temper-verify lib tests all green.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Resolves #101.
Summary
&&,||, parens, and!negationmigrations_ok && typecheck_ok && unit_tests_oknow works as a single-expression invariant, so safety properties spanning N gates no longer have to be replicated as per-transition guardsDetails
crates/temper-spec/src/automaton/assert_parser.rs) rewritten as recursive-descent tokenizer + parser; addsParsedAssert::BoolRequired{var,expect},And(Vec),Or(Vec)temper-runtime/scheduler/{sim_handler,sim_actor_system}) adds matchingSpecAssertvariants and a recursiveevaluate_spec_asserthelper; newSimActorHandler::bool_field(var)trait accessortemper-server/entity_actor/sim_handler) translates newParsedAssertvariants and exposes booleanstemper-verify) addsInvariantKind::And/Or, updatesBoolRequiredto carryexpect, recursively evaluates acrossproptest_gen,simulation,stateright_impl, andsmtUnverifiableso model checking stays safeAndsound via per-part check;Ordefers to runtime (joint encoding out of scope)Test plan
cargo test -p temper-spec— 194 pass (26 parser tests including compound coverage)cargo test -p temper-runtime --lib— 92 passcargo test -p temper-server --lib— 226 passcargo test -p temper-verify --lib— 76 pass + 3 new compound testscargo buildcleancode-revieweragent findings — all green with low-severity follow-ups)🤖 Generated with Claude Code