Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
kondylidou wants to merge 5 commits into from
Closed

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

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
bae1d9d
fix(verify): unblock modifies-array + call-site verification, bump St…
kondylidou Jul 21, 2026
dddcd1a
Merge branch 'main' into fix/partition-modifies-global-threading
kondylidou Aug 12, 2026
059dd2e
fix(build): increase lean tstack to 32 MB for Linux/x86-64 CI
kondylidou Aug 19, 2026
a6e63c1
fix
kondylidou Aug 19, 2026
a0fd441
undersc
kondylidou Aug 19, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
65 changes: 38 additions & 27 deletions StrataBoole/Verify.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 _annots ds => lowerVarStatement m ds
| _ => return [← toCoreStmt s]
return parts.flatten
termination_by SizeOf.sizeOf b
Expand Down Expand Up @@ -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 _annots ds =>

@joscoh joscoh Aug 18, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Not blocking, but slightly better to use an underscore if the variable is unused IMO

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 _annots 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 _annots _ lhs rhs =>
let rec lhsParts (lhs : BooleDDM.Lhs SourceRange) : TranslateM (String × List Core.Expression.Expr) := do
match lhs with
| .lhsIdent _ ⟨_, n⟩ => return (n, [])
Expand All @@ -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 _annots ⟨_, 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 _annots c t e =>
let thenb ← withBVars [] (toCoreBlock t)
let elseb ← withBVars [] <| match e with
| .else0 _ => pure []
Expand All @@ -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 _annots ⟨_, n⟩ =>
return Core.Statement.havoc (mkIdent n) (← toCoreMetaData m)
| .while_statement m g ⟨_, decr?⟩ invs b =>
| .while_statement m _annots g ⟨_, decr?⟩ invs b =>
let guard ← match g with
| .condDet _ expr => pure (.det (← toCoreExpr expr))
| .condNondet _ => pure .nondet
Expand All @@ -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 _annots ⟨_, 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
Expand All @@ -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 _annots ⟨_, l⟩ b =>
return .block l (← withBVars [] (toCoreBlock b)) (← toCoreMetaData m)
| .exit_statement m ⟨_, l⟩ =>
| .exit_statement m _annots ⟨_, l⟩ =>
return .exit l (← toCoreMetaData m)
| .typeDecl_statement m ⟨_, n⟩ ⟨_, args?⟩ =>
| .typeDecl_statement m _annots ⟨_, 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 _annots ⟨_, n⟩ ⟨_, targs?⟩ bs ret ⟨_, pres⟩ body ⟨_, inline?⟩ =>
let tys := match targs? with | none => [] | some ts => typeArgsToList ts
withTypeBVars tys do
let bsList := bindingsToList bs
Expand Down Expand Up @@ -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 _annots 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 _annots 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 _annots ⟨_, 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 =>
Expand Down Expand Up @@ -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 _ _annots ⟨_, 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
Expand All @@ -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 _annots ⟨_, l?⟩ e =>
return [.ax { name := ← defaultLabel m "axiom" l?, e := ← toCoreExpr e } .empty]
| .command_distinct m ⟨_, l?⟩ ⟨_, es⟩ =>
| .command_distinct m _annots ⟨_, 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
Expand All @@ -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 _ _annots ⟨_, decls⟩ =>
let datatypes ← decls.toList.mapM toCoreDatatypeDecl
return [.type (.data datatypes) .empty]

Expand Down Expand Up @@ -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 ()
Expand Down
1 change: 1 addition & 0 deletions StrataBooleTest.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
76 changes: 38 additions & 38 deletions StrataBooleTest/FeatureRequests/bitvector_ops.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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).
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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
Expand Down
Loading
Loading