fix(verify): correct modifies-array call-site argument binding

StrataBoole/Verify.lean

@@ -609,7 +609,7 @@ private def toCoreBlock (b : BooleDDM.Block SourceRange) : TranslateM (List Core
   | .block _ ⟨_, ss⟩ =>
     let parts ← ss.toList.mapM fun s =>
       match s with
-      | .varStatement m ds => lowerVarStatement m ds
+      | .varStatement m _ ds => lowerVarStatement m ds
       | _ => return [← toCoreStmt s]
     return parts.flatten
   termination_by SizeOf.sizeOf b
@@ -639,20 +639,31 @@ private def constructProcArgsPrefix (n : String)
     fun (id, _) => Core.CallArg.inArg (Lambda.LExpr.fvar () id none : Core.Expression.Expr)
   return modifiesArgs ++ readOnlyArgs
 
+/-- Returns `true` when the annotation contains a bare `@[reachCheck]` flag,
+    indicating that this `assert`/`cover` is a reachability check. -/
+private def hasReachCheckAnn
+    (ann : Ann (Option (BooleDDM.MetadataAnn SourceRange)) SourceRange) : Bool :=
+  match ann.val with
+  | none => false
+  | some (.mdAnn _ ⟨_, entries⟩) =>
+    entries.toList.any fun entry => match entry with
+      | .mdAnnFlag _ (.mdAnnKeyBare _ ⟨_, "reachCheck"⟩) => true
+      | _ => false
+
 private def toCoreStmt (s : BooleDDM.Statement SourceRange) : TranslateM Core.Statement := do
   match s with
-  | .varStatement m ds =>
+  | .varStatement m _ ds =>
     let out ← lowerVarStatement m ds
     let some first := out.head?
       | throwAt m "Empty var declaration list"
     match ds with
     | .declAtom _ _ => return first
     | _ => return .block "var" out (← toCoreMetaData m)
-  | .initStatement m ty ⟨_, n⟩ e =>
+  | .initStatement m _ ty ⟨_, n⟩ e =>
     let rhs ← toCoreExpr e
     modify fun st => { st with bvars := st.bvars.push (.fvar () (mkIdent n) none) }
     return Core.Statement.init (mkIdent n) (← toCoreType ty) (.det rhs) (← toCoreMetaData m)
-  | .assign m _ lhs rhs =>
+  | .assign m _ _ lhs rhs =>
     let rec lhsParts (lhs : BooleDDM.Lhs SourceRange) : TranslateM (String × List Core.Expression.Expr) := do
       match lhs with
       | .lhsIdent _ ⟨_, n⟩ => return (n, [])
@@ -663,17 +674,17 @@ private def toCoreStmt (s : BooleDDM.Statement SourceRange) : TranslateM Core.St
     let idxs := idxsRev.reverse
     let base := .fvar () (mkIdent n) none
     return Core.Statement.set (mkIdent n) (nestMapSet base idxs (← toCoreExpr rhs)) (← toCoreMetaData m)
-  | .assume m ⟨_, l?⟩ e =>
+  | .assume m _ ⟨_, l?⟩ e =>
     return Core.Statement.assume (← defaultLabel m "assume" l?) (← toCoreExpr e) (← toCoreMetaData m)
   | .assert m rc? ⟨_, l?⟩ e =>
     let md ← toCoreMetaData m
-    let md := if rc? matches ⟨_, some _⟩ then md.pushElem Imperative.MetaData.reachCheck (.switch true) else md
+    let md := if hasReachCheckAnn rc? then md.pushElem Imperative.MetaData.reachCheck (.switch true) else md
     return Core.Statement.assert (← defaultLabel m "assert" l?) (← toCoreExpr e) md
   | .cover m rc? ⟨_, l?⟩ e =>
     let md ← toCoreMetaData m
-    let md := if rc? matches ⟨_, some _⟩ then md.pushElem Imperative.MetaData.reachCheck (.switch true) else md
+    let md := if hasReachCheckAnn rc? then md.pushElem Imperative.MetaData.reachCheck (.switch true) else md
     return Core.Statement.cover (← defaultLabel m "cover" l?) (← toCoreExpr e) md
-  | .if_statement m c t e =>
+  | .if_statement m _ c t e =>
     let thenb ← withBVars [] (toCoreBlock t)
     let elseb ← withBVars [] <| match e with
       | .else0 _ => pure []
@@ -700,9 +711,9 @@ private def toCoreStmt (s : BooleDDM.Statement SourceRange) : TranslateM Core.St
     let havocStmt := Core.Statement.havoc (mkIdent lhs) md
     let assumeStmt := Core.Statement.assume label predExpr md
     return .block label [existenceAssert, havocStmt, assumeStmt] md
-  | .havoc_statement m ⟨_, n⟩ =>
+  | .havoc_statement m _ ⟨_, n⟩ =>
     return Core.Statement.havoc (mkIdent n) (← toCoreMetaData m)
-  | .while_statement m g ⟨_, decr?⟩ invs b =>
+  | .while_statement m _ g ⟨_, decr?⟩ invs b =>
     let guard ← match g with
       | .condDet _ expr => pure (.det (← toCoreExpr expr))
       | .condNondet _ => pure .nondet
@@ -715,7 +726,7 @@ private def toCoreStmt (s : BooleDDM.Statement SourceRange) : TranslateM Core.St
     let userIn := (← args.toList.mapM toCoreExpr).map Core.CallArg.inArg
     let userOut := (lhs.toList.map (mkIdent ·.val)).map Core.CallArg.outArg
     return Core.Statement.call n (globalsPrefix ++ userIn ++ userOut) (← toCoreMetaData m)
-  | .call_statement m ⟨_, n⟩ ⟨_, callArgs⟩ => do
+  | .call_statement m _ ⟨_, n⟩ ⟨_, callArgs⟩ => do
     -- Reject Core-only out/inout call argument syntax in Boole.
     -- Boole uses `call lhs := f(args)` for calls with outputs.
     for ca in callArgs.toList do
@@ -731,16 +742,16 @@ private def toCoreStmt (s : BooleDDM.Statement SourceRange) : TranslateM Core.St
       | .callArgExpr _ e => return some (Core.CallArg.inArg (← toCoreExpr e))
       | _ => return none  -- unreachable: out/inout rejected above
     return Core.Statement.call n (globalsPrefix ++ userIn) (← toCoreMetaData m)
-  | .block_statement m ⟨_, l⟩ b =>
+  | .block_statement m _ ⟨_, l⟩ b =>
     return .block l (← withBVars [] (toCoreBlock b)) (← toCoreMetaData m)
-  | .exit_statement m ⟨_, l⟩ =>
+  | .exit_statement m _ ⟨_, l⟩ =>
     return .exit l (← toCoreMetaData m)
-  | .typeDecl_statement m ⟨_, n⟩ ⟨_, args?⟩ =>
+  | .typeDecl_statement m _ ⟨_, n⟩ ⟨_, args?⟩ =>
     let params := match args? with
       | none => []
       | some bs => (bindingsToList bs).map bindingName
     return Core.Statement.typeDecl { name := n, params := params } (← toCoreMetaData m)
-  | .funcDecl_statement m ⟨_, n⟩ ⟨_, targs?⟩ bs ret ⟨_, pres⟩ body ⟨_, inline?⟩ =>
+  | .funcDecl_statement m _ ⟨_, n⟩ ⟨_, targs?⟩ bs ret ⟨_, pres⟩ body ⟨_, inline?⟩ =>
     let tys := match targs? with | none => [] | some ts => typeArgsToList ts
     withTypeBVars tys do
       let bsList := bindingsToList bs
@@ -992,38 +1003,38 @@ private def toCoreDecls (cmd : BooleDDM.Command SourceRange) : TranslateM (List
         | none => pure []
         | some os => (monoDeclListToList os).mapM toCoreMonoBind
       translateProcedureDecl m n tys inputs outputs specAnn.val bodyAnn.val
-  | .command_procedure m nameAnn targsAnn ins specAnn bodyAnn =>
+  | .command_procedure m _ nameAnn targsAnn ins specAnn bodyAnn =>
     let n := nameAnn.val
     if let some (param, kind) := hasOutOrInoutBinding ins then
       throwAt m s!"Boole procedure '{n}': '{kind}' modifier on parameter '{param}' is not supported. Use 'returns' syntax instead, e.g. 'procedure {n}(...) returns ({param} : T)'."
     let tys := match targsAnn.val with | none => [] | some ts => typeArgsToList ts
     withTypeBVars tys do
       let inputs ← (bindingsToList ins).mapM toCoreBinding
       translateProcedureDecl m n tys inputs [] specAnn.val bodyAnn.val
-  | .command_cfg_procedure m nameAnn _ _ _ _ =>
+  | .command_cfg_procedure m _ nameAnn _ _ _ _ =>
     throwAt m s!"Boole procedure '{nameAnn.val}': CFG-form procedure bodies (`cfg ENTRY \{ ... }`) are not supported in Boole; use a structured body."
-  | .command_typedecl _ ⟨_, n⟩ ⟨_, args?⟩ =>
+  | .command_typedecl _ _ ⟨_, n⟩ ⟨_, args?⟩ =>
     let params := match args? with
       | none => []
       | some bs => (bindingsToList bs).map bindingName
     return [.type (.con { name := n, params := params }) .empty]
-  | .command_typesynonym _ ⟨_, n⟩ ⟨_, args?⟩ _ rhs =>
+  | .command_typesynonym _ _ ⟨_, n⟩ ⟨_, args?⟩ _ rhs =>
     let tys := match args? with
       | none => []
       | some bs => (bindingsToList bs).map bindingName
     withTypeBVars tys do
       return [.type (.syn { name := n, typeArgs := tys, type := ← toCoreMonoType rhs }) .empty]
-  | .command_constdecl _ ⟨_, n⟩ ⟨_, targs?⟩ ret =>
+  | .command_constdecl _ _ ⟨_, n⟩ ⟨_, targs?⟩ ret =>
     let tys := match targs? with | none => [] | some ts => typeArgsToList ts
     withTypeBVars tys do
       return [.func { name := mkIdent n, typeArgs := tys, inputs := [], output := ← toCoreMonoType ret, body := none, concreteEval := none, attr := #[], axioms := [] } .empty]
-  | .command_fndecl _ ⟨_, n⟩ ⟨_, targs?⟩ bs ret =>
+  | .command_fndecl _ _ ⟨_, n⟩ ⟨_, targs?⟩ bs ret =>
     let tys := match targs? with | none => [] | some ts => typeArgsToList ts
     withTypeBVars tys do
       return [
         .func { name := mkIdent n, typeArgs := tys, inputs := ← (bindingsToList bs).mapM toCoreBinding, output := ← toCoreMonoType ret, body := none, concreteEval := none, attr := #[], axioms := [] }
            .empty]
-  | .command_fndef m ⟨_, n⟩ ⟨_, targs?⟩ bs ret ⟨_, pres⟩ body ⟨_, inline?⟩ =>
+  | .command_fndef m _ ⟨_, n⟩ ⟨_, targs?⟩ bs ret ⟨_, pres⟩ body ⟨_, inline?⟩ =>
     let tys := match targs? with | none => [] | some ts => typeArgsToList ts
     return [.func (← lowerPureFuncDef m n tys bs ret pres body inline?.isSome) .empty]
   | .command_choosefndef _ ⟨_, n⟩ ⟨_, targs?⟩ bs ret v pred =>
@@ -1066,7 +1077,7 @@ private def toCoreDecls (cmd : BooleDDM.Command SourceRange) : TranslateM (List
       let axiomDecl : Core.Decl :=
         .ax { name := s!"{n}_choose_axiom", e := axiomExpr } .empty
       return [funcDecl, axiomDecl]
-  | .command_recfndefs _ ⟨_, funcs⟩ =>
+  | .command_recfndefs _ _ ⟨_, funcs⟩ =>
     -- Mirror the DDM elaborator's @[declareFn] sibling-bvar accumulation:
     -- the i-th function's body sees the i preceding siblings as bvars.
     let funcList := funcs.toList
@@ -1085,9 +1096,9 @@ private def toCoreDecls (cmd : BooleDDM.Command SourceRange) : TranslateM (List
     return [.recFuncBlock fsRev.reverse .empty]
   | .command_var _m _b =>
     return []
-  | .command_axiom m ⟨_, l?⟩ e =>
+  | .command_axiom m _ ⟨_, l?⟩ e =>
     return [.ax { name := ← defaultLabel m "axiom" l?, e := ← toCoreExpr e } .empty]
-  | .command_distinct m ⟨_, l?⟩ ⟨_, es⟩ =>
+  | .command_distinct m _ ⟨_, l?⟩ ⟨_, es⟩ =>
     return [.distinct (mkIdent (← defaultLabel m "distinct" l?)) (← es.toList.mapM toCoreExpr) .empty]
   | .command_block _ b =>
     -- Core decls do not have a standalone "top-level block" form, so a Boole
@@ -1097,7 +1108,7 @@ private def toCoreDecls (cmd : BooleDDM.Command SourceRange) : TranslateM (List
       spec := { preconditions := [], postconditions := [] }
       body := .structured (← toCoreBlock b)
     } .empty]
-  | .command_datatypes _ ⟨_, decls⟩ =>
+  | .command_datatypes _ _ ⟨_, decls⟩ =>
     let datatypes ← decls.toList.mapM toCoreDatatypeDecl
     return [.type (.data datatypes) .empty]
 
@@ -1133,7 +1144,7 @@ def toCoreProgram (p : Boole.Program) (gctx : GlobalContext := {}) (fileName : S
       | .boole_procedure _ nameAnn _ _ _ _ specAnn _ =>
         let mods ← collectModifiesFromSpec fileName nameAnn.val specAnn.val varTypes
         if !mods.isEmpty then modMap := modMap.insert nameAnn.val mods
-      | .command_procedure _ nameAnn _ _ specAnn _ =>
+      | .command_procedure _ _ nameAnn _ _ specAnn _ =>
         let mods ← collectModifiesFromSpec fileName nameAnn.val specAnn.val varTypes
         if !mods.isEmpty then modMap := modMap.insert nameAnn.val mods
       | _ => pure ()

StrataBooleTest.lean

@@ -21,6 +21,7 @@ import StrataBooleTest.grammar_extensions
 import StrataBooleTest.insertion_sort
 import StrataBooleTest.loop_simple
 import StrataBooleTest.procedure_signatures
+import StrataBooleTest.quicksort
 import StrataBooleTest.square_matrix_multiply
 import StrataBooleTest.stack_array_based
 import StrataBooleTest.string_operators

StrataBooleTest/FeatureRequests/bitvector_ops.lean

@@ -18,10 +18,10 @@ Near-upstream anchors:
 - Source: dalek-lite scalar multiplication — bit extraction uses `>>` to read
   individual scalar bits; conditional swap uses `^` and `~` for constant-time
   branching; nibble reconstruction uses `<<` and `|`.
-- Implemented: bitwise operators (`&`, `|`, `^`, `>>`, `>>s`, `<<`, `~`) on `bvN`
+- Implemented: bitwise operators (`&`, `|`, `^`, `>>`, `ashr`, `<<`, `~`) on `bvN`
   types are now supported in the Boole grammar and lower to the corresponding
   `Bv{N}.And`, `Bv{N}.Or`, `Bv{N}.Xor`, `Bv{N}.UShr`, `Bv{N}.SShr`, `Bv{N}.Shl`,
-  `Bv{N}.Not` Core operations. `>>` is unsigned (UShr); `>>s` is signed (SShr).
+  `Bv{N}.Not` Core operations. `>>` is unsigned (UShr); `ashr` is signed (SShr).
 -/
 
 -- Exercises & and | (X25519 scalar clamping).
@@ -44,23 +44,23 @@ spec {
 #end
 
 /-- info:
-Obligation: clamp_seed_ensures_0_1145
+Obligation: clamp_seed_ensures_0_1147
 Property: assert
 Result: ✅ pass
 
-Obligation: clamp_seed_ensures_1_1187
+Obligation: clamp_seed_ensures_1_1189
 Property: assert
 Result: ✅ pass
 
-Obligation: clamp_seed_ensures_2_1251
+Obligation: clamp_seed_ensures_2_1253
 Property: assert
 Result: ✅ pass
 
-Obligation: clamp_seed_ensures_3_1298
+Obligation: clamp_seed_ensures_3_1300
 Property: assert
 Result: ✅ pass
 
-Obligation: clamp_seed_ensures_4_1345
+Obligation: clamp_seed_ensures_4_1347
 Property: assert
 Result: ✅ pass-/
 #guard_msgs in
@@ -99,35 +99,35 @@ spec {
 #end
 
 /-- info:
-Obligation: bv_shift_xor_ensures_0_2339
+Obligation: bv_shift_xor_ensures_0_2341
 Property: assert
 Result: ✅ pass
 
-Obligation: bv_shift_xor_ensures_1_2362
+Obligation: bv_shift_xor_ensures_1_2364
 Property: assert
 Result: ✅ pass
 
-Obligation: bv_shift_xor_ensures_2_2388
+Obligation: bv_shift_xor_ensures_2_2390
 Property: assert
 Result: ✅ pass
 
-Obligation: bv_shift_xor_ensures_3_2422
+Obligation: bv_shift_xor_ensures_3_2424
 Property: assert
 Result: ✅ pass
 
-Obligation: bv_shift_xor_ensures_4_2497
+Obligation: bv_shift_xor_ensures_4_2499
 Property: assert
 Result: ✅ pass
 
-Obligation: bv_shift_xor_ensures_5_2560
+Obligation: bv_shift_xor_ensures_5_2562
 Property: assert
 Result: ✅ pass
 
-Obligation: bv_shift_xor_ensures_6_2638
+Obligation: bv_shift_xor_ensures_6_2640
 Property: assert
 Result: ✅ pass
 
-Obligation: bv_shift_xor_ensures_7_2731
+Obligation: bv_shift_xor_ensures_7_2733
 Property: assert
 Result: ✅ pass-/
 #guard_msgs in
@@ -137,35 +137,35 @@ example : Strata.smtVCsCorrectBoole bitvectorShiftXorSeed := by
   gen_smt_vcs_boole
   all_goals (first | grind | decide)
 
--- Exercises >>s (arithmetic/signed right shift): vacated bits are filled with
+-- Exercises ashr (arithmetic/signed right shift): vacated bits are filled with
 -- the sign bit, unlike >> which fills with 0.
 private def bitvectorSShrSeed : StrataDDM.Program :=
 #strata
 program Boole;
 
 procedure bv_sshr(b: bv8) returns (r: bv8)
 spec {
-  ensures r == b >>s bv{8}(1);
+  ensures r == b ashr bv{8}(1);
   // negative value: sign bit propagates into vacated position
-  ensures bv{8}(0b10000000) >>s bv{8}(1) == bv{8}(0b11000000);
+  ensures bv{8}(0b10000000) ashr bv{8}(1) == bv{8}(0b11000000);
   // positive value: behaves like unsigned shift
-  ensures bv{8}(0b01000000) >>s bv{8}(1) == bv{8}(0b00100000);
+  ensures bv{8}(0b01000000) ashr bv{8}(1) == bv{8}(0b00100000);
 }
 {
-  r := b >>s bv{8}(1);
+  r := b ashr bv{8}(1);
 };
 #end
 
 /-- info:
-Obligation: bv_sshr_ensures_0_3965
+Obligation: bv_sshr_ensures_0_3968
 Property: assert
 Result: ✅ pass
 
-Obligation: bv_sshr_ensures_1_4059
+Obligation: bv_sshr_ensures_1_4063
 Property: assert
 Result: ✅ pass
 
-Obligation: bv_sshr_ensures_2_4171
+Obligation: bv_sshr_ensures_2_4176
 Property: assert
 Result: ✅ pass-/
 #guard_msgs in
@@ -175,51 +175,51 @@ example : Strata.smtVCsCorrectBoole bitvectorSShrSeed := by
   gen_smt_vcs_boole
   all_goals (first | grind | decide)
 
--- Exercises signed bitvector comparisons (<s, <=s, >s, >=s).
+-- Exercises signed bitvector comparisons (slt, sle, sgt, sge).
 -- In bv8 signed interpretation: 0xFF = -1, 0x7F = 127.
 private def bitvectorSignedCmpSeed : StrataDDM.Program :=
 #strata
 program Boole;
 
 procedure bv_signed_cmp(a: bv8, b: bv8) returns ()
 spec {
-  ensures bv{8}(255) <s  bv{8}(0);
-  ensures bv{8}(127) >s  bv{8}(0);
-  ensures bv{8}(255) <=s bv{8}(0);
-  ensures bv{8}(127) >=s bv{8}(0);
-  ensures bv{8}(0)   <=s bv{8}(0);
-  ensures bv{8}(0)   >=s bv{8}(0);
-  ensures bv{8}(255) <s  bv{8}(1);
+  ensures bv{8}(255) slt bv{8}(0);
+  ensures bv{8}(127) sgt bv{8}(0);
+  ensures bv{8}(255) sle bv{8}(0);
+  ensures bv{8}(127) sge bv{8}(0);
+  ensures bv{8}(0)   sle bv{8}(0);
+  ensures bv{8}(0)   sge bv{8}(0);
+  ensures bv{8}(255) slt bv{8}(1);
 }
 { };
 #end
 
 /-- info:
-Obligation: bv_signed_cmp_ensures_0_4954
+Obligation: bv_signed_cmp_ensures_0_4963
 Property: assert
 Result: ✅ pass
 
-Obligation: bv_signed_cmp_ensures_1_4989
+Obligation: bv_signed_cmp_ensures_1_4998
 Property: assert
 Result: ✅ pass
 
-Obligation: bv_signed_cmp_ensures_2_5024
+Obligation: bv_signed_cmp_ensures_2_5033
 Property: assert
 Result: ✅ pass
 
-Obligation: bv_signed_cmp_ensures_3_5059
+Obligation: bv_signed_cmp_ensures_3_5068
 Property: assert
 Result: ✅ pass
 
-Obligation: bv_signed_cmp_ensures_4_5094
+Obligation: bv_signed_cmp_ensures_4_5103
 Property: assert
 Result: ✅ pass
 
-Obligation: bv_signed_cmp_ensures_5_5129
+Obligation: bv_signed_cmp_ensures_5_5138
 Property: assert
 Result: ✅ pass
 
-Obligation: bv_signed_cmp_ensures_6_5164
+Obligation: bv_signed_cmp_ensures_6_5173
 Property: assert
 Result: ✅ pass-/
 #guard_msgs in