From b61b560e9862d67a3242e25b08e3bf29a43af1ff Mon Sep 17 00:00:00 2001 From: Yash Mehta Date: Mon, 28 Sep 2026 21:22:15 -0400 Subject: [PATCH 1/2] Lower =~= on sequences to equal length and in-bounds equality. --- StrataBoole/Verify.lean | 15 +- .../FeatureRequests/map_extensionality.lean | 33 +++- docs/BooleFeatureRequests.md | 187 ++++++++++-------- 3 files changed, 146 insertions(+), 89 deletions(-) diff --git a/StrataBoole/Verify.lean b/StrataBoole/Verify.lean index d477641..d4a363d 100644 --- a/StrataBoole/Verify.lean +++ b/StrataBoole/Verify.lean @@ -348,8 +348,21 @@ private def toCoreExtensionalEq let rhs := mkCoreApp Core.mapSelectOp [b, idx] let trigger := lhs return .quant () .all "" (some keyTy') trigger (.eq () lhs rhs) + | .Sequence _ _ => + let lenEq := .eq () (mkCoreApp Core.seqLengthOp [a]) (mkCoreApp Core.seqLengthOp [b]) + let idx : Core.Expression.Expr := .bvar () 0 + let a := Lambda.LExpr.liftBVars 1 a + let b := Lambda.LExpr.liftBVars 1 b + let lhs := mkCoreApp Core.seqSelectUnsafeOp [a, idx] + let rhs := mkCoreApp Core.seqSelectUnsafeOp [b, idx] + let inBounds := mkCoreApp Core.boolAndOp [ + mkCoreApp Core.intLeOp [.intConst () 0, idx], + mkCoreApp Core.intLtOp [idx, mkCoreApp Core.seqLengthOp [a]]] + let body := mkCoreApp Core.boolImpliesOp [inBounds, .eq () lhs rhs] + let trigger := lhs + return mkCoreApp Core.boolAndOp [lenEq, .quant () .all "" (some .int) trigger body] | _ => - throwAt m s!"Extensional equality is currently only supported for Map types, got: {repr ty}" + throwAt m s!"Extensional equality is currently only supported for Map and Sequence types, got: {repr ty}" private def oldifyExpr (inoutNames : List String) : Core.Expression.Expr → Core.Expression.Expr | .fvar m ident ty => diff --git a/StrataBooleTest/FeatureRequests/map_extensionality.lean b/StrataBooleTest/FeatureRequests/map_extensionality.lean index 421d3a2..3443c07 100644 --- a/StrataBooleTest/FeatureRequests/map_extensionality.lean +++ b/StrataBooleTest/FeatureRequests/map_extensionality.lean @@ -18,7 +18,7 @@ Near-upstream anchors from `differential_status.md`: - Original gap: extensional equality lowered to ordinary equality - Current status: implemented for direct `Map` types via Boole `=~=` - Lowering: `a =~= b` becomes `∀ i . a[i] == b[i]` -- Remaining gap: named map synonyms and non-map extensional equality +- Remaining gap: named map synonyms and higher-order extensional equality -/ private def mapExtensionalitySeed : StrataDDM.Program := @@ -39,11 +39,11 @@ spec { #end /-- info: -Obligation: assert_2_983 +Obligation: assert_2_988 Property: assert Result: ✅ pass -Obligation: map_extensionality_seed_ensures_1_960 +Obligation: map_extensionality_seed_ensures_1_965 Property: assert Result: ✅ pass-/ #guard_msgs in @@ -116,3 +116,30 @@ private def expectedQuantifiedMapExtensionalityCapture : Core.Expression.Expr := (.quant () .all "" (some .int) lhs (.eq () lhs rhs))) #guard loweredQuantifiedMapExtensionalityCapture? == some expectedQuantifiedMapExtensionalityCapture + +/- +For any element type `T` and any sequences `a` and `b`, `a =~= b` exactly when +they have equal length and in-bounds pointwise equality via `Sequence.select!`. +-/ + +private def seqExtensionalitySeed : StrataDDM.Program := +#strata +program Boole; + +procedure seq_ext_spec(a: Sequence T, b: Sequence T) returns () +spec { + ensures (a =~= b) <==> + (Sequence.length(a) == Sequence.length(b) && + (∀ i: int . 0 <= i && i < Sequence.length(a) ==> + Sequence.select!(a, i) == Sequence.select!(b, i))); +} +{ +}; +#end + +/-- info: +Obligation: seq_ext_spec_ensures_0_3992 +Property: assert +Result: ✅ pass-/ +#guard_msgs in +#eval Strata.Boole.verify "cvc5" seqExtensionalitySeed (options := .quiet) diff --git a/docs/BooleFeatureRequests.md b/docs/BooleFeatureRequests.md index 501442c..2c1e602 100644 --- a/docs/BooleFeatureRequests.md +++ b/docs/BooleFeatureRequests.md @@ -1,159 +1,176 @@ # Boole Feature Request Inventory This document tracks the selected Boole feature-request seeds. Most seeds live in -[`StrataBooleTest/FeatureRequests/`](../StrataBooleTest/FeatureRequests), including +`[StrataBooleTest/FeatureRequests/](../StrataBooleTest/FeatureRequests)`, including several that are now fully implemented; a few have moved to -[`StrataBooleTest/`](../StrataBooleTest/). +`[StrataBooleTest/](../StrataBooleTest/)`. ## Implemented feature requests - **Extensional equality** (#684) - - `a =~= b` lowers to `∀ i : k . a[i] == b[i]`. - - Remaining gaps: named map synonyms, sequences, higher-order extensionality. + - On `Map k v`, `a =~= b` lowers to `∀ i : k . a[i] == b[i]`. + - On `Sequence T`, `a =~= b` lowers to equal length and `∀ i : int . 0 <= i && i < Sequence.length(a) ⇒ Sequence.select!(a, i) == Sequence.select!(b, i)`. + - Remaining gaps: named map synonyms, higher-order extensionality. + - Benchmark: `[map_extensionality.lean](../StrataBooleTest/FeatureRequests/map_extensionality.lean)`. - **Array axiomatization as standalone SMT-IR pass** (#795) - Post-encoding pass rewrites Array-theory SMT-IR to `Map` sorts with read-over-write axioms (generated only for type pairs used); fixes type-mismatch bug for datatypes with `Map` fields. - Remaining Boole-syntax gaps for `[T; N]`: see Gap #15. -- **Nested `for`-loop lowering** (range-style: `for i in 0..N`) +- **Nested** `for`**-loop lowering** (range-style: `for i in 0..N`) - Fresh Core block labels prevent inner loops from shadowing the enclosing `"for"` label; loop elimination havocs only loop-carried variables. - - Benchmark: [`square_matrix_multiply.lean`](../StrataBooleTest/square_matrix_multiply.lean). + - Benchmark: `[square_matrix_multiply.lean](../StrataBooleTest/square_matrix_multiply.lean)`. - Note: covers `for i in 0..N` range loops only. Iterator-based `for x in iter.iter()` is a separate gap (#23). - **Bitvector loop variables** (`for i : bvN := init to limit`) - `for_to_by` and `for_downto_by` dispatch guard/step/increment to `Bv{N}.ULe/Add/Sub` when the loop variable is a bitvector type instead of `int`. - - Benchmark: [`sha256_compact_indexed.lean`](../StrataBooleTest/FeatureRequests/sha256_compact_indexed.lean). + - Benchmark: `[sha256_compact_indexed.lean](../StrataBooleTest/FeatureRequests/sha256_compact_indexed.lean)`. - **Early return** (#871) - `exit functionName;` exits the labeled Core block wrapping the procedure body, acting as an early return. - - Benchmark: [`early_return.lean`](../StrataBooleTest/FeatureRequests/early_return.lean). -- **Bitwise operators on `bvN` types** (#970) + - Benchmark: `[early_return.lean](../StrataBooleTest/FeatureRequests/early_return.lean)`. +- **Bitwise operators on** `bvN` **types** (#970) - `&`, `|`, `^`, `>>` (UShr), `>>s` (SShr), `<<`, `~` lower to `Bv{N}.And/Or/Xor/UShr/SShr/Shl/Not` Core ops. - `bvWidth` helper extracts the bit-width from the Boole type and dispatches to the right-sized op. - - Benchmark: [`bitvector_ops.lean`](../StrataBooleTest/FeatureRequests/bitvector_ops.lean) (X25519 scalar clamping with `bv8` `&` and `|`). + - Benchmark: `[bitvector_ops.lean](../StrataBooleTest/FeatureRequests/bitvector_ops.lean)` (X25519 scalar clamping with `bv8` `&` and `|`). - **Bitvector comparisons** (#1075) - Unsigned (`<`, `<=`, `>`, `>=`) lower to `Bv{N}.ULt/ULe/UGt/UGe` via `toBvCmpOp` (plain comparisons on bitvector operands default to unsigned). - Signed (`s`, `>=s`) lower to `Bv{N}.SLt/SLe/SGt/SGe`. - - Benchmark: [`bitvector_ops.lean`](../StrataBooleTest/FeatureRequests/bitvector_ops.lean). + - Benchmark: `[bitvector_ops.lean](../StrataBooleTest/FeatureRequests/bitvector_ops.lean)`. - **Mutual recursion** (#599, #1167) - `rec function ... ;` blocks work for structural recursion over datatypes and for `int`-typed functions with `decreases`. - Remaining gap: int-recursive functions are opaque UFs — functional properties (e.g. `even(1) == false`) cannot be proved without unfolding axioms. Blocked by Gap #1 (`opaque`/`reveal`). - - Benchmark: [`mutual_recursion.lean`](../StrataBooleTest/FeatureRequests/mutual_recursion.lean). -- **`choose` (Hilbert ε)** + - Benchmark: `[mutual_recursion.lean](../StrataBooleTest/FeatureRequests/mutual_recursion.lean)`. +- `choose` **(Hilbert ε)** - Statement form: `w := ε z : T . pred(z)` desugars to `assert ∃ z : T . pred(z); havoc w; assume pred[z/w]`. - The existence assertion guards soundness: without it, an unsatisfiable `pred` silently becomes `assume false`, making every downstream obligation a false positive. - Function form (Strata-Boole #4): `function f(params) : R := ε z . pred(z, params)` declares an uninterpreted `f` with the axiom `∀ params, ∀ z, z = f(params) → pred(z, params)`. - Remaining gap: the function form has no existence guard. Its axiom is sound only if `pred` is satisfiable for every parameter value; otherwise the context becomes inconsistent. Callers must supply that guarantee, e.g. with `requires ∃ z . pred(z, params)`. - - Benchmark: [`choose_operator.lean`](../StrataBooleTest/FeatureRequests/choose_operator.lean). -- **`decreases` annotation on functions, procedures, and `for` loops** + - Benchmark: `[choose_operator.lean](../StrataBooleTest/FeatureRequests/choose_operator.lean)`. +- `decreases` **annotation on functions, procedures, and** `for` **loops** - Parsing/forwarding implemented (#1075): accepted in function preconds, `spec {}` blocks, procedure headers, and `for v := init to/downto limit` loops; the `for`-loop measure is forwarded to the Core while-loop measure field and actively verified. - `decreases` on functions (structural): termination verification implemented (#1092). - `decreases ` on `rec function`: implemented (#1167). Non-negativity and strict-decrease obligations generated at each call site. Int-recursive functions are pure UFs in SMT — functional properties (e.g. `even(1) == false`) cannot be proved without unfolding axioms; blocked by Gap #1. - `decreases` on procedures: `decr : Option Measure` parameter on `boole_procedure`, reusing Core's existing `Measure` category; currently parsed and silently dropped. - - Benchmark: [`decreases_metadata.lean`](../StrataBooleTest/FeatureRequests/decreases_metadata.lean). -- **`Sequence T` type and slicing ops** + - Benchmark: `[decreases_metadata.lean](../StrataBooleTest/FeatureRequests/decreases_metadata.lean)`. +- `Sequence T` **type and slicing ops** - All 8 Core inherited ops wired up; wrappers added for `Sequence.skip`, `Sequence.dropFirst`, `Sequence.subrange`. - Typed empty-sequence constants: `Sequence.empty_bv8/bv16/bv32/bv64/int`. Each needs a distinct token — 0-ary polymorphic `Sequence.empty` has no arguments to infer the type from. - Recursive spec functions over sequences: `decreases Sequence.length(s)` supported (#1167); `reconstruct` seed now active. - Sequence literals: `Sequence.of_bv8/bv16/bv32/bv64/int[v0, …, vn]` lower to a left fold of `Sequence.build` over the typed empty constant. The empty literal `Sequence.of_[]` keeps its element type (#1214). - - Benchmarks: [`seq_slicing.lean`](../StrataBooleTest/FeatureRequests/seq_slicing.lean), [`seq_empty_literal.lean`](../StrataBooleTest/FeatureRequests/seq_empty_literal.lean). -- **Inline `let`-block postconditions** + - Benchmarks: `[seq_slicing.lean](../StrataBooleTest/FeatureRequests/seq_slicing.lean)`, `[seq_empty_literal.lean](../StrataBooleTest/FeatureRequests/seq_empty_literal.lean)`. +- **Inline** `let`**-block postconditions** - `ensures ({ let x = e; ... })` now lowers correctly; enables dalek-lite's `mul_clamped` postcondition style. - - Benchmark: [`embedded_postcondition.lean`](../StrataBooleTest/embedded_postcondition.lean). + - Benchmark: `[embedded_postcondition.lean](../StrataBooleTest/embedded_postcondition.lean)`. - **Lambda abstraction and application** - `fun x : T => body` lowers to nested Core `.abs` nodes; `(f)(x)` lowers to `.app () f x`. - Remaining gap: first-class function values as procedure parameters / local variables still need abstract-type encoding for the SMT path. - - Benchmark: [`lambda_closure.lean`](../StrataBooleTest/FeatureRequests/lambda_closure.lean). + - Benchmark: `[lambda_closure.lean](../StrataBooleTest/FeatureRequests/lambda_closure.lean)`. - **SMT-LIB 2.7 cast operators** (`e as_int`, `e as_sint`, `e as_bv{n}`) (Gap #6) - `e as_int` → `Bv{n}.ToUInt` → SMT-LIB 2.7 `ubv_to_int` (unsigned); widths 1/8/16/32/64/128. - `e as_sint` → `Bv{n}.ToInt` → SMT-LIB 2.7 `sbv_to_int` (signed); widths 1/8/16/32/64/128. - `e as_bv{n}` → `Int.ToBv{n}` → SMT-LIB 2.7 `(_ int_to_bv n)` (truncating mod 2^n); widths 1/8/16/32/64/128. - - Benchmarks: [`cast_expr.lean`](../StrataBooleTest/cast_expr.lean), [`widening_casts.lean`](../StrataBooleTest/widening_casts.lean), [`cast_all_directions.lean`](../StrataBooleTest/cast_all_directions.lean), [`cast_nested.lean`](../StrataBooleTest/cast_nested.lean). -- **Native `nat`** (Gap #8; Strata-Boole #10, #14; Strata #1439) + - Benchmarks: `[cast_expr.lean](../StrataBooleTest/cast_expr.lean)`, `[widening_casts.lean](../StrataBooleTest/widening_casts.lean)`, `[cast_all_directions.lean](../StrataBooleTest/cast_all_directions.lean)`, `[cast_nested.lean](../StrataBooleTest/cast_nested.lean)`. +- **Native** `nat` (Gap #8; Strata-Boole #10, #14; Strata #1439) - `nat` and `pos` are grammar-level types; `nat_toInt`, `nat_fromInt`, `nat_add/sub/mul/div/mod`, `nat_lt/le/gt/ge` are in scope in every Boole program. - Encoding: binary datatypes `pos` (`xH`, `xO`, `xI`) and `nat` (`N0`, `Npos`), built programmatically (`natCorePreamble`, `Verify.lean`) and injected only when a program uses `nat`/`pos`. `StrataBoole/Nat.lean` is the readable spec, not used by the implementation. - `nat.toInt`, `nat.fromInt` and the operators have no bodies and are defined by axioms. Bodies were inlined as SMT macros, which forced a case split at every `nat.toInt` use and a `fromInt(toInt …)` round trip at every `+`; on dalek `sum_of_slice` 3 obligations timed out. With axioms it verifies 43/43. - Counterexamples: `natCandidatePhase` validates cvc5's candidate model and promotes it to `❌ fail`. - Gap: `pos.toInt`/`pos.fromInt` are UF + axioms, not `define-fun-rec`, so cvc5 cannot evaluate them during model search and some false obligations return `❓ unknown` (sound, no model). `nat_counterexample.lean` Test 2. Fix, both parts needed: the encoder's `define-fun-rec` opt-in (Strata #1478) and a re-query of the unknown obligation without axioms that uses it (Strata-Boole follow-up). - - Benchmarks: [`nat_native.lean`](../StrataBooleTest/nat_native.lean), [`nat_detection.lean`](../StrataBooleTest/nat_detection.lean), [`nat_counterexample.lean`](../StrataBooleTest/nat_counterexample.lean), [`nat_counterexample_extended.lean`](../StrataBooleTest/nat_counterexample_extended.lean). + - Benchmarks: `[nat_native.lean](../StrataBooleTest/nat_native.lean)`, `[nat_detection.lean](../StrataBooleTest/nat_detection.lean)`, `[nat_counterexample.lean](../StrataBooleTest/nat_counterexample.lean)`, `[nat_counterexample_extended.lean](../StrataBooleTest/nat_counterexample_extended.lean)`. + + ## Semantic preservation requests -1. **Generic `opaque` / `reveal`**: Lower priority. Preserve reveals for generic spec functions instead of dropping them. Also blocks functional reasoning about int-recursive functions: without unfolding axioms, `even` and `odd` are opaque UFs and concrete values like `even(1) == false` cannot be proved. The fix is to auto-emit defining equations as SMT assertions (bounded by a trigger) when `decreases` is present — the same mechanism as Dafny's `reveal` and Verus's `reveal_with_fuel`. See [`mutual_recursion.lean`](../StrataBooleTest/FeatureRequests/mutual_recursion.lean) for a concrete example. -2. **`hide`**: Lower priority. Emit a real hiding boundary so a revealed body does not stay globally visible. -3. **`reveal_with_fuel`**: Lower priority. Preserve the requested fuel amount instead of lowering it to an unrestricted reveal. -4. **`closed` visibility**: Lower priority. Keep closed spec-function bodies hidden across module boundaries. +1. **Generic** `opaque` **/** `reveal`: Lower priority. Preserve reveals for generic spec functions instead of dropping them. Also blocks functional reasoning about int-recursive functions: without unfolding axioms, `even` and `odd` are opaque UFs and concrete values like `even(1) == false` cannot be proved. The fix is to auto-emit defining equations as SMT assertions (bounded by a trigger) when `decreases` is present — the same mechanism as Dafny's `reveal` and Verus's `reveal_with_fuel`. See `[mutual_recursion.lean](../StrataBooleTest/FeatureRequests/mutual_recursion.lean)` for a concrete example. +2. `hide`: Lower priority. Emit a real hiding boundary so a revealed body does not stay globally visible. +3. `reveal_with_fuel`: Lower priority. Preserve the requested fuel amount instead of lowering it to an unrestricted reveal. +4. `closed` **visibility**: Lower priority. Keep closed spec-function bodies hidden across module boundaries. 5. **Overflow guards**: Lower priority. Preserve `HasType`-style arithmetic overflow checks if Verus-specific guards are worth modeling directly. 6. **SMT-LIB 2.7 cast operators** (`as_int`, `as_sint`, `as_bv{n}`): Implemented. -7. **`decreases` metadata**: Implemented. +7. `decreases` **metadata**: Implemented. + + ## Type/model requests -8. **Native `nat` support**: Implemented (#10, #14). Remaining: some false obligations return `❓ unknown` instead of a counterexample (see the entry above). -9. **Missing model types**: Add or standardize support for model types such as `Cell`, `Atomic`, `Thread`, `Rwlock`, `Unit`, and `Arithmetic_overflow`. -10. **On-demand stdlib/pervasive stubs**: Some pervasive stubs may be droppable after pruning translation output. -11. **Sequence slicing**: Implemented. Int-based termination for recursive seq functions: implemented (#1167). -12. **Generic/category typing cleanup**: Reduce `nat`/`int`/bitvector width mismatches and generic type-shape mismatches in the type-checker. -13. **Struct/record types with named field access**: `type T := { f1: A, f2: B }` declarations, `.field` accessor expressions, struct literal construction, and quantification over fixed-size field arrays (e.g. `∀ i < 5 . fe.limbs[i] < 2^51`). Used in every dalek spec function. -14. **`Option` in spec functions**: Native `Option` return type so fallible spec functions can be represented faithfully; currently encoded as `is_some` flag plus component functions. Every Vest parser returns `Option<(int, T)>`. -15. **Fixed-size array `[T; N]` syntax** (#795): SMT backend resolved by PR #795. Remaining Boole-syntax gaps: - - **Repeat initializer `[expr; N]`**: `[0u32; 16]` — lower to a constant-valued Map. - - **Array literal `[x, y, z, ...]`**: `K32: [u32; 64] = [0x428a2f98, ...]` — compact literal syntax. - - **Mutable write-back `arr[i] = v`**: `block[i % 16] = new_w` — lower to `Map.put`. +1. **Native** `nat` **support**: Implemented (#10, #14). Remaining: some false obligations return `❓ unknown` instead of a counterexample (see the entry above). +2. **Missing model types**: Add or standardize support for model types such as `Cell`, `Atomic`, `Thread`, `Rwlock`, `Unit`, and `Arithmetic_overflow`. +3. **On-demand stdlib/pervasive stubs**: Some pervasive stubs may be droppable after pruning translation output. +4. **Sequence slicing**: Implemented. Int-based termination for recursive seq functions: implemented (#1167). +5. **Generic/category typing cleanup**: Reduce `nat`/`int`/bitvector width mismatches and generic type-shape mismatches in the type-checker. +6. **Struct/record types with named field access**: `type T := { f1: A, f2: B }` declarations, `.field` accessor expressions, struct literal construction, and quantification over fixed-size field arrays (e.g. `∀ i < 5 . fe.limbs[i] < 2^51`). Used in every dalek spec function. +7. `Option` **in spec functions**: Native `Option` return type so fallible spec functions can be represented faithfully; currently encoded as `is_some` flag plus component functions. Every Vest parser returns `Option<(int, T)>`. +8. **Fixed-size array** `[T; N]` **syntax** (#795): SMT backend resolved by PR #795. Remaining Boole-syntax gaps: + - **Repeat initializer** `[expr; N]`: `[0u32; 16]` — lower to a constant-valued Map. + - **Array literal** `[x, y, z, ...]`: `K32: [u32; 64] = [0x428a2f98, ...]` — compact literal syntax. + - **Mutable write-back** `arr[i] = v`: `block[i % 16] = new_w` — lower to `Map.put`. - Note: `FieldElement51.limbs: [u64; 5]` handled by Gap #13, not this gap. - Confirmed in sha256: `[u32; 64]`, `[u32; 16]`, `[u8; 64]`, `[0u32; 16]`, `K32: [u32; 64] = [...]`. -16. **Slice types and slice indexing**: `&[T]` and `&[T; N]` — length, indexing, sub-slicing. Distinct from sequence slicing (#11): slices are runtime-sized Rust borrows. Confirmed in sha256: `blocks: &[[u8; 64]]`, `blocks[k]`, `to_u32s(&blocks[k])`. +9. **Slice types and slice indexing**: `&[T]` and `&[T; N]` — length, indexing, sub-slicing. Distinct from sequence slicing (#11): slices are runtime-sized Rust borrows. Confirmed in sha256: `blocks: &[[u8; 64]]`, `blocks[k]`, `to_u32s(&blocks[k])`. + + ## Expressiveness requests -17. **Higher-order / lambda / closure support**: Implemented. Remaining gap: first-class function values as procedure parameters or local variables. -18. **`choose`**: Implemented, as a statement and as a function declaration. Remaining gap: the function form has no existence guard. -19. **Mutual recursion / forward references**: Implemented for datatypes (#599) and `int` (#1167). Remaining gap: functional reasoning about int-recursive functions blocked by Gap #1 (unfolding axioms). -20. **Trait-spec symbol resolution**: Preserve trait-spec symbols across module boundaries. -21. **Trait / interface with spec and proof methods**: `interface` declarations bundling `spec function` and `lemma` members, with `matches` pattern syntax in `ensures` and `external_body`-style trusted bodies. Confirmed as the backbone of Vest combinators. -22. **Reusable math spec support**: `pow2`, summation, and modular arithmetic helpers for functional specs; avoids re-axiomatising arithmetic in each seed. -23. **Rust iterator protocol lowering** (`for x in iter.iter()`): Leaves symbols undefined — `Iter_Traits_Iterator_Iterator_next`, `Pervasive_ghost_decrease/invariant`, `Std_specs_Slice_spec_slice_iter`, `Option_option..isOption_option_Some`; loop locals `VERUS_iter/exec_iter/ghost_iter`. Distinct from `for i in 0..N` (implemented). Confirmed in sha256: `for block in blocks.iter()`. +1. **Higher-order / lambda / closure support**: Implemented. Remaining gap: first-class function values as procedure parameters or local variables. +2. `choose`: Implemented, as a statement and as a function declaration. Remaining gap: the function form has no existence guard. +3. **Mutual recursion / forward references**: Implemented for datatypes (#599) and `int` (#1167). Remaining gap: functional reasoning about int-recursive functions blocked by Gap #1 (unfolding axioms). +4. **Trait-spec symbol resolution**: Preserve trait-spec symbols across module boundaries. +5. **Trait / interface with spec and proof methods**: `interface` declarations bundling `spec function` and `lemma` members, with `matches` pattern syntax in `ensures` and `external_body`-style trusted bodies. Confirmed as the backbone of Vest combinators. +6. **Reusable math spec support**: `pow2`, summation, and modular arithmetic helpers for functional specs; avoids re-axiomatising arithmetic in each seed. +7. **Rust iterator protocol lowering** (`for x in iter.iter()`): Leaves symbols undefined — `Iter_Traits_Iterator_Iterator_next`, `Pervasive_ghost_decrease/invariant`, `Std_specs_Slice_spec_slice_iter`, `Option_option..isOption_option_Some`; loop locals `VERUS_iter/exec_iter/ghost_iter`. Distinct from `for i in 0..N` (implemented). Confirmed in sha256: `for block in blocks.iter()`. + + ## Robustness requests -24. **Datatype constructor/selector verification robustness**: Improve solver/type-checker handling for richer datatype VCs that are already emitted faithfully. The small selector/constructor seed passes; the remaining issue is larger datatype examples whose generated VCs still fail. -25. **Complex recursive type shapes**: Support more nested recursive datatype shapes during type-checking. -26. **Non-Boole SST artifacts**: Decide whether `RevealString` / `Air`-style statements need first-class treatment or an explicit erase/lower policy. +1. **Datatype constructor/selector verification robustness**: Improve solver/type-checker handling for richer datatype VCs that are already emitted faithfully. The small selector/constructor seed passes; the remaining issue is larger datatype examples whose generated VCs still fail. +2. **Complex recursive type shapes**: Support more nested recursive datatype shapes during type-checking. +3. **Non-Boole SST artifacts**: Decide whether `RevealString` / `Air`-style statements need first-class treatment or an explicit erase/lower policy. + + ## Bitvector requests -27. **`by (bit_vector)` proof mode**: Route pure bitvector sub-goals to a bitvector decision procedure automatically. Confirmed in Vest LEB128 (`assert(...) by (bit_vector)`). -28. **`bv` rotate_left / rotate_right as primitives**: Currently emitted as `(x >> n) | (x << (w - n))` with `requires 1 <= n < w`; SMT-LIB 2 has native ops. Confirmed in sha256: `rotate_right` with n ∈ {2, 6, 7, 11, 13, 17, 18, 19, 22, 25}. +1. `by (bit_vector)` **proof mode**: Route pure bitvector sub-goals to a bitvector decision procedure automatically. Confirmed in Vest LEB128 (`assert(...) by (bit_vector)`). +2. `bv` **rotate_left / rotate_right as primitives**: Currently emitted as `(x >> n) | (x << (w - n))` with `requires 1 <= n < w`; SMT-LIB 2 has native ops. Confirmed in sha256: `rotate_right` with n ∈ {2, 6, 7, 11, 13, 17, 18, 19, 22, 25}. + + ## Boole seed examples The table below tracks all seeds regardless of location. -| Definition | Primary request(s) | Source | Current status | -| --- | --- | --- | --- | -| [`datatypes_and_selectors.lean`](../StrataBooleTest/FeatureRequests/datatypes_and_selectors.lean) | Datatype constructor/selector robustness (#24) | Verus `guide/datatypes`, `adts`; VLIR `rec_adt_structural` | Basic seed passes; richer cases still active | -| [`abstract_types_and_stubs.lean`](../StrataBooleTest/FeatureRequests/abstract_types_and_stubs.lean) | Missing model types (#9), stdlib/pervasive stubs (#10) | Verus `guide/quants`, `broadcast_proof`, `guide/higher_order_fns` | Active; `Sequence` lowering now implemented; primary gaps: Thread, Cell, Rwlock model types and pervasive stubs | -| [`nat_int_boundary.lean`](../StrataBooleTest/FeatureRequests/nat_int_boundary.lean) | Native `nat` (#8), widening coercions (#6) | Verus `quantifiers`, `guide/integers`, `power_of_2`; VLIR `rec_adt_structural` | Implemented; seed still uses an abstract `nat` with explicit coercions — port to native `nat` open | -| [`nat_native.lean`](../StrataBooleTest/nat_native.lean) | Native `nat` (#8) | Grammar-level `nat`/`pos` operator surface; counterexample battery in `nat_counterexample*.lean` | Implemented; counterexample gap as above | -| [`map_extensionality.lean`](../StrataBooleTest/FeatureRequests/map_extensionality.lean) | Extensional equality | Verus `guide/ext_equal` | Implemented (#684, #795); named synonyms and non-map types still open | -| [`overflow_guard.lean`](../StrataBooleTest/FeatureRequests/overflow_guard.lean) | Overflow guards (#5) | Verus `guide/overflow`, `overflow` | Lower priority | -| [`opaque_reveal_hide.lean`](../StrataBooleTest/FeatureRequests/opaque_reveal_hide.lean) | `opaque`/`reveal` (#1), `hide` (#2), `closed` (#4) | Verus `generics`, `test_expand_errors`, `debug_expand`, `modules` | Lower priority | -| [`reveal_with_fuel.lean`](../StrataBooleTest/FeatureRequests/reveal_with_fuel.lean) | `reveal_with_fuel` (#3) | Verus `test_expand_errors`, `recursion` | Lower priority | -| [`early_return.lean`](../StrataBooleTest/FeatureRequests/early_return.lean) | Early return | Verus SST `return` translation gap from `differential_status.md` | Implemented (#871) | -| [`widening_casts.lean`](../StrataBooleTest/widening_casts.lean) | SMT-LIB 2.7 cast operators (#6) | Verus `guide/integers`, `quantifiers`, `statements` | Implemented | -| [`cast_expr.lean`](../StrataBooleTest/cast_expr.lean) | SMT-LIB 2.7 cast operators (#6) | dalek-lite `scalar.rs` B2/B5 | Implemented | -| [`cast_all_directions.lean`](../StrataBooleTest/cast_all_directions.lean) | SMT-LIB 2.7 cast operators (#6) | All three cast directions | Implemented | -| [`cast_nested.lean`](../StrataBooleTest/cast_nested.lean) | SMT-LIB 2.7 cast operators (#6), `decreases` preservation (#7) | dalek-lite `bytes_seq_as_nat` / `seq_as_nat_52` (B2) | Implemented | -| [`choose_operator.lean`](../StrataBooleTest/FeatureRequests/choose_operator.lean) | `choose` (#18) | Verus `trigger_loops` (`choose_example`, `quantifier_example`) | Implemented (#1075; function form: Strata-Boole #4); function form has no existence guard | -| [`higher_order_encoding.lean`](../StrataBooleTest/FeatureRequests/higher_order_encoding.lean) | Higher-order values (#17) | Verus `fun_ext`, `trait_for_fn` | Active | -| [`lambda_closure.lean`](../StrataBooleTest/FeatureRequests/lambda_closure.lean) | Lambda / closure (#17) | Local reduced Rust/Verus-style lambda example | Implemented (#1075); remaining gap: first-class function values as procedure parameters/variables | -| [`mutual_recursion.lean`](../StrataBooleTest/FeatureRequests/mutual_recursion.lean) | Mutual recursion (#19) | Verus `guide/recursion`; VLIR `mutual_recursion`, `recursion` | Implemented for datatypes (#599) and `int` (#1167); functional reasoning blocked by Gap #1 (unfolding axioms) | -| [`decreases_metadata.lean`](../StrataBooleTest/FeatureRequests/decreases_metadata.lean) | `decreases` preservation (#7) | Verus `proposal-rw2022`, `rw2022_script`, `recursion`; VLIR `LoopSimpleWithSpec` | Implemented (#1092, #1167); procedure `decreases` parsed, silently dropped | -| [`horner_poly_eval.lean`](../StrataBooleTest/FeatureRequests/horner_poly_eval.lean) | Reusable math spec (#22) | CLRS Horner’s rule, Exercise 2.3 | Type-checks; full math spec still open | -| [`embedded_postcondition.lean`](../StrataBooleTest/embedded_postcondition.lean) | Inline `let`-binding blocks in `ensures` clauses | dalek-lite `montgomery.rs` `mul_clamped`, `mul_bits_be` | Implemented (#1075) | -| [`montgomery_loop_invariant.lean`](../StrataBooleTest/FeatureRequests/montgomery_loop_invariant.lean) | Relational loop invariants over two co-evolving variables | dalek-lite `montgomery.rs` `mul_bits_be` (Montgomery ladder) | Linear arithmetic case: implemented (#1075); elliptic curve case: open — requires group-law axioms (Costello-Smith 2017, eq. 4); whether cvc5 closes the invariant with those axioms is untested | -| [`bitvector_ops.lean`](../StrataBooleTest/FeatureRequests/bitvector_ops.lean) | Bitwise operators on `bvN` types | dalek-lite `scalar_specs.rs` | Implemented (#970) | -| [`bitvector_proof_mode.lean`](../StrataBooleTest/FeatureRequests/bitvector_proof_mode.lean) | `by (bit_vector)` proof mode (#27) | VeruSAGE-Bench Vest `leb128` | Active | -| [`seq_slicing.lean`](../StrataBooleTest/FeatureRequests/seq_slicing.lean) | Sequence slicing (#11) | dalek-lite `scalar_specs.rs`, `core_specs.rs`; Vest `leb128`, `repetition` | Implemented (#1075, #1167) | -| [`seq_empty_literal.lean`](../StrataBooleTest/FeatureRequests/seq_empty_literal.lean) | Sequence literals (#11): typed empty literal | Regression for `Sequence.of_[]` losing its element type | Implemented (#1214) | -| [`scalar_reduce.lean`](../StrataBooleTest/FeatureRequests/scalar_reduce.lean) | `reduce()` spec axiom for B2 (`Scalar::from_bytes_mod_order_wide`) | dalek-lite `scalar.rs` | Implemented (#1075) | -| [`struct_field_access.lean`](../StrataBooleTest/FeatureRequests/struct_field_access.lean) | Struct/record field access (#13) | dalek-lite `field_specs.rs`, `edwards_specs.rs` | Active | -| [`trait_spec_methods.lean`](../StrataBooleTest/FeatureRequests/trait_spec_methods.lean) | Trait / interface with spec methods (#21) | VeruSAGE-Bench Vest `SecureSpecCombinator` | Active | -| [`option_matches.lean`](../StrataBooleTest/FeatureRequests/option_matches.lean) | `Option` in spec functions (#14) | VeruSAGE-Bench Vest `SecureSpecCombinator`, `leb128` | Active | -| [`sha256_compact_indexed.lean`](../StrataBooleTest/FeatureRequests/sha256_compact_indexed.lean) | Iterator protocol lowering (#23), array syntax (#15), slice types (#16), `bv` rotate primitives (#28) | RustCrypto SHA-256 compact port (indexed `Sequence` encoding) | Active — all 17 VCs pass (#1075); open gaps: iterator protocol (#23), array syntax (#15), slice types (#16) | + +| Definition | Primary request(s) | Source | Current status | +| ----------------------------------------------------------------------------------------------------- | ----------------------------------------------------------------------------------------------------- | ------------------------------------------------------------------------------------------------ | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ | +| `[datatypes_and_selectors.lean](../StrataBooleTest/FeatureRequests/datatypes_and_selectors.lean)` | Datatype constructor/selector robustness (#24) | Verus `guide/datatypes`, `adts`; VLIR `rec_adt_structural` | Basic seed passes; richer cases still active | +| `[abstract_types_and_stubs.lean](../StrataBooleTest/FeatureRequests/abstract_types_and_stubs.lean)` | Missing model types (#9), stdlib/pervasive stubs (#10) | Verus `guide/quants`, `broadcast_proof`, `guide/higher_order_fns` | Active; `Sequence` lowering now implemented; primary gaps: Thread, Cell, Rwlock model types and pervasive stubs | +| `[nat_int_boundary.lean](../StrataBooleTest/FeatureRequests/nat_int_boundary.lean)` | Native `nat` (#8), widening coercions (#6) | Verus `quantifiers`, `guide/integers`, `power_of_2`; VLIR `rec_adt_structural` | Implemented; seed still uses an abstract `nat` with explicit coercions — port to native `nat` open | +| `[nat_native.lean](../StrataBooleTest/nat_native.lean)` | Native `nat` (#8) | Grammar-level `nat`/`pos` operator surface; counterexample battery in `nat_counterexample*.lean` | Implemented; counterexample gap as above | +| `[map_extensionality.lean](../StrataBooleTest/FeatureRequests/map_extensionality.lean)` | Extensional equality | Verus `guide/ext_equal` | Maps (#684, #795) and sequences implemented; named synonyms and higher-order extensionality still open | +| `[overflow_guard.lean](../StrataBooleTest/FeatureRequests/overflow_guard.lean)` | Overflow guards (#5) | Verus `guide/overflow`, `overflow` | Lower priority | +| `[opaque_reveal_hide.lean](../StrataBooleTest/FeatureRequests/opaque_reveal_hide.lean)` | `opaque`/`reveal` (#1), `hide` (#2), `closed` (#4) | Verus `generics`, `test_expand_errors`, `debug_expand`, `modules` | Lower priority | +| `[reveal_with_fuel.lean](../StrataBooleTest/FeatureRequests/reveal_with_fuel.lean)` | `reveal_with_fuel` (#3) | Verus `test_expand_errors`, `recursion` | Lower priority | +| `[early_return.lean](../StrataBooleTest/FeatureRequests/early_return.lean)` | Early return | Verus SST `return` translation gap from `differential_status.md` | Implemented (#871) | +| `[widening_casts.lean](../StrataBooleTest/widening_casts.lean)` | SMT-LIB 2.7 cast operators (#6) | Verus `guide/integers`, `quantifiers`, `statements` | Implemented | +| `[cast_expr.lean](../StrataBooleTest/cast_expr.lean)` | SMT-LIB 2.7 cast operators (#6) | dalek-lite `scalar.rs` B2/B5 | Implemented | +| `[cast_all_directions.lean](../StrataBooleTest/cast_all_directions.lean)` | SMT-LIB 2.7 cast operators (#6) | All three cast directions | Implemented | +| `[cast_nested.lean](../StrataBooleTest/cast_nested.lean)` | SMT-LIB 2.7 cast operators (#6), `decreases` preservation (#7) | dalek-lite `bytes_seq_as_nat` / `seq_as_nat_52` (B2) | Implemented | +| `[choose_operator.lean](../StrataBooleTest/FeatureRequests/choose_operator.lean)` | `choose` (#18) | Verus `trigger_loops` (`choose_example`, `quantifier_example`) | Implemented (#1075; function form: Strata-Boole #4); function form has no existence guard | +| `[higher_order_encoding.lean](../StrataBooleTest/FeatureRequests/higher_order_encoding.lean)` | Higher-order values (#17) | Verus `fun_ext`, `trait_for_fn` | Active | +| `[lambda_closure.lean](../StrataBooleTest/FeatureRequests/lambda_closure.lean)` | Lambda / closure (#17) | Local reduced Rust/Verus-style lambda example | Implemented (#1075); remaining gap: first-class function values as procedure parameters/variables | +| `[mutual_recursion.lean](../StrataBooleTest/FeatureRequests/mutual_recursion.lean)` | Mutual recursion (#19) | Verus `guide/recursion`; VLIR `mutual_recursion`, `recursion` | Implemented for datatypes (#599) and `int` (#1167); functional reasoning blocked by Gap #1 (unfolding axioms) | +| `[decreases_metadata.lean](../StrataBooleTest/FeatureRequests/decreases_metadata.lean)` | `decreases` preservation (#7) | Verus `proposal-rw2022`, `rw2022_script`, `recursion`; VLIR `LoopSimpleWithSpec` | Implemented (#1092, #1167); procedure `decreases` parsed, silently dropped | +| `[horner_poly_eval.lean](../StrataBooleTest/FeatureRequests/horner_poly_eval.lean)` | Reusable math spec (#22) | CLRS Horner’s rule, Exercise 2.3 | Type-checks; full math spec still open | +| `[embedded_postcondition.lean](../StrataBooleTest/embedded_postcondition.lean)` | Inline `let`-binding blocks in `ensures` clauses | dalek-lite `montgomery.rs` `mul_clamped`, `mul_bits_be` | Implemented (#1075) | +| `[montgomery_loop_invariant.lean](../StrataBooleTest/FeatureRequests/montgomery_loop_invariant.lean)` | Relational loop invariants over two co-evolving variables | dalek-lite `montgomery.rs` `mul_bits_be` (Montgomery ladder) | Linear arithmetic case: implemented (#1075); elliptic curve case: open — requires group-law axioms (Costello-Smith 2017, eq. 4); whether cvc5 closes the invariant with those axioms is untested | +| `[bitvector_ops.lean](../StrataBooleTest/FeatureRequests/bitvector_ops.lean)` | Bitwise operators on `bvN` types | dalek-lite `scalar_specs.rs` | Implemented (#970) | +| `[bitvector_proof_mode.lean](../StrataBooleTest/FeatureRequests/bitvector_proof_mode.lean)` | `by (bit_vector)` proof mode (#27) | VeruSAGE-Bench Vest `leb128` | Active | +| `[seq_slicing.lean](../StrataBooleTest/FeatureRequests/seq_slicing.lean)` | Sequence slicing (#11) | dalek-lite `scalar_specs.rs`, `core_specs.rs`; Vest `leb128`, `repetition` | Implemented (#1075, #1167) | +| `[seq_empty_literal.lean](../StrataBooleTest/FeatureRequests/seq_empty_literal.lean)` | Sequence literals (#11): typed empty literal | Regression for `Sequence.of_[]` losing its element type | Implemented (#1214) | +| `[scalar_reduce.lean](../StrataBooleTest/FeatureRequests/scalar_reduce.lean)` | `reduce()` spec axiom for B2 (`Scalar::from_bytes_mod_order_wide`) | dalek-lite `scalar.rs` | Implemented (#1075) | +| `[struct_field_access.lean](../StrataBooleTest/FeatureRequests/struct_field_access.lean)` | Struct/record field access (#13) | dalek-lite `field_specs.rs`, `edwards_specs.rs` | Active | +| `[trait_spec_methods.lean](../StrataBooleTest/FeatureRequests/trait_spec_methods.lean)` | Trait / interface with spec methods (#21) | VeruSAGE-Bench Vest `SecureSpecCombinator` | Active | +| `[option_matches.lean](../StrataBooleTest/FeatureRequests/option_matches.lean)` | `Option` in spec functions (#14) | VeruSAGE-Bench Vest `SecureSpecCombinator`, `leb128` | Active | +| `[sha256_compact_indexed.lean](../StrataBooleTest/FeatureRequests/sha256_compact_indexed.lean)` | Iterator protocol lowering (#23), array syntax (#15), slice types (#16), `bv` rotate primitives (#28) | RustCrypto SHA-256 compact port (indexed `Sequence` encoding) | Active — all 17 VCs pass (#1075); open gaps: iterator protocol (#23), array syntax (#15), slice types (#16) | + + From 2e46dbecd066e8e55bc6d068ac468e70ae7f2f4b Mon Sep 17 00:00:00 2001 From: Yash Mehta Date: Wed, 30 Sep 2026 11:47:10 -0400 Subject: [PATCH 2/2] function form: existence guard added to emitted axiom --- StrataBoole/Grammar.lean | 3 +- StrataBoole/Verify.lean | 24 +++--- .../FeatureRequests/choose_operator.lean | 86 ++++++++++++++++--- .../FeatureRequests/map_extensionality.lean | 2 +- docs/BooleFeatureRequests.md | 8 +- 5 files changed, 95 insertions(+), 28 deletions(-) diff --git a/StrataBoole/Grammar.lean b/StrataBoole/Grammar.lean index 6ecc85c..fde84cc 100644 --- a/StrataBoole/Grammar.lean +++ b/StrataBoole/Grammar.lean @@ -92,7 +92,8 @@ op choose_assign (lhs : Ident, v : MonoBind, @[scope(v)] pred : bool) : Statemen lhs " := ε " v " :: " pred ";"; // choose function declaration: `function f(params) : R := ε z . pred(z, params);` -// Lowers to: uninterpreted function f + axiom ∀ params, ∀ z, z = f(params) → pred(z, params). +// Lowers to: uninterpreted f + axiom ∀ params, (∃ z, pred(z, params)) → +// (∀ z, z = f(params) → pred(z, params)). Without a witness, the result is unconstrained. // `@[scope(b)] v` makes b's parameter names available in v's type and (via the scope chain // @[scope(v)]) in pred, so pred can reference both z (bvar 0) and all params (bvars 1..n). @[declareFn(name, b, r)] diff --git a/StrataBoole/Verify.lean b/StrataBoole/Verify.lean index d4a363d..460d577 100644 --- a/StrataBoole/Verify.lean +++ b/StrataBoole/Verify.lean @@ -1075,14 +1075,12 @@ private def toCoreDecls (cmd : BooleDDM.Command SourceRange) : TranslateM (List | .command_choosefndef _ ⟨_, n⟩ ⟨_, targs?⟩ bs ret v pred => -- `function f(params) : R := ε z :: pred(z, params)` -- Emits: uninterpreted function declaration + axiom - -- ∀ p1:T1,...,pn:Tn, ∀ z:Tz, (z = f(p1,...,pn)) → pred(z, p1,...,pn) - -- Note: unlike `w := ε z . pred` (which guards soundness by asserting ∃ z . pred(z) - -- before havocing), this form emits the axiom unconditionally. The axiom is sound only - -- when pred is satisfiable for all parameter values; callers must supply that guarantee - -- (e.g. via a `requires ∃ z . pred(z, params)` precondition). + -- ∀ params, (∃ z, pred(z, params)) → (∀ z, z = f(params) → pred(z, params)) + -- The function is total; its result satisfies pred only when a witness exists. + -- An unsatisfiable predicate imposes no guarantee on the result. -- De Bruijn context for pred (from @[scope(b)] v + @[scope(v)] pred): -- bvar 0 = z, bvar 1 = pn (innermost param), ..., bvar n = p1 (outermost param) - -- This matches the 3-forall wrapping (z innermost, params outer) exactly. + -- Both the existential and universal bind z innermost, with params outermost. let tys := match targs? with | none => [] | some ts => typeArgsToList ts withTypeBVars tys do let bsList := bindingsToList bs @@ -1095,7 +1093,7 @@ private def toCoreDecls (cmd : BooleDDM.Command SourceRange) : TranslateM (List body := none, attr := #[], axioms := [] } .empty -- Push n+1 passthrough bvar entries (for z=bvar0, pn=bvar1, ..., p1=bvar n) so that -- getBVarExpr doesn't throw. Passthrough entries return the original index unchanged, - -- so pred's natural de Bruijn indices are preserved exactly as needed by the 3-forall. + -- so pred's natural de Bruijn indices are preserved in both branches of the guard. let bvarPassthroughs := Array.range (numParams + 1) |>.map (.bvar () ·) let predCore ← withBVarExprs bvarPassthroughs (toCoreExpr pred) -- f(p1,...,pn): p1 = bvar n (outermost), p2 = bvar n-1, ..., pn = bvar 1 (innermost param) @@ -1105,10 +1103,14 @@ private def toCoreDecls (cmd : BooleDDM.Command SourceRange) : TranslateM (List (.op () (mkIdent n) none) let zEqF : Core.Expression.Expr := .eq () (.bvar () 0) funcCallBvar let axiomInner := mkCoreApp Core.boolImpliesOp [zEqF, predCore] - -- Wrap ∀ p1:T1,...,∀ pn:Tn, ∀ z:Tz using foldr (z innermost = processed first by foldr) - let allTys := (inputs.map Prod.snd) ++ [vTy] - let axiomExpr := allTys.foldr (fun ty acc => - .quant () .all "" (some ty) (.bvar () 0) acc) axiomInner + -- Both branches bind their own z; parameter indices stay unchanged. + let existsExpr : Core.Expression.Expr := + .quant () .exist "" (some vTy) (.bvar () 0) predCore + let choiceExpr : Core.Expression.Expr := + .quant () .all "" (some vTy) (.bvar () 0) axiomInner + let guardedChoice := mkCoreApp Core.boolImpliesOp [existsExpr, choiceExpr] + let axiomExpr := (inputs.map Prod.snd).foldr (fun ty acc => + .quant () .all "" (some ty) (.bvar () 0) acc) guardedChoice let axiomDecl : Core.Decl := .ax { name := s!"{n}_choose_axiom", e := axiomExpr } .empty return [funcDecl, axiomDecl] diff --git a/StrataBooleTest/FeatureRequests/choose_operator.lean b/StrataBooleTest/FeatureRequests/choose_operator.lean index 054ed7a..640cafc 100644 --- a/StrataBooleTest/FeatureRequests/choose_operator.lean +++ b/StrataBooleTest/FeatureRequests/choose_operator.lean @@ -84,15 +84,13 @@ Result: ✅ pass-/ `function f(params) : R := ε z . pred(z, params);` declares an uninterpreted function `f` together with the axiom: - ∀ params, ∀ z, z = f(params) → pred(z, params) + ∀ params, (∃ z, pred(z, params)) → (∀ z, z = f(params) → pred(z, params)) This lets a specification define a function by its property rather than its implementation — similar to Verus choose-based spec functions. -Note: unlike `w := ε z . pred(z)` (which guards soundness with an existence -assertion), the function form emits the axiom unconditionally. The user must -ensure `pred` is satisfiable for all inputs (e.g. via a precondition) to avoid -an unsound axiom. +The function is total even when no witness exists. To conclude that its result +satisfies `pred`, establish existence, for example with a precondition. -/ private def chooseFnSeed : StrataDDM.Program := @@ -115,15 +113,14 @@ spec { #end /-- info: -Obligation: test_choose_fn_ensures_1_2749 +Obligation: test_choose_fn_ensures_1_2680 Property: assert Result: ✅ pass-/ #guard_msgs in #eval Strata.Boole.verify "cvc5" chooseFnSeed (options := .quiet) --- Without the ∃ precondition the ensures still passes, because the axiom --- `∀ z, z = best(x) → good(z, x)` unconditionally asserts good(best(x), x). --- This demonstrates that soundness relies on the caller supplying the witness. +-- Without the ∃ precondition, the guarded axiom does not establish good(best(x), x). +-- The solver must not report a pass without an existence fact. private def chooseFnNoPrecondSeed : StrataDDM.Program := #strata program Boole; @@ -143,8 +140,75 @@ spec { #end /-- info: -Obligation: test_no_precond_ensures_0_3444 +Obligation: test_no_precond_ensures_0_3290 Property: assert -Result: ✅ pass-/ +Result: ❓ unknown-/ #guard_msgs in #eval Strata.Boole.verify "cvc5" chooseFnNoPrecondSeed (options := .quiet) + +/-! +The guarded choice law holds for an arbitrary predicate. +-/ +private def chooseGuardedAxiomSpec : StrataDDM.Program := +#strata +program Boole; + +type R; +type P; + +function pred(z: R, params: P) : bool; + +function f(params: P) : R := + ε z: R . pred(z, params); + +procedure choice_guarded_axiom() returns () +spec { + ensures ∀ params: P . + ((∃ z: R . pred(z, params)) ==> + (∀ z: R . z == f(params) ==> pred(z, params))); +} +{ +}; +#end + +/-- info: +Obligation: choice_guarded_axiom_ensures_0_3837 +Property: assert +Result: ✅ pass-/ +#guard_msgs in +#eval Strata.Boole.verify "cvc5" chooseGuardedAxiomSpec + (options := .quiet) + +/-! +The old unconditional choice law admits a countermodel. + +The constant-false predicate supplies the witness, on abstract types. +The cover checks that the exact negation of the old law is satisfiable +under the generated axioms. An inconsistent axiom cannot pass it. +-/ +private def chooseOldAxiomCountermodelSpec : StrataDDM.Program := +#strata +program Boole; + +type R; +type P; + +function unsat_pred(z: R, params: P) : bool { false } + +function f(params: P) : R := + ε z: R . unsat_pred(z, params); + +procedure choice_old_axiom_has_countermodel() returns () +{ + cover !(∀ params: P . ∀ z: R . + z == f(params) ==> unsat_pred(z, params)); +}; +#end + +/-- info: +Obligation: cover_0_4714 +Property: cover +Result: ✅ pass-/ +#guard_msgs in +#eval Strata.Boole.verify "cvc5" chooseOldAxiomCountermodelSpec + (options := .quiet) diff --git a/StrataBooleTest/FeatureRequests/map_extensionality.lean b/StrataBooleTest/FeatureRequests/map_extensionality.lean index 3443c07..ccb969c 100644 --- a/StrataBooleTest/FeatureRequests/map_extensionality.lean +++ b/StrataBooleTest/FeatureRequests/map_extensionality.lean @@ -138,7 +138,7 @@ spec { #end /-- info: -Obligation: seq_ext_spec_ensures_0_3992 +Obligation: seq_ext_spec_ensures_0_4004 Property: assert Result: ✅ pass-/ #guard_msgs in diff --git a/docs/BooleFeatureRequests.md b/docs/BooleFeatureRequests.md index 2c1e602..88217fa 100644 --- a/docs/BooleFeatureRequests.md +++ b/docs/BooleFeatureRequests.md @@ -40,8 +40,8 @@ several that are now fully implemented; a few have moved to - `choose` **(Hilbert ε)** - Statement form: `w := ε z : T . pred(z)` desugars to `assert ∃ z : T . pred(z); havoc w; assume pred[z/w]`. - The existence assertion guards soundness: without it, an unsatisfiable `pred` silently becomes `assume false`, making every downstream obligation a false positive. - - Function form (Strata-Boole #4): `function f(params) : R := ε z . pred(z, params)` declares an uninterpreted `f` with the axiom `∀ params, ∀ z, z = f(params) → pred(z, params)`. - - Remaining gap: the function form has no existence guard. Its axiom is sound only if `pred` is satisfiable for every parameter value; otherwise the context becomes inconsistent. Callers must supply that guarantee, e.g. with `requires ∃ z . pred(z, params)`. + - Function form (Strata-Boole #4): `function f(params) : R := ε z . pred(z, params)` declares a total uninterpreted `f` with the guarded axiom `∀ params, (∃ z, pred(z, params)) → (∀ z, z = f(params) → pred(z, params))`. + - Function choice follows Verus semantics: establish existence to obtain the predicate guarantee, e.g. with `requires ∃ z . pred(z, params)`. If no witness exists, the result is arbitrary and imposes no predicate guarantee; the axiom remains consistent. - Benchmark: `[choose_operator.lean](../StrataBooleTest/FeatureRequests/choose_operator.lean)`. - `decreases` **annotation on functions, procedures, and** `for` **loops** - Parsing/forwarding implemented (#1075): accepted in function preconds, `spec {}` blocks, procedure headers, and `for v := init to/downto limit` loops; the `for`-loop measure is forwarded to the Core while-loop measure field and actively verified. @@ -111,7 +111,7 @@ several that are now fully implemented; a few have moved to ## Expressiveness requests 1. **Higher-order / lambda / closure support**: Implemented. Remaining gap: first-class function values as procedure parameters or local variables. -2. `choose`: Implemented, as a statement and as a function declaration. Remaining gap: the function form has no existence guard. +2. `choose`: Implemented, as a statement with an existence obligation and as a total function declaration with an existence-guarded axiom. 3. **Mutual recursion / forward references**: Implemented for datatypes (#599) and `int` (#1167). Remaining gap: functional reasoning about int-recursive functions blocked by Gap #1 (unfolding axioms). 4. **Trait-spec symbol resolution**: Preserve trait-spec symbols across module boundaries. 5. **Trait / interface with spec and proof methods**: `interface` declarations bundling `spec function` and `lemma` members, with `matches` pattern syntax in `ensures` and `external_body`-style trusted bodies. Confirmed as the backbone of Vest combinators. @@ -155,7 +155,7 @@ The table below tracks all seeds regardless of location. | `[cast_expr.lean](../StrataBooleTest/cast_expr.lean)` | SMT-LIB 2.7 cast operators (#6) | dalek-lite `scalar.rs` B2/B5 | Implemented | | `[cast_all_directions.lean](../StrataBooleTest/cast_all_directions.lean)` | SMT-LIB 2.7 cast operators (#6) | All three cast directions | Implemented | | `[cast_nested.lean](../StrataBooleTest/cast_nested.lean)` | SMT-LIB 2.7 cast operators (#6), `decreases` preservation (#7) | dalek-lite `bytes_seq_as_nat` / `seq_as_nat_52` (B2) | Implemented | -| `[choose_operator.lean](../StrataBooleTest/FeatureRequests/choose_operator.lean)` | `choose` (#18) | Verus `trigger_loops` (`choose_example`, `quantifier_example`) | Implemented (#1075; function form: Strata-Boole #4); function form has no existence guard | +| `[choose_operator.lean](../StrataBooleTest/FeatureRequests/choose_operator.lean)` | `choose` (#18) | Verus `trigger_loops` (`choose_example`, `quantifier_example`) | Implemented (#1075; function form: Strata-Boole #4); existence guard implemented; guarded-law and countermodel regressions pass | | `[higher_order_encoding.lean](../StrataBooleTest/FeatureRequests/higher_order_encoding.lean)` | Higher-order values (#17) | Verus `fun_ext`, `trait_for_fn` | Active | | `[lambda_closure.lean](../StrataBooleTest/FeatureRequests/lambda_closure.lean)` | Lambda / closure (#17) | Local reduced Rust/Verus-style lambda example | Implemented (#1075); remaining gap: first-class function values as procedure parameters/variables | | `[mutual_recursion.lean](../StrataBooleTest/FeatureRequests/mutual_recursion.lean)` | Mutual recursion (#19) | Verus `guide/recursion`; VLIR `mutual_recursion`, `recursion` | Implemented for datatypes (#599) and `int` (#1167); functional reasoning blocked by Gap #1 (unfolding axioms) |