From 5755d39167cbe5423eaea34a5c2f0c5c66fb9500 Mon Sep 17 00:00:00 2001 From: Lydia Kondylidou <33327056+kondylidou@users.noreply.github.com> Date: Fri, 15 May 2026 21:03:18 +0200 Subject: [PATCH 01/20] Implement `e as_int` widening cast via native Bv{n}.ToNat Core op MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Boole `e as_int` lowers to `Bv{n}.ToNat` (Core named op); the SMT encoder maps it to standard SMT-LIB `bv2nat`; no axioms injected. Supported widths: bv1/8/16/32/64/128 — covers all bitvector cast patterns in B2–B5 (u8/u64/u128 as nat in dalek-lite scalar.rs). Changes: - CoreOp: add BvOpKind.ToNat (cross-sort conversion) - SMTEncoder: .bv ⟨_, .ToNat⟩ → Op.bv2nat / .int - Op.lean: add Op.BV.bv2nat + mkName entry - Denote/Translate: handle .app .bv2nat for semantics and Lean reflection - Core Grammar: add type bv128 + bv128Lit - Core DDM Translate: add bv128 → .bitvec 128 - Factory: add bvToNatFunc for widths 1/8/16/32/64/128, register in WFFactory - Boole Verify: wire bv128 through typeRange/toCoreMonoType/bvWidth/cast_to_int - Boole Grammar: update cast_to_int comment - Tests: cast_expr.lean (new, all 6 widths), widening_casts.lean refactored to use as_int; StatisticsTest/ProgramEvalTests snapshots updated (+6 factory ops) - Docs: BooleFeatureRequests/BooleBenchmarks updated to reflect Gap #6 closed Co-Authored-By: Claude Sonnet 4.6 --- Strata/DL/SMT/Denote.lean | 3 + Strata/DL/SMT/Op.lean | 4 +- Strata/DL/SMT/Translate.lean | 3 + Strata/Languages/Boole/Grammar.lean | 4 + Strata/Languages/Boole/Verify.lean | 12 +- Strata/Languages/Core/CoreOp.lean | 7 +- .../Languages/Core/DDMTransform/Grammar.lean | 2 + .../Core/DDMTransform/Translate.lean | 1 + Strata/Languages/Core/Factory.lean | 16 +++ Strata/Languages/Core/SMTEncoder.lean | 1 + .../Boole/FeatureRequests/cast_expr.lean | 127 ++++++++++++++++++ .../Boole/FeatureRequests/widening_casts.lean | 32 ++--- .../Core/Tests/ProgramEvalTests.lean | 6 + .../Languages/Core/Tests/StatisticsTest.lean | 4 +- docs/BooleBenchmarks.md | 29 ++-- docs/BooleFeatureRequests.md | 12 +- 16 files changed, 215 insertions(+), 48 deletions(-) create mode 100644 StrataTest/Languages/Boole/FeatureRequests/cast_expr.lean diff --git a/Strata/DL/SMT/Denote.lean b/Strata/DL/SMT/Denote.lean index d1b84925d8..b7206bc4ec 100644 --- a/Strata/DL/SMT/Denote.lean +++ b/Strata/DL/SMT/Denote.lean @@ -854,6 +854,9 @@ and semantics when successful. | .app (.zero_extend i) [x] _ => let ⟨.prim (.bitvec n), _, x⟩ ← denoteTerm ctx x | none return ⟨.prim (.bitvec (n + i)), rfl, fun Γ => BitVec.zeroExtend (n + i) (x Γ)⟩ + | .app .bv2nat [x] _ => + let ⟨.prim (.bitvec _), _, x⟩ ← denoteTerm ctx x | none + return ⟨.prim .int, rfl, fun Γ => Int.ofNat (x Γ).toNat⟩ -- SMT-Lib theory of strings | .prim (.string s) => return ⟨.prim .string, rfl, fun _ => s⟩ diff --git a/Strata/DL/SMT/Op.lean b/Strata/DL/SMT/Op.lean index 5983f16541..920f27af4a 100644 --- a/Strata/DL/SMT/Op.lean +++ b/Strata/DL/SMT/Op.lean @@ -122,6 +122,7 @@ inductive Op.BV : Type where | bvsmulo -- bit-vector signed multiplication overflow predicate | bvconcat | zero_extend : Nat → Op.BV + | bv2nat deriving Repr, DecidableEq, Inhabited, Hashable inductive Op.Strings : Type where @@ -254,7 +255,7 @@ elab "#genOpAbbrevs" : command => do /-- -info: Generated abbrevs: #[Op.not, Op.and, Op.or, Op.eq, Op.ite, Op.implies, Op.distinct, Op.uf, Op.neg, Op.sub, Op.add, Op.mul, Op.div, Op.rdiv, Op.mod, Op.abs, Op.le, Op.lt, Op.ge, Op.gt, Op.bvneg, Op.bvadd, Op.bvsub, Op.bvmul, Op.bvnot, Op.bvand, Op.bvor, Op.bvxor, Op.bvshl, Op.bvlshr, Op.bvashr, Op.bvslt, Op.bvsle, Op.bvult, Op.bvsge, Op.bvsgt, Op.bvule, Op.bvugt, Op.bvuge, Op.bvudiv, Op.bvurem, Op.bvsdiv, Op.bvsrem, Op.bvnego, Op.bvsaddo, Op.bvssubo, Op.bvsmulo, Op.bvconcat, Op.zero_extend, Op.str_length, Op.str_concat, Op.str_lt, Op.str_le, Op.str_at, Op.str_substr, Op.str_prefixof, Op.str_suffixof, Op.str_contains, Op.str_indexof, Op.str_replace, Op.str_replace_all, Op.str_to_re, Op.str_in_re, Op.re_none, Op.re_all, Op.re_allchar, Op.re_concat, Op.re_union, Op.re_inter, Op.re_star, Op.str_replace_re, Op.str_replace_re_all, Op.re_comp, Op.re_diff, Op.re_plus, Op.re_opt, Op.re_range, Op.re_loop, Op.re_index, Op.select, Op.store] +info: Generated abbrevs: #[Op.not, Op.and, Op.or, Op.eq, Op.ite, Op.implies, Op.distinct, Op.uf, Op.neg, Op.sub, Op.add, Op.mul, Op.div, Op.rdiv, Op.mod, Op.abs, Op.le, Op.lt, Op.ge, Op.gt, Op.bvneg, Op.bvadd, Op.bvsub, Op.bvmul, Op.bvnot, Op.bvand, Op.bvor, Op.bvxor, Op.bvshl, Op.bvlshr, Op.bvashr, Op.bvslt, Op.bvsle, Op.bvult, Op.bvsge, Op.bvsgt, Op.bvule, Op.bvugt, Op.bvuge, Op.bvudiv, Op.bvurem, Op.bvsdiv, Op.bvsrem, Op.bvnego, Op.bvsaddo, Op.bvssubo, Op.bvsmulo, Op.bvconcat, Op.zero_extend, Op.bv2nat, Op.str_length, Op.str_concat, Op.str_lt, Op.str_le, Op.str_at, Op.str_substr, Op.str_prefixof, Op.str_suffixof, Op.str_contains, Op.str_indexof, Op.str_replace, Op.str_replace_all, Op.str_to_re, Op.str_in_re, Op.re_none, Op.re_all, Op.re_allchar, Op.re_concat, Op.re_union, Op.re_inter, Op.re_star, Op.str_replace_re, Op.str_replace_re_all, Op.re_comp, Op.re_diff, Op.re_plus, Op.re_opt, Op.re_range, Op.re_loop, Op.re_index, Op.select, Op.store] -/ #guard_msgs in #genOpAbbrevs @@ -309,6 +310,7 @@ def Op.mkName : Op → String | .bvsmulo => "bvsmulo" | .bvconcat => "concat" | .zero_extend _ => "zero_extend" + | .bv2nat => "bv2nat" | .triggers => "triggers" | .option_get => "option.get" | .datatype_op .tester name => s!"is-{name}" diff --git a/Strata/DL/SMT/Translate.lean b/Strata/DL/SMT/Translate.lean index c6de9007fa..e4961c5e66 100644 --- a/Strata/DL/SMT/Translate.lean +++ b/Strata/DL/SMT/Translate.lean @@ -542,6 +542,9 @@ def translateTerm (t : SMT.Term) : TranslateM (Expr × Expr) := do expectString γ return e return (mkString, as.foldl (mkApp2 mkStringAppend) (mkApp2 mkStringAppend a b)) + | .app .bv2nat [x] _ => + let (_, x) ← translateTerm x + return (mkInt, mkApp (.const ``Int.ofNat []) (mkApp (.const ``BitVec.toNat []) x)) | t => throw m!"Error: unsupported term '{repr t}'" where leftAssocOp (op : Expr) (as : List SMT.Term) : TranslateM (Expr × Expr) := do diff --git a/Strata/Languages/Boole/Grammar.lean b/Strata/Languages/Boole/Grammar.lean index efc1ec6e8f..2605b72ced 100644 --- a/Strata/Languages/Boole/Grammar.lean +++ b/Strata/Languages/Boole/Grammar.lean @@ -134,6 +134,10 @@ fn seq_drop_first (A : Type, s : Sequence A) : Sequence A => fn seq_subrange (A : Type, s : Sequence A, lo : int, hi : int) : Sequence A => "Sequence.subrange" "(" s ", " lo ", " hi ")"; +// Widening cast: `e as_int` converts any bitvector to an integer (unsigned). +// Lowers to a native `Bv{n}.ToNat : bvN → int` Core op → SMT-LIB `bv2nat`. +// Supported widths: 1, 8, 16, 32, 64, 128. No axioms injected. +fn cast_to_int (T : Type, e : T) : int => @[prec(80)] e " as_int"; category Step; op step(e: Expr) : Step => diff --git a/Strata/Languages/Boole/Verify.lean b/Strata/Languages/Boole/Verify.lean index 927f39fc17..fe5268ce65 100644 --- a/Strata/Languages/Boole/Verify.lean +++ b/Strata/Languages/Boole/Verify.lean @@ -230,6 +230,7 @@ private def typeRange : Boole.Type → SourceRange | .bv16 m => m | .bv32 m => m | .bv64 m => m + | .bv128 m => m | .Map m _ _ => m | .Sequence m _ => m @@ -247,6 +248,7 @@ def toCoreMonoType (t : Boole.Type) : TranslateM Lambda.LMonoTy := do | .bv16 _ => return .bitvec 16 | .bv32 _ => return .bitvec 32 | .bv64 _ => return .bitvec 64 + | .bv128 _ => return .bitvec 128 | .Map _ v k => return .tcons "Map" [← toCoreMonoType k, ← toCoreMonoType v] | .Sequence _ elem => return .tcons "Sequence" [← toCoreMonoType elem] | _ => throwAt (typeRange t) s!"Unsupported Boole type: {repr t}" @@ -287,7 +289,8 @@ private def bvWidth (m : SourceRange) (ty : Boole.Type) : TranslateM Nat := | .bv8 _ => return 8 | .bv16 _ => return 16 | .bv32 _ => return 32 - | .bv64 _ => return 64 + | .bv64 _ => return 64 + | .bv128 _ => return 128 | _ => throwAt m s!"Expected bitvector type, got: {repr ty}" private def toCoreBvUn (m : SourceRange) (ty : Boole.Type) (op : String) (a : Core.Expression.Expr) : TranslateM Core.Expression.Expr := do @@ -487,6 +490,13 @@ partial def toCoreExpr (e : Boole.Expr) : TranslateM Core.Expression.Expr := do return tys.foldr (fun ty acc => .abs () "" (some ty) acc) body' -- Function application: `(f)(x)` → Core .app | .apply_expr _ _ _ f x => return .app () (← toCoreExpr f) (← toCoreExpr x) + | .cast_to_int m ty e => + match ty with + | .bv1 _ | .bv8 _ | .bv16 _ | .bv32 _ | .bv64 _ | .bv128 _ => do + let n ← bvWidth m ty + return mkCoreApp (.op () (mkIdent s!"Bv{n}.ToNat") none) [← toCoreExpr e] + | .int _ => toCoreExpr e + | _ => throwAt m s!"'as int' requires a bitvector source type" | _ => throw (.fromMessage s!"Unsupported expression: {repr e}") end diff --git a/Strata/Languages/Core/CoreOp.lean b/Strata/Languages/Core/CoreOp.lean index 071bf70b86..657f7b6868 100644 --- a/Strata/Languages/Core/CoreOp.lean +++ b/Strata/Languages/Core/CoreOp.lean @@ -51,6 +51,8 @@ inductive BvOpKind where -- Overflow predicates | SAddOverflow | SSubOverflow | SMulOverflow | SNegOverflow | SDivOverflow | UAddOverflow | USubOverflow | UMulOverflow | UNegOverflow + -- Cross-sort conversion + | ToNat deriving Repr, DecidableEq, Inhabited, BEq, Hashable structure BvOp where @@ -69,7 +71,7 @@ def BvOpKind.isPredicate : BvOpKind → Bool | _ => false def BvOpKind.isUnary : BvOpKind → Bool - | .Neg | .Not => true + | .Neg | .Not | .ToNat => true | _ => false def BvOpKind.names : List (BvOpKind × String) := @@ -89,7 +91,8 @@ def BvOpKind.names : List (BvOpKind × String) := (.SMulOverflow, "SMulOverflow"), (.SNegOverflow, "SNegOverflow"), (.SDivOverflow, "SDivOverflow"), (.UAddOverflow, "UAddOverflow"), (.USubOverflow, "USubOverflow"), - (.UMulOverflow, "UMulOverflow"), (.UNegOverflow, "UNegOverflow")] + (.UMulOverflow, "UMulOverflow"), (.UNegOverflow, "UNegOverflow"), + (.ToNat, "ToNat")] def BvOpKind.toString (k : BvOpKind) : String := lookupName names k instance : ToString BvOpKind := ⟨BvOpKind.toString⟩ diff --git a/Strata/Languages/Core/DDMTransform/Grammar.lean b/Strata/Languages/Core/DDMTransform/Grammar.lean index 206b72e7d5..15e7571b8f 100644 --- a/Strata/Languages/Core/DDMTransform/Grammar.lean +++ b/Strata/Languages/Core/DDMTransform/Grammar.lean @@ -50,6 +50,7 @@ type bv8; type bv16; type bv32; type bv64; +type bv128; type Map (dom : Type, range : Type); type Sequence (elem : Type); @@ -92,6 +93,7 @@ fn bv8Lit (n : Num) : bv8 => "bv{8}" "(" n ")"; fn bv16Lit (n : Num) : bv16 => "bv{16}" "(" n ")"; fn bv32Lit (n : Num) : bv32 => "bv{32}" "(" n ")"; fn bv64Lit (n : Num) : bv64 => "bv{64}" "(" n ")"; +fn bv128Lit (n : Num) : bv128 => "bv{128}" "(" n ")"; fn strLit (s : Str) : string => s; fn realLit (d : Decimal) : real => d; diff --git a/Strata/Languages/Core/DDMTransform/Translate.lean b/Strata/Languages/Core/DDMTransform/Translate.lean index 8cd2563698..db89ddec28 100644 --- a/Strata/Languages/Core/DDMTransform/Translate.lean +++ b/Strata/Languages/Core/DDMTransform/Translate.lean @@ -234,6 +234,7 @@ partial def translateLMonoTy (bindings : TransBindings) (arg : Arg) : | .ident _ q`Core.bv16 #[] => pure <| .bitvec 16 | .ident _ q`Core.bv32 #[] => pure <| .bitvec 32 | .ident _ q`Core.bv64 #[] => pure <| .bitvec 64 + | .ident _ q`Core.bv128 #[] => pure <| .bitvec 128 | .ident _ i argst => let argst' ← translateLMonoTys bindings (argst.map ArgF.type) pure <| (.tcons i.name argst'.toList.reverse) diff --git a/Strata/Languages/Core/Factory.lean b/Strata/Languages/Core/Factory.lean index ef99656a5b..e5845a30d7 100644 --- a/Strata/Languages/Core/Factory.lean +++ b/Strata/Languages/Core/Factory.lean @@ -770,10 +770,20 @@ def bvExtractFunc (size hi lo : Nat) : WFLFunc CoreLParams := unaryFuncUneval s!"Bv{size}.Extract_{hi}_{lo}" (.bitvec size) (.bitvec (hi + 1 - lo)) rfl rfl +def bvToNatFunc (size : Nat) : WFLFunc CoreLParams := + unaryFuncUneval s!"Bv{size}.ToNat" (.bitvec size) .int rfl rfl + def bv8ConcatFunc := bvConcatFunc 8 def bv16ConcatFunc := bvConcatFunc 16 def bv32ConcatFunc := bvConcatFunc 32 +def bv1ToNatFunc := bvToNatFunc 1 +def bv8ToNatFunc := bvToNatFunc 8 +def bv16ToNatFunc := bvToNatFunc 16 +def bv32ToNatFunc := bvToNatFunc 32 +def bv64ToNatFunc := bvToNatFunc 64 +def bv128ToNatFunc := bvToNatFunc 128 + def bv8Extract_7_7_Func := bvExtractFunc 8 7 7 def bv16Extract_15_15_Func := bvExtractFunc 16 15 15 def bv16Extract_7_0_Func := bvExtractFunc 16 7 0 @@ -864,6 +874,12 @@ def WFFactory : Lambda.WFLFactory CoreLParams := bv8ConcatFunc, bv16ConcatFunc, bv32ConcatFunc, + bv1ToNatFunc, + bv8ToNatFunc, + bv16ToNatFunc, + bv32ToNatFunc, + bv64ToNatFunc, + bv128ToNatFunc, bv8Extract_7_7_Func, bv16Extract_15_15_Func, bv16Extract_7_0_Func, diff --git a/Strata/Languages/Core/SMTEncoder.lean b/Strata/Languages/Core/SMTEncoder.lean index e60e63fbca..d8049b036a 100644 --- a/Strata/Languages/Core/SMTEncoder.lean +++ b/Strata/Languages/Core/SMTEncoder.lean @@ -547,6 +547,7 @@ partial def toSMTOp (E : Env) (fn : CoreIdent) (fnty : LMonoTy) (ctx : SMT.Conte | .bv ⟨_, .SGt⟩ => .ok (.app Op.bvsgt, .bool, ctx) | .bv ⟨_, .SGe⟩ => .ok (.app Op.bvsge, .bool, ctx) | .bv ⟨n, .Concat⟩ => .ok (.app Op.bvconcat, .bitvec (n * 2), ctx) + | .bv ⟨_, .ToNat⟩ => .ok (.app Op.bv2nat, .int, ctx) | .str .Length => .ok (.app Op.str_length, .int, ctx) | .str .Concat => .ok (.app Op.str_concat, .string, ctx) diff --git a/StrataTest/Languages/Boole/FeatureRequests/cast_expr.lean b/StrataTest/Languages/Boole/FeatureRequests/cast_expr.lean new file mode 100644 index 0000000000..0a0e70313d --- /dev/null +++ b/StrataTest/Languages/Boole/FeatureRequests/cast_expr.lean @@ -0,0 +1,127 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import Strata.MetaVerifier + +open Strata + +/- +Near-upstream anchor: +- Source: dalek-lite `curve25519-dalek/src/scalar.rs` + (`from_bytes_mod_order_wide`, B2) and `from_bytes_mod_order` (B2/B5). + Rust `u8 as usize`, `u64 as u128`, etc. are widening casts; this seed + exercises the Boole `e as_int` surface syntax for all supported widths + (bv1, bv8, bv16, bv32, bv64, bv128). + +Feature: `e as_int` — widening cast from any bitvector type to `int`. + +Lowers to a native `Bv{n}.ToNat : bvN → int` Core op; the SMT encoder maps +it to the standard SMT-LIB `bv2nat` function. No axioms injected. +-/ + +private def castExprSeed : Strata.Program := +#strata +program Boole; + +procedure cast_bv8_nonneg(x: bv8) returns () +spec { + ensures 0 <= (x as_int); +} +{ + assert 0 <= (x as_int); +}; + +procedure cast_bv64_nonneg(x: bv64) returns () +spec { + ensures 0 <= (x as_int); +} +{ + assert 0 <= (x as_int); +}; + +procedure cast_bv32_bounded(x: bv32) returns () +spec { + ensures 0 <= (x as_int) && (x as_int) < 4294967296; +} +{ + assert 0 <= (x as_int) && (x as_int) < 4294967296; +}; + +procedure cast_bv1_nonneg(x: bv1) returns () +spec { + ensures 0 <= (x as_int); +} +{ + assert 0 <= (x as_int); +}; + +procedure cast_bv16_nonneg(x: bv16) returns () +spec { + ensures 0 <= (x as_int); +} +{ + assert 0 <= (x as_int); +}; + +procedure cast_bv128_nonneg(x: bv128) returns () +spec { + ensures 0 <= (x as_int); +} +{ + assert 0 <= (x as_int); +}; +#end + +/-- info: +Obligation: assert_1_836 +Property: assert +Result: ✅ pass + +Obligation: cast_bv8_nonneg_ensures_0_805 +Property: assert +Result: ✅ pass + +Obligation: assert_3_951 +Property: assert +Result: ✅ pass + +Obligation: cast_bv64_nonneg_ensures_2_920 +Property: assert +Result: ✅ pass + +Obligation: assert_5_1094 +Property: assert +Result: ✅ pass + +Obligation: cast_bv32_bounded_ensures_4_1036 +Property: assert +Result: ✅ pass + +Obligation: assert_7_1234 +Property: assert +Result: ✅ pass + +Obligation: cast_bv1_nonneg_ensures_6_1203 +Property: assert +Result: ✅ pass + +Obligation: assert_9_1349 +Property: assert +Result: ✅ pass + +Obligation: cast_bv16_nonneg_ensures_8_1318 +Property: assert +Result: ✅ pass + +Obligation: assert_11_1466 +Property: assert +Result: ✅ pass + +Obligation: cast_bv128_nonneg_ensures_10_1435 +Property: assert +Result: ✅ pass-/ +#guard_msgs in +#eval Strata.Boole.verify "cvc5" castExprSeed (options := .quiet) diff --git a/StrataTest/Languages/Boole/FeatureRequests/widening_casts.lean b/StrataTest/Languages/Boole/FeatureRequests/widening_casts.lean index 43f7d328e6..82dfdc3d1b 100644 --- a/StrataTest/Languages/Boole/FeatureRequests/widening_casts.lean +++ b/StrataTest/Languages/Boole/FeatureRequests/widening_casts.lean @@ -17,47 +17,33 @@ Near-upstream anchors from `differential_status.md`: `guide/integers`: https://github.com/verus-lang/verus/blob/main/examples/guide/integers.rs `quantifiers`: https://github.com/verus-lang/verus/blob/main/examples/quantifiers.rs `statements`: https://github.com/verus-lang/verus/blob/main/examples/statements.rs -- Gap: widening casts only partially inserted -- Current status: the seed verifies after coercion points are spelled out -- Remaining gap: centralized insertion/preservation of widening casts + +Gap #6 implemented: `e as_int` lowers to native `Bv{n}.ToNat` Core op → SMT-LIB `bv2nat`. +No axioms injected. -/ private def wideningCastsSeed : Strata.Program := #strata program Boole; -// Target shape: explicit widening/coercion pressure in a quantified formula, -// not only at function/procedure call sites. - -type BvVec := Map int bv32; - -function bv32_to_int_u(x: bv32) : int; - -axiom (∀ x: bv32 . 0 <= bv32_to_int_u(x)); - -procedure widening_cast_seed(v: BvVec, n: int) returns () +// `v[i] as_int` lowers to `Bv32.ToNat` Core op → SMT-LIB `bv2nat`. +procedure widening_cast_seed(v: Map int bv32, n: int) returns () spec { requires 0 <= n; - ensures ∀ i: int . 0 <= i && i < n ==> 0 <= bv32_to_int_u(v[i]); + ensures ∀ i: int . 0 <= i && i < n ==> 0 <= (v[i] as_int); } { - assert ∀ i: int . 0 <= i && i < n ==> 0 <= bv32_to_int_u(v[i]); + assert ∀ i: int . 0 <= i && i < n ==> 0 <= (v[i] as_int); }; #end /-- info: -Obligation: assert_3_1226 +Obligation: assert_2_979 Property: assert Result: ✅ pass -Obligation: widening_cast_seed_ensures_2_1152 +Obligation: widening_cast_seed_ensures_1_911 Property: assert Result: ✅ pass-/ #guard_msgs in #eval Strata.Boole.verify "cvc5" wideningCastsSeed (options := .quiet) - -example : Strata.smtVCsCorrect wideningCastsSeed := by - gen_smt_vcs - all_goals - intro Map inst n bv32_to_int_u select v hNonneg hn i hi - exact hNonneg (select v i) diff --git a/StrataTest/Languages/Core/Tests/ProgramEvalTests.lean b/StrataTest/Languages/Core/Tests/ProgramEvalTests.lean index d9ee5b06a5..23ae46ac40 100644 --- a/StrataTest/Languages/Core/Tests/ProgramEvalTests.lean +++ b/StrataTest/Languages/Core/Tests/ProgramEvalTests.lean @@ -98,6 +98,12 @@ func TriggerGroup.addTrigger : ∀[a]. ((x : a) (t : TriggerGroup)) → TriggerG func Bv8.Concat : ((x : bv8) (y : bv8)) → bv16; func Bv16.Concat : ((x : bv16) (y : bv16)) → bv32; func Bv32.Concat : ((x : bv32) (y : bv32)) → bv64; +func Bv1.ToNat : ((x : bv1)) → int; +func Bv8.ToNat : ((x : bv8)) → int; +func Bv16.ToNat : ((x : bv16)) → int; +func Bv32.ToNat : ((x : bv32)) → int; +func Bv64.ToNat : ((x : bv64)) → int; +func Bv128.ToNat : ((x : bv128)) → int; func Bv8.Extract_7_7 : ((x : bv8)) → bv1; func Bv16.Extract_15_15 : ((x : bv16)) → bv1; func Bv16.Extract_7_0 : ((x : bv16)) → bv8; diff --git a/StrataTest/Languages/Core/Tests/StatisticsTest.lean b/StrataTest/Languages/Core/Tests/StatisticsTest.lean index 7371461e55..7fd98ba80f 100644 --- a/StrataTest/Languages/Core/Tests/StatisticsTest.lean +++ b/StrataTest/Languages/Core/Tests/StatisticsTest.lean @@ -32,7 +32,7 @@ spec { #end /-- -info: [statistics] Evaluator.factoryOps: 286 +info: [statistics] Evaluator.factoryOps: 292 [statistics] Evaluator.procedures: 1 [statistics] Evaluator.simulatedStmts: 2 [statistics] Evaluator.verificationEnvironments: 1 @@ -74,7 +74,7 @@ spec { #end /-- -info: [statistics] Evaluator.factoryOps: 286 +info: [statistics] Evaluator.factoryOps: 292 [statistics] Evaluator.functions: 1 [statistics] Evaluator.procedures: 2 [statistics] Evaluator.simulatedStmts: 4 diff --git a/docs/BooleBenchmarks.md b/docs/BooleBenchmarks.md index 36e898d090..e07645961e 100644 --- a/docs/BooleBenchmarks.md +++ b/docs/BooleBenchmarks.md @@ -154,18 +154,19 @@ seeds live in **Additional gaps per benchmark:** -| B | Gap | Status | Notes | -|---|-----|--------|-------| -| 1 | `u128` intermediate products | ○ open | 25 u64×u64 cross-limb products are u128 in Rust; in Boole, model as `int` — no separate feature needed, resolves with #13 | -| 1 | #13 `FieldElement51.limbs: [u64; 5]` | ○ open | Sub-case of #13: `limbs` is a struct field whose type is itself a fixed-size array. Planned encoding: flatten into five named `int` fields (`limb0`…`limb4`) rather than `Map int bv64` — same gap, not a separate one | -| 2 | #15 `[u8; 64]` byte arrays | ○ open | `input: &[u8; 64]` as `Map int bv8`; SMT backend resolved by PR #795; remaining gap is Boole syntax (initializer, write-back) | -| 5 | #15 `[u8; 32]` byte arrays | ○ open | Same as B2; SMT backend resolved by PR #795 | -| 2 | `reduce()` spec function | ✓ done | Axiom pattern verified in [`scalar_reduce.lean`](../StrataTest/Languages/Boole/FeatureRequests/scalar_reduce.lean); `u8_64_as_group_canonical` can now use recursive form (#1167 merged); manual axioms unchanged | -| 2 | `is_uniform_scalar` axiom | ○ open | Probabilistic postcondition needs abstract `is_uniform_bytes`/`is_uniform_scalar` predicates as Boole axioms | -| 3 | #14 `Option` return | ○ open | Boole has no native `Option` type and no `matches` destructuring in spec clauses; see [`option_matches.lean`](../StrataTest/Languages/Boole/FeatureRequests/option_matches.lean) | -| 3 | `field_square` / `sqrt_ratio_i` axioms | ○ open | Needed for the full decompress body | -| 4 | Pair return type | ○ open | `invsqrt()` returns `(bool, FieldElement51)`; needs tuple/pair type support in Boole | -| 4 | Field op axioms | ○ open | `add`, `sub`, `square`, `invsqrt`, `conditional_negate`, `as_bytes` — each needs a Boole axiom | -| 5 | Inline `let`-block postcondition | ✓ done | Implemented; see [`embedded_postcondition.lean`](../StrataTest/Languages/Boole/embedded_postcondition.lean) | -| 5 | Montgomery ladder invariant | ○ open | Needs Montgomery curve differential addition axioms (Costello-Smith 2017, eq. 4); loop structure demonstrated in [`montgomery_loop_invariant.lean`](../StrataTest/Languages/Boole/FeatureRequests/montgomery_loop_invariant.lean) | +| # | Gap | FR# | Status | Notes | +|---|-----|-----|--------|-------| +| 1 | `u128` intermediate products | — | ○ open | 25 u64×u64 cross-limb products are u128 in Rust; in Boole, model as `int` — no separate feature needed, resolves with Gap #13 | +| 1 | `FieldElement51.limbs: [u64; 5]` | #13 | ○ open | Sub-case of Gap #13: `limbs` is a struct field whose type is itself a fixed-size array. Planned encoding: flatten into five named `int` fields (`limb0`…`limb4`) rather than `Map int bv64` — same gap, not a separate one | +| 2 | `[u8; 64]` byte arrays | #25 | ○ open | `input: &[u8; 64]` as `Map int bv8`; SMT backend resolved by PR #795; remaining gap is Boole syntax (initializer, write-back) | +| 5 | `[u8; 32]` byte arrays | #25 | ○ open | Same as B2; SMT backend resolved by PR #795 | +| 2,5 | Widening casts (`e as_int`) | #6 | ✓ done | `Bv{n}.ToNat` → `bv2nat`; bv1/8/16/32/64/128; see [`cast_expr.lean`](../StrataTest/Languages/Boole/FeatureRequests/cast_expr.lean) | +| 2 | `reduce()` spec function | — | ✓ done | Axiom pattern verified in [`scalar_reduce.lean`](../StrataTest/Languages/Boole/FeatureRequests/scalar_reduce.lean); `u8_64_as_group_canonical` gains a recursive definition once Gap #11 closes (→ #1167), pure UF in SMT, manual axioms unchanged | +| 2 | `is_uniform_scalar` axiom | — | ○ open | Probabilistic postcondition needs abstract `is_uniform_bytes`/`is_uniform_scalar` predicates as Boole axioms | +| 3 | `Option` return | — | ○ open | Boole has no native `Option` type and no `matches` destructuring in spec clauses; see [`option_matches.lean`](../StrataTest/Languages/Boole/FeatureRequests/option_matches.lean) | +| 3 | `field_square` / `sqrt_ratio_i` axioms | — | ○ open | Needed for the full decompress body | +| 4 | Pair return type | — | ○ open | `invsqrt()` returns `(bool, FieldElement51)`; needs tuple/pair type support in Boole | +| 4 | Field op axioms | — | ○ open | `add`, `sub`, `square`, `invsqrt`, `conditional_negate`, `as_bytes` — each needs a Boole axiom | +| 5 | Inline `let`-block postcondition | — | ✓ done | Implemented; see [`embedded_postcondition.lean`](../StrataTest/Languages/Boole/embedded_postcondition.lean) | +| 5 | Montgomery ladder invariant | — | ○ open | Needs Montgomery curve differential addition axioms (Costello-Smith 2017, eq. 4); loop structure demonstrated in [`montgomery_loop_invariant.lean`](../StrataTest/Languages/Boole/FeatureRequests/montgomery_loop_invariant.lean) | diff --git a/docs/BooleFeatureRequests.md b/docs/BooleFeatureRequests.md index e162c367c3..ceac0f119c 100644 --- a/docs/BooleFeatureRequests.md +++ b/docs/BooleFeatureRequests.md @@ -8,9 +8,7 @@ This document tracks the selected Boole feature-request seeds kept under - Prioritize Rust-facing language support over Verus-only proof-visibility features. - Treat `opaque`, `reveal`, `hide`, `reveal_with_fuel`, `closed`, and `HasType` as lower-priority compatibility items unless they unblock a broader Rust path. -- Keep widening casts/coercions active; prefer a centralized type-directed coercion - pass. This likely overlaps with `nat`/`int` boundary work given how Verus - internalizes fixed-width arithmetic. +- Widening casts (`e as_int`) fully implemented (Gap #6) for bv1/8/16/32/64/128; covers all B2–B5 bitvector casts. Gap #8 (`nat` as a first-class type) is not a cast blocker — Boole has no `nat` type, so `nat`/`int` coercions are identity. ## Implemented feature requests @@ -64,6 +62,9 @@ This document tracks the selected Boole feature-request seeds kept under - `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`](../StrataTest/Languages/Boole/FeatureRequests/lambda_closure.lean). +- **Widening casts** (`e as_int`) + - `e as_int` lowers to `Bv{n}.ToNat` (Core op) → SMT-LIB `bv2nat`; widths 1/8/16/32/64/128. + - Benchmarks: [`cast_expr.lean`](../StrataTest/Languages/Boole/FeatureRequests/cast_expr.lean), [`widening_casts.lean`](../StrataTest/Languages/Boole/FeatureRequests/widening_casts.lean). ## Semantic preservation requests @@ -72,7 +73,7 @@ This document tracks the selected Boole feature-request seeds kept under 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. **Widening casts outside call sites**: Insert or preserve cast/coercion structure in comparisons, quantifiers, and other expressions with a centralized type-directed coercion pass. +6. **Widening casts**: Implemented. 7. **`decreases` metadata**: Implemented. ## Type/model requests @@ -127,7 +128,8 @@ These are the curated one-gap Boole seeds. | [`opaque_reveal_hide.lean`](../StrataTest/Languages/Boole/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`](../StrataTest/Languages/Boole/FeatureRequests/reveal_with_fuel.lean) | `reveal_with_fuel` (#3) | Verus `test_expand_errors`, `recursion` | Lower priority | | [`early_return.lean`](../StrataTest/Languages/Boole/early_return.lean) | Early return | Verus SST `return` translation gap from `differential_status.md` | Implemented (#871) | -| [`widening_casts.lean`](../StrataTest/Languages/Boole/FeatureRequests/widening_casts.lean) | Widening casts (#6) | Verus `guide/integers`, `quantifiers`, `statements` | Active | +| [`widening_casts.lean`](../StrataTest/Languages/Boole/FeatureRequests/widening_casts.lean) | Widening casts (#6) | Verus `guide/integers`, `quantifiers`, `statements` | Updated to use `e as_int`; map-lookup case `v[i] as_int` verified | +| [`cast_expr.lean`](../StrataTest/Languages/Boole/FeatureRequests/cast_expr.lean) | `e as_int` widening cast (#6) | dalek-lite `scalar.rs` B2/B5 | Gap #6 closed; bv1/8/16/32/64/128 | | [`choose_operator.lean`](../StrataTest/Languages/Boole/choose_operator.lean) | `choose` (#18) | Verus `trigger_loops` (`choose_example`, `quantifier_example`) | Implemented (#1075) | | [`higher_order_encoding.lean`](../StrataTest/Languages/Boole/FeatureRequests/higher_order_encoding.lean) | Higher-order values (#17) | Verus `fun_ext`, `trait_for_fn` | Active | | [`lambda_closure.lean`](../StrataTest/Languages/Boole/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 | From 932f7efb574de524278d88cd162e64787a188394 Mon Sep 17 00:00:00 2001 From: Lydia Kondylidou <33327056+kondylidou@users.noreply.github.com> Date: Tue, 19 May 2026 17:13:30 +0200 Subject: [PATCH 02/20] feat(Boole): type nat := int synonym + auto non-negativity axioms MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Collect nullary type synonyms whose RHS is `int` (e.g. `type nat := int`) in a pre-pass into `TranslateState.natSynonyms`. For each non-parameterised datatype whose constructor has a `nat`-typed field, automatically emit a Core axiom: ∀ x : DT . DT..isCtor(x) ⟹ DT..field(x) ≥ 0 `isNatType` recognises these fields; `toCoreTypedBin`/`toCoreTypedUn` route nat-typed arithmetic to `Int.*` ops instead of the BV path. New test files: - cast_nested.lean — as_int in quantifier bodies, compound BV exprs, let bindings, exists, and a rec function with decreases (16 VCs pass) - nat_axiom_discussion.lean — meeting document: working NatList case, the mixed nat/int Pair soundness hole, the minimal SMT reproducer, and four design alternatives (A–D) - from_bytes_mod_order_wide_minimal.lean — B2 seed: bytes_seq_as_nat / seq_as_nat_52 using as_int (107 pass, 6 unknown for abstract UFs) Co-Authored-By: Claude Sonnet 4.6 --- Strata/Languages/Boole/Verify.lean | 77 ++++- .../Boole/FeatureRequests/cast_nested.lean | 162 +++++++++++ .../FeatureRequests/nat_axiom_discussion.lean | 179 ++++++++++++ .../from_bytes_mod_order_wide_minimal.lean | 275 ++++++++++++++++++ 4 files changed, 689 insertions(+), 4 deletions(-) create mode 100644 StrataTest/Languages/Boole/FeatureRequests/cast_nested.lean create mode 100644 StrataTest/Languages/Boole/FeatureRequests/nat_axiom_discussion.lean create mode 100644 StrataTest/Languages/Boole/from_bytes_mod_order_wide_minimal.lean diff --git a/Strata/Languages/Boole/Verify.lean b/Strata/Languages/Boole/Verify.lean index fe5268ce65..de5d54f13f 100644 --- a/Strata/Languages/Boole/Verify.lean +++ b/Strata/Languages/Boole/Verify.lean @@ -50,6 +50,10 @@ structure TranslateState where `getFVarIsOp` as the `command_var` carve-out for op-vs-var classification. -/ globalVarTypes : Std.HashMap String Lambda.LMonoTy := {} + /-- Names of nullary type synonyms that expand directly to `int`, collected + in a pre-pass. A field whose Boole type resolves to one of these names + is treated as `nat` and gets an automatic non-negativity axiom. -/ + natSynonyms : Std.HashSet String := {} abbrev TranslateM := StateT TranslateState (Except DiagnosticModel) @@ -256,6 +260,13 @@ def toCoreMonoType (t : Boole.Type) : TranslateM Lambda.LMonoTy := do def toCoreType (t : Boole.Type) : TranslateM Core.Expression.Ty := do return .forAll [] (← toCoreMonoType t) +private def isNatType (t : Boole.Type) : TranslateM Bool := do + match t with + | .fvar m i _ => + let name ← getFVarName m i + return (← get).natSynonyms.contains name + | _ => return false + private def toCoreBinding (b : BooleDDM.Binding SourceRange) : TranslateM (Core.Expression.Ident × Lambda.LMonoTy) := do match b with | .mkBinding _ ⟨_, n⟩ tp | .outBinding _ ⟨_, n⟩ tp @@ -306,7 +317,10 @@ def toCoreTypedUn (m : SourceRange) (ty : Boole.Type) (op : String) (a : Core.Ex | .int _ => let iop : Core.Expression.Expr := .op () ⟨s!"Int.{op}", ()⟩ none return .app () iop a - | _ => toCoreBvUn m ty op a + | _ => + if ← isNatType ty then + return .app () (.op () ⟨s!"Int.{op}", ()⟩ none) a + else toCoreBvUn m ty op a -- Bitvector comparison operators use unsigned variants by default (Le→ULe, etc.). -- Signed variants use the explicit bvslt/bvsle nodes. @@ -320,7 +334,10 @@ def toCoreTypedBin (m : SourceRange) (ty : Boole.Type) (op : String) (a b : Core | .int _ => let iop : Core.Expression.Expr := .op () ⟨s!"Int.{op}", ()⟩ none return mkCoreApp iop [a, b] - | _ => toCoreBvBin m ty (toBvCmpOp op) a b + | _ => + if ← isNatType ty then + return mkCoreApp (.op () ⟨s!"Int.{op}", ()⟩ none) [a, b] + else toCoreBvBin m ty (toBvCmpOp op) a b private def toCoreExtensionalEq (m : SourceRange) @@ -821,6 +838,43 @@ private def toCoreDatatype constrs := constrs constrs_ne := by simp } +-- For each constructor field whose Boole type is nat-like, emit an axiom: +-- ∀ x : DatatypeName . DatatypeName..isCtor(x) ⟹ DatatypeName..field(x) ≥ 0 +-- Only generated for datatypes without type parameters (parameterised datatypes +-- would require type-level quantification not currently supported here). +private def natAxiomsForDatatype + (dtypeName : String) + (typeParams : List String) + (ctors : BooleDDM.ConstructorList SourceRange) : TranslateM (List Core.Decl) := do + if !typeParams.isEmpty then return [] + let dtypeTy : Lambda.LMonoTy := .tcons dtypeName [] + let bv0 : Core.Expression.Expr := .bvar () 0 + let mut axioms : List Core.Decl := [] + for ctor in constructorListToList ctors do + match ctor with + | .constructor_mk _ ⟨_, cname⟩ ⟨_, fields?⟩ => + let fields : List (BooleDDM.Binding SourceRange) := match fields? with + | none => [] + | some ⟨_, fs⟩ => fs.toList + let testerName := s!"{dtypeName}..is{cname}" + for field in fields do + match field with + | .mkBinding _ ⟨_, fieldName⟩ tp => + match tp with + | .expr fieldTy => + if ← isNatType fieldTy then + let selectorName := s!"{dtypeName}..{fieldName}" + let tester := mkCoreApp (.op () ⟨testerName, ()⟩ none) [bv0] + let selector := mkCoreApp (.op () ⟨selectorName, ()⟩ none) [bv0] + let geZero := mkCoreApp Core.intGeOp [selector, .intConst () 0] + let implies := mkCoreApp Core.boolImpliesOp [tester, geZero] + let axExpr : Core.Expression.Expr := .quant () .all "" (some dtypeTy) bv0 implies + let axName := s!"{dtypeName}_{cname}_{fieldName}_nonneg" + axioms := axioms ++ [.ax { name := axName, e := axExpr } .empty] + | _ => pure () + | _ => pure () + return axioms + private def toCoreDatatypeDecl (decl : BooleDDM.DatatypeDecl SourceRange) : TranslateM (Lambda.LDatatype Unit) := do match decl with | .datatype_decl m ⟨_, dtypeName⟩ ⟨_, typeParams?⟩ ctors => @@ -1020,7 +1074,15 @@ def toCoreDecls (cmd : BooleDDM.Command SourceRange) : TranslateM (List Core.Dec body := ← toCoreBlock b } .empty] | .command_datatypes _ ⟨_, decls⟩ => - return [.type (.data (← decls.toList.mapM toCoreDatatypeDecl)) .empty] + let datatypes ← decls.toList.mapM toCoreDatatypeDecl + let natAxioms ← decls.toList.mapM fun decl => + match decl with + | .datatype_decl _ ⟨_, dtypeName⟩ ⟨_, typeParams?⟩ ctors => + let typeParams := match typeParams? with + | none => [] + | some bs => (bindingsToList bs).map bindingName + withTypeBVars typeParams (natAxiomsForDatatype dtypeName typeParams ctors) + return .type (.data datatypes) .empty :: natAxioms.flatten /-- Render a `Boole.Program` to a format object using the provided `GlobalContext` and `DialectMap`. These should come from the originating `Strata.Program` (i.e. `env.globalContext` @@ -1040,9 +1102,10 @@ def formatProgram (prog : Boole.Program) (gctx : GlobalContext) (dialects : Dial def toCoreProgram (p : Boole.Program) (gctx : GlobalContext := {}) (fileName : String := "") : Except DiagnosticModel Core.Program := do match p with | .prog _ ⟨_, cmds⟩ => - -- Pre-pass: collect global variable types and modifies info per procedure. + -- Pre-pass: collect global variable types, modifies info, and nat synonyms. let mut varTypes : Std.HashMap String Lambda.LMonoTy := {} let mut modMap : Std.HashMap String (List (Core.Expression.Ident × Lambda.LMonoTy)) := {} + let mut natSynonyms : Std.HashSet String := {} for cmd in cmds do match cmd with | .command_var _ b => @@ -1057,12 +1120,18 @@ def toCoreProgram (p : Boole.Program) (gctx : GlobalContext := {}) (fileName : S | .command_procedure _ nameAnn _ _ specAnn _ => let mods ← collectModifiesFromSpec fileName nameAnn.val specAnn.val varTypes if !mods.isEmpty then modMap := modMap.insert nameAnn.val mods + | .command_typesynonym _ ⟨_, n⟩ ⟨_, args?⟩ _ rhs => + if args?.isNone then + match (toCoreMonoType rhs).run' { gctx := gctx } with + | .ok .int => natSynonyms := natSynonyms.insert n + | _ => pure () | _ => pure () let init : TranslateState := { fileName := fileName gctx := gctx modifiesMap := modMap globalVarTypes := varTypes + natSynonyms := natSynonyms } let act : TranslateM Core.Program := do let decls := (← cmds.mapM toCoreDecls).toList.flatten diff --git a/StrataTest/Languages/Boole/FeatureRequests/cast_nested.lean b/StrataTest/Languages/Boole/FeatureRequests/cast_nested.lean new file mode 100644 index 0000000000..80e495f673 --- /dev/null +++ b/StrataTest/Languages/Boole/FeatureRequests/cast_nested.lean @@ -0,0 +1,162 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import Strata.MetaVerifier + +open Strata + +/- +Near-upstream anchor: dalek-lite `bytes_seq_as_nat` / `seq_as_nat_52` (B2). + +Exercises `e as_int` in contexts beyond the flat `x as_int` covered by +`cast_expr.lean`: + +- Cast inside a ∀-quantifier body over a sequence +- Cast of a compound BV expression (bitwise &) +- Cast in an arithmetic sum bound +- Cast inside a `let_in_expr` binding +- Cast inside a ∃-quantifier body +- Cast inside a `rec function` body with `decreases`, plus axiom-backed + properties (single-byte decode and empty-sequence base case) +-/ + +private def castNestedSeed : Strata.Program := +#strata +program Boole; + +procedure cast_in_forall(s: Sequence bv8, n: int) returns () +spec { + requires 0 <= n && n <= Sequence.length(s); + ensures ∀ i: int . 0 <= i && i < n ==> (Sequence.select(s, i) as_int) < 256; +} +{ + assert ∀ i: int . 0 <= i && i < n ==> (Sequence.select(s, i) as_int) < 256; +}; + +procedure cast_compound_bv(a: bv8, b: bv8) returns () +spec { + ensures 0 <= ((a & b) as_int); + ensures ((a & b) as_int) < 256; +} +{ + assert 0 <= ((a & b) as_int); + assert ((a & b) as_int) < 256; +}; + +procedure cast_sum_bound(a: bv8, b: bv8) returns () +spec { + ensures (a as_int) + (b as_int) < 512; +} +{ + assert (a as_int) + (b as_int) < 512; +}; + +procedure cast_in_let(x: bv8) returns () +spec { + ensures let n : int := (x as_int) in n >= 0 && n < 256; +} +{ + assert let n : int := (x as_int) in n >= 0 && n < 256; +}; + +procedure cast_in_exists(s: Sequence bv64) returns () +spec { + requires Sequence.length(s) > 0; + ensures ∃ i: int . 0 <= i && i < Sequence.length(s) && (Sequence.select(s, i) as_int) >= 0; +} +{ + assert ∃ i: int . 0 <= i && i < Sequence.length(s) && (Sequence.select(s, i) as_int) >= 0; +}; + +rec function bytes_to_nat(s: Sequence bv8) : int + decreases Sequence.length(s) +{ + if Sequence.length(s) == 0 then 0 + else (Sequence.select(s, 0) as_int) + 256 * bytes_to_nat(Sequence.skip(s, 1)) +} +; + +axiom bytes_to_nat(Sequence.empty_bv8) == 0; +axiom (∀ h: bv8 . ∀ t: Sequence bv8 . + bytes_to_nat(Sequence.build(t, h)) == (h as_int) + 256 * bytes_to_nat(t)); + +procedure test_rec_empty() returns () +spec { + ensures bytes_to_nat(Sequence.empty_bv8) == 0; +} { exit test_rec_empty; }; + +procedure test_rec_single_byte(x: bv8) returns () +spec { + ensures bytes_to_nat(Sequence.build(Sequence.empty_bv8, x)) == (x as_int); +} { exit test_rec_single_byte; }; +#end + +/-- info: +Obligation: assert_2_915 +Property: assert +Result: ✅ pass + +Obligation: cast_in_forall_ensures_1_829 +Property: assert +Result: ✅ pass + +Obligation: assert_5_1132 +Property: assert +Result: ✅ pass + +Obligation: assert_6_1164 +Property: assert +Result: ✅ pass + +Obligation: cast_compound_bv_ensures_3_1061 +Property: assert +Result: ✅ pass + +Obligation: cast_compound_bv_ensures_4_1094 +Property: assert +Result: ✅ pass + +Obligation: assert_8_1305 +Property: assert +Result: ✅ pass + +Obligation: cast_sum_bound_ensures_7_1260 +Property: assert +Result: ✅ pass + +Obligation: assert_10_1459 +Property: assert +Result: ✅ pass + +Obligation: cast_in_let_ensures_9_1397 +Property: assert +Result: ✅ pass + +Obligation: assert_13_1717 +Property: assert +Result: ✅ pass + +Obligation: cast_in_exists_ensures_12_1616 +Property: assert +Result: ✅ pass + +Obligation: bytes_to_nat_terminates_0 +Property: assert +Result: ✅ pass + +Obligation: bytes_to_nat_terminates_1 +Property: assert +Result: ✅ pass + +Obligation: test_rec_empty_ensures_16_2232 +Property: assert +Result: ✅ pass + +Obligation: test_rec_single_byte_ensures_17_2367 +Property: assert +Result: ✅ pass-/ +#guard_msgs in +#eval Strata.Boole.verify "cvc5" castNestedSeed (options := .quiet) diff --git a/StrataTest/Languages/Boole/FeatureRequests/nat_axiom_discussion.lean b/StrataTest/Languages/Boole/FeatureRequests/nat_axiom_discussion.lean new file mode 100644 index 0000000000..d16d171428 --- /dev/null +++ b/StrataTest/Languages/Boole/FeatureRequests/nat_axiom_discussion.lean @@ -0,0 +1,179 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import Strata.MetaVerifier + +open Strata + +/- +Meeting discussion: `type nat := int` + auto-generated non-negativity axioms + +Abdal's proposed design +─────────────────────── + type nat := int; + datatype NatList { Nil(), Cons(head: nat, tail: NatList) }; + -- auto-generated: + axiom (∀ l : NatList :: NatList..isCons(l) ==> NatList..head(l) >= 0) + +The auto-axiom lets any procedure that receives a NatList immediately derive +`head(l) >= 0` from `isCons(l)`, without a manual assumes/requires. + +──────────────────────────────────────────────────────────────────────────── +CASE 1 — WORKS: homogeneous nat-field list +──────────────────────────────────────────────────────────────────────────── +NatList has only `nat` fields. The auto-axiom fires and the postcondition +`head(l) >= 0` is proved without a manual requires. ✅ intended behaviour. +-/ + +private def natListCase : Strata.Program := +#strata +program Boole; + +type nat := int; + +datatype NatList { + Nil(), + Cons(head: nat, tail: NatList) +}; + +procedure use_nat_list(l: NatList) returns () +spec { + requires NatList..isCons(l); + ensures NatList..head(l) >= 0; +} { + exit use_nat_list; +}; +#end + +/-- info: +Obligation: use_nat_list_post_use_nat_list_ensures_1_373_calls_NatList..head_0 +Property: assert +Result: ✅ pass + +Obligation: use_nat_list_ensures_1_373 +Property: assert +Result: ✅ pass-/ +#guard_msgs in +#eval Strata.Boole.verify "cvc5" natListCase (options := .quiet) + +/- +──────────────────────────────────────────────────────────────────────────── +CASE 2 — BROKEN: mixed nat/int fields in the same datatype +──────────────────────────────────────────────────────────────────────────── +`Pair` has `first : nat` (gets the auto-axiom) and `second : int` (does not). + +The auto-axiom emitted is: + ∀ x : Pair . Pair..isPair_mk(x) ==> Pair..first(x) >= 0 + +Problem: the SMT solver (cvc5 1.3.3) can instantiate this forall with the +synthetic term x := Pair_mk(Pair_second(p), 0). +By the ADT selector axiom, Pair_first(Pair_mk(Pair_second(p), 0)) = Pair_second(p). +So the axiom instance becomes: Pair_second(p) >= 0. + +This means ANY query that contains both this datatype and a negative `int` +value becomes inconsistent in the SMT model — even when `second` is +completely unrelated to `first`. + +Illustration: the procedure below has precondition `second(p) < 0` and +postcondition `second(p) >= 0`, which is logically false. But it passes (✅) +because the auto-axiom makes the SMT context inconsistent. +This is a soundness hole for the mixed-field case. +-/ + +private def mixedPairCase : Strata.Program := +#strata +program Boole; + +type nat := int; + +datatype Pair { + Pair_mk(first: nat, second: int) +}; + +procedure unsound_example(p: Pair) returns () +spec { + requires Pair..isPair_mk(p) && Pair..second(p) < 0; + ensures Pair..second(p) >= 0; +} { + exit unsound_example; +}; +#end + +-- ⚠️ This should be ❌ fail but is ✅ pass — the auto-axiom is too strong. +/-- info: +Obligation: unsound_example_pre_unsound_example_requires_0_318_calls_Pair..second_0 +Property: assert +Result: ✅ pass + +Obligation: unsound_example_post_unsound_example_ensures_1_393_calls_Pair..second_0 +Property: assert +Result: ✅ pass + +Obligation: unsound_example_ensures_1_393 +Property: assert +Result: ✅ pass-/ +#guard_msgs in +#eval Strata.Boole.verify "cvc5" mixedPairCase (options := .quiet) + +/- +Why it happens — the minimal SMT formula +───────────────────────────────────────── +The SMT problem sent to cvc5 for `unsound_example_ensures` is: + + (set-logic ALL) + (declare-datatype Pair ((Pair_mk (Pair..first Int) (Pair..second Int)))) + ; auto-axiom for first : nat + (assert (forall (($bv0 Pair)) (=> (|is-Pair_mk| $bv0) (>= (Pair..first $bv0) 0)))) + ; precondition + (assert (and (|is-Pair_mk| p) (< (Pair..second p) 0))) + ; negated goal (validity check) + (assert (not (>= (Pair..second p) 0))) + (check-sat) ; → unsat (should be sat) + +Manually verified: `cvc5 min.smt2` returns `unsat` with this formula. +Without the forall assert it returns `sat` (correct). + +Root cause: the `forall` is a global SMT assertion over ALL Pair terms in +the universe, including synthetic ones. Instantiating with + $bv0 := Pair_mk(Pair..second(p), 0) +gives Pair..first(Pair_mk(Pair..second(p), 0)) >= 0, +which simplifies to Pair..second(p) >= 0 (by the ADT selector axiom). +This contradicts Pair..second(p) < 0, making the context inconsistent. + +──────────────────────────────────────────────────────────────────────────── +DESIGN ALTERNATIVES — discussion points for the meeting +──────────────────────────────────────────────────────────────────────────── + +Option A — Status quo + documented restriction + Keep the auto-axiom. Document that `nat` fields must not be mixed with + unconstrained `int` fields in the same datatype when the `nat` axiom is + active. Works for all five dalek-lite benchmarks (B1–B5) since their + `nat`-like fields are either separate datatypes or all-`nat` constructors. + Simplest path; no SMT change required. + +Option B — Distinct abstract type (existing nat_int_boundary.lean approach) + Keep `type nat;` as an abstract sort (not a synonym for int). + Add explicit coercions: + function nat_to_int(n: nat) : int; + axiom (∀ n : nat . nat_to_int(n) >= 0); -- one axiom, no ADT interaction + `nat` and `int` live in separate SMT sorts — no quantifier instantiation + issue. Downside: every use of a `nat` field requires an explicit + `nat_to_int` call, adding coercion noise to specs. + +Option C — Constructor-site preconditions instead of a global axiom + Don't emit a global forall axiom. Instead, when a procedure receives a + datatype value, add a ghost `requires` (or an `assume`) that the `nat` + fields are non-negative. This is local and never interacts with unrelated + `int` values. Downside: either the user must state it manually, or the + translator must detect "datatype parameter" inputs and inject the assumes + automatically — more complex but semantically precise. + +Option D — Keep auto-axiom but restrict it to programs with no bare `int` fields + Only emit the nonneg axiom if ALL non-recursive fields of the datatype are + `nat` (or other non-negative types). Mixed nat/int datatypes fall back to + Option B or C. Conservative; avoids the soundness hole without any SMT + change. +-/ diff --git a/StrataTest/Languages/Boole/from_bytes_mod_order_wide_minimal.lean b/StrataTest/Languages/Boole/from_bytes_mod_order_wide_minimal.lean new file mode 100644 index 0000000000..135810ce8e --- /dev/null +++ b/StrataTest/Languages/Boole/from_bytes_mod_order_wide_minimal.lean @@ -0,0 +1,275 @@ +import Strata.MetaVerifier + +open Strata + +private def from_bytes_mod_order_wide_minimal_program : Strata.Program := +#strata +program Boole; + + type Set (T : Type); + function Seq_len (s : Sequence T) : int { + Sequence.length(s) +} + function Seq_lib_insert (s : Sequence T, i : int, val : T) : Sequence T { + Sequence.append(Sequence.build(Sequence.take(s, i), val), Sequence.drop(s, i)) +} + function Seq_new (len : int, f : int -> T) : Sequence T; + function Seq_lib_map (s : Sequence T, f : int -> T -> U) : Sequence U; + function Seq_lib_map_values (s : Sequence T, f : T -> U) : Sequence U; + function Seq_lib_filter (s : Sequence T, p : T -> bool) : Sequence T; + function Seq_lib_sort_by (s : Sequence T, less : T -> T -> bool) : Sequence T; + function Seq_lib_to_set (s : Sequence T) : Set T; + function Set_finite (s : Set T) : bool; + datatype scalar { + scalar_ctor(bytes : Sequence bv8) +}; + datatype scalar52 { + scalar52_ctor(limbs : Sequence bv64) +}; + function Seq_subrange (self : Sequence A, start_inclusive : int, end_exclusive : int) : Sequence A; + function Array_spec_array_as_slice (ar : Sequence T) : Sequence T; + function Arithmetic_Power2_pow2 (e : int) : int; + function is_uniform_bytes (bytes : Sequence bv8) : bool; + function is_uniform_scalar (s : scalar) : bool; + rec function bytes_seq_as_nat (bytes : Sequence bv8) : int + decreases Sequence.length(bytes) + { + if Sequence.length(bytes) == 0 then 0 else (Sequence.select(bytes, 0) as_int) + Arithmetic_Power2_pow2(8) * bytes_seq_as_nat(Sequence.subrange(bytes, 1, Sequence.length(bytes))) + } + ; + function u8_32_as_nat (bytes : Sequence bv8) : int; + function group_order () : int; + function group_canonical (n : int) : int; + rec function seq_as_nat_52 (limbs : Sequence bv64) : int + decreases Sequence.length(limbs) + { + if Sequence.length(limbs) == 0 then 0 else (Sequence.select(limbs, 0) as_int) + seq_as_nat_52(Sequence.subrange(limbs, 1, Sequence.length(limbs))) * Arithmetic_Power2_pow2(52) + } + ; + function limbs52_as_nat (limbs : Sequence bv64) : int { + seq_as_nat_52(limbs) +} + function scalar52_as_nat (s : scalar52) : int { + limbs52_as_nat(Array_spec_array_as_slice(scalar52..limbs(s))) +} + function limbs_bounded (s : scalar52) : bool { + ∀ i : int :: 0 <= i && i < 5 ==> Sequence.select(scalar52..limbs(s), i) < bv{64}(1) << bv{64}(52) +} + function is_canonical_scalar52 (s : scalar52) : bool { + limbs_bounded(s) && scalar52_as_nat(s) < group_order +} + function is_canonical_scalar (s : scalar) : bool { + u8_32_as_nat(scalar..bytes(s)) < group_order && Sequence.select(scalar..bytes(s), 31) <= bv{8}(127) +} + function scalar_as_canonical (s : scalar) : int { + group_canonical(u8_32_as_nat(scalar..bytes(s))) +} + procedure Impl__2_clone (self : scalar52) returns (_pct_return : scalar52) +spec { + ensures _pct_return == self; + } { + _pct_return := self; + exit Impl__2_clone; +}; + procedure Impl__3_from_bytes_wide (bytes : Sequence bv8) returns (s : scalar52) +spec { + ensures is_canonical_scalar52(s); + ensures scalar52_as_nat(s) == group_canonical(bytes_seq_as_nat(bytes)); + } { + assume false; + s := scalar52_ctor(Sequence.of_bv64[bv{64}(0), bv{64}(0), bv{64}(0), bv{64}(0), bv{64}(0)]); + exit Impl__3_from_bytes_wide; +}; + procedure Impl__3_pack (self : scalar52) returns (result : scalar) +spec { + requires limbs_bounded(self); + ensures u8_32_as_nat(scalar..bytes(result)) == scalar52_as_nat(self) mod Arithmetic_Power2_pow2(256); + ensures scalar52_as_nat(self) < group_order ==> is_canonical_scalar(result); + } { + assume false; + result := scalar_ctor(scalar..bytes(result)); + exit Impl__3_pack; +}; + procedure Impl__4_from_bytes_mod_order_wide (input : Sequence bv8) returns (result : scalar) +spec { + ensures scalar_as_canonical(result) == group_canonical(bytes_seq_as_nat(input)); + ensures is_canonical_scalar(result); + ensures is_uniform_bytes(input) ==> is_uniform_scalar(result); + } { + var tmp1 : int; + var tmp2 : int; + var tmp3 : int; + var tmp4 : int; + var tmp5 : int; + var tmp6 : int; + var unpacked : scalar52; + call unpacked := Impl__3_from_bytes_wide(input); + call result := Impl__3_pack(unpacked); + call lemma_group_order_smaller_than_pow256(); + call lemma_scalar52_lt_pow2_256_if_canonical(unpacked); + tmp1 := scalar52_as_nat(unpacked); + tmp2 := Arithmetic_Power2_pow2(256); + call Arithmetic_Div_mod_lemma_small_mod(tmp1, tmp2); + tmp3 := bytes_seq_as_nat(input); + tmp4 := group_order; + call Arithmetic_Div_mod_lemma_mod_bound(tmp3, tmp4); + tmp5 := u8_32_as_nat(scalar..bytes(result)); + tmp6 := group_order; + call Arithmetic_Div_mod_lemma_small_mod(tmp5, tmp6); + call axiom_uniform_mod_reduction(input, result); + result := result; + exit Impl__4_from_bytes_mod_order_wide; +}; + procedure Arithmetic_Div_mod_lemma_small_mod (x : int, m : int) returns () +spec { + requires x < m; + requires 0 < m; + ensures x mod m == x; + } { + assume false; +}; + procedure Arithmetic_Div_mod_lemma_mod_bound (x : int, m : int) returns () +spec { + requires 0 < m; + ensures 0 <= x mod m && x mod m < m; + } { + assume false; +}; + procedure Arithmetic_Power2_lemma_pow2_adds (e1 : int, e2 : int) returns () +spec { + ensures Arithmetic_Power2_pow2(e1 + e2) == Arithmetic_Power2_pow2(e1) * Arithmetic_Power2_pow2(e2); + } { + assume false; +}; + procedure Arithmetic_Power2_lemma_pow2_strictly_increases (e1 : int, e2 : int) returns () +spec { + requires e1 < e2; + ensures Arithmetic_Power2_pow2(e1) < Arithmetic_Power2_pow2(e2); + } { + assume false; +}; + procedure Arithmetic_Power2_lemma2_to64 () returns () +spec { + ensures Arithmetic_Power2_pow2(0) == 1; + ensures Arithmetic_Power2_pow2(1) == 2; + ensures Arithmetic_Power2_pow2(2) == 4; + ensures Arithmetic_Power2_pow2(3) == 8; + ensures Arithmetic_Power2_pow2(4) == 16; + ensures Arithmetic_Power2_pow2(5) == 32; + ensures Arithmetic_Power2_pow2(6) == 64; + ensures Arithmetic_Power2_pow2(7) == 128; + ensures Arithmetic_Power2_pow2(8) == 256; + ensures Arithmetic_Power2_pow2(9) == 512; + ensures Arithmetic_Power2_pow2(10) == 1024; + ensures Arithmetic_Power2_pow2(11) == 2048; + ensures Arithmetic_Power2_pow2(12) == 4096; + ensures Arithmetic_Power2_pow2(13) == 8192; + ensures Arithmetic_Power2_pow2(14) == 16384; + ensures Arithmetic_Power2_pow2(15) == 32768; + ensures Arithmetic_Power2_pow2(16) == 65536; + ensures Arithmetic_Power2_pow2(17) == 131072; + ensures Arithmetic_Power2_pow2(18) == 262144; + ensures Arithmetic_Power2_pow2(19) == 524288; + ensures Arithmetic_Power2_pow2(20) == 1048576; + ensures Arithmetic_Power2_pow2(21) == 2097152; + ensures Arithmetic_Power2_pow2(22) == 4194304; + ensures Arithmetic_Power2_pow2(23) == 8388608; + ensures Arithmetic_Power2_pow2(24) == 16777216; + ensures Arithmetic_Power2_pow2(25) == 33554432; + ensures Arithmetic_Power2_pow2(26) == 67108864; + ensures Arithmetic_Power2_pow2(27) == 134217728; + ensures Arithmetic_Power2_pow2(28) == 268435456; + ensures Arithmetic_Power2_pow2(29) == 536870912; + ensures Arithmetic_Power2_pow2(30) == 1073741824; + ensures Arithmetic_Power2_pow2(31) == 2147483648; + ensures Arithmetic_Power2_pow2(32) == 4294967296; + ensures Arithmetic_Power2_pow2(64) == 18446744073709551616; + } { + assume false; +}; + procedure Arithmetic_Power2_lemma2_to64_rest () returns () +spec { + ensures Arithmetic_Power2_pow2(33) == 8589934592; + ensures Arithmetic_Power2_pow2(34) == 17179869184; + ensures Arithmetic_Power2_pow2(35) == 34359738368; + ensures Arithmetic_Power2_pow2(36) == 68719476736; + ensures Arithmetic_Power2_pow2(37) == 137438953472; + ensures Arithmetic_Power2_pow2(38) == 274877906944; + ensures Arithmetic_Power2_pow2(39) == 549755813888; + ensures Arithmetic_Power2_pow2(40) == 1099511627776; + ensures Arithmetic_Power2_pow2(41) == 2199023255552; + ensures Arithmetic_Power2_pow2(42) == 4398046511104; + ensures Arithmetic_Power2_pow2(43) == 8796093022208; + ensures Arithmetic_Power2_pow2(44) == 17592186044416; + ensures Arithmetic_Power2_pow2(45) == 35184372088832; + ensures Arithmetic_Power2_pow2(46) == 70368744177664; + ensures Arithmetic_Power2_pow2(47) == 140737488355328; + ensures Arithmetic_Power2_pow2(48) == 281474976710656; + ensures Arithmetic_Power2_pow2(49) == 562949953421312; + ensures Arithmetic_Power2_pow2(50) == 1125899906842624; + ensures Arithmetic_Power2_pow2(51) == 2251799813685248; + ensures Arithmetic_Power2_pow2(52) == 4503599627370496; + ensures Arithmetic_Power2_pow2(53) == 9007199254740992; + ensures Arithmetic_Power2_pow2(54) == 18014398509481984; + ensures Arithmetic_Power2_pow2(55) == 36028797018963968; + ensures Arithmetic_Power2_pow2(56) == 72057594037927936; + ensures Arithmetic_Power2_pow2(57) == 144115188075855872; + ensures Arithmetic_Power2_pow2(58) == 288230376151711744; + ensures Arithmetic_Power2_pow2(59) == 576460752303423488; + ensures Arithmetic_Power2_pow2(60) == 1152921504606846976; + ensures Arithmetic_Power2_pow2(61) == 2305843009213693952; + ensures Arithmetic_Power2_pow2(62) == 4611686018427387904; + ensures Arithmetic_Power2_pow2(63) == 9223372036854775808; + ensures Arithmetic_Power2_pow2(64) == 18446744073709551616; + } { + assume false; +}; + procedure lemma_group_order_bound () returns () +spec { + ensures group_order < Arithmetic_Power2_pow2(255); + } { + assume 27742317777372353535851937790883648493 < 85070591730234615865843651857942052864; + call Arithmetic_Power2_lemma2_to64_rest(); + assert Arithmetic_Power2_pow2(63) == 9223372036854775808; + assume Arithmetic_Power2_pow2(63) == 9223372036854775808; + call Arithmetic_Power2_lemma_pow2_adds(63, 63); + assert Arithmetic_Power2_pow2(126) == 85070591730234615865843651857942052864; + assert 27742317777372353535851937790883648493 < Arithmetic_Power2_pow2(126); + call Arithmetic_Power2_lemma_pow2_strictly_increases(126, 252); + assert group_order < Arithmetic_Power2_pow2(252) + Arithmetic_Power2_pow2(252); + call Arithmetic_Power2_lemma_pow2_adds(1, 252); + call Arithmetic_Power2_lemma2_to64(); + assert Arithmetic_Power2_pow2(252) + Arithmetic_Power2_pow2(252) == Arithmetic_Power2_pow2(253); + assume Arithmetic_Power2_pow2(252) + Arithmetic_Power2_pow2(252) == Arithmetic_Power2_pow2(253); + call Arithmetic_Power2_lemma_pow2_strictly_increases(253, 255); + exit lemma_group_order_bound; +}; + procedure lemma_group_order_smaller_than_pow256 () returns () +spec { + ensures group_order < Arithmetic_Power2_pow2(256); + } { + call lemma_group_order_bound(); + call Arithmetic_Power2_lemma_pow2_strictly_increases(255, 256); + exit lemma_group_order_smaller_than_pow256; +}; + procedure lemma_scalar52_lt_pow2_256_if_canonical (a : scalar52) returns () +spec { + requires limbs_bounded(a); + requires scalar52_as_nat(a) < group_order; + ensures scalar52_as_nat(a) < Arithmetic_Power2_pow2(256); + } { + call lemma_group_order_bound(); + call Arithmetic_Power2_lemma_pow2_strictly_increases(255, 256); + exit lemma_scalar52_lt_pow2_256_if_canonical; +}; + procedure axiom_uniform_mod_reduction (input : Sequence bv8, result : scalar) returns () +spec { + requires scalar_as_canonical(result) == bytes_seq_as_nat(input) mod group_order; + ensures is_uniform_bytes(input) ==> is_uniform_scalar(result); + } { + assume false; + exit axiom_uniform_mod_reduction; +}; +#end + +#eval Strata.Boole.verify "cvc5" from_bytes_mod_order_wide_minimal_program (options := .quiet) From 23e7403c56404f705156945eefefacc1030c6906 Mon Sep 17 00:00:00 2001 From: Lydia Kondylidou <33327056+kondylidou@users.noreply.github.com> Date: Tue, 19 May 2026 17:42:24 +0200 Subject: [PATCH 03/20] fix(B2): close all 6 unknown VCs in from_bytes_mod_order_wide_minimal - Drop dead declarations (Seq_new, Seq_lib_map, Seq_lib_filter, etc.) that were never called in any VC and would crash the SMT encoder if they ever were (arrow-typed parameters) - Define group_order as its concrete Ed25519 prime value - Define group_canonical(n) := n mod group_order (from Verus source) - Add assume Arithmetic_Power2_pow2(252) == 2^252 inside lemma_group_order_bound so the assert group_order < 2*pow2(252) can be discharged by integer arithmetic Result: 113 pass, 0 fail, 0 unknown (was 107/0/6) Co-Authored-By: Claude Sonnet 4.6 --- .../from_bytes_mod_order_wide_minimal.lean | 23 ++++++------------- 1 file changed, 7 insertions(+), 16 deletions(-) diff --git a/StrataTest/Languages/Boole/from_bytes_mod_order_wide_minimal.lean b/StrataTest/Languages/Boole/from_bytes_mod_order_wide_minimal.lean index 135810ce8e..b39083c3fa 100644 --- a/StrataTest/Languages/Boole/from_bytes_mod_order_wide_minimal.lean +++ b/StrataTest/Languages/Boole/from_bytes_mod_order_wide_minimal.lean @@ -6,20 +6,6 @@ private def from_bytes_mod_order_wide_minimal_program : Strata.Program := #strata program Boole; - type Set (T : Type); - function Seq_len (s : Sequence T) : int { - Sequence.length(s) -} - function Seq_lib_insert (s : Sequence T, i : int, val : T) : Sequence T { - Sequence.append(Sequence.build(Sequence.take(s, i), val), Sequence.drop(s, i)) -} - function Seq_new (len : int, f : int -> T) : Sequence T; - function Seq_lib_map (s : Sequence T, f : int -> T -> U) : Sequence U; - function Seq_lib_map_values (s : Sequence T, f : T -> U) : Sequence U; - function Seq_lib_filter (s : Sequence T, p : T -> bool) : Sequence T; - function Seq_lib_sort_by (s : Sequence T, less : T -> T -> bool) : Sequence T; - function Seq_lib_to_set (s : Sequence T) : Set T; - function Set_finite (s : Set T) : bool; datatype scalar { scalar_ctor(bytes : Sequence bv8) }; @@ -38,8 +24,12 @@ program Boole; } ; function u8_32_as_nat (bytes : Sequence bv8) : int; - function group_order () : int; - function group_canonical (n : int) : int; + function group_order () : int { + 7237005577332262213973186563042994240857116359379907606001950938285454250989 +} + function group_canonical (n : int) : int { + n mod group_order +} rec function seq_as_nat_52 (limbs : Sequence bv64) : int decreases Sequence.length(limbs) { @@ -236,6 +226,7 @@ spec { assert Arithmetic_Power2_pow2(126) == 85070591730234615865843651857942052864; assert 27742317777372353535851937790883648493 < Arithmetic_Power2_pow2(126); call Arithmetic_Power2_lemma_pow2_strictly_increases(126, 252); + assume Arithmetic_Power2_pow2(252) == 7237005577332262213973186563042994240829374041602535252466099000494570602496; assert group_order < Arithmetic_Power2_pow2(252) + Arithmetic_Power2_pow2(252); call Arithmetic_Power2_lemma_pow2_adds(1, 252); call Arithmetic_Power2_lemma2_to64(); From 02950c70554982e2d2607576c7dcb27d17c2e565 Mon Sep 17 00:00:00 2001 From: Lydia Kondylidou <33327056+kondylidou@users.noreply.github.com> Date: Tue, 19 May 2026 17:42:44 +0200 Subject: [PATCH 04/20] small --- .../Languages/Boole/FeatureRequests/nat_axiom_discussion.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/StrataTest/Languages/Boole/FeatureRequests/nat_axiom_discussion.lean b/StrataTest/Languages/Boole/FeatureRequests/nat_axiom_discussion.lean index d16d171428..2855e26270 100644 --- a/StrataTest/Languages/Boole/FeatureRequests/nat_axiom_discussion.lean +++ b/StrataTest/Languages/Boole/FeatureRequests/nat_axiom_discussion.lean @@ -9,7 +9,7 @@ import Strata.MetaVerifier open Strata /- -Meeting discussion: `type nat := int` + auto-generated non-negativity axioms +Discussion: `type nat := int` + auto-generated non-negativity axioms Abdal's proposed design ─────────────────────── From 5646d80fe8dad1b85d369844e42ee7e22a1c22cf Mon Sep 17 00:00:00 2001 From: Lydia Kondylidou <33327056+kondylidou@users.noreply.github.com> Date: Tue, 19 May 2026 17:47:13 +0200 Subject: [PATCH 05/20] fix --- .../Boole/FeatureRequests/nat_axiom_discussion.lean | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/StrataTest/Languages/Boole/FeatureRequests/nat_axiom_discussion.lean b/StrataTest/Languages/Boole/FeatureRequests/nat_axiom_discussion.lean index 2855e26270..4df7588872 100644 --- a/StrataTest/Languages/Boole/FeatureRequests/nat_axiom_discussion.lean +++ b/StrataTest/Languages/Boole/FeatureRequests/nat_axiom_discussion.lean @@ -49,11 +49,11 @@ spec { #end /-- info: -Obligation: use_nat_list_post_use_nat_list_ensures_1_373_calls_NatList..head_0 +Obligation: use_nat_list_post_use_nat_list_ensures_1_1512_calls_NatList..head_0 Property: assert Result: ✅ pass -Obligation: use_nat_list_ensures_1_373 +Obligation: use_nat_list_ensures_1_1512 Property: assert Result: ✅ pass-/ #guard_msgs in @@ -104,15 +104,15 @@ spec { -- ⚠️ This should be ❌ fail but is ✅ pass — the auto-axiom is too strong. /-- info: -Obligation: unsound_example_pre_unsound_example_requires_0_318_calls_Pair..second_0 +Obligation: unsound_example_pre_unsound_example_requires_0_3451_calls_Pair..second_0 Property: assert Result: ✅ pass -Obligation: unsound_example_post_unsound_example_ensures_1_393_calls_Pair..second_0 +Obligation: unsound_example_post_unsound_example_ensures_1_3505_calls_Pair..second_0 Property: assert Result: ✅ pass -Obligation: unsound_example_ensures_1_393 +Obligation: unsound_example_ensures_1_3505 Property: assert Result: ✅ pass-/ #guard_msgs in From 6557cce143673b1bb214d78a961c8d90207bc060 Mon Sep 17 00:00:00 2001 From: Lydia Kondylidou <33327056+kondylidou@users.noreply.github.com> Date: Tue, 19 May 2026 23:56:59 +0200 Subject: [PATCH 06/20] some fixes --- docs/BooleFeatureRequests.md | 16 +++++++--------- 1 file changed, 7 insertions(+), 9 deletions(-) diff --git a/docs/BooleFeatureRequests.md b/docs/BooleFeatureRequests.md index ceac0f119c..c8c23ab248 100644 --- a/docs/BooleFeatureRequests.md +++ b/docs/BooleFeatureRequests.md @@ -3,13 +3,6 @@ This document tracks the selected Boole feature-request seeds kept under [`StrataTest/Languages/Boole/FeatureRequests`](../StrataTest/Languages/Boole/FeatureRequests). -## Current priorities - -- Prioritize Rust-facing language support over Verus-only proof-visibility features. -- Treat `opaque`, `reveal`, `hide`, `reveal_with_fuel`, `closed`, and `HasType` - as lower-priority compatibility items unless they unblock a broader Rust path. -- Widening casts (`e as_int`) fully implemented (Gap #6) for bv1/8/16/32/64/128; covers all B2–B5 bitvector casts. Gap #8 (`nat` as a first-class type) is not a cast blocker — Boole has no `nat` type, so `nat`/`int` coercions are identity. - ## Implemented feature requests - **Extensional equality** (#684) @@ -62,9 +55,14 @@ This document tracks the selected Boole feature-request seeds kept under - `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`](../StrataTest/Languages/Boole/FeatureRequests/lambda_closure.lean). -- **Widening casts** (`e as_int`) +- **Widening casts** (`e as_int`) (Gap #6 partial) - `e as_int` lowers to `Bv{n}.ToNat` (Core op) → SMT-LIB `bv2nat`; widths 1/8/16/32/64/128. + - Remaining: int→BV cast (`x as bv32` etc.). - Benchmarks: [`cast_expr.lean`](../StrataTest/Languages/Boole/FeatureRequests/cast_expr.lean), [`widening_casts.lean`](../StrataTest/Languages/Boole/FeatureRequests/widening_casts.lean). +- **`type nat := int` synonym** (Gap #8 partial) + - Nullary synonyms expanding to `int` trigger auto-axioms `∀ x : DT . DT..isCtor(x) ⟹ DT..field(x) ≥ 0` for each `nat`-typed constructor field. + - Known limitation: axiom may be unsound for mixed `nat`/`int` datatypes. See [`nat_axiom_discussion.lean`](../StrataTest/Languages/Boole/FeatureRequests/nat_axiom_discussion.lean). + - Benchmark: [`cast_nested.lean`](../StrataTest/Languages/Boole/FeatureRequests/cast_nested.lean). ## Semantic preservation requests @@ -78,7 +76,7 @@ This document tracks the selected Boole feature-request seeds kept under ## Type/model requests -8. **Native `nat` support**: Stop modeling `nat` as a purely abstract type with uninterpreted coercions. +8. **Native `nat` support**: `type nat := int` synonym implemented. 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). From a7d3ced4a77801971b13001bb49e327336048220 Mon Sep 17 00:00:00 2001 From: Lydia Kondylidou <33327056+kondylidou@users.noreply.github.com> Date: Tue, 19 May 2026 23:58:10 +0200 Subject: [PATCH 07/20] chore: revert BooleBenchmarks.md to main2 version Co-Authored-By: Claude Sonnet 4.6 --- docs/BooleBenchmarks.md | 29 ++++++++++++++--------------- 1 file changed, 14 insertions(+), 15 deletions(-) diff --git a/docs/BooleBenchmarks.md b/docs/BooleBenchmarks.md index e07645961e..36e898d090 100644 --- a/docs/BooleBenchmarks.md +++ b/docs/BooleBenchmarks.md @@ -154,19 +154,18 @@ seeds live in **Additional gaps per benchmark:** -| # | Gap | FR# | Status | Notes | -|---|-----|-----|--------|-------| -| 1 | `u128` intermediate products | — | ○ open | 25 u64×u64 cross-limb products are u128 in Rust; in Boole, model as `int` — no separate feature needed, resolves with Gap #13 | -| 1 | `FieldElement51.limbs: [u64; 5]` | #13 | ○ open | Sub-case of Gap #13: `limbs` is a struct field whose type is itself a fixed-size array. Planned encoding: flatten into five named `int` fields (`limb0`…`limb4`) rather than `Map int bv64` — same gap, not a separate one | -| 2 | `[u8; 64]` byte arrays | #25 | ○ open | `input: &[u8; 64]` as `Map int bv8`; SMT backend resolved by PR #795; remaining gap is Boole syntax (initializer, write-back) | -| 5 | `[u8; 32]` byte arrays | #25 | ○ open | Same as B2; SMT backend resolved by PR #795 | -| 2,5 | Widening casts (`e as_int`) | #6 | ✓ done | `Bv{n}.ToNat` → `bv2nat`; bv1/8/16/32/64/128; see [`cast_expr.lean`](../StrataTest/Languages/Boole/FeatureRequests/cast_expr.lean) | -| 2 | `reduce()` spec function | — | ✓ done | Axiom pattern verified in [`scalar_reduce.lean`](../StrataTest/Languages/Boole/FeatureRequests/scalar_reduce.lean); `u8_64_as_group_canonical` gains a recursive definition once Gap #11 closes (→ #1167), pure UF in SMT, manual axioms unchanged | -| 2 | `is_uniform_scalar` axiom | — | ○ open | Probabilistic postcondition needs abstract `is_uniform_bytes`/`is_uniform_scalar` predicates as Boole axioms | -| 3 | `Option` return | — | ○ open | Boole has no native `Option` type and no `matches` destructuring in spec clauses; see [`option_matches.lean`](../StrataTest/Languages/Boole/FeatureRequests/option_matches.lean) | -| 3 | `field_square` / `sqrt_ratio_i` axioms | — | ○ open | Needed for the full decompress body | -| 4 | Pair return type | — | ○ open | `invsqrt()` returns `(bool, FieldElement51)`; needs tuple/pair type support in Boole | -| 4 | Field op axioms | — | ○ open | `add`, `sub`, `square`, `invsqrt`, `conditional_negate`, `as_bytes` — each needs a Boole axiom | -| 5 | Inline `let`-block postcondition | — | ✓ done | Implemented; see [`embedded_postcondition.lean`](../StrataTest/Languages/Boole/embedded_postcondition.lean) | -| 5 | Montgomery ladder invariant | — | ○ open | Needs Montgomery curve differential addition axioms (Costello-Smith 2017, eq. 4); loop structure demonstrated in [`montgomery_loop_invariant.lean`](../StrataTest/Languages/Boole/FeatureRequests/montgomery_loop_invariant.lean) | +| B | Gap | Status | Notes | +|---|-----|--------|-------| +| 1 | `u128` intermediate products | ○ open | 25 u64×u64 cross-limb products are u128 in Rust; in Boole, model as `int` — no separate feature needed, resolves with #13 | +| 1 | #13 `FieldElement51.limbs: [u64; 5]` | ○ open | Sub-case of #13: `limbs` is a struct field whose type is itself a fixed-size array. Planned encoding: flatten into five named `int` fields (`limb0`…`limb4`) rather than `Map int bv64` — same gap, not a separate one | +| 2 | #15 `[u8; 64]` byte arrays | ○ open | `input: &[u8; 64]` as `Map int bv8`; SMT backend resolved by PR #795; remaining gap is Boole syntax (initializer, write-back) | +| 5 | #15 `[u8; 32]` byte arrays | ○ open | Same as B2; SMT backend resolved by PR #795 | +| 2 | `reduce()` spec function | ✓ done | Axiom pattern verified in [`scalar_reduce.lean`](../StrataTest/Languages/Boole/FeatureRequests/scalar_reduce.lean); `u8_64_as_group_canonical` can now use recursive form (#1167 merged); manual axioms unchanged | +| 2 | `is_uniform_scalar` axiom | ○ open | Probabilistic postcondition needs abstract `is_uniform_bytes`/`is_uniform_scalar` predicates as Boole axioms | +| 3 | #14 `Option` return | ○ open | Boole has no native `Option` type and no `matches` destructuring in spec clauses; see [`option_matches.lean`](../StrataTest/Languages/Boole/FeatureRequests/option_matches.lean) | +| 3 | `field_square` / `sqrt_ratio_i` axioms | ○ open | Needed for the full decompress body | +| 4 | Pair return type | ○ open | `invsqrt()` returns `(bool, FieldElement51)`; needs tuple/pair type support in Boole | +| 4 | Field op axioms | ○ open | `add`, `sub`, `square`, `invsqrt`, `conditional_negate`, `as_bytes` — each needs a Boole axiom | +| 5 | Inline `let`-block postcondition | ✓ done | Implemented; see [`embedded_postcondition.lean`](../StrataTest/Languages/Boole/embedded_postcondition.lean) | +| 5 | Montgomery ladder invariant | ○ open | Needs Montgomery curve differential addition axioms (Costello-Smith 2017, eq. 4); loop structure demonstrated in [`montgomery_loop_invariant.lean`](../StrataTest/Languages/Boole/FeatureRequests/montgomery_loop_invariant.lean) | From f4050e0536b027e290baf624b2d2388196aba0eb Mon Sep 17 00:00:00 2001 From: Lydia Kondylidou <33327056+kondylidou@users.noreply.github.com> Date: Wed, 20 May 2026 00:05:10 +0200 Subject: [PATCH 08/20] test(B2): add #guard_msgs to lock in 113-pass result Co-Authored-By: Claude Sonnet 4.6 --- .../from_bytes_mod_order_wide_minimal.lean | 453 ++++++++++++++++++ 1 file changed, 453 insertions(+) diff --git a/StrataTest/Languages/Boole/from_bytes_mod_order_wide_minimal.lean b/StrataTest/Languages/Boole/from_bytes_mod_order_wide_minimal.lean index b39083c3fa..53f001f930 100644 --- a/StrataTest/Languages/Boole/from_bytes_mod_order_wide_minimal.lean +++ b/StrataTest/Languages/Boole/from_bytes_mod_order_wide_minimal.lean @@ -263,4 +263,457 @@ spec { }; #end +/-- info: +Obligation: bytes_seq_as_nat_terminates_0 +Property: assert +Result: ✅ pass + +Obligation: bytes_seq_as_nat_terminates_1 +Property: assert +Result: ✅ pass + +Obligation: seq_as_nat_52_terminates_0 +Property: assert +Result: ✅ pass + +Obligation: seq_as_nat_52_terminates_1 +Property: assert +Result: ✅ pass + +Obligation: scalar52_as_nat_body_calls_scalar52..limbs_0 +Property: assert +Result: ✅ pass + +Obligation: limbs_bounded_body_calls_scalar52..limbs_0 +Property: assert +Result: ✅ pass + +Obligation: is_canonical_scalar_body_calls_scalar..bytes_0 +Property: assert +Result: ✅ pass + +Obligation: is_canonical_scalar_body_calls_scalar..bytes_1 +Property: assert +Result: ✅ pass + +Obligation: scalar_as_canonical_body_calls_scalar..bytes_0 +Property: assert +Result: ✅ pass + +Obligation: Impl__2_clone_ensures_0_2199 +Property: assert +Result: ✅ pass + +Obligation: Impl__3_from_bytes_wide_ensures_1_2372 +Property: assert +Result: ✅ pass + +Obligation: Impl__3_from_bytes_wide_ensures_2_2408 +Property: assert +Result: ✅ pass + +Obligation: Impl__3_pack_post_Impl__3_pack_ensures_5_2741_calls_scalar..bytes_0 +Property: assert +Result: ✅ pass + +Obligation: set_result_calls_scalar..bytes_0 +Property: assert +Result: ✅ pass + +Obligation: Impl__3_pack_ensures_5_2741 +Property: assert +Result: ✅ pass + +Obligation: Impl__3_pack_ensures_6_2845 +Property: assert +Result: ✅ pass + +Obligation: callElimAssert_Impl__3_pack_requires_4_2709_25 +Property: assert +Result: ✅ pass + +Obligation: assume_callElimAssume_Impl__3_pack_ensures_5_2741_26_calls_scalar..bytes_0 +Property: assert +Result: ✅ pass + +Obligation: callElimAssert_lemma_scalar52_lt_pow2_256_if_canonical_requires_102_10101_19 +Property: assert +Result: ✅ pass + +Obligation: callElimAssert_lemma_scalar52_lt_pow2_256_if_canonical_requires_103_10130_20 +Property: assert +Result: ✅ pass + +Obligation: callElimAssert_Arithmetic_Div_mod_lemma_small_mod_requires_11_4213_15 +Property: assert +Result: ✅ pass + +Obligation: callElimAssert_Arithmetic_Div_mod_lemma_small_mod_requires_12_4231_16 +Property: assert +Result: ✅ pass + +Obligation: callElimAssert_Arithmetic_Div_mod_lemma_mod_bound_requires_15_4381_11 +Property: assert +Result: ✅ pass + +Obligation: set_tmp5_calls_scalar..bytes_0 +Property: assert +Result: ✅ pass + +Obligation: callElimAssert_Arithmetic_Div_mod_lemma_small_mod_requires_11_4213_6 +Property: assert +Result: ✅ pass + +Obligation: callElimAssert_Arithmetic_Div_mod_lemma_small_mod_requires_12_4231_7 +Property: assert +Result: ✅ pass + +Obligation: callElimAssert_axiom_uniform_mod_reduction_requires_105_10489_2 +Property: assert +Result: ✅ pass + +Obligation: Impl__4_from_bytes_mod_order_wide_ensures_8_3119 +Property: assert +Result: ✅ pass + +Obligation: Impl__4_from_bytes_mod_order_wide_ensures_9_3202 +Property: assert +Result: ✅ pass + +Obligation: Impl__4_from_bytes_mod_order_wide_ensures_10_3241 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Div_mod_lemma_small_mod_ensures_13_4249 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Div_mod_lemma_mod_bound_ensures_16_4399 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma_pow2_adds_ensures_18_4547 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma_pow2_strictly_increases_ensures_21_4792 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_ensures_23_4946 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_ensures_24_4988 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_ensures_25_5030 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_ensures_26_5072 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_ensures_27_5114 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_ensures_28_5157 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_ensures_29_5200 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_ensures_30_5243 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_ensures_31_5287 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_ensures_32_5331 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_ensures_33_5375 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_ensures_34_5421 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_ensures_35_5467 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_ensures_36_5513 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_ensures_37_5559 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_ensures_38_5606 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_ensures_39_5653 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_ensures_40_5700 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_ensures_41_5748 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_ensures_42_5796 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_ensures_43_5844 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_ensures_44_5893 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_ensures_45_5942 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_ensures_46_5991 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_ensures_47_6040 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_ensures_48_6090 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_ensures_49_6140 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_ensures_50_6190 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_ensures_51_6241 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_ensures_52_6292 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_ensures_53_6343 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_ensures_54_6395 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_ensures_55_6447 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_ensures_56_6499 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_58_6653 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_59_6705 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_60_6758 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_61_6811 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_62_6864 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_63_6918 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_64_6972 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_65_7026 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_66_7081 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_67_7136 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_68_7191 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_69_7246 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_70_7302 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_71_7358 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_72_7414 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_73_7471 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_74_7528 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_75_7585 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_76_7643 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_77_7701 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_78_7759 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_79_7817 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_80_7876 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_81_7935 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_82_7994 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_83_8054 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_84_8114 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_85_8174 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_86_8235 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_87_8296 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_88_8357 +Property: assert +Result: ✅ pass + +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_89_8418 +Property: assert +Result: ✅ pass + +Obligation: assert_93_8755 +Property: assert +Result: ✅ pass + +Obligation: assert_95_8925 +Property: assert +Result: ✅ pass + +Obligation: assert_96_9005 +Property: assert +Result: ✅ pass + +Obligation: callElimAssert_Arithmetic_Power2_lemma_pow2_strictly_increases_requires_20_4772_75 +Property: assert +Result: ✅ pass + +Obligation: assert_98_9268 +Property: assert +Result: ✅ pass + +Obligation: assert_99_9440 +Property: assert +Result: ✅ pass + +Obligation: callElimAssert_Arithmetic_Power2_lemma_pow2_strictly_increases_requires_20_4772_34 +Property: assert +Result: ✅ pass + +Obligation: lemma_group_order_bound_ensures_91_8561 +Property: assert +Result: ✅ pass + +Obligation: callElimAssert_Arithmetic_Power2_lemma_pow2_strictly_increases_requires_20_4772_114 +Property: assert +Result: ✅ pass + +Obligation: lemma_group_order_smaller_than_pow256_ensures_101_9809 +Property: assert +Result: ✅ pass + +Obligation: callElimAssert_Arithmetic_Power2_lemma_pow2_strictly_increases_requires_20_4772_119 +Property: assert +Result: ✅ pass + +Obligation: lemma_scalar52_lt_pow2_256_if_canonical_ensures_104_10175 +Property: assert +Result: ✅ pass + +Obligation: axiom_uniform_mod_reduction_ensures_106_10572 +Property: assert +Result: ✅ pass-/ +#guard_msgs in #eval Strata.Boole.verify "cvc5" from_bytes_mod_order_wide_minimal_program (options := .quiet) From 19808a40d5e87b8aaf77075c91c4cb37f60c4b87 Mon Sep 17 00:00:00 2001 From: Lydia Kondylidou <33327056+kondylidou@users.noreply.github.com> Date: Wed, 20 May 2026 00:10:22 +0200 Subject: [PATCH 09/20] Fix binder name and add mixed-nat/int warning in natAxiomsForDatatype MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - Rename quantifier binder `""` → `"x"` in the auto-generated non-negativity axiom so it prints as a named binder in Core pretty-prints. - Detect constructors with both `nat`- and `int`-typed fields and emit a `dbg_trace` warning at translation time; the mixed case is a known soundness hole (documented in `nat_axiom_discussion.lean`). Co-Authored-By: Claude Sonnet 4.6 --- Strata/Languages/Boole/Verify.lean | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/Strata/Languages/Boole/Verify.lean b/Strata/Languages/Boole/Verify.lean index de5d54f13f..9fb79fbc98 100644 --- a/Strata/Languages/Boole/Verify.lean +++ b/Strata/Languages/Boole/Verify.lean @@ -857,6 +857,19 @@ private def natAxiomsForDatatype | none => [] | some ⟨_, fs⟩ => fs.toList let testerName := s!"{dtypeName}..is{cname}" + -- Check for mixed nat/int constructor: if some fields are nat and others are + -- int, the generated axiom applies to all SMT terms of this datatype type and + -- may create an inconsistency if the solver introduces a synthetic term with a + -- negative nat field. Warn so the user is aware. + let fieldTypes := fields.filterMap fun f => match f with + | .mkBinding _ _ (.expr ty) => some ty | _ => none + let hasNat := (← fieldTypes.mapM isNatType).any id + let hasInt := fieldTypes.any fun ty => match ty with | .int _ => true | _ => false + if hasNat && hasInt then + dbg_trace s!"[Boole] Warning: constructor `{dtypeName}.{cname}` has both `nat`- and `int`-typed fields. \ + The auto-generated non-negativity axiom is globally quantified over all SMT terms of type `{dtypeName}`, \ + which may be unsound if the solver introduces synthetic terms with negative nat fields. \ + See `nat_axiom_discussion.lean` for design alternatives." for field in fields do match field with | .mkBinding _ ⟨_, fieldName⟩ tp => @@ -868,7 +881,7 @@ private def natAxiomsForDatatype let selector := mkCoreApp (.op () ⟨selectorName, ()⟩ none) [bv0] let geZero := mkCoreApp Core.intGeOp [selector, .intConst () 0] let implies := mkCoreApp Core.boolImpliesOp [tester, geZero] - let axExpr : Core.Expression.Expr := .quant () .all "" (some dtypeTy) bv0 implies + let axExpr : Core.Expression.Expr := .quant () .all "x" (some dtypeTy) bv0 implies let axName := s!"{dtypeName}_{cname}_{fieldName}_nonneg" axioms := axioms ++ [.ax { name := axName, e := axExpr } .empty] | _ => pure () From e9e0605cf7366e3e31b1bffb8b606004cc83945d Mon Sep 17 00:00:00 2001 From: Lydia Kondylidou <33327056+kondylidou@users.noreply.github.com> Date: Wed, 20 May 2026 00:13:28 +0200 Subject: [PATCH 10/20] fix(Boole): nat-synonym passthrough in cast_to_int A `nat`-typed expression (`type nat := int` synonym) used with `e as_int` now returns the expression unchanged instead of throwing, since nat is already modeled as int. Co-Authored-By: Claude Sonnet 4.6 --- Strata/Languages/Boole/Verify.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/Strata/Languages/Boole/Verify.lean b/Strata/Languages/Boole/Verify.lean index 9fb79fbc98..ea5a302dc1 100644 --- a/Strata/Languages/Boole/Verify.lean +++ b/Strata/Languages/Boole/Verify.lean @@ -513,7 +513,9 @@ partial def toCoreExpr (e : Boole.Expr) : TranslateM Core.Expression.Expr := do let n ← bvWidth m ty return mkCoreApp (.op () (mkIdent s!"Bv{n}.ToNat") none) [← toCoreExpr e] | .int _ => toCoreExpr e - | _ => throwAt m s!"'as int' requires a bitvector source type" + | _ => + if ← isNatType ty then toCoreExpr e + else throwAt m s!"'as int' requires a bitvector source type" | _ => throw (.fromMessage s!"Unsupported expression: {repr e}") end From 0e142495165a93dd1217ad357ebd3b9ee38e404e Mon Sep 17 00:00:00 2001 From: Lydia Kondylidou <33327056+kondylidou@users.noreply.github.com> Date: Wed, 20 May 2026 00:14:25 +0200 Subject: [PATCH 11/20] docs: note transitive nat-synonym limitation in Gap #8 entry Co-Authored-By: Claude Sonnet 4.6 --- docs/BooleFeatureRequests.md | 1 + 1 file changed, 1 insertion(+) diff --git a/docs/BooleFeatureRequests.md b/docs/BooleFeatureRequests.md index c8c23ab248..e84713444d 100644 --- a/docs/BooleFeatureRequests.md +++ b/docs/BooleFeatureRequests.md @@ -62,6 +62,7 @@ This document tracks the selected Boole feature-request seeds kept under - **`type nat := int` synonym** (Gap #8 partial) - Nullary synonyms expanding to `int` trigger auto-axioms `∀ x : DT . DT..isCtor(x) ⟹ DT..field(x) ≥ 0` for each `nat`-typed constructor field. - Known limitation: axiom may be unsound for mixed `nat`/`int` datatypes. See [`nat_axiom_discussion.lean`](../StrataTest/Languages/Boole/FeatureRequests/nat_axiom_discussion.lean). + - Known limitation: only direct synonyms (`type mynat := int`) are recognised; transitive chains (`type mynat := nat`) are not followed, so fields typed `mynat` get no axiom. - Benchmark: [`cast_nested.lean`](../StrataTest/Languages/Boole/FeatureRequests/cast_nested.lean). ## Semantic preservation requests From 4a364298af6d6be826b32b74cd78014aacf84dd8 Mon Sep 17 00:00:00 2001 From: Lydia Kondylidou <33327056+kondylidou@users.noreply.github.com> Date: Wed, 20 May 2026 11:21:09 +0200 Subject: [PATCH 12/20] rename --- Strata/Languages/Boole/Verify.lean | 2 +- .../{nat_axiom_discussion.lean => nat_axiom_limitation.lean} | 0 docs/BooleFeatureRequests.md | 2 +- 3 files changed, 2 insertions(+), 2 deletions(-) rename StrataTest/Languages/Boole/FeatureRequests/{nat_axiom_discussion.lean => nat_axiom_limitation.lean} (100%) diff --git a/Strata/Languages/Boole/Verify.lean b/Strata/Languages/Boole/Verify.lean index ea5a302dc1..077b5e6efe 100644 --- a/Strata/Languages/Boole/Verify.lean +++ b/Strata/Languages/Boole/Verify.lean @@ -871,7 +871,7 @@ private def natAxiomsForDatatype dbg_trace s!"[Boole] Warning: constructor `{dtypeName}.{cname}` has both `nat`- and `int`-typed fields. \ The auto-generated non-negativity axiom is globally quantified over all SMT terms of type `{dtypeName}`, \ which may be unsound if the solver introduces synthetic terms with negative nat fields. \ - See `nat_axiom_discussion.lean` for design alternatives." + See `nat_axiom_limitation.lean` for design alternatives." for field in fields do match field with | .mkBinding _ ⟨_, fieldName⟩ tp => diff --git a/StrataTest/Languages/Boole/FeatureRequests/nat_axiom_discussion.lean b/StrataTest/Languages/Boole/FeatureRequests/nat_axiom_limitation.lean similarity index 100% rename from StrataTest/Languages/Boole/FeatureRequests/nat_axiom_discussion.lean rename to StrataTest/Languages/Boole/FeatureRequests/nat_axiom_limitation.lean diff --git a/docs/BooleFeatureRequests.md b/docs/BooleFeatureRequests.md index e84713444d..c41c49e8b2 100644 --- a/docs/BooleFeatureRequests.md +++ b/docs/BooleFeatureRequests.md @@ -61,7 +61,7 @@ This document tracks the selected Boole feature-request seeds kept under - Benchmarks: [`cast_expr.lean`](../StrataTest/Languages/Boole/FeatureRequests/cast_expr.lean), [`widening_casts.lean`](../StrataTest/Languages/Boole/FeatureRequests/widening_casts.lean). - **`type nat := int` synonym** (Gap #8 partial) - Nullary synonyms expanding to `int` trigger auto-axioms `∀ x : DT . DT..isCtor(x) ⟹ DT..field(x) ≥ 0` for each `nat`-typed constructor field. - - Known limitation: axiom may be unsound for mixed `nat`/`int` datatypes. See [`nat_axiom_discussion.lean`](../StrataTest/Languages/Boole/FeatureRequests/nat_axiom_discussion.lean). + - Known limitation: axiom may be unsound for mixed `nat`/`int` datatypes. See [`nat_axiom_limitation.lean`](../StrataTest/Languages/Boole/FeatureRequests/nat_axiom_limitation.lean). - Known limitation: only direct synonyms (`type mynat := int`) are recognised; transitive chains (`type mynat := nat`) are not followed, so fields typed `mynat` get no axiom. - Benchmark: [`cast_nested.lean`](../StrataTest/Languages/Boole/FeatureRequests/cast_nested.lean). From 90050d2d9d50ae9c165714fd797a68867e109486 Mon Sep 17 00:00:00 2001 From: Lydia Kondylidou <33327056+kondylidou@users.noreply.github.com> Date: Wed, 20 May 2026 11:27:05 +0200 Subject: [PATCH 13/20] fix msgs --- Strata/Languages/Boole/Verify.lean | 3 +-- .../Languages/Boole/FeatureRequests/nat_axiom_limitation.lean | 4 +++- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/Strata/Languages/Boole/Verify.lean b/Strata/Languages/Boole/Verify.lean index 077b5e6efe..f2749d3cd2 100644 --- a/Strata/Languages/Boole/Verify.lean +++ b/Strata/Languages/Boole/Verify.lean @@ -870,8 +870,7 @@ private def natAxiomsForDatatype if hasNat && hasInt then dbg_trace s!"[Boole] Warning: constructor `{dtypeName}.{cname}` has both `nat`- and `int`-typed fields. \ The auto-generated non-negativity axiom is globally quantified over all SMT terms of type `{dtypeName}`, \ - which may be unsound if the solver introduces synthetic terms with negative nat fields. \ - See `nat_axiom_limitation.lean` for design alternatives." + which may be unsound if the solver introduces synthetic terms with negative nat fields." for field in fields do match field with | .mkBinding _ ⟨_, fieldName⟩ tp => diff --git a/StrataTest/Languages/Boole/FeatureRequests/nat_axiom_limitation.lean b/StrataTest/Languages/Boole/FeatureRequests/nat_axiom_limitation.lean index 4df7588872..a0dc4ea22e 100644 --- a/StrataTest/Languages/Boole/FeatureRequests/nat_axiom_limitation.lean +++ b/StrataTest/Languages/Boole/FeatureRequests/nat_axiom_limitation.lean @@ -103,7 +103,9 @@ spec { #end -- ⚠️ This should be ❌ fail but is ✅ pass — the auto-axiom is too strong. -/-- info: +/-- info: [Boole] Warning: constructor `Pair.Pair_mk` has both `nat`- and `int`-typed fields. The auto-generated non-negativity axiom is globally quantified over all SMT terms of type `Pair`, which may be unsound if the solver introduces synthetic terms with negative nat fields. +--- +info: Obligation: unsound_example_pre_unsound_example_requires_0_3451_calls_Pair..second_0 Property: assert Result: ✅ pass From a450792928ff9e0b7be3d226d4a1d50faec192cb Mon Sep 17 00:00:00 2001 From: Lydia Kondylidou <33327056+kondylidou@users.noreply.github.com> Date: Wed, 20 May 2026 15:40:47 +0200 Subject: [PATCH 14/20] some reorg --- .../FeatureRequests/mutual_recursion.lean | 118 ------------ .../sha256_compact_indexed.lean | 9 + .../{FeatureRequests => }/cast_expr.lean | 0 .../{FeatureRequests => }/cast_nested.lean | 0 .../Languages/Boole/mutual_recursion.lean | 173 ++++++++++++++++++ .../{FeatureRequests => }/seq_slicing.lean | 0 .../{FeatureRequests => }/widening_casts.lean | 0 docs/BooleFeatureRequests.md | 40 ++-- 8 files changed, 203 insertions(+), 137 deletions(-) delete mode 100644 StrataTest/Languages/Boole/FeatureRequests/mutual_recursion.lean rename StrataTest/Languages/Boole/{FeatureRequests => }/cast_expr.lean (100%) rename StrataTest/Languages/Boole/{FeatureRequests => }/cast_nested.lean (100%) create mode 100644 StrataTest/Languages/Boole/mutual_recursion.lean rename StrataTest/Languages/Boole/{FeatureRequests => }/seq_slicing.lean (100%) rename StrataTest/Languages/Boole/{FeatureRequests => }/widening_casts.lean (100%) diff --git a/StrataTest/Languages/Boole/FeatureRequests/mutual_recursion.lean b/StrataTest/Languages/Boole/FeatureRequests/mutual_recursion.lean deleted file mode 100644 index 42aa91a297..0000000000 --- a/StrataTest/Languages/Boole/FeatureRequests/mutual_recursion.lean +++ /dev/null @@ -1,118 +0,0 @@ -/- - Copyright Strata Contributors - - SPDX-License-Identifier: Apache-2.0 OR MIT --/ - -import Strata.MetaVerifier - -open Strata - -/- -Near-upstream anchors from `differential_status.md`: -- `verus-examples:guide/recursion` -- `vlir-tests:mutual_recursion` -- `vlir-tests:recursion` -- Verus link: - `guide/recursion`: https://github.com/verus-lang/verus/blob/main/examples/guide/recursion.rs - -Implemented (#599): -- Mutual recursion for spec functions over datatypes works end-to-end. - The `rec function ... function ... ;` block pre-registers all sibling - names before elaborating any body, so forward references are resolved. - Termination is justified by structural recursion on the `@[cases]` param. - -Remaining gap: -- Mutual recursion over `int` (or other non-datatype types) is not yet - supported. Structural recursion does not apply; an explicit `decreases` - clause would be needed for each function in the block, and the - infrastructure for that is not yet in place. --/ - -private def mutualRecursionSeed : Strata.Program := -#strata -program Boole; - -datatype MyNat () { Zero(), Succ(pred: MyNat) }; - -rec -function even(@[cases] n : MyNat) : bool -{ - if MyNat..isZero(n) then true else odd(MyNat..pred(n)) -} -function odd(@[cases] n : MyNat) : bool -{ - if MyNat..isZero(n) then false else even(MyNat..pred(n)) -} -; - -procedure test_parity() returns () -spec { - ensures even(Zero()) == true; - ensures odd(Zero()) == false; - ensures even(Succ(Zero())) == false; - ensures odd(Succ(Zero())) == true; -} -{ - assert even(Zero()) == true; - assert odd(Zero()) == false; - assert even(Succ(Zero())) == false; - assert odd(Succ(Zero())) == true; -}; -#end - -/-- info: -Obligation: even_body_calls_MyNat..pred_0 -Property: assert -Result: ✅ pass - -Obligation: odd_body_calls_MyNat..pred_0 -Property: assert -Result: ✅ pass - -Obligation: even_terminates_0 -Property: assert -Result: ✅ pass - -Obligation: odd_terminates_0 -Property: assert -Result: ✅ pass - -Obligation: assert_4_1499 -Property: assert -Result: ✅ pass - -Obligation: assert_5_1530 -Property: assert -Result: ✅ pass - -Obligation: assert_6_1561 -Property: assert -Result: ✅ pass - -Obligation: assert_7_1599 -Property: assert -Result: ✅ pass - -Obligation: test_parity_ensures_0_1355 -Property: assert -Result: ✅ pass - -Obligation: test_parity_ensures_1_1387 -Property: assert -Result: ✅ pass - -Obligation: test_parity_ensures_2_1419 -Property: assert -Result: ✅ pass - -Obligation: test_parity_ensures_3_1458 -Property: assert -Result: ✅ pass-/ -#guard_msgs in -#eval Strata.Boole.verify "cvc5" mutualRecursionSeed (options := .quiet) - -example : Strata.smtVCsCorrect mutualRecursionSeed := by - gen_smt_vcs - all_goals (try grind) - diff --git a/StrataTest/Languages/Boole/FeatureRequests/sha256_compact_indexed.lean b/StrataTest/Languages/Boole/FeatureRequests/sha256_compact_indexed.lean index 47ded901b9..fbe9a9f1a5 100644 --- a/StrataTest/Languages/Boole/FeatureRequests/sha256_compact_indexed.lean +++ b/StrataTest/Languages/Boole/FeatureRequests/sha256_compact_indexed.lean @@ -18,6 +18,15 @@ not a bitvector. Encoding it as `bv64` requires a `bv64_to_int_u` cast to use it as a `Sequence` index; as an uninterpreted function that cast causes unknown VCs for loop invariants that mix the counter with `Sequence.length`. `int` with range bounds is the faithful encoding and eliminates the cast. + +All 17 VCs in this seed pass. It remains in FeatureRequests because the +original Rust source uses three features not yet supported in Boole: +- Gap #23: iterator protocol (`for x in iter.iter()` style loops) +- Gap #15: fixed-size array syntax (`[u8; 64]`) +- Gap #16: slice types + +This seed works around all three (using `Sequence`, `int` counters, and +`Sequence bv8` instead of slices). A fuller port would need those gaps closed. -/ private def sha256_compact_indexed_program : Strata.Program := diff --git a/StrataTest/Languages/Boole/FeatureRequests/cast_expr.lean b/StrataTest/Languages/Boole/cast_expr.lean similarity index 100% rename from StrataTest/Languages/Boole/FeatureRequests/cast_expr.lean rename to StrataTest/Languages/Boole/cast_expr.lean diff --git a/StrataTest/Languages/Boole/FeatureRequests/cast_nested.lean b/StrataTest/Languages/Boole/cast_nested.lean similarity index 100% rename from StrataTest/Languages/Boole/FeatureRequests/cast_nested.lean rename to StrataTest/Languages/Boole/cast_nested.lean diff --git a/StrataTest/Languages/Boole/mutual_recursion.lean b/StrataTest/Languages/Boole/mutual_recursion.lean new file mode 100644 index 0000000000..368c9790bb --- /dev/null +++ b/StrataTest/Languages/Boole/mutual_recursion.lean @@ -0,0 +1,173 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import Strata.MetaVerifier + +open Strata + +/- +Near-upstream anchors from `differential_status.md`: +- `verus-examples:guide/recursion` +- `vlir-tests:mutual_recursion` +- `vlir-tests:recursion` +- Verus link: + `guide/recursion`: https://github.com/verus-lang/verus/blob/main/examples/guide/recursion.rs + +Implemented (#599): +- Mutual recursion for spec functions over datatypes works end-to-end. + The `rec function ... function ... ;` block pre-registers all sibling + names before elaborating any body, so forward references are resolved. + Termination is justified by structural recursion on the `@[cases]` param. + +Implemented (#1167): +- Mutual recursion over `int`: each function in a `rec` block may carry a + `decreases` clause; termination VCs are discharged by cvc5. + The functions remain opaque UFs in the SMT model, so concrete evaluation + (e.g. `even(1) == false`) requires manual axioms. +-/ + +private def mutualRecursionSeed : Strata.Program := +#strata +program Boole; + +datatype MyNat () { Zero(), Succ(pred: MyNat) }; + +rec +function even(@[cases] n : MyNat) : bool +{ + if MyNat..isZero(n) then true else odd(MyNat..pred(n)) +} +function odd(@[cases] n : MyNat) : bool +{ + if MyNat..isZero(n) then false else even(MyNat..pred(n)) +} +; + +procedure test_parity() returns () +spec { + ensures even(Zero()) == true; + ensures odd(Zero()) == false; + ensures even(Succ(Zero())) == false; + ensures odd(Succ(Zero())) == true; +} +{ + assert even(Zero()) == true; + assert odd(Zero()) == false; + assert even(Succ(Zero())) == false; + assert odd(Succ(Zero())) == true; +}; +#end + +/-- info: +Obligation: even_body_calls_MyNat..pred_0 +Property: assert +Result: ✅ pass + +Obligation: odd_body_calls_MyNat..pred_0 +Property: assert +Result: ✅ pass + +Obligation: even_terminates_0 +Property: assert +Result: ✅ pass + +Obligation: odd_terminates_0 +Property: assert +Result: ✅ pass + +Obligation: assert_4_1511 +Property: assert +Result: ✅ pass + +Obligation: assert_5_1542 +Property: assert +Result: ✅ pass + +Obligation: assert_6_1573 +Property: assert +Result: ✅ pass + +Obligation: assert_7_1611 +Property: assert +Result: ✅ pass + +Obligation: test_parity_ensures_0_1367 +Property: assert +Result: ✅ pass + +Obligation: test_parity_ensures_1_1399 +Property: assert +Result: ✅ pass + +Obligation: test_parity_ensures_2_1431 +Property: assert +Result: ✅ pass + +Obligation: test_parity_ensures_3_1470 +Property: assert +Result: ✅ pass-/ +#guard_msgs in +#eval Strata.Boole.verify "cvc5" mutualRecursionSeed (options := .quiet) + +example : Strata.smtVCsCorrect mutualRecursionSeed := by + gen_smt_vcs + all_goals (try grind) + +/- +Mutual recursion over int (#1167): +- `decreases n` on each function in the `rec` block; the termination VCs + (`even_terminates_*`, `odd_terminates_*`) are discharged by cvc5. + +Open gap — unfolding (Gap #1 / opaque+reveal): +- `even` and `odd` are emitted as uninterpreted functions (UFs) in the SMT + query. The solver knows their types and that they terminate, but not what + they return at any specific argument. Proving `even(1) == false` requires + the defining equations as SMT assertions: + ∀ n . n <= 0 ==> even(n) == true + ∀ n . n > 0 ==> even(n) == odd(n - 1) + (and symmetrically for `odd`). +- These are exactly the unfolding axioms that Dafny emits via `reveal` and + that Verus controls via `opaque`/`reveal_with_fuel`. The fix in Boole is + to auto-emit them when `decreases` is present — bounded by a trigger on the + function symbol to avoid infinite E-matching instantiation. +- Tracked as Gap #1 (`opaque`/`reveal`) in BooleFeatureRequests.md. +-/ +private def mutualRecursionIntSeed : Strata.Program := +#strata +program Boole; + +rec +function even(n: int) : bool + decreases n +{ + if n <= 0 then true else odd(n - 1) +} +function odd(n: int) : bool + decreases n +{ + if n <= 0 then false else even(n - 1) +} +; +#end + +/-- info: +Obligation: even_terminates_0 +Property: assert +Result: ✅ pass + +Obligation: even_terminates_1 +Property: assert +Result: ✅ pass + +Obligation: odd_terminates_0 +Property: assert +Result: ✅ pass + +Obligation: odd_terminates_1 +Property: assert +Result: ✅ pass-/ +#guard_msgs in +#eval Strata.Boole.verify "cvc5" mutualRecursionIntSeed (options := .quiet) diff --git a/StrataTest/Languages/Boole/FeatureRequests/seq_slicing.lean b/StrataTest/Languages/Boole/seq_slicing.lean similarity index 100% rename from StrataTest/Languages/Boole/FeatureRequests/seq_slicing.lean rename to StrataTest/Languages/Boole/seq_slicing.lean diff --git a/StrataTest/Languages/Boole/FeatureRequests/widening_casts.lean b/StrataTest/Languages/Boole/widening_casts.lean similarity index 100% rename from StrataTest/Languages/Boole/FeatureRequests/widening_casts.lean rename to StrataTest/Languages/Boole/widening_casts.lean diff --git a/docs/BooleFeatureRequests.md b/docs/BooleFeatureRequests.md index c41c49e8b2..85cc03dbd8 100644 --- a/docs/BooleFeatureRequests.md +++ b/docs/BooleFeatureRequests.md @@ -1,7 +1,9 @@ # Boole Feature Request Inventory -This document tracks the selected Boole feature-request seeds kept under -[`StrataTest/Languages/Boole/FeatureRequests`](../StrataTest/Languages/Boole/FeatureRequests). +This document tracks the selected Boole feature-request seeds. Fully-implemented +seeds live in [`StrataTest/Languages/Boole/`](../StrataTest/Languages/Boole/); +seeds with at least one open gap remain in +[`StrataTest/Languages/Boole/FeatureRequests/`](../StrataTest/Languages/Boole/FeatureRequests). ## Implemented feature requests @@ -29,10 +31,10 @@ This document tracks the selected Boole feature-request seeds kept under - 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`](../StrataTest/Languages/Boole/bitvector_ops.lean). -- **Mutual recursion over datatypes** (#599) - - `rec function ... ;` blocks work end-to-end for structural recursion over datatypes. - - Remaining gap: mutual recursion over `int` — unblocked by #1167; see #19. - - Benchmark: [`mutual_recursion.lean`](../StrataTest/Languages/Boole/FeatureRequests/mutual_recursion.lean) (`even`/`odd` over `MyNat`). +- **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`](../StrataTest/Languages/Boole/mutual_recursion.lean). - **`choose` syntax** - `w := choose 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. @@ -47,7 +49,7 @@ This document tracks the selected Boole feature-request seeds kept under - 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. - - Benchmark: [`seq_slicing.lean`](../StrataTest/Languages/Boole/FeatureRequests/seq_slicing.lean). + - Benchmark: [`seq_slicing.lean`](../StrataTest/Languages/Boole/seq_slicing.lean). - **Inline `let`-block postconditions** - `ensures ({ let x = e; ... })` now lowers correctly; enables dalek-lite's `mul_clamped` postcondition style. - Benchmark: [`embedded_postcondition.lean`](../StrataTest/Languages/Boole/embedded_postcondition.lean). @@ -58,16 +60,16 @@ This document tracks the selected Boole feature-request seeds kept under - **Widening casts** (`e as_int`) (Gap #6 partial) - `e as_int` lowers to `Bv{n}.ToNat` (Core op) → SMT-LIB `bv2nat`; widths 1/8/16/32/64/128. - Remaining: int→BV cast (`x as bv32` etc.). - - Benchmarks: [`cast_expr.lean`](../StrataTest/Languages/Boole/FeatureRequests/cast_expr.lean), [`widening_casts.lean`](../StrataTest/Languages/Boole/FeatureRequests/widening_casts.lean). + - Benchmarks: [`cast_expr.lean`](../StrataTest/Languages/Boole/cast_expr.lean), [`widening_casts.lean`](../StrataTest/Languages/Boole/widening_casts.lean). - **`type nat := int` synonym** (Gap #8 partial) - Nullary synonyms expanding to `int` trigger auto-axioms `∀ x : DT . DT..isCtor(x) ⟹ DT..field(x) ≥ 0` for each `nat`-typed constructor field. - Known limitation: axiom may be unsound for mixed `nat`/`int` datatypes. See [`nat_axiom_limitation.lean`](../StrataTest/Languages/Boole/FeatureRequests/nat_axiom_limitation.lean). - Known limitation: only direct synonyms (`type mynat := int`) are recognised; transitive chains (`type mynat := nat`) are not followed, so fields typed `mynat` get no axiom. - - Benchmark: [`cast_nested.lean`](../StrataTest/Languages/Boole/FeatureRequests/cast_nested.lean). + - Benchmark: [`cast_nested.lean`](../StrataTest/Languages/Boole/cast_nested.lean). ## Semantic preservation requests -1. **Generic `opaque` / `reveal`**: Lower priority. Preserve reveals for generic spec functions instead of dropping them. +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`](../StrataTest/Languages/Boole/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. @@ -96,7 +98,7 @@ This document tracks the selected Boole feature-request seeds kept under 17. **Higher-order / lambda / closure support**: Implemented. Remaining gap: first-class function values as procedure parameters or local variables. 18. **`choose`**: Implemented. -19. **Mutual recursion / forward references**: Implemented for functions over datatypes (structural recursion via `@[cases]`). Remaining gap: mutual recursion over `int` or other non-datatype types — now unblocked by #1167 (same mechanism as Gap #11). +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. @@ -115,7 +117,7 @@ This document tracks the selected Boole feature-request seeds kept under ## Boole seed examples -These are the curated one-gap Boole seeds. +Seeds with all gaps closed have been moved to `StrataTest/Languages/Boole/`; the table below tracks all seeds regardless of location. | Definition | Primary request(s) | Source | Current status | | --- | --- | --- | --- | @@ -127,21 +129,21 @@ These are the curated one-gap Boole seeds. | [`opaque_reveal_hide.lean`](../StrataTest/Languages/Boole/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`](../StrataTest/Languages/Boole/FeatureRequests/reveal_with_fuel.lean) | `reveal_with_fuel` (#3) | Verus `test_expand_errors`, `recursion` | Lower priority | | [`early_return.lean`](../StrataTest/Languages/Boole/early_return.lean) | Early return | Verus SST `return` translation gap from `differential_status.md` | Implemented (#871) | -| [`widening_casts.lean`](../StrataTest/Languages/Boole/FeatureRequests/widening_casts.lean) | Widening casts (#6) | Verus `guide/integers`, `quantifiers`, `statements` | Updated to use `e as_int`; map-lookup case `v[i] as_int` verified | -| [`cast_expr.lean`](../StrataTest/Languages/Boole/FeatureRequests/cast_expr.lean) | `e as_int` widening cast (#6) | dalek-lite `scalar.rs` B2/B5 | Gap #6 closed; bv1/8/16/32/64/128 | +| [`widening_casts.lean`](../StrataTest/Languages/Boole/widening_casts.lean) | Widening casts (#6) | Verus `guide/integers`, `quantifiers`, `statements` | Updated to use `e as_int`; map-lookup case `v[i] as_int` verified | +| [`cast_expr.lean`](../StrataTest/Languages/Boole/cast_expr.lean) | `e as_int` widening cast (#6) | dalek-lite `scalar.rs` B2/B5 | Implemented (#1191) | | [`choose_operator.lean`](../StrataTest/Languages/Boole/choose_operator.lean) | `choose` (#18) | Verus `trigger_loops` (`choose_example`, `quantifier_example`) | Implemented (#1075) | | [`higher_order_encoding.lean`](../StrataTest/Languages/Boole/FeatureRequests/higher_order_encoding.lean) | Higher-order values (#17) | Verus `fun_ext`, `trait_for_fn` | Active | | [`lambda_closure.lean`](../StrataTest/Languages/Boole/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`](../StrataTest/Languages/Boole/FeatureRequests/mutual_recursion.lean) | Mutual recursion (#19) | Verus `guide/recursion`; VLIR `mutual_recursion`, `recursion` | Implemented for datatypes (#599); mutual recursion over `int` now unblocked by #1167 | -| [`decreases_metadata.lean`](../StrataTest/Languages/Boole/FeatureRequests/decreases_metadata.lean) | `decreases` preservation (#7) | Verus `proposal-rw2022`, `rw2022_script`, `recursion`; VLIR `LoopSimpleWithSpec` | For-loop `decreases` actively verified; function `decreases` verified by #1092; int-recursive functions: verified (#1167 merged); procedure `decreases` parsed, silently dropped | +| [`mutual_recursion.lean`](../StrataTest/Languages/Boole/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`](../StrataTest/Languages/Boole/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`](../StrataTest/Languages/Boole/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`](../StrataTest/Languages/Boole/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`](../StrataTest/Languages/Boole/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`](../StrataTest/Languages/Boole/bitvector_ops.lean) | Bitwise operators on `bvN` types | dalek-lite `scalar_specs.rs` | Implemented (#970) | | [`bitvector_proof_mode.lean`](../StrataTest/Languages/Boole/FeatureRequests/bitvector_proof_mode.lean) | `by (bit_vector)` proof mode (#27) | VeruSAGE-Bench Vest `leb128` | Active | -| [`seq_slicing.lean`](../StrataTest/Languages/Boole/FeatureRequests/seq_slicing.lean) | Sequence slicing (#11) | dalek-lite `scalar_specs.rs`, `core_specs.rs`; Vest `leb128`, `repetition` | Implemented (#1075); recursive spec functions implemented (#1167 merged); `reconstruct` seed active | -| [`scalar_reduce.lean`](../StrataTest/Languages/Boole/FeatureRequests/scalar_reduce.lean) | `reduce()` spec axiom for B2 (`Scalar::from_bytes_mod_order_wide`) | dalek-lite `scalar.rs` | Implemented (#1075); `u8_64_as_group_canonical` can now use recursive form (#1167 merged); manual axioms unchanged | +| [`seq_slicing.lean`](../StrataTest/Languages/Boole/seq_slicing.lean) | Sequence slicing (#11) | dalek-lite `scalar_specs.rs`, `core_specs.rs`; Vest `leb128`, `repetition` | Implemented (#1075, #1167) | +| [`scalar_reduce.lean`](../StrataTest/Languages/Boole/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`](../StrataTest/Languages/Boole/FeatureRequests/struct_field_access.lean) | Struct/record field access (#13) | dalek-lite `field_specs.rs`, `edwards_specs.rs` | Active | | [`trait_spec_methods.lean`](../StrataTest/Languages/Boole/FeatureRequests/trait_spec_methods.lean) | Trait / interface with spec methods (#21) | VeruSAGE-Bench Vest `SecureSpecCombinator` | Active | | [`option_matches.lean`](../StrataTest/Languages/Boole/FeatureRequests/option_matches.lean) | `Option` in spec functions (#14) | VeruSAGE-Bench Vest `SecureSpecCombinator`, `leb128` | Active | -| [`sha256_compact_indexed.lean`](../StrataTest/Languages/Boole/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 19 VCs pass (#1075); open gaps: iterator protocol (#23), array syntax (#15), slice types (#16) | +| [`sha256_compact_indexed.lean`](../StrataTest/Languages/Boole/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 e5f5ba24eb284dfb81f8e63e8e76f973ce7c7c72 Mon Sep 17 00:00:00 2001 From: Lydia Kondylidou <33327056+kondylidou@users.noreply.github.com> Date: Wed, 20 May 2026 15:42:34 +0200 Subject: [PATCH 15/20] fix --- .../sha256_compact_indexed.lean | 34 +++++++++---------- 1 file changed, 17 insertions(+), 17 deletions(-) diff --git a/StrataTest/Languages/Boole/FeatureRequests/sha256_compact_indexed.lean b/StrataTest/Languages/Boole/FeatureRequests/sha256_compact_indexed.lean index fbe9a9f1a5..35f5590536 100644 --- a/StrataTest/Languages/Boole/FeatureRequests/sha256_compact_indexed.lean +++ b/StrataTest/Languages/Boole/FeatureRequests/sha256_compact_indexed.lean @@ -204,71 +204,71 @@ spec { #end /-- info: -Obligation: assert_1_3021 +Obligation: assert_1_3452 Property: assert Result: ✅ pass -Obligation: assert_2_3064 +Obligation: assert_2_3495 Property: assert Result: ✅ pass -Obligation: assert_3_3596 +Obligation: assert_3_4027 Property: assert Result: ✅ pass -Obligation: assert_4_3627 +Obligation: assert_4_4058 Property: assert Result: ✅ pass -Obligation: assert_5_3658 +Obligation: assert_5_4089 Property: assert Result: ✅ pass -Obligation: callElimAssert_rotate_right_requires_0_2970_39 +Obligation: callElimAssert_rotate_right_requires_0_3401_39 Property: assert Result: ✅ pass -Obligation: callElimAssert_rotate_right_requires_0_2970_35 +Obligation: callElimAssert_rotate_right_requires_0_3401_35 Property: assert Result: ✅ pass -Obligation: assert_7_5332 +Obligation: assert_7_5763 Property: assert Result: ✅ pass -Obligation: callElimAssert_rotate_right_requires_0_2970_31 +Obligation: callElimAssert_rotate_right_requires_0_3401_31 Property: assert Result: ✅ pass -Obligation: callElimAssert_rotate_right_requires_0_2970_27 +Obligation: callElimAssert_rotate_right_requires_0_3401_27 Property: assert Result: ✅ pass -Obligation: assert_8_5571 +Obligation: assert_8_6002 Property: assert Result: ✅ pass -Obligation: callElimAssert_rotate_right_requires_0_2970_23 +Obligation: callElimAssert_rotate_right_requires_0_3401_23 Property: assert Result: ✅ pass -Obligation: callElimAssert_rotate_right_requires_0_2970_19 +Obligation: callElimAssert_rotate_right_requires_0_3401_19 Property: assert Result: ✅ pass -Obligation: callElimAssert_rotate_right_requires_0_2970_15 +Obligation: callElimAssert_rotate_right_requires_0_3401_15 Property: assert Result: ✅ pass -Obligation: callElimAssert_rotate_right_requires_0_2970_11 +Obligation: callElimAssert_rotate_right_requires_0_3401_11 Property: assert Result: ✅ pass -Obligation: callElimAssert_rotate_right_requires_0_2970_7 +Obligation: callElimAssert_rotate_right_requires_0_3401_7 Property: assert Result: ✅ pass -Obligation: callElimAssert_rotate_right_requires_0_2970_3 +Obligation: callElimAssert_rotate_right_requires_0_3401_3 Property: assert Result: ✅ pass-/ #guard_msgs in From 6d33c1810b502125666f316e16023b5b5840f574 Mon Sep 17 00:00:00 2001 From: Lydia Kondylidou <33327056+kondylidou@users.noreply.github.com> Date: Wed, 20 May 2026 16:23:49 +0200 Subject: [PATCH 16/20] small --- .../Languages/Boole/FeatureRequests/nat_axiom_limitation.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/StrataTest/Languages/Boole/FeatureRequests/nat_axiom_limitation.lean b/StrataTest/Languages/Boole/FeatureRequests/nat_axiom_limitation.lean index a0dc4ea22e..0a63a10853 100644 --- a/StrataTest/Languages/Boole/FeatureRequests/nat_axiom_limitation.lean +++ b/StrataTest/Languages/Boole/FeatureRequests/nat_axiom_limitation.lean @@ -146,7 +146,7 @@ which simplifies to Pair..second(p) >= 0 (by the ADT selector axiom). This contradicts Pair..second(p) < 0, making the context inconsistent. ──────────────────────────────────────────────────────────────────────────── -DESIGN ALTERNATIVES — discussion points for the meeting +DESIGN ALTERNATIVES ──────────────────────────────────────────────────────────────────────────── Option A — Status quo + documented restriction From 6935c72e37a69deed28f90bf19f5e85e336300d1 Mon Sep 17 00:00:00 2001 From: Lydia Kondylidou <33327056+kondylidou@users.noreply.github.com> Date: Wed, 20 May 2026 16:31:25 +0200 Subject: [PATCH 17/20] small fix in docu --- docs/BooleFeatureRequests.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/BooleFeatureRequests.md b/docs/BooleFeatureRequests.md index 85cc03dbd8..d9b869bbd3 100644 --- a/docs/BooleFeatureRequests.md +++ b/docs/BooleFeatureRequests.md @@ -42,7 +42,7 @@ seeds with at least one open gap remain in - **`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 — no definitional axioms; manual axioms still needed for functional properties. + - `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`](../StrataTest/Languages/Boole/FeatureRequests/decreases_metadata.lean). - **`Sequence T` type and slicing ops** From ca54b071e13d6b6b1277c767032ff64378859773 Mon Sep 17 00:00:00 2001 From: Lydia Kondylidou <33327056+kondylidou@users.noreply.github.com> Date: Wed, 20 May 2026 22:58:09 +0200 Subject: [PATCH 18/20] correct types --- Strata/DL/SMT/DDMTransform/Translate.lean | 4 + Strata/DL/SMT/Denote.lean | 8 +- Strata/DL/SMT/Op.lean | 14 +- Strata/DL/SMT/Translate.lean | 12 +- Strata/Languages/Boole/Grammar.lean | 18 +- Strata/Languages/Boole/Verify.lean | 14 +- Strata/Languages/Core/CoreOp.lean | 15 +- Strata/Languages/Core/Factory.lean | 60 +++-- Strata/Languages/Core/SMTEncoder.lean | 6 +- .../Languages/Boole/cast_all_directions.lean | 98 ++++++++ StrataTest/Languages/Boole/cast_expr.lean | 4 +- .../from_bytes_mod_order_wide_minimal.lean | 210 +++++++++--------- .../Languages/Boole/widening_casts.lean | 8 +- .../Core/Tests/ProgramEvalTests.lean | 24 +- .../Languages/Core/Tests/StatisticsTest.lean | 4 +- docs/BooleFeatureRequests.md | 12 +- 16 files changed, 360 insertions(+), 151 deletions(-) create mode 100644 StrataTest/Languages/Boole/cast_all_directions.lean diff --git a/Strata/DL/SMT/DDMTransform/Translate.lean b/Strata/DL/SMT/DDMTransform/Translate.lean index 740314bc4c..663c825b67 100644 --- a/Strata/DL/SMT/DDMTransform/Translate.lean +++ b/Strata/DL/SMT/DDMTransform/Translate.lean @@ -206,6 +206,10 @@ partial def translateFromTerm (t:SMT.Term): Except String (SMTDDM.Term Provenanc let iden := SMTIdentifier.iden_indexed smtProv (mkSymbol "zero_extend") (smtAnn #[.ind_numeral smtProv n]) return mk_qual_identifier (.qi_ident smtProv iden) + | .bv (.int_to_bv n) => + let iden := SMTIdentifier.iden_indexed smtProv (mkSymbol "int_to_bv") + (smtAnn #[.ind_numeral smtProv n]) + return mk_qual_identifier (.qi_ident smtProv iden) | .str (.re_index n) => let iden := SMTIdentifier.iden_indexed smtProv (mkSymbol "re.^") (smtAnn #[.ind_numeral smtProv n]) diff --git a/Strata/DL/SMT/Denote.lean b/Strata/DL/SMT/Denote.lean index b7206bc4ec..4f4a4fe04a 100644 --- a/Strata/DL/SMT/Denote.lean +++ b/Strata/DL/SMT/Denote.lean @@ -854,9 +854,15 @@ and semantics when successful. | .app (.zero_extend i) [x] _ => let ⟨.prim (.bitvec n), _, x⟩ ← denoteTerm ctx x | none return ⟨.prim (.bitvec (n + i)), rfl, fun Γ => BitVec.zeroExtend (n + i) (x Γ)⟩ - | .app .bv2nat [x] _ => + | .app .ubv_to_int [x] _ => let ⟨.prim (.bitvec _), _, x⟩ ← denoteTerm ctx x | none return ⟨.prim .int, rfl, fun Γ => Int.ofNat (x Γ).toNat⟩ + | .app .sbv_to_int [x] _ => + let ⟨.prim (.bitvec _), _, x⟩ ← denoteTerm ctx x | none + return ⟨.prim .int, rfl, fun Γ => (x Γ).toInt⟩ + | .app (.int_to_bv n) [x] _ => + let ⟨.prim .int, _, x⟩ ← denoteTerm ctx x | none + return ⟨.prim (.bitvec n), rfl, fun Γ => BitVec.ofInt n (x Γ)⟩ -- SMT-Lib theory of strings | .prim (.string s) => return ⟨.prim .string, rfl, fun _ => s⟩ diff --git a/Strata/DL/SMT/Op.lean b/Strata/DL/SMT/Op.lean index 920f27af4a..2dc1d2e6be 100644 --- a/Strata/DL/SMT/Op.lean +++ b/Strata/DL/SMT/Op.lean @@ -122,7 +122,9 @@ inductive Op.BV : Type where | bvsmulo -- bit-vector signed multiplication overflow predicate | bvconcat | zero_extend : Nat → Op.BV - | bv2nat + | ubv_to_int -- unsigned bitvector → Int (SMT-LIB 2.7: ubv_to_int) + | sbv_to_int -- signed bitvector → Int (SMT-LIB 2.7: sbv_to_int) + | int_to_bv : Nat → Op.BV -- Int → bitvector (SMT-LIB 2.7: (_ int_to_bv n)) deriving Repr, DecidableEq, Inhabited, Hashable inductive Op.Strings : Type where @@ -224,6 +226,9 @@ elab "#genOpAbbrevs" : command => do if ctorName == "zero_extend" then let abbrevCmd ← `(command| abbrev $(mkIdent name) (n : Nat) := Op.bv (Op.BV.zero_extend n)) abbrevs := abbrevs.push (name, abbrevCmd) + else if ctorName == "int_to_bv" then + let abbrevCmd ← `(command| abbrev $(mkIdent name) (n : Nat) := Op.bv (Op.BV.int_to_bv n)) + abbrevs := abbrevs.push (name, abbrevCmd) else let abbrevCmd ← `(command| abbrev $(mkIdent name) := Op.bv $(mkIdent ctor)) abbrevs := abbrevs.push (name, abbrevCmd) @@ -255,7 +260,7 @@ elab "#genOpAbbrevs" : command => do /-- -info: Generated abbrevs: #[Op.not, Op.and, Op.or, Op.eq, Op.ite, Op.implies, Op.distinct, Op.uf, Op.neg, Op.sub, Op.add, Op.mul, Op.div, Op.rdiv, Op.mod, Op.abs, Op.le, Op.lt, Op.ge, Op.gt, Op.bvneg, Op.bvadd, Op.bvsub, Op.bvmul, Op.bvnot, Op.bvand, Op.bvor, Op.bvxor, Op.bvshl, Op.bvlshr, Op.bvashr, Op.bvslt, Op.bvsle, Op.bvult, Op.bvsge, Op.bvsgt, Op.bvule, Op.bvugt, Op.bvuge, Op.bvudiv, Op.bvurem, Op.bvsdiv, Op.bvsrem, Op.bvnego, Op.bvsaddo, Op.bvssubo, Op.bvsmulo, Op.bvconcat, Op.zero_extend, Op.bv2nat, Op.str_length, Op.str_concat, Op.str_lt, Op.str_le, Op.str_at, Op.str_substr, Op.str_prefixof, Op.str_suffixof, Op.str_contains, Op.str_indexof, Op.str_replace, Op.str_replace_all, Op.str_to_re, Op.str_in_re, Op.re_none, Op.re_all, Op.re_allchar, Op.re_concat, Op.re_union, Op.re_inter, Op.re_star, Op.str_replace_re, Op.str_replace_re_all, Op.re_comp, Op.re_diff, Op.re_plus, Op.re_opt, Op.re_range, Op.re_loop, Op.re_index, Op.select, Op.store] +info: Generated abbrevs: #[Op.not, Op.and, Op.or, Op.eq, Op.ite, Op.implies, Op.distinct, Op.uf, Op.neg, Op.sub, Op.add, Op.mul, Op.div, Op.rdiv, Op.mod, Op.abs, Op.le, Op.lt, Op.ge, Op.gt, Op.bvneg, Op.bvadd, Op.bvsub, Op.bvmul, Op.bvnot, Op.bvand, Op.bvor, Op.bvxor, Op.bvshl, Op.bvlshr, Op.bvashr, Op.bvslt, Op.bvsle, Op.bvult, Op.bvsge, Op.bvsgt, Op.bvule, Op.bvugt, Op.bvuge, Op.bvudiv, Op.bvurem, Op.bvsdiv, Op.bvsrem, Op.bvnego, Op.bvsaddo, Op.bvssubo, Op.bvsmulo, Op.bvconcat, Op.zero_extend, Op.ubv_to_int, Op.sbv_to_int, Op.int_to_bv, Op.str_length, Op.str_concat, Op.str_lt, Op.str_le, Op.str_at, Op.str_substr, Op.str_prefixof, Op.str_suffixof, Op.str_contains, Op.str_indexof, Op.str_replace, Op.str_replace_all, Op.str_to_re, Op.str_in_re, Op.re_none, Op.re_all, Op.re_allchar, Op.re_concat, Op.re_union, Op.re_inter, Op.re_star, Op.str_replace_re, Op.str_replace_re_all, Op.re_comp, Op.re_diff, Op.re_plus, Op.re_opt, Op.re_range, Op.re_loop, Op.re_index, Op.select, Op.store] -/ #guard_msgs in #genOpAbbrevs @@ -310,7 +315,9 @@ def Op.mkName : Op → String | .bvsmulo => "bvsmulo" | .bvconcat => "concat" | .zero_extend _ => "zero_extend" - | .bv2nat => "bv2nat" + | .ubv_to_int => "ubv_to_int" + | .sbv_to_int => "sbv_to_int" + | .int_to_bv _ => "int_to_bv" | .triggers => "triggers" | .option_get => "option.get" | .datatype_op .tester name => s!"is-{name}" @@ -351,6 +358,7 @@ def Op.mkName : Op → String def Op.LT : Op → Op → Bool | .uf f₁, .uf f₂ => f₁ < f₂ | .zero_extend n₁, .zero_extend n₂ => n₁ < n₂ + | .int_to_bv n₁, .int_to_bv n₂ => n₁ < n₂ | .re_index n₁, .re_index n₂ => n₁ < n₂ | .re_loop n₁ n₂, .re_loop m₁ m₂ => n₁ < n₂ && m₁ < m₂ | ty₁, ty₂ => ty₁.mkName < ty₂.mkName diff --git a/Strata/DL/SMT/Translate.lean b/Strata/DL/SMT/Translate.lean index e4961c5e66..aa9c58c1de 100644 --- a/Strata/DL/SMT/Translate.lean +++ b/Strata/DL/SMT/Translate.lean @@ -520,6 +520,15 @@ def translateTerm (t : SMT.Term) : TranslateM (Expr × Expr) := do let (α, x) ← translateTerm x let w ← getBitVecWidth α return (mkBitVec (w + i), mkApp3 (.const ``BitVec.zeroExtend []) (toExpr w) (toExpr (w + i)) x) + | .app .ubv_to_int [x] _ => + let (_, x) ← translateTerm x + return (mkInt, mkApp (.const ``Int.ofNat []) (mkApp (.const ``BitVec.toNat []) x)) + | .app .sbv_to_int [x] _ => + let (_, x) ← translateTerm x + return (mkInt, mkApp (.const ``BitVec.toInt []) x) + | .app (.int_to_bv n) [x] _ => + let (_, x) ← translateTerm x + return (mkBitVec n, mkApp2 (.const ``BitVec.ofInt []) (toExpr n) x) -- SMT-Lib theory of strings | .prim (.string s) => return (mkString, toExpr s) @@ -542,9 +551,6 @@ def translateTerm (t : SMT.Term) : TranslateM (Expr × Expr) := do expectString γ return e return (mkString, as.foldl (mkApp2 mkStringAppend) (mkApp2 mkStringAppend a b)) - | .app .bv2nat [x] _ => - let (_, x) ← translateTerm x - return (mkInt, mkApp (.const ``Int.ofNat []) (mkApp (.const ``BitVec.toNat []) x)) | t => throw m!"Error: unsupported term '{repr t}'" where leftAssocOp (op : Expr) (as : List SMT.Term) : TranslateM (Expr × Expr) := do diff --git a/Strata/Languages/Boole/Grammar.lean b/Strata/Languages/Boole/Grammar.lean index 2605b72ced..a41a0fba82 100644 --- a/Strata/Languages/Boole/Grammar.lean +++ b/Strata/Languages/Boole/Grammar.lean @@ -134,11 +134,23 @@ fn seq_drop_first (A : Type, s : Sequence A) : Sequence A => fn seq_subrange (A : Type, s : Sequence A, lo : int, hi : int) : Sequence A => "Sequence.subrange" "(" s ", " lo ", " hi ")"; -// Widening cast: `e as_int` converts any bitvector to an integer (unsigned). -// Lowers to a native `Bv{n}.ToNat : bvN → int` Core op → SMT-LIB `bv2nat`. -// Supported widths: 1, 8, 16, 32, 64, 128. No axioms injected. +// Unsigned widening cast: `e as_int` converts a bitvector to Int (unsigned). +// Lowers to `Bv{n}.ToUInt` Core op → SMT-LIB 2.7 `ubv_to_int`. fn cast_to_int (T : Type, e : T) : int => @[prec(80)] e " as_int"; +// Signed widening cast: `e as_sint` converts a bitvector to Int (signed, two's complement). +// Lowers to `Bv{n}.ToInt` Core op → SMT-LIB 2.7 `sbv_to_int`. +fn cast_to_sint (T : Type, e : T) : int => @[prec(80)] e " as_sint"; + +// Narrowing cast: `e as_bv{n}` converts an Int to a bitvector of width n (truncating mod 2^n). +// Lowers to `Int.ToBv{n}` Core op → SMT-LIB 2.7 `(_ int_to_bv n)`. +fn cast_to_bv1 (e : int) : bv1 => @[prec(80)] e " as_bv1"; +fn cast_to_bv8 (e : int) : bv8 => @[prec(80)] e " as_bv8"; +fn cast_to_bv16 (e : int) : bv16 => @[prec(80)] e " as_bv16"; +fn cast_to_bv32 (e : int) : bv32 => @[prec(80)] e " as_bv32"; +fn cast_to_bv64 (e : int) : bv64 => @[prec(80)] e " as_bv64"; +fn cast_to_bv128 (e : int) : bv128 => @[prec(80)] e " as_bv128"; + category Step; op step(e: Expr) : Step => " by " e; diff --git a/Strata/Languages/Boole/Verify.lean b/Strata/Languages/Boole/Verify.lean index f2749d3cd2..f900f39bbd 100644 --- a/Strata/Languages/Boole/Verify.lean +++ b/Strata/Languages/Boole/Verify.lean @@ -511,11 +511,23 @@ partial def toCoreExpr (e : Boole.Expr) : TranslateM Core.Expression.Expr := do match ty with | .bv1 _ | .bv8 _ | .bv16 _ | .bv32 _ | .bv64 _ | .bv128 _ => do let n ← bvWidth m ty - return mkCoreApp (.op () (mkIdent s!"Bv{n}.ToNat") none) [← toCoreExpr e] + return mkCoreApp (.op () (mkIdent s!"Bv{n}.ToUInt") none) [← toCoreExpr e] | .int _ => toCoreExpr e | _ => if ← isNatType ty then toCoreExpr e else throwAt m s!"'as int' requires a bitvector source type" + | .cast_to_sint m ty e => + match ty with + | .bv1 _ | .bv8 _ | .bv16 _ | .bv32 _ | .bv64 _ | .bv128 _ => do + let n ← bvWidth m ty + return mkCoreApp (.op () (mkIdent s!"Bv{n}.ToInt") none) [← toCoreExpr e] + | _ => throwAt m s!"'as sint' requires a bitvector source type" + | .cast_to_bv1 _ e => return mkCoreApp (.op () (mkIdent "Int.ToBv1") none) [← toCoreExpr e] + | .cast_to_bv8 _ e => return mkCoreApp (.op () (mkIdent "Int.ToBv8") none) [← toCoreExpr e] + | .cast_to_bv16 _ e => return mkCoreApp (.op () (mkIdent "Int.ToBv16") none) [← toCoreExpr e] + | .cast_to_bv32 _ e => return mkCoreApp (.op () (mkIdent "Int.ToBv32") none) [← toCoreExpr e] + | .cast_to_bv64 _ e => return mkCoreApp (.op () (mkIdent "Int.ToBv64") none) [← toCoreExpr e] + | .cast_to_bv128 _ e => return mkCoreApp (.op () (mkIdent "Int.ToBv128") none) [← toCoreExpr e] | _ => throw (.fromMessage s!"Unsupported expression: {repr e}") end diff --git a/Strata/Languages/Core/CoreOp.lean b/Strata/Languages/Core/CoreOp.lean index 657f7b6868..af2d2590dc 100644 --- a/Strata/Languages/Core/CoreOp.lean +++ b/Strata/Languages/Core/CoreOp.lean @@ -52,7 +52,8 @@ inductive BvOpKind where | SAddOverflow | SSubOverflow | SMulOverflow | SNegOverflow | SDivOverflow | UAddOverflow | USubOverflow | UMulOverflow | UNegOverflow -- Cross-sort conversion - | ToNat + | ToUInt -- unsigned bv → int (ubv_to_int) + | ToInt -- signed bv → int (sbv_to_int) deriving Repr, DecidableEq, Inhabited, BEq, Hashable structure BvOp where @@ -71,7 +72,7 @@ def BvOpKind.isPredicate : BvOpKind → Bool | _ => false def BvOpKind.isUnary : BvOpKind → Bool - | .Neg | .Not | .ToNat => true + | .Neg | .Not | .ToUInt | .ToInt => true | _ => false def BvOpKind.names : List (BvOpKind × String) := @@ -92,7 +93,7 @@ def BvOpKind.names : List (BvOpKind × String) := (.SDivOverflow, "SDivOverflow"), (.UAddOverflow, "UAddOverflow"), (.USubOverflow, "USubOverflow"), (.UMulOverflow, "UMulOverflow"), (.UNegOverflow, "UNegOverflow"), - (.ToNat, "ToNat")] + (.ToUInt, "ToUInt"), (.ToInt, "ToInt")] def BvOpKind.toString (k : BvOpKind) : String := lookupName names k instance : ToString BvOpKind := ⟨BvOpKind.toString⟩ @@ -244,6 +245,7 @@ inductive CoreOp where | map (kind : MapOpKind) | seq (kind : SeqOpKind) | bvExtract (size hi lo : Nat) + | intToBv (n : Nat) -- int → bv of width n (int_to_bv) | trigger (kind : TriggerOpKind) | other (name : String) deriving Repr, DecidableEq, Inhabited, BEq, Hashable @@ -260,6 +262,7 @@ def CoreOp.toString : CoreOp → String | .map kind => kind.toString | .seq kind => s!"Sequence.{kind}" | .bvExtract size hi lo => s!"Bv{size}.Extract_{hi}_{lo}" + | .intToBv n => s!"Int.ToBv{n}" | .trigger kind => kind.toString | .other name => name @@ -294,6 +297,12 @@ def CoreOp.ofString (name : String) : CoreOp := match parseBvOp? name with | some op => op | none => + -- Try "Int.ToBv{n}": int → bitvector of width n + if name.startsWith "Int.ToBv" then + match (name.drop 8).toString.toNat? with + | some n => .intToBv n + | none => .other name + else -- Try numeric ops: "Int.{kind}" or "Real.{kind}" let numPrefixes := [("Int.", NumericType.int), ("Real.", NumericType.real)] let numResult := numPrefixes.findSome? fun (pfx, ty) => diff --git a/Strata/Languages/Core/Factory.lean b/Strata/Languages/Core/Factory.lean index e5845a30d7..6410b529bf 100644 --- a/Strata/Languages/Core/Factory.lean +++ b/Strata/Languages/Core/Factory.lean @@ -770,19 +770,39 @@ def bvExtractFunc (size hi lo : Nat) : WFLFunc CoreLParams := unaryFuncUneval s!"Bv{size}.Extract_{hi}_{lo}" (.bitvec size) (.bitvec (hi + 1 - lo)) rfl rfl -def bvToNatFunc (size : Nat) : WFLFunc CoreLParams := - unaryFuncUneval s!"Bv{size}.ToNat" (.bitvec size) .int rfl rfl +def bvToUIntFunc (size : Nat) : WFLFunc CoreLParams := + unaryFuncUneval s!"Bv{size}.ToUInt" (.bitvec size) .int rfl rfl + +def bvToIntFunc (size : Nat) : WFLFunc CoreLParams := + unaryFuncUneval s!"Bv{size}.ToInt" (.bitvec size) .int rfl rfl + +def intToBvFunc (size : Nat) : WFLFunc CoreLParams := + unaryFuncUneval s!"Int.ToBv{size}" .int (.bitvec size) rfl rfl def bv8ConcatFunc := bvConcatFunc 8 def bv16ConcatFunc := bvConcatFunc 16 def bv32ConcatFunc := bvConcatFunc 32 -def bv1ToNatFunc := bvToNatFunc 1 -def bv8ToNatFunc := bvToNatFunc 8 -def bv16ToNatFunc := bvToNatFunc 16 -def bv32ToNatFunc := bvToNatFunc 32 -def bv64ToNatFunc := bvToNatFunc 64 -def bv128ToNatFunc := bvToNatFunc 128 +def bv1ToUIntFunc := bvToUIntFunc 1 +def bv8ToUIntFunc := bvToUIntFunc 8 +def bv16ToUIntFunc := bvToUIntFunc 16 +def bv32ToUIntFunc := bvToUIntFunc 32 +def bv64ToUIntFunc := bvToUIntFunc 64 +def bv128ToUIntFunc := bvToUIntFunc 128 + +def bv1ToIntFunc := bvToIntFunc 1 +def bv8ToIntFunc := bvToIntFunc 8 +def bv16ToIntFunc := bvToIntFunc 16 +def bv32ToIntFunc := bvToIntFunc 32 +def bv64ToIntFunc := bvToIntFunc 64 +def bv128ToIntFunc := bvToIntFunc 128 + +def int1ToBvFunc := intToBvFunc 1 +def int8ToBvFunc := intToBvFunc 8 +def int16ToBvFunc := intToBvFunc 16 +def int32ToBvFunc := intToBvFunc 32 +def int64ToBvFunc := intToBvFunc 64 +def int128ToBvFunc := intToBvFunc 128 def bv8Extract_7_7_Func := bvExtractFunc 8 7 7 def bv16Extract_15_15_Func := bvExtractFunc 16 15 15 @@ -874,12 +894,24 @@ def WFFactory : Lambda.WFLFactory CoreLParams := bv8ConcatFunc, bv16ConcatFunc, bv32ConcatFunc, - bv1ToNatFunc, - bv8ToNatFunc, - bv16ToNatFunc, - bv32ToNatFunc, - bv64ToNatFunc, - bv128ToNatFunc, + bv1ToUIntFunc, + bv8ToUIntFunc, + bv16ToUIntFunc, + bv32ToUIntFunc, + bv64ToUIntFunc, + bv128ToUIntFunc, + bv1ToIntFunc, + bv8ToIntFunc, + bv16ToIntFunc, + bv32ToIntFunc, + bv64ToIntFunc, + bv128ToIntFunc, + int1ToBvFunc, + int8ToBvFunc, + int16ToBvFunc, + int32ToBvFunc, + int64ToBvFunc, + int128ToBvFunc, bv8Extract_7_7_Func, bv16Extract_15_15_Func, bv16Extract_7_0_Func, diff --git a/Strata/Languages/Core/SMTEncoder.lean b/Strata/Languages/Core/SMTEncoder.lean index d8049b036a..176842c750 100644 --- a/Strata/Languages/Core/SMTEncoder.lean +++ b/Strata/Languages/Core/SMTEncoder.lean @@ -546,8 +546,10 @@ partial def toSMTOp (E : Env) (fn : CoreIdent) (fnty : LMonoTy) (ctx : SMT.Conte | .bv ⟨_, .SLe⟩ => .ok (.app Op.bvsle, .bool, ctx) | .bv ⟨_, .SGt⟩ => .ok (.app Op.bvsgt, .bool, ctx) | .bv ⟨_, .SGe⟩ => .ok (.app Op.bvsge, .bool, ctx) - | .bv ⟨n, .Concat⟩ => .ok (.app Op.bvconcat, .bitvec (n * 2), ctx) - | .bv ⟨_, .ToNat⟩ => .ok (.app Op.bv2nat, .int, ctx) + | .bv ⟨n, .Concat⟩ => .ok (.app Op.bvconcat, .bitvec (n * 2), ctx) + | .bv ⟨_, .ToUInt⟩ => .ok (.app Op.ubv_to_int, .int, ctx) + | .bv ⟨_, .ToInt⟩ => .ok (.app Op.sbv_to_int, .int, ctx) + | .intToBv n => .ok (.app (Op.int_to_bv n), .bitvec n, ctx) | .str .Length => .ok (.app Op.str_length, .int, ctx) | .str .Concat => .ok (.app Op.str_concat, .string, ctx) diff --git a/StrataTest/Languages/Boole/cast_all_directions.lean b/StrataTest/Languages/Boole/cast_all_directions.lean new file mode 100644 index 0000000000..c53a52bcd3 --- /dev/null +++ b/StrataTest/Languages/Boole/cast_all_directions.lean @@ -0,0 +1,98 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import Strata.MetaVerifier + +open Strata + +/- +Tests all three SMT-LIB 2.7 cast directions: + 1. `e as_int` — unsigned bv → Int (ubv_to_int) + 2. `e as_sint` — signed bv → Int (sbv_to_int) + 3. `e as_bv{n}` — Int → bv ((_ int_to_bv n)) +-/ + +private def castAllDirectionsSeed : Strata.Program := +#strata +program Boole; + +// (1) ubv_to_int: unsigned interpretation, always in [0, 255] +procedure test_ubv_to_int(x: bv8) returns () +spec { + ensures x as_int >= 0; + ensures x as_int <= 255; +} { + exit test_ubv_to_int; +}; + +// (2) sbv_to_int: signed interpretation, range [-128, 127] +procedure test_sbv_to_int(x: bv8) returns () +spec { + ensures x as_sint >= -128; + ensures x as_sint <= 127; +} { + exit test_sbv_to_int; +}; + +// (3) int_to_bv: truncating cast, result as_int == n for n in [0, 255] +procedure test_int_to_bv(n: int) returns (result: bv8) +spec { + requires 0 <= n && n < 256; + ensures result as_int == n; +} { + result := n as_bv8; + exit test_int_to_bv; +}; + +// Round-trip: (n as_bv8) as_int == n for n in [0, 255] +procedure test_roundtrip(n: int) returns () +spec { + requires 0 <= n && n < 256; + ensures (n as_bv8) as_int == n; +} { + exit test_roundtrip; +}; + +// Signed and unsigned agree when value is non-negative +procedure test_sign_agreement(x: bv8) returns () +spec { + requires x as_sint >= 0; + ensures x as_int == x as_sint; +} { + exit test_sign_agreement; +}; +#end + +/-- info: +Obligation: test_ubv_to_int_ensures_0_546 +Property: assert +Result: ✅ pass + +Obligation: test_ubv_to_int_ensures_1_571 +Property: assert +Result: ✅ pass + +Obligation: test_sbv_to_int_ensures_2_742 +Property: assert +Result: ✅ pass + +Obligation: test_sbv_to_int_ensures_3_771 +Property: assert +Result: ✅ pass + +Obligation: test_int_to_bv_ensures_5_995 +Property: assert +Result: ✅ pass + +Obligation: test_roundtrip_ensures_7_1215 +Property: assert +Result: ✅ pass + +Obligation: test_sign_agreement_ensures_9_1419 +Property: assert +Result: ✅ pass-/ +#guard_msgs in +#eval Strata.Boole.verify "cvc5" castAllDirectionsSeed (options := .quiet) diff --git a/StrataTest/Languages/Boole/cast_expr.lean b/StrataTest/Languages/Boole/cast_expr.lean index 0a0e70313d..76265cbb55 100644 --- a/StrataTest/Languages/Boole/cast_expr.lean +++ b/StrataTest/Languages/Boole/cast_expr.lean @@ -18,8 +18,8 @@ Near-upstream anchor: Feature: `e as_int` — widening cast from any bitvector type to `int`. -Lowers to a native `Bv{n}.ToNat : bvN → int` Core op; the SMT encoder maps -it to the standard SMT-LIB `bv2nat` function. No axioms injected. +Lowers to a native `Bv{n}.ToUInt : bvN → int` Core op; the SMT encoder maps +it to the SMT-LIB 2.7 `ubv_to_int` function. No axioms injected. -/ private def castExprSeed : Strata.Program := diff --git a/StrataTest/Languages/Boole/from_bytes_mod_order_wide_minimal.lean b/StrataTest/Languages/Boole/from_bytes_mod_order_wide_minimal.lean index 53f001f930..1f4d472f3f 100644 --- a/StrataTest/Languages/Boole/from_bytes_mod_order_wide_minimal.lean +++ b/StrataTest/Languages/Boole/from_bytes_mod_order_wide_minimal.lean @@ -1,3 +1,9 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + import Strata.MetaVerifier open Strata @@ -300,19 +306,19 @@ Obligation: scalar_as_canonical_body_calls_scalar..bytes_0 Property: assert Result: ✅ pass -Obligation: Impl__2_clone_ensures_0_2199 +Obligation: Impl__2_clone_ensures_0_2284 Property: assert Result: ✅ pass -Obligation: Impl__3_from_bytes_wide_ensures_1_2372 +Obligation: Impl__3_from_bytes_wide_ensures_1_2457 Property: assert Result: ✅ pass -Obligation: Impl__3_from_bytes_wide_ensures_2_2408 +Obligation: Impl__3_from_bytes_wide_ensures_2_2493 Property: assert Result: ✅ pass -Obligation: Impl__3_pack_post_Impl__3_pack_ensures_5_2741_calls_scalar..bytes_0 +Obligation: Impl__3_pack_post_Impl__3_pack_ensures_5_2826_calls_scalar..bytes_0 Property: assert Result: ✅ pass @@ -320,39 +326,39 @@ Obligation: set_result_calls_scalar..bytes_0 Property: assert Result: ✅ pass -Obligation: Impl__3_pack_ensures_5_2741 +Obligation: Impl__3_pack_ensures_5_2826 Property: assert Result: ✅ pass -Obligation: Impl__3_pack_ensures_6_2845 +Obligation: Impl__3_pack_ensures_6_2930 Property: assert Result: ✅ pass -Obligation: callElimAssert_Impl__3_pack_requires_4_2709_25 +Obligation: callElimAssert_Impl__3_pack_requires_4_2794_25 Property: assert Result: ✅ pass -Obligation: assume_callElimAssume_Impl__3_pack_ensures_5_2741_26_calls_scalar..bytes_0 +Obligation: assume_callElimAssume_Impl__3_pack_ensures_5_2826_26_calls_scalar..bytes_0 Property: assert Result: ✅ pass -Obligation: callElimAssert_lemma_scalar52_lt_pow2_256_if_canonical_requires_102_10101_19 +Obligation: callElimAssert_lemma_scalar52_lt_pow2_256_if_canonical_requires_102_10186_19 Property: assert Result: ✅ pass -Obligation: callElimAssert_lemma_scalar52_lt_pow2_256_if_canonical_requires_103_10130_20 +Obligation: callElimAssert_lemma_scalar52_lt_pow2_256_if_canonical_requires_103_10215_20 Property: assert Result: ✅ pass -Obligation: callElimAssert_Arithmetic_Div_mod_lemma_small_mod_requires_11_4213_15 +Obligation: callElimAssert_Arithmetic_Div_mod_lemma_small_mod_requires_11_4298_15 Property: assert Result: ✅ pass -Obligation: callElimAssert_Arithmetic_Div_mod_lemma_small_mod_requires_12_4231_16 +Obligation: callElimAssert_Arithmetic_Div_mod_lemma_small_mod_requires_12_4316_16 Property: assert Result: ✅ pass -Obligation: callElimAssert_Arithmetic_Div_mod_lemma_mod_bound_requires_15_4381_11 +Obligation: callElimAssert_Arithmetic_Div_mod_lemma_mod_bound_requires_15_4466_11 Property: assert Result: ✅ pass @@ -360,359 +366,359 @@ Obligation: set_tmp5_calls_scalar..bytes_0 Property: assert Result: ✅ pass -Obligation: callElimAssert_Arithmetic_Div_mod_lemma_small_mod_requires_11_4213_6 +Obligation: callElimAssert_Arithmetic_Div_mod_lemma_small_mod_requires_11_4298_6 Property: assert Result: ✅ pass -Obligation: callElimAssert_Arithmetic_Div_mod_lemma_small_mod_requires_12_4231_7 +Obligation: callElimAssert_Arithmetic_Div_mod_lemma_small_mod_requires_12_4316_7 Property: assert Result: ✅ pass -Obligation: callElimAssert_axiom_uniform_mod_reduction_requires_105_10489_2 +Obligation: callElimAssert_axiom_uniform_mod_reduction_requires_105_10574_2 Property: assert Result: ✅ pass -Obligation: Impl__4_from_bytes_mod_order_wide_ensures_8_3119 +Obligation: Impl__4_from_bytes_mod_order_wide_ensures_8_3204 Property: assert Result: ✅ pass -Obligation: Impl__4_from_bytes_mod_order_wide_ensures_9_3202 +Obligation: Impl__4_from_bytes_mod_order_wide_ensures_9_3287 Property: assert Result: ✅ pass -Obligation: Impl__4_from_bytes_mod_order_wide_ensures_10_3241 +Obligation: Impl__4_from_bytes_mod_order_wide_ensures_10_3326 Property: assert Result: ✅ pass -Obligation: Arithmetic_Div_mod_lemma_small_mod_ensures_13_4249 +Obligation: Arithmetic_Div_mod_lemma_small_mod_ensures_13_4334 Property: assert Result: ✅ pass -Obligation: Arithmetic_Div_mod_lemma_mod_bound_ensures_16_4399 +Obligation: Arithmetic_Div_mod_lemma_mod_bound_ensures_16_4484 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma_pow2_adds_ensures_18_4547 +Obligation: Arithmetic_Power2_lemma_pow2_adds_ensures_18_4632 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma_pow2_strictly_increases_ensures_21_4792 +Obligation: Arithmetic_Power2_lemma_pow2_strictly_increases_ensures_21_4877 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_ensures_23_4946 +Obligation: Arithmetic_Power2_lemma2_to64_ensures_23_5031 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_ensures_24_4988 +Obligation: Arithmetic_Power2_lemma2_to64_ensures_24_5073 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_ensures_25_5030 +Obligation: Arithmetic_Power2_lemma2_to64_ensures_25_5115 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_ensures_26_5072 +Obligation: Arithmetic_Power2_lemma2_to64_ensures_26_5157 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_ensures_27_5114 +Obligation: Arithmetic_Power2_lemma2_to64_ensures_27_5199 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_ensures_28_5157 +Obligation: Arithmetic_Power2_lemma2_to64_ensures_28_5242 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_ensures_29_5200 +Obligation: Arithmetic_Power2_lemma2_to64_ensures_29_5285 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_ensures_30_5243 +Obligation: Arithmetic_Power2_lemma2_to64_ensures_30_5328 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_ensures_31_5287 +Obligation: Arithmetic_Power2_lemma2_to64_ensures_31_5372 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_ensures_32_5331 +Obligation: Arithmetic_Power2_lemma2_to64_ensures_32_5416 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_ensures_33_5375 +Obligation: Arithmetic_Power2_lemma2_to64_ensures_33_5460 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_ensures_34_5421 +Obligation: Arithmetic_Power2_lemma2_to64_ensures_34_5506 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_ensures_35_5467 +Obligation: Arithmetic_Power2_lemma2_to64_ensures_35_5552 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_ensures_36_5513 +Obligation: Arithmetic_Power2_lemma2_to64_ensures_36_5598 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_ensures_37_5559 +Obligation: Arithmetic_Power2_lemma2_to64_ensures_37_5644 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_ensures_38_5606 +Obligation: Arithmetic_Power2_lemma2_to64_ensures_38_5691 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_ensures_39_5653 +Obligation: Arithmetic_Power2_lemma2_to64_ensures_39_5738 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_ensures_40_5700 +Obligation: Arithmetic_Power2_lemma2_to64_ensures_40_5785 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_ensures_41_5748 +Obligation: Arithmetic_Power2_lemma2_to64_ensures_41_5833 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_ensures_42_5796 +Obligation: Arithmetic_Power2_lemma2_to64_ensures_42_5881 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_ensures_43_5844 +Obligation: Arithmetic_Power2_lemma2_to64_ensures_43_5929 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_ensures_44_5893 +Obligation: Arithmetic_Power2_lemma2_to64_ensures_44_5978 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_ensures_45_5942 +Obligation: Arithmetic_Power2_lemma2_to64_ensures_45_6027 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_ensures_46_5991 +Obligation: Arithmetic_Power2_lemma2_to64_ensures_46_6076 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_ensures_47_6040 +Obligation: Arithmetic_Power2_lemma2_to64_ensures_47_6125 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_ensures_48_6090 +Obligation: Arithmetic_Power2_lemma2_to64_ensures_48_6175 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_ensures_49_6140 +Obligation: Arithmetic_Power2_lemma2_to64_ensures_49_6225 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_ensures_50_6190 +Obligation: Arithmetic_Power2_lemma2_to64_ensures_50_6275 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_ensures_51_6241 +Obligation: Arithmetic_Power2_lemma2_to64_ensures_51_6326 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_ensures_52_6292 +Obligation: Arithmetic_Power2_lemma2_to64_ensures_52_6377 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_ensures_53_6343 +Obligation: Arithmetic_Power2_lemma2_to64_ensures_53_6428 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_ensures_54_6395 +Obligation: Arithmetic_Power2_lemma2_to64_ensures_54_6480 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_ensures_55_6447 +Obligation: Arithmetic_Power2_lemma2_to64_ensures_55_6532 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_ensures_56_6499 +Obligation: Arithmetic_Power2_lemma2_to64_ensures_56_6584 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_58_6653 +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_58_6738 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_59_6705 +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_59_6790 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_60_6758 +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_60_6843 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_61_6811 +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_61_6896 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_62_6864 +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_62_6949 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_63_6918 +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_63_7003 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_64_6972 +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_64_7057 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_65_7026 +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_65_7111 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_66_7081 +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_66_7166 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_67_7136 +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_67_7221 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_68_7191 +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_68_7276 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_69_7246 +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_69_7331 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_70_7302 +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_70_7387 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_71_7358 +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_71_7443 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_72_7414 +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_72_7499 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_73_7471 +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_73_7556 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_74_7528 +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_74_7613 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_75_7585 +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_75_7670 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_76_7643 +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_76_7728 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_77_7701 +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_77_7786 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_78_7759 +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_78_7844 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_79_7817 +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_79_7902 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_80_7876 +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_80_7961 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_81_7935 +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_81_8020 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_82_7994 +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_82_8079 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_83_8054 +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_83_8139 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_84_8114 +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_84_8199 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_85_8174 +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_85_8259 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_86_8235 +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_86_8320 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_87_8296 +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_87_8381 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_88_8357 +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_88_8442 Property: assert Result: ✅ pass -Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_89_8418 +Obligation: Arithmetic_Power2_lemma2_to64_rest_ensures_89_8503 Property: assert Result: ✅ pass -Obligation: assert_93_8755 +Obligation: assert_93_8840 Property: assert Result: ✅ pass -Obligation: assert_95_8925 +Obligation: assert_95_9010 Property: assert Result: ✅ pass -Obligation: assert_96_9005 +Obligation: assert_96_9090 Property: assert Result: ✅ pass -Obligation: callElimAssert_Arithmetic_Power2_lemma_pow2_strictly_increases_requires_20_4772_75 +Obligation: callElimAssert_Arithmetic_Power2_lemma_pow2_strictly_increases_requires_20_4857_75 Property: assert Result: ✅ pass -Obligation: assert_98_9268 +Obligation: assert_98_9353 Property: assert Result: ✅ pass -Obligation: assert_99_9440 +Obligation: assert_99_9525 Property: assert Result: ✅ pass -Obligation: callElimAssert_Arithmetic_Power2_lemma_pow2_strictly_increases_requires_20_4772_34 +Obligation: callElimAssert_Arithmetic_Power2_lemma_pow2_strictly_increases_requires_20_4857_34 Property: assert Result: ✅ pass -Obligation: lemma_group_order_bound_ensures_91_8561 +Obligation: lemma_group_order_bound_ensures_91_8646 Property: assert Result: ✅ pass -Obligation: callElimAssert_Arithmetic_Power2_lemma_pow2_strictly_increases_requires_20_4772_114 +Obligation: callElimAssert_Arithmetic_Power2_lemma_pow2_strictly_increases_requires_20_4857_114 Property: assert Result: ✅ pass -Obligation: lemma_group_order_smaller_than_pow256_ensures_101_9809 +Obligation: lemma_group_order_smaller_than_pow256_ensures_101_9894 Property: assert Result: ✅ pass -Obligation: callElimAssert_Arithmetic_Power2_lemma_pow2_strictly_increases_requires_20_4772_119 +Obligation: callElimAssert_Arithmetic_Power2_lemma_pow2_strictly_increases_requires_20_4857_119 Property: assert Result: ✅ pass -Obligation: lemma_scalar52_lt_pow2_256_if_canonical_ensures_104_10175 +Obligation: lemma_scalar52_lt_pow2_256_if_canonical_ensures_104_10260 Property: assert Result: ✅ pass -Obligation: axiom_uniform_mod_reduction_ensures_106_10572 +Obligation: axiom_uniform_mod_reduction_ensures_106_10657 Property: assert Result: ✅ pass-/ #guard_msgs in diff --git a/StrataTest/Languages/Boole/widening_casts.lean b/StrataTest/Languages/Boole/widening_casts.lean index 82dfdc3d1b..0c9a2ccc21 100644 --- a/StrataTest/Languages/Boole/widening_casts.lean +++ b/StrataTest/Languages/Boole/widening_casts.lean @@ -18,7 +18,7 @@ Near-upstream anchors from `differential_status.md`: `quantifiers`: https://github.com/verus-lang/verus/blob/main/examples/quantifiers.rs `statements`: https://github.com/verus-lang/verus/blob/main/examples/statements.rs -Gap #6 implemented: `e as_int` lowers to native `Bv{n}.ToNat` Core op → SMT-LIB `bv2nat`. +Gap #6 implemented: `e as_int` lowers to native `Bv{n}.ToUInt` Core op → SMT-LIB 2.7 `ubv_to_int`. No axioms injected. -/ @@ -26,7 +26,7 @@ private def wideningCastsSeed : Strata.Program := #strata program Boole; -// `v[i] as_int` lowers to `Bv32.ToNat` Core op → SMT-LIB `bv2nat`. +// `v[i] as_int` lowers to `Bv32.ToUInt` Core op → SMT-LIB 2.7 `ubv_to_int`. procedure widening_cast_seed(v: Map int bv32, n: int) returns () spec { requires 0 <= n; @@ -38,11 +38,11 @@ spec { #end /-- info: -Obligation: assert_2_979 +Obligation: assert_2_997 Property: assert Result: ✅ pass -Obligation: widening_cast_seed_ensures_1_911 +Obligation: widening_cast_seed_ensures_1_929 Property: assert Result: ✅ pass-/ #guard_msgs in diff --git a/StrataTest/Languages/Core/Tests/ProgramEvalTests.lean b/StrataTest/Languages/Core/Tests/ProgramEvalTests.lean index 23ae46ac40..eaacd65b0c 100644 --- a/StrataTest/Languages/Core/Tests/ProgramEvalTests.lean +++ b/StrataTest/Languages/Core/Tests/ProgramEvalTests.lean @@ -98,12 +98,24 @@ func TriggerGroup.addTrigger : ∀[a]. ((x : a) (t : TriggerGroup)) → TriggerG func Bv8.Concat : ((x : bv8) (y : bv8)) → bv16; func Bv16.Concat : ((x : bv16) (y : bv16)) → bv32; func Bv32.Concat : ((x : bv32) (y : bv32)) → bv64; -func Bv1.ToNat : ((x : bv1)) → int; -func Bv8.ToNat : ((x : bv8)) → int; -func Bv16.ToNat : ((x : bv16)) → int; -func Bv32.ToNat : ((x : bv32)) → int; -func Bv64.ToNat : ((x : bv64)) → int; -func Bv128.ToNat : ((x : bv128)) → int; +func Bv1.ToUInt : ((x : bv1)) → int; +func Bv8.ToUInt : ((x : bv8)) → int; +func Bv16.ToUInt : ((x : bv16)) → int; +func Bv32.ToUInt : ((x : bv32)) → int; +func Bv64.ToUInt : ((x : bv64)) → int; +func Bv128.ToUInt : ((x : bv128)) → int; +func Bv1.ToInt : ((x : bv1)) → int; +func Bv8.ToInt : ((x : bv8)) → int; +func Bv16.ToInt : ((x : bv16)) → int; +func Bv32.ToInt : ((x : bv32)) → int; +func Bv64.ToInt : ((x : bv64)) → int; +func Bv128.ToInt : ((x : bv128)) → int; +func Int.ToBv1 : ((x : int)) → bv1; +func Int.ToBv8 : ((x : int)) → bv8; +func Int.ToBv16 : ((x : int)) → bv16; +func Int.ToBv32 : ((x : int)) → bv32; +func Int.ToBv64 : ((x : int)) → bv64; +func Int.ToBv128 : ((x : int)) → bv128; func Bv8.Extract_7_7 : ((x : bv8)) → bv1; func Bv16.Extract_15_15 : ((x : bv16)) → bv1; func Bv16.Extract_7_0 : ((x : bv16)) → bv8; diff --git a/StrataTest/Languages/Core/Tests/StatisticsTest.lean b/StrataTest/Languages/Core/Tests/StatisticsTest.lean index 7fd98ba80f..78cbfd751e 100644 --- a/StrataTest/Languages/Core/Tests/StatisticsTest.lean +++ b/StrataTest/Languages/Core/Tests/StatisticsTest.lean @@ -32,7 +32,7 @@ spec { #end /-- -info: [statistics] Evaluator.factoryOps: 292 +info: [statistics] Evaluator.factoryOps: 304 [statistics] Evaluator.procedures: 1 [statistics] Evaluator.simulatedStmts: 2 [statistics] Evaluator.verificationEnvironments: 1 @@ -74,7 +74,7 @@ spec { #end /-- -info: [statistics] Evaluator.factoryOps: 292 +info: [statistics] Evaluator.factoryOps: 304 [statistics] Evaluator.functions: 1 [statistics] Evaluator.procedures: 2 [statistics] Evaluator.simulatedStmts: 4 diff --git a/docs/BooleFeatureRequests.md b/docs/BooleFeatureRequests.md index d9b869bbd3..e22466e445 100644 --- a/docs/BooleFeatureRequests.md +++ b/docs/BooleFeatureRequests.md @@ -57,10 +57,12 @@ seeds with at least one open gap remain in - `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`](../StrataTest/Languages/Boole/FeatureRequests/lambda_closure.lean). -- **Widening casts** (`e as_int`) (Gap #6 partial) - - `e as_int` lowers to `Bv{n}.ToNat` (Core op) → SMT-LIB `bv2nat`; widths 1/8/16/32/64/128. - - Remaining: int→BV cast (`x as bv32` etc.). - - Benchmarks: [`cast_expr.lean`](../StrataTest/Languages/Boole/cast_expr.lean), [`widening_casts.lean`](../StrataTest/Languages/Boole/widening_casts.lean). +- **SMT-LIB 2.7 cast operators** (`e as_int`, `e as_sint`, `e as_bv{n}`) (Gap #6) + - `e as_int` lowers to `Bv{n}.ToUInt` (Core op) → SMT-LIB 2.7 `ubv_to_int` (unsigned); widths 1/8/16/32/64/128. + - `e as_sint` lowers to `Bv{n}.ToInt` (Core op) → SMT-LIB 2.7 `sbv_to_int` (signed/two's complement); widths 1/8/16/32/64/128. + - `e as_bv{n}` lowers to `Int.ToBv{n}` (Core op) → SMT-LIB 2.7 `(_ int_to_bv n)` (truncating mod 2^n); widths 1/8/16/32/64/128. + - All three directions fully implemented end-to-end (grammar → Core → SMT encoder → denotation). + - Benchmarks: [`cast_expr.lean`](../StrataTest/Languages/Boole/cast_expr.lean), [`widening_casts.lean`](../StrataTest/Languages/Boole/widening_casts.lean), [`cast_all_directions.lean`](../StrataTest/Languages/Boole/cast_all_directions.lean). - **`type nat := int` synonym** (Gap #8 partial) - Nullary synonyms expanding to `int` trigger auto-axioms `∀ x : DT . DT..isCtor(x) ⟹ DT..field(x) ≥ 0` for each `nat`-typed constructor field. - Known limitation: axiom may be unsound for mixed `nat`/`int` datatypes. See [`nat_axiom_limitation.lean`](../StrataTest/Languages/Boole/FeatureRequests/nat_axiom_limitation.lean). @@ -74,7 +76,7 @@ seeds with at least one open gap remain in 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. **Widening casts**: Implemented. +6. **SMT-LIB 2.7 cast operators** (`as_int`, `as_sint`, `as_bv{n}`): Implemented. 7. **`decreases` metadata**: Implemented. ## Type/model requests From 8eeb90992ee4fd69c80b7eec05f18a6eac40bf06 Mon Sep 17 00:00:00 2001 From: Lydia Kondylidou <33327056+kondylidou@users.noreply.github.com> Date: Wed, 20 May 2026 23:10:20 +0200 Subject: [PATCH 19/20] delete the nat int synonym --- Strata/Languages/Boole/Verify.lean | 92 +-------- .../FeatureRequests/nat_axiom_limitation.lean | 181 ------------------ docs/BooleFeatureRequests.md | 14 +- 3 files changed, 10 insertions(+), 277 deletions(-) delete mode 100644 StrataTest/Languages/Boole/FeatureRequests/nat_axiom_limitation.lean diff --git a/Strata/Languages/Boole/Verify.lean b/Strata/Languages/Boole/Verify.lean index f900f39bbd..df288aae5c 100644 --- a/Strata/Languages/Boole/Verify.lean +++ b/Strata/Languages/Boole/Verify.lean @@ -50,10 +50,6 @@ structure TranslateState where `getFVarIsOp` as the `command_var` carve-out for op-vs-var classification. -/ globalVarTypes : Std.HashMap String Lambda.LMonoTy := {} - /-- Names of nullary type synonyms that expand directly to `int`, collected - in a pre-pass. A field whose Boole type resolves to one of these names - is treated as `nat` and gets an automatic non-negativity axiom. -/ - natSynonyms : Std.HashSet String := {} abbrev TranslateM := StateT TranslateState (Except DiagnosticModel) @@ -260,13 +256,6 @@ def toCoreMonoType (t : Boole.Type) : TranslateM Lambda.LMonoTy := do def toCoreType (t : Boole.Type) : TranslateM Core.Expression.Ty := do return .forAll [] (← toCoreMonoType t) -private def isNatType (t : Boole.Type) : TranslateM Bool := do - match t with - | .fvar m i _ => - let name ← getFVarName m i - return (← get).natSynonyms.contains name - | _ => return false - private def toCoreBinding (b : BooleDDM.Binding SourceRange) : TranslateM (Core.Expression.Ident × Lambda.LMonoTy) := do match b with | .mkBinding _ ⟨_, n⟩ tp | .outBinding _ ⟨_, n⟩ tp @@ -317,10 +306,7 @@ def toCoreTypedUn (m : SourceRange) (ty : Boole.Type) (op : String) (a : Core.Ex | .int _ => let iop : Core.Expression.Expr := .op () ⟨s!"Int.{op}", ()⟩ none return .app () iop a - | _ => - if ← isNatType ty then - return .app () (.op () ⟨s!"Int.{op}", ()⟩ none) a - else toCoreBvUn m ty op a + | _ => toCoreBvUn m ty op a -- Bitvector comparison operators use unsigned variants by default (Le→ULe, etc.). -- Signed variants use the explicit bvslt/bvsle nodes. @@ -334,10 +320,7 @@ def toCoreTypedBin (m : SourceRange) (ty : Boole.Type) (op : String) (a b : Core | .int _ => let iop : Core.Expression.Expr := .op () ⟨s!"Int.{op}", ()⟩ none return mkCoreApp iop [a, b] - | _ => - if ← isNatType ty then - return mkCoreApp (.op () ⟨s!"Int.{op}", ()⟩ none) [a, b] - else toCoreBvBin m ty (toBvCmpOp op) a b + | _ => toCoreBvBin m ty (toBvCmpOp op) a b private def toCoreExtensionalEq (m : SourceRange) @@ -513,9 +496,7 @@ partial def toCoreExpr (e : Boole.Expr) : TranslateM Core.Expression.Expr := do let n ← bvWidth m ty return mkCoreApp (.op () (mkIdent s!"Bv{n}.ToUInt") none) [← toCoreExpr e] | .int _ => toCoreExpr e - | _ => - if ← isNatType ty then toCoreExpr e - else throwAt m s!"'as int' requires a bitvector source type" + | _ => throwAt m s!"'as int' requires a bitvector source type" | .cast_to_sint m ty e => match ty with | .bv1 _ | .bv8 _ | .bv16 _ | .bv32 _ | .bv64 _ | .bv128 _ => do @@ -852,55 +833,6 @@ private def toCoreDatatype constrs := constrs constrs_ne := by simp } --- For each constructor field whose Boole type is nat-like, emit an axiom: --- ∀ x : DatatypeName . DatatypeName..isCtor(x) ⟹ DatatypeName..field(x) ≥ 0 --- Only generated for datatypes without type parameters (parameterised datatypes --- would require type-level quantification not currently supported here). -private def natAxiomsForDatatype - (dtypeName : String) - (typeParams : List String) - (ctors : BooleDDM.ConstructorList SourceRange) : TranslateM (List Core.Decl) := do - if !typeParams.isEmpty then return [] - let dtypeTy : Lambda.LMonoTy := .tcons dtypeName [] - let bv0 : Core.Expression.Expr := .bvar () 0 - let mut axioms : List Core.Decl := [] - for ctor in constructorListToList ctors do - match ctor with - | .constructor_mk _ ⟨_, cname⟩ ⟨_, fields?⟩ => - let fields : List (BooleDDM.Binding SourceRange) := match fields? with - | none => [] - | some ⟨_, fs⟩ => fs.toList - let testerName := s!"{dtypeName}..is{cname}" - -- Check for mixed nat/int constructor: if some fields are nat and others are - -- int, the generated axiom applies to all SMT terms of this datatype type and - -- may create an inconsistency if the solver introduces a synthetic term with a - -- negative nat field. Warn so the user is aware. - let fieldTypes := fields.filterMap fun f => match f with - | .mkBinding _ _ (.expr ty) => some ty | _ => none - let hasNat := (← fieldTypes.mapM isNatType).any id - let hasInt := fieldTypes.any fun ty => match ty with | .int _ => true | _ => false - if hasNat && hasInt then - dbg_trace s!"[Boole] Warning: constructor `{dtypeName}.{cname}` has both `nat`- and `int`-typed fields. \ - The auto-generated non-negativity axiom is globally quantified over all SMT terms of type `{dtypeName}`, \ - which may be unsound if the solver introduces synthetic terms with negative nat fields." - for field in fields do - match field with - | .mkBinding _ ⟨_, fieldName⟩ tp => - match tp with - | .expr fieldTy => - if ← isNatType fieldTy then - let selectorName := s!"{dtypeName}..{fieldName}" - let tester := mkCoreApp (.op () ⟨testerName, ()⟩ none) [bv0] - let selector := mkCoreApp (.op () ⟨selectorName, ()⟩ none) [bv0] - let geZero := mkCoreApp Core.intGeOp [selector, .intConst () 0] - let implies := mkCoreApp Core.boolImpliesOp [tester, geZero] - let axExpr : Core.Expression.Expr := .quant () .all "x" (some dtypeTy) bv0 implies - let axName := s!"{dtypeName}_{cname}_{fieldName}_nonneg" - axioms := axioms ++ [.ax { name := axName, e := axExpr } .empty] - | _ => pure () - | _ => pure () - return axioms - private def toCoreDatatypeDecl (decl : BooleDDM.DatatypeDecl SourceRange) : TranslateM (Lambda.LDatatype Unit) := do match decl with | .datatype_decl m ⟨_, dtypeName⟩ ⟨_, typeParams?⟩ ctors => @@ -1101,14 +1033,7 @@ def toCoreDecls (cmd : BooleDDM.Command SourceRange) : TranslateM (List Core.Dec } .empty] | .command_datatypes _ ⟨_, decls⟩ => let datatypes ← decls.toList.mapM toCoreDatatypeDecl - let natAxioms ← decls.toList.mapM fun decl => - match decl with - | .datatype_decl _ ⟨_, dtypeName⟩ ⟨_, typeParams?⟩ ctors => - let typeParams := match typeParams? with - | none => [] - | some bs => (bindingsToList bs).map bindingName - withTypeBVars typeParams (natAxiomsForDatatype dtypeName typeParams ctors) - return .type (.data datatypes) .empty :: natAxioms.flatten + return [.type (.data datatypes) .empty] /-- Render a `Boole.Program` to a format object using the provided `GlobalContext` and `DialectMap`. These should come from the originating `Strata.Program` (i.e. `env.globalContext` @@ -1128,10 +1053,9 @@ def formatProgram (prog : Boole.Program) (gctx : GlobalContext) (dialects : Dial def toCoreProgram (p : Boole.Program) (gctx : GlobalContext := {}) (fileName : String := "") : Except DiagnosticModel Core.Program := do match p with | .prog _ ⟨_, cmds⟩ => - -- Pre-pass: collect global variable types, modifies info, and nat synonyms. + -- Pre-pass: collect global variable types and modifies info. let mut varTypes : Std.HashMap String Lambda.LMonoTy := {} let mut modMap : Std.HashMap String (List (Core.Expression.Ident × Lambda.LMonoTy)) := {} - let mut natSynonyms : Std.HashSet String := {} for cmd in cmds do match cmd with | .command_var _ b => @@ -1146,18 +1070,12 @@ def toCoreProgram (p : Boole.Program) (gctx : GlobalContext := {}) (fileName : S | .command_procedure _ nameAnn _ _ specAnn _ => let mods ← collectModifiesFromSpec fileName nameAnn.val specAnn.val varTypes if !mods.isEmpty then modMap := modMap.insert nameAnn.val mods - | .command_typesynonym _ ⟨_, n⟩ ⟨_, args?⟩ _ rhs => - if args?.isNone then - match (toCoreMonoType rhs).run' { gctx := gctx } with - | .ok .int => natSynonyms := natSynonyms.insert n - | _ => pure () | _ => pure () let init : TranslateState := { fileName := fileName gctx := gctx modifiesMap := modMap globalVarTypes := varTypes - natSynonyms := natSynonyms } let act : TranslateM Core.Program := do let decls := (← cmds.mapM toCoreDecls).toList.flatten diff --git a/StrataTest/Languages/Boole/FeatureRequests/nat_axiom_limitation.lean b/StrataTest/Languages/Boole/FeatureRequests/nat_axiom_limitation.lean deleted file mode 100644 index 0a63a10853..0000000000 --- a/StrataTest/Languages/Boole/FeatureRequests/nat_axiom_limitation.lean +++ /dev/null @@ -1,181 +0,0 @@ -/- - Copyright Strata Contributors - - SPDX-License-Identifier: Apache-2.0 OR MIT --/ - -import Strata.MetaVerifier - -open Strata - -/- -Discussion: `type nat := int` + auto-generated non-negativity axioms - -Abdal's proposed design -─────────────────────── - type nat := int; - datatype NatList { Nil(), Cons(head: nat, tail: NatList) }; - -- auto-generated: - axiom (∀ l : NatList :: NatList..isCons(l) ==> NatList..head(l) >= 0) - -The auto-axiom lets any procedure that receives a NatList immediately derive -`head(l) >= 0` from `isCons(l)`, without a manual assumes/requires. - -──────────────────────────────────────────────────────────────────────────── -CASE 1 — WORKS: homogeneous nat-field list -──────────────────────────────────────────────────────────────────────────── -NatList has only `nat` fields. The auto-axiom fires and the postcondition -`head(l) >= 0` is proved without a manual requires. ✅ intended behaviour. --/ - -private def natListCase : Strata.Program := -#strata -program Boole; - -type nat := int; - -datatype NatList { - Nil(), - Cons(head: nat, tail: NatList) -}; - -procedure use_nat_list(l: NatList) returns () -spec { - requires NatList..isCons(l); - ensures NatList..head(l) >= 0; -} { - exit use_nat_list; -}; -#end - -/-- info: -Obligation: use_nat_list_post_use_nat_list_ensures_1_1512_calls_NatList..head_0 -Property: assert -Result: ✅ pass - -Obligation: use_nat_list_ensures_1_1512 -Property: assert -Result: ✅ pass-/ -#guard_msgs in -#eval Strata.Boole.verify "cvc5" natListCase (options := .quiet) - -/- -──────────────────────────────────────────────────────────────────────────── -CASE 2 — BROKEN: mixed nat/int fields in the same datatype -──────────────────────────────────────────────────────────────────────────── -`Pair` has `first : nat` (gets the auto-axiom) and `second : int` (does not). - -The auto-axiom emitted is: - ∀ x : Pair . Pair..isPair_mk(x) ==> Pair..first(x) >= 0 - -Problem: the SMT solver (cvc5 1.3.3) can instantiate this forall with the -synthetic term x := Pair_mk(Pair_second(p), 0). -By the ADT selector axiom, Pair_first(Pair_mk(Pair_second(p), 0)) = Pair_second(p). -So the axiom instance becomes: Pair_second(p) >= 0. - -This means ANY query that contains both this datatype and a negative `int` -value becomes inconsistent in the SMT model — even when `second` is -completely unrelated to `first`. - -Illustration: the procedure below has precondition `second(p) < 0` and -postcondition `second(p) >= 0`, which is logically false. But it passes (✅) -because the auto-axiom makes the SMT context inconsistent. -This is a soundness hole for the mixed-field case. --/ - -private def mixedPairCase : Strata.Program := -#strata -program Boole; - -type nat := int; - -datatype Pair { - Pair_mk(first: nat, second: int) -}; - -procedure unsound_example(p: Pair) returns () -spec { - requires Pair..isPair_mk(p) && Pair..second(p) < 0; - ensures Pair..second(p) >= 0; -} { - exit unsound_example; -}; -#end - --- ⚠️ This should be ❌ fail but is ✅ pass — the auto-axiom is too strong. -/-- info: [Boole] Warning: constructor `Pair.Pair_mk` has both `nat`- and `int`-typed fields. The auto-generated non-negativity axiom is globally quantified over all SMT terms of type `Pair`, which may be unsound if the solver introduces synthetic terms with negative nat fields. ---- -info: -Obligation: unsound_example_pre_unsound_example_requires_0_3451_calls_Pair..second_0 -Property: assert -Result: ✅ pass - -Obligation: unsound_example_post_unsound_example_ensures_1_3505_calls_Pair..second_0 -Property: assert -Result: ✅ pass - -Obligation: unsound_example_ensures_1_3505 -Property: assert -Result: ✅ pass-/ -#guard_msgs in -#eval Strata.Boole.verify "cvc5" mixedPairCase (options := .quiet) - -/- -Why it happens — the minimal SMT formula -───────────────────────────────────────── -The SMT problem sent to cvc5 for `unsound_example_ensures` is: - - (set-logic ALL) - (declare-datatype Pair ((Pair_mk (Pair..first Int) (Pair..second Int)))) - ; auto-axiom for first : nat - (assert (forall (($bv0 Pair)) (=> (|is-Pair_mk| $bv0) (>= (Pair..first $bv0) 0)))) - ; precondition - (assert (and (|is-Pair_mk| p) (< (Pair..second p) 0))) - ; negated goal (validity check) - (assert (not (>= (Pair..second p) 0))) - (check-sat) ; → unsat (should be sat) - -Manually verified: `cvc5 min.smt2` returns `unsat` with this formula. -Without the forall assert it returns `sat` (correct). - -Root cause: the `forall` is a global SMT assertion over ALL Pair terms in -the universe, including synthetic ones. Instantiating with - $bv0 := Pair_mk(Pair..second(p), 0) -gives Pair..first(Pair_mk(Pair..second(p), 0)) >= 0, -which simplifies to Pair..second(p) >= 0 (by the ADT selector axiom). -This contradicts Pair..second(p) < 0, making the context inconsistent. - -──────────────────────────────────────────────────────────────────────────── -DESIGN ALTERNATIVES -──────────────────────────────────────────────────────────────────────────── - -Option A — Status quo + documented restriction - Keep the auto-axiom. Document that `nat` fields must not be mixed with - unconstrained `int` fields in the same datatype when the `nat` axiom is - active. Works for all five dalek-lite benchmarks (B1–B5) since their - `nat`-like fields are either separate datatypes or all-`nat` constructors. - Simplest path; no SMT change required. - -Option B — Distinct abstract type (existing nat_int_boundary.lean approach) - Keep `type nat;` as an abstract sort (not a synonym for int). - Add explicit coercions: - function nat_to_int(n: nat) : int; - axiom (∀ n : nat . nat_to_int(n) >= 0); -- one axiom, no ADT interaction - `nat` and `int` live in separate SMT sorts — no quantifier instantiation - issue. Downside: every use of a `nat` field requires an explicit - `nat_to_int` call, adding coercion noise to specs. - -Option C — Constructor-site preconditions instead of a global axiom - Don't emit a global forall axiom. Instead, when a procedure receives a - datatype value, add a ghost `requires` (or an `assume`) that the `nat` - fields are non-negative. This is local and never interacts with unrelated - `int` values. Downside: either the user must state it manually, or the - translator must detect "datatype parameter" inputs and inject the assumes - automatically — more complex but semantically precise. - -Option D — Keep auto-axiom but restrict it to programs with no bare `int` fields - Only emit the nonneg axiom if ALL non-recursive fields of the datatype are - `nat` (or other non-negative types). Mixed nat/int datatypes fall back to - Option B or C. Conservative; avoids the soundness hole without any SMT - change. --/ diff --git a/docs/BooleFeatureRequests.md b/docs/BooleFeatureRequests.md index e22466e445..0e855b3732 100644 --- a/docs/BooleFeatureRequests.md +++ b/docs/BooleFeatureRequests.md @@ -63,11 +63,6 @@ seeds with at least one open gap remain in - `e as_bv{n}` lowers to `Int.ToBv{n}` (Core op) → SMT-LIB 2.7 `(_ int_to_bv n)` (truncating mod 2^n); widths 1/8/16/32/64/128. - All three directions fully implemented end-to-end (grammar → Core → SMT encoder → denotation). - Benchmarks: [`cast_expr.lean`](../StrataTest/Languages/Boole/cast_expr.lean), [`widening_casts.lean`](../StrataTest/Languages/Boole/widening_casts.lean), [`cast_all_directions.lean`](../StrataTest/Languages/Boole/cast_all_directions.lean). -- **`type nat := int` synonym** (Gap #8 partial) - - Nullary synonyms expanding to `int` trigger auto-axioms `∀ x : DT . DT..isCtor(x) ⟹ DT..field(x) ≥ 0` for each `nat`-typed constructor field. - - Known limitation: axiom may be unsound for mixed `nat`/`int` datatypes. See [`nat_axiom_limitation.lean`](../StrataTest/Languages/Boole/FeatureRequests/nat_axiom_limitation.lean). - - Known limitation: only direct synonyms (`type mynat := int`) are recognised; transitive chains (`type mynat := nat`) are not followed, so fields typed `mynat` get no axiom. - - Benchmark: [`cast_nested.lean`](../StrataTest/Languages/Boole/cast_nested.lean). ## Semantic preservation requests @@ -81,7 +76,7 @@ seeds with at least one open gap remain in ## Type/model requests -8. **Native `nat` support**: `type nat := int` synonym implemented. +8. **Native `nat` support**: Approach TBD. 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). @@ -125,14 +120,15 @@ Seeds with all gaps closed have been moved to `StrataTest/Languages/Boole/`; the | --- | --- | --- | --- | | [`datatypes_and_selectors.lean`](../StrataTest/Languages/Boole/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`](../StrataTest/Languages/Boole/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`](../StrataTest/Languages/Boole/FeatureRequests/nat_int_boundary.lean) | Native `nat` (#8), widening coercions (#6) | Verus `quantifiers`, `guide/integers`, `power_of_2`; VLIR `rec_adt_structural` | Active | +| [`nat_int_boundary.lean`](../StrataTest/Languages/Boole/FeatureRequests/nat_int_boundary.lean) | Native `nat` (#8) | Verus `quantifiers`, `guide/integers`, `power_of_2`; VLIR `rec_adt_structural` | Active | | [`map_extensionality.lean`](../StrataTest/Languages/Boole/FeatureRequests/map_extensionality.lean) | Extensional equality | Verus `guide/ext_equal` | Implemented (#684, #795); named synonyms and non-map types still open | | [`overflow_guard.lean`](../StrataTest/Languages/Boole/FeatureRequests/overflow_guard.lean) | Overflow guards (#5) | Verus `guide/overflow`, `overflow` | Lower priority | | [`opaque_reveal_hide.lean`](../StrataTest/Languages/Boole/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`](../StrataTest/Languages/Boole/FeatureRequests/reveal_with_fuel.lean) | `reveal_with_fuel` (#3) | Verus `test_expand_errors`, `recursion` | Lower priority | | [`early_return.lean`](../StrataTest/Languages/Boole/early_return.lean) | Early return | Verus SST `return` translation gap from `differential_status.md` | Implemented (#871) | -| [`widening_casts.lean`](../StrataTest/Languages/Boole/widening_casts.lean) | Widening casts (#6) | Verus `guide/integers`, `quantifiers`, `statements` | Updated to use `e as_int`; map-lookup case `v[i] as_int` verified | -| [`cast_expr.lean`](../StrataTest/Languages/Boole/cast_expr.lean) | `e as_int` widening cast (#6) | dalek-lite `scalar.rs` B2/B5 | Implemented (#1191) | +| [`widening_casts.lean`](../StrataTest/Languages/Boole/widening_casts.lean) | SMT-LIB 2.7 cast operators (#6) | Verus `guide/integers`, `quantifiers`, `statements` | Implemented | +| [`cast_expr.lean`](../StrataTest/Languages/Boole/cast_expr.lean) | SMT-LIB 2.7 cast operators (#6) | dalek-lite `scalar.rs` B2/B5 | Implemented | +| [`cast_all_directions.lean`](../StrataTest/Languages/Boole/cast_all_directions.lean) | SMT-LIB 2.7 cast operators (#6) | All three cast directions: `as_int`, `as_sint`, `as_bv{n}` | Implemented | | [`choose_operator.lean`](../StrataTest/Languages/Boole/choose_operator.lean) | `choose` (#18) | Verus `trigger_loops` (`choose_example`, `quantifier_example`) | Implemented (#1075) | | [`higher_order_encoding.lean`](../StrataTest/Languages/Boole/FeatureRequests/higher_order_encoding.lean) | Higher-order values (#17) | Verus `fun_ext`, `trait_for_fn` | Active | | [`lambda_closure.lean`](../StrataTest/Languages/Boole/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 | From 1d5402f33af78433405c3555ec76f9c3ef92ce1d Mon Sep 17 00:00:00 2001 From: Lydia Kondylidou <33327056+kondylidou@users.noreply.github.com> Date: Wed, 20 May 2026 23:15:27 +0200 Subject: [PATCH 20/20] error msgs --- Strata/Languages/Boole/Verify.lean | 4 +- Strata/Languages/Core/SMTEncoder.lean | 2 +- StrataTest/Languages/Boole/cast_errors.lean | 73 +++++++++++++++++++++ 3 files changed, 76 insertions(+), 3 deletions(-) create mode 100644 StrataTest/Languages/Boole/cast_errors.lean diff --git a/Strata/Languages/Boole/Verify.lean b/Strata/Languages/Boole/Verify.lean index df288aae5c..8ad98bc49c 100644 --- a/Strata/Languages/Boole/Verify.lean +++ b/Strata/Languages/Boole/Verify.lean @@ -496,13 +496,13 @@ partial def toCoreExpr (e : Boole.Expr) : TranslateM Core.Expression.Expr := do let n ← bvWidth m ty return mkCoreApp (.op () (mkIdent s!"Bv{n}.ToUInt") none) [← toCoreExpr e] | .int _ => toCoreExpr e - | _ => throwAt m s!"'as int' requires a bitvector source type" + | _ => throwAt m s!"'as int' requires a bitvector source type, got: {repr ty}" | .cast_to_sint m ty e => match ty with | .bv1 _ | .bv8 _ | .bv16 _ | .bv32 _ | .bv64 _ | .bv128 _ => do let n ← bvWidth m ty return mkCoreApp (.op () (mkIdent s!"Bv{n}.ToInt") none) [← toCoreExpr e] - | _ => throwAt m s!"'as sint' requires a bitvector source type" + | _ => throwAt m s!"'as sint' requires a bitvector source type, got: {repr ty}" | .cast_to_bv1 _ e => return mkCoreApp (.op () (mkIdent "Int.ToBv1") none) [← toCoreExpr e] | .cast_to_bv8 _ e => return mkCoreApp (.op () (mkIdent "Int.ToBv8") none) [← toCoreExpr e] | .cast_to_bv16 _ e => return mkCoreApp (.op () (mkIdent "Int.ToBv16") none) [← toCoreExpr e] diff --git a/Strata/Languages/Core/SMTEncoder.lean b/Strata/Languages/Core/SMTEncoder.lean index 176842c750..5f89f3bfcb 100644 --- a/Strata/Languages/Core/SMTEncoder.lean +++ b/Strata/Languages/Core/SMTEncoder.lean @@ -548,7 +548,7 @@ partial def toSMTOp (E : Env) (fn : CoreIdent) (fnty : LMonoTy) (ctx : SMT.Conte | .bv ⟨_, .SGe⟩ => .ok (.app Op.bvsge, .bool, ctx) | .bv ⟨n, .Concat⟩ => .ok (.app Op.bvconcat, .bitvec (n * 2), ctx) | .bv ⟨_, .ToUInt⟩ => .ok (.app Op.ubv_to_int, .int, ctx) - | .bv ⟨_, .ToInt⟩ => .ok (.app Op.sbv_to_int, .int, ctx) + | .bv ⟨_, .ToInt⟩ => .ok (.app Op.sbv_to_int, .int, ctx) | .intToBv n => .ok (.app (Op.int_to_bv n), .bitvec n, ctx) | .str .Length => .ok (.app Op.str_length, .int, ctx) diff --git a/StrataTest/Languages/Boole/cast_errors.lean b/StrataTest/Languages/Boole/cast_errors.lean new file mode 100644 index 0000000000..bac12a9e7a --- /dev/null +++ b/StrataTest/Languages/Boole/cast_errors.lean @@ -0,0 +1,73 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import Strata.MetaVerifier + +open Strata + +/- +Error cases for cast operators: + 1. `e as_sint` where `e : int` → rejected (not a bitvector) + 2. `e as_int` where `e` is a Map → rejected (not a bitvector or int) + 3. `e as_sint` where `e` is a Map → rejected (not a bitvector) +-/ + +private def helper (p : Strata.Program) : Except String Unit := do + let prog ← (Boole.getProgram p).mapError toString + let _ ← (Boole.toCoreProgram prog p.globalContext).mapError + fun e => toString (e.format none) + return () + +private def containsSubstr (haystack needle : String) : Bool := + (haystack.splitOn needle).length > 1 + +-- (1) `as_sint` on an `int` — must be rejected +private def sintOnInt := +#strata +program Boole; +procedure bad_sint(n: int) returns () +spec { + ensures n as_sint >= 0; +} { + exit bad_sint; +}; +#end + +#guard match helper sintOnInt with + | .error e => containsSubstr e "'as sint' requires a bitvector source type" + | .ok _ => false + +-- (2) `as_int` on a `Map int bv8` — must be rejected +private def asIntOnMap := +#strata +program Boole; +procedure bad_as_int(m: Map int bv8) returns () +spec { + ensures m as_int >= 0; +} { + exit bad_as_int; +}; +#end + +#guard match helper asIntOnMap with + | .error e => containsSubstr e "'as int' requires a bitvector source type" + | .ok _ => false + +-- (3) `as_sint` on a `Map int bv8` — must be rejected +private def sintOnMap := +#strata +program Boole; +procedure bad_sint_map(m: Map int bv8) returns () +spec { + ensures m as_sint >= 0; +} { + exit bad_sint_map; +}; +#end + +#guard match helper sintOnMap with + | .error e => containsSubstr e "'as sint' requires a bitvector source type" + | .ok _ => false