feat(Boole): nat/pos as first-class types with UF+axiom SMT encoding#6
Open
kondylidou wants to merge 27 commits into
Open
feat(Boole): nat/pos as first-class types with UF+axiom SMT encoding#6kondylidou wants to merge 27 commits into
kondylidou wants to merge 27 commits into
Conversation
kondylidou
marked this pull request as draft
July 8, 2026 15:22
Add `StrataBoole.Nat` — a reusable binary algebraic nat library built on the new `define-fun-rec` infrastructure in Strata Core: - `pos` / `nat` algebraic datatypes (Coq-style binary positives) - `pos.toInt` via structural recursion (@[cases]) → define-fun-rec - `pos.fromInt` via int-valued recursion (decreases x) → define-fun-rec; replaces the previous opaque UF + 3 axioms formulation - `nat.toInt` / `nat.fromInt` as non-recursive wrappers - Three bridge axioms kept as E-matching hints - Full arithmetic operator surface (add/sub/mul/div/mod/lt/le/gt/ge) - `Strata.BooleNat.prepend` helper to inject the library into any program Add `StrataBooleTest/nat_binary_datatype.lean` with Options A (unary), B (binary inline), and C (via natLibrary); 38 VCs all pass including 4 new termination obligations for `pos.fromInt`. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Adds test_sat_exists_sum and test_sat_lt to Option B — both satisfiable but not universally true. cvc5 returns unknown (expected: the three bridge axioms are universally quantified and block concrete model search). Locked in via #guard_msgs as regression documentation. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
define-fun-rec gives no observable difference through Strata's current verify interface — both approaches return unknown for SAT queries. The algebraic datatype is the actual fix; the Strata PR is being closed. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
After `import StrataBoole.Nat`, every `#strata program Boole;` block automatically has pos, nat, nat.toInt, nat.fromInt, bridge axioms, and arithmetic operators in scope — no explicit declarations needed. Changes: - StrataBoole/Nat.lean: add `import StrataDDM.Integration.Lean.HashCommands` and `#register_preamble Boole Strata.BooleNat.natLibrary` to register the binary-nat library as the Boole dialect preamble. - StrataBooleTest/nat_binary_datatype.lean: remove `import StrataBoole.Nat` (Options A/B declare their own nat, which would conflict with the preamble); remove Option C (moved to nat_native.lean). Update obligation IDs. - StrataBooleTest/nat_motivation.lean: remove `import StrataBoole.Nat` so unary/binary examples aren't shadowed by the preamble. Update obligation IDs. - StrataBooleTest/nat_native.lean: new test demonstrating preamble injection — procedures use nat/pos without declarations; also verifies natLibrary directly. - StrataBooleTest.lean: add nat_native import. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
When the incremental SMT solver returns `unknown (some m)` for a nat-using obligation, evaluate the obligation expression against the candidate model with pure-Lean nat arithmetic. If evaluation yields a concrete Boolean, promote `unknown (some m)` to `.sat m`. Adds `LeanPos`/`LeanNat` mirror types (deriving Inhabited so `partial` compiles), a two-pass SMT-term parser (`termToLeanPos`/`termToLeanNat`), and a purely structural evaluator (`evalExpr`) that uses `EvalVal.VPartial` for curried binary operators — avoiding the kernel-rejected non-positive occurrence that `VFn : (EvalVal → Option EvalVal) → EvalVal` would create. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
The proposal specifies `requires nat.toInt(b) <= nat.toInt(a)` for nat.sub, which generates a proof obligation at every call site. The previous implementation silently saturated to N0 when b > a (Lean's Nat.sub semantics), which is a semantic deviation from the proposal. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
The batch-mode candidate-model fix (SMTUtils: parse get-value output on unknown) lives on kondylidou/Strata until the PR is merged to strata-org/Strata main. Switch back to the org git+rev once merged. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Add nat validate-candidate phase: - EvalVal.VPartial replaces VFn (avoids non-positive occurrence) - evalExpr handles curried binary ops via VPartial - natCandidatePhase promotes unknown(some model) → sat when evalExpr succeeds - Pass natBridgeAxioms to Core.verify as requeryDropAxioms so unknown obligations are re-queried without bridge axioms to expose counterexamples - nat.sub changed to requires-guard precondition (nat.toInt(b) <= nat.toInt(a)) Also update lake-manifest.json to pin Strata fork branch fix/batch-unknown-candidate-model (batch unknown model parsing + requeryDropAxioms). Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Two features completing the proposal's counterexample workflow: 1. Model display (Task 1): add lExprToLeanNat/lExprToLeanPos decoders for LExpr constructor terms, plus decodeModel post-processing in verify so that candidate counterexamples show e.g. `b = 2` instead of `b = Npos(xO(xH))`. 2. Counterexample battery (Task 2): add nat_counterexample.lean with two tests covering the SAT direction — a simple false claim and a constrained sum — both now produce `❌ fail` with concrete nat models. 3. Validation fix: evalExpr now accepts an ANF definition map built from the path-condition varDecl entries, so that ANF intermediates like `$__anf.2 = nat_toInt(a) < nat_toInt(b)` are expanded before evaluation. Without this, validateNatModel always returned false (the obligation was an opaque ANF variable absent from the solver model). 4. Core fix (in fork): dischargeObligationIncremental was querying boolean assumption IDs instead of actual user-typed variables; fixed to build SMT terms from vars + typedVarToSMTFn + estate.ufs. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
…ttery - coreProgUsesNatOrPos now scans .type (.data block) declarations so that user-defined datatypes with nat-typed constructor fields (e.g. NatList) correctly trigger natLibrary injection; previously only funcs/procs were checked, causing "Undefined type 'nat'" at TypeFactory validation - validateNatModel now also checks that no ground path-condition assumption evaluates to false against the candidate; rejects broken partial assignments from timed-out solver sessions (e.g. candidate a=N0 contradicts requires toInt(a)=73) so they don't surface as spurious counterexamples - nat_counterexample: update test 2 (constrained sum) expected output to ❓ unknown and document the conservative-soundness reason - nat_counterexample_extended: new test file with 4 additional tests: range constraint (❌ fail), IntList head-zero (❌ fail), nonlinear mul (✅ pass), and NatList with nat-typed constructor fields (✅ pass, 13 obligations) Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
evalUnaryOp: add pos.fromInt → VPos case; previously expressions calling pos.fromInt in path conditions produced VPartial, silently accepting inconsistent candidates. evalBinaryOp nat.sub: guard precondition (toInt(b) <= toInt(a)); previously underflowing subtraction clamped to N0 via natFromInt, promoting candidates that violate nat.sub's requires as valid counterexamples. evalExpr .eq: return none (not Some false) on type mismatch; the old catch-all `_, _ => false` caused groundAssumptionsHold to reject genuine counterexamples when one operand evaluated to VPartial. evalExpr .fvar: erase defMap key before recursing to break circular definitions x ↦ fvar x that would otherwise loop indefinitely. validateNatModel obligationOk: require VBool result, not just isSome; VPartial (partially-applied operator) is not a usable evaluation result. decodeEntry: try lExprToLeanPos after lExprToLeanNat fails so that pos-typed model variables are decoded to integers, not left as raw constructor terms. verify: cache coreProgUsesNatOrPos result to avoid traversing the program twice (once for injection guard, once for usesGrammarNat). Nat.lean: correct three comment blocks that falsely claimed pos.toInt and pos.fromInt are emitted as define-fun-rec; they are UF + per-constructor axioms in the current Strata encoder. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
…ogUsesNatOrPos Previously, a procedure with `var z : nat := ...` in the body but no nat/pos in its header signature would silently skip natLibrary injection, causing a compilation error. Now stmtListHasNatOrPos recursively checks Cmd.init type annotations across structured statement lists (including nested ite/block/loop bodies), covering deviation 4 from the proposal. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
- evalBinaryOp: add nat.div / nat.mod arms (silent accept on zero divisor) - validateNatModel obligationOk: tighten VBool _ → VBool false so P=true does not count as a counterexample - lExprUsesNatOrPos: new helper scans operator ids and sub-expressions - coreProgUsesNatOrPos: scan function/recFuncBlock bodies and proc spec preconditions/postconditions via lExprUsesNatOrPos - usesGrammarNat: remove !hasUserNatDecl guard so prepend-based programs still get natCandidatePhase and natBridgeAxioms - decodeModel: guard with usesGrammarNat (maybeDecodeModel) to skip the nat model decode pass when no nat types are in use Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Points to feat/def-fun-rec commit that fixes the re-query axiom existence check: guard now reads axiom names from program.decls (the original input) instead of oblProgram.decls (which never has .ax declarations after toCoreProofObligationProgram strips them). Resolves the false warning "none of [nat_nonneg, ...] matched any axiom declaration" that was preventing the re-query from running for nat_sum_prog. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Three correctness fixes to the nat/pos detection pass and one manifest bump: 1. lExprUsesNatOrPos: add .abs and .quant cases so nat ops inside quantifier bodies (forall n : nat ::) and lambda expressions are not invisible to natLibrary injection. 2. stmtListHasNatOrPos: scan assert/assume/cover/set expression content, not just local variable type annotations. Procedure bodies that assert nat arithmetic were silently skipping natLibrary injection. 3. lake-manifest.json / lakefile.toml: bump Strata dependency to feat/def-fun-rec @ c4833a31 which fixes the re-query pass to actually strip bridge axiom assume statements from obligation procedure bodies before the axiom-free re-query. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
stmtListHasNatOrPos was silently dropping nat ops in: - .ite condition (ExprOrNondet .det e) - .loop guard, termination measure, and invariant expressions - .funcDecl body, axioms, and measure lExprUsesNatOrPos was already complete after the previous commit (.abs and .quant added); the nine LExpr constructors are now all handled with no unintended wildcard falls. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
… tests Add `nat_axiom_battery` to `nat_native.lean` (6 procedures covering round-trip 2, add/sub correctness, ground literal, monotonicity, and toInt-injectivity) and a new `nat_detection.lean` with 3 regression tests for the detection code paths fixed on this branch: * `test_ite_cond` — nat ops appear only in an ite condition, exercising the `.ite (.det c)` case added to `stmtListHasNatOrPos` * `test_loop_inv` — nat ops appear only in a while-loop invariant, exercising the `.loop _ _ invs body` case * `test_spec_quant` — nat ops appear only in a spec-ensures quantifier body, exercising the `.quant _ _ _ _ tr b` case added to `lExprUsesNatOrPos` If any of these detection fixes is reverted, the corresponding test fails because natLibrary is not injected and the `nat` sort is undefined in the SMT encoding. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Drop unused `dummy : int` from `test_literal` and `test_ite_cond`, and
remove the tautological `assert 0 <= dummy || 0 > dummy` body (with its
accompanying `dummy` parameter) from `test_spec_quant`, replacing it with
an empty body `{}`. Update all downstream obligation IDs that shifted as
a result.
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
kondylidou
force-pushed
the
nat-binary-datatype
branch
from
July 16, 2026 12:46
7a5b9b1 to
74c4fc5
Compare
Two upstream breaking changes required porting: 1. All Core grammar ops (`command_*`, `varStatement`, `initStatement`, `assign`, `assume`, `assert`, `cover`, `if_statement`, `havoc_statement`, `while_statement`, `call_statement`, `block_statement`, `exit_statement`, `typeDecl_statement`, `funcDecl_statement`, `command_cfg_procedure`, `command_typedecl`, `command_typesynonym`, `command_constdecl`, `command_fndecl`, `command_fndef`, `command_recfndefs`, `command_axiom`, `command_distinct`, `command_datatypes`) gained a leading `annots : Option MetadataAnn` parameter. All pattern matches in Verify.lean extended with a leading `_` wildcard. The `assert`/`cover` reachCheck field was replaced by annots; drop the now-invalid reachCheck metadata injection. 2. StrataDDM `@[noExponent]` arg-level format marker (needed by Strata/DL/SMT/DDMTransform/Parse.lean) and parenthesization of arrow types in type applications require StrataDDM >= 4ea13cd. Bump lake-manifest accordingly; update one guard_msgs docstring in stack_array_based.lean where ite-in-implication now prints with surrounding parens. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
kondylidou
changed the title
kondylidou
marked this pull request as ready for review
July 16, 2026 13:56
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.
Adds
natandposas built-in Boole types. No imports or declarationsrequired — every
#strata program Boole;block has them in scope automatically.The binary-nat algebraic datatype (
poswith constructorsxH/xO/xI,natwithN0/Npos) is emitted as SMTdeclare-datatypeswith a recursivepos.toIntdefinition and bridge axioms (nat_nonneg,nat_fromInt_toInt,nat_toInt_fromInt). The library is injected automatically whencoreProgUsesNatOrPosdetects nat or pos anywhere in the program — procedureheaders, spec clauses, ite conditions, loop invariants, or quantifier bodies.
Nat operations (
nat_toInt,nat_fromInt,nat_add,nat_sub,nat_mul,nat_lt,nat_le) are available as surface-syntax operators in all Booleprograms.
Changes
StrataBoole/Grammar.lean— nat/pos type categories and operator surfacesyntax
StrataBoole/Nat.lean— natLibrary SMT preamble (algebraic datatypes +bridge axioms)
StrataBoole/Verify.lean—coreProgUsesNatOrPosdetection; natLibraryinjection; port of all Core grammar pattern matches to the new
annots : Option MetadataAnnleading field (upstream breaking change)StrataBooleTest/nat_native.lean— axiom-coverage battery (round-trip,add, sub, literal, monotonicity, injectivity)
StrataBooleTest/nat_counterexample.lean,nat_counterexample_extended.lean— counterexample display andvalidation tests
StrataBooleTest/nat_detection.lean— regression tests for ite-condition,loop-invariant, and spec-quantifier detection paths
lakefile.toml+lake-manifest.json— Strata dependency updated tofeat/nat-binary-datatype