Skip to content
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

feat: remove toNat lemmas from bitvec_rules #208

Merged
merged 3 commits into from
Oct 3, 2024
Merged

feat: remove toNat lemmas from bitvec_rules #208

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
df94680
feat: remove .toNat rewrites from bitvec_rules.
alexkeizer Oct 2, 2024
a0e78b7
Merge branch 'main' into remove-toNat-bitvec-rules
shigoel Oct 3, 2024
4d56b94
Merge branch 'main' into remove-toNat-bitvec-rules
shigoel Oct 3, 2024
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
24 changes: 15 additions & 9 deletions Arm/BitVec.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -43,12 +43,13 @@ attribute [bitvec_rules] BitVec.msb_zero
attribute [bitvec_rules] BitVec.toNat_cast
attribute [bitvec_rules] BitVec.getLsbD_cast
attribute [bitvec_rules] BitVec.getMsbD_cast
attribute [bitvec_rules] BitVec.toNat_ofInt
-- attribute [bitvec_rules] BitVec.toNat_ofInt -- TODO: not tagged bv_toNat.
bollu marked this conversation as resolved.
Show resolved Hide resolved
attribute [bv_toNat] BitVec.toNat_ofInt
attribute [bitvec_rules] BitVec.toInt_ofInt
attribute [bitvec_rules] BitVec.ofInt_natCast
attribute [bitvec_rules] BitVec.toNat_zeroExtend'
attribute [bitvec_rules] BitVec.toNat_zeroExtend
attribute [bitvec_rules] BitVec.toNat_truncate
-- attribute [bitvec_rules] BitVec.toNat_zeroExtend
-- attribute [bitvec_rules] BitVec.toNat_truncate
attribute [bitvec_rules] BitVec.zeroExtend_zero
attribute [bitvec_rules] BitVec.ofNat_toNat
attribute [bitvec_rules] BitVec.getLsbD_zeroExtend'
Expand Down Expand Up @@ -82,15 +83,15 @@ attribute [bitvec_rules] BitVec.toNat_xor
attribute [bitvec_rules] BitVec.toFin_xor
attribute [bitvec_rules] BitVec.getLsbD_xor
attribute [bitvec_rules] BitVec.truncate_xor
attribute [bitvec_rules] BitVec.toNat_not
-- attribute [bitvec_rules] BitVec.toNat_not
attribute [bitvec_rules] BitVec.toFin_not
attribute [bitvec_rules] BitVec.getLsbD_not
attribute [bitvec_rules] BitVec.truncate_not
attribute [bitvec_rules] BitVec.not_cast
attribute [bitvec_rules] BitVec.and_cast
attribute [bitvec_rules] BitVec.or_cast
attribute [bitvec_rules] BitVec.xor_cast
attribute [bitvec_rules] BitVec.toNat_shiftLeft
-- attribute [bitvec_rules] BitVec.toNat_shiftLeft
attribute [bitvec_rules] BitVec.toFin_shiftLeft
attribute [bitvec_rules] BitVec.getLsbD_shiftLeft
attribute [bitvec_rules] BitVec.getMsbD_shiftLeft
Expand Down Expand Up @@ -124,23 +125,24 @@ attribute [bitvec_rules] BitVec.not_concat
attribute [bitvec_rules] BitVec.concat_or_concat
attribute [bitvec_rules] BitVec.concat_and_concat
attribute [bitvec_rules] BitVec.concat_xor_concat
attribute [bitvec_rules] BitVec.toNat_add
-- attribute [bitvec_rules] BitVec.toNat_add
attribute [bitvec_rules] BitVec.toFin_add
attribute [bitvec_rules] BitVec.ofFin_add
attribute [bitvec_rules] BitVec.add_ofFin
attribute [bitvec_rules] BitVec.add_zero
attribute [bitvec_rules] BitVec.zero_add
attribute [bitvec_rules] BitVec.toInt_add
attribute [bitvec_rules] BitVec.toNat_sub
-- attribute [bitvec_rules] BitVec.toNat_sub
attribute [bv_toNat] toNat_sub
attribute [bitvec_rules] BitVec.toFin_sub
attribute [bitvec_rules] BitVec.ofFin_sub
attribute [bitvec_rules] BitVec.sub_ofFin
attribute [bitvec_rules] BitVec.sub_zero
attribute [bitvec_rules] BitVec.sub_self
attribute [bitvec_rules] BitVec.toNat_neg
-- attribute [bitvec_rules] BitVec.toNat_neg
attribute [bitvec_rules] BitVec.toFin_neg
attribute [bitvec_rules] BitVec.neg_zero
attribute [bitvec_rules] BitVec.toNat_mul
-- attribute [bitvec_rules] BitVec.toNat_mul
attribute [bitvec_rules] BitVec.toFin_mul
attribute [bitvec_rules] BitVec.mul_zero
attribute [bitvec_rules] BitVec.mul_one
Expand Down Expand Up @@ -246,6 +248,10 @@ attribute [bitvec_rules] Nat.reduceLeDiff
attribute [bitvec_rules] Nat.reduceSubDiff
attribute [bitvec_rules] BitVec.toNat_ofNat

-- This might be a neccesary evil: it introduces a modulus,
-- but it's also really useful.
attribute [bitvec_rules] BitVec.toNat_ofNat

-- Some Fin lemmas useful for bitvector reasoning:
attribute [bitvec_rules] Fin.eta
attribute [bitvec_rules] Fin.isLt
Expand Down
2 changes: 1 addition & 1 deletion Arm/Memory/SeparateAutomation.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -405,7 +405,7 @@ def simpAndIntroDef (name : String) (hdefVal : Expr) : SimpMemM FVarId := do

/- Simp to gain some more juice out of the defn.. -/
let mut simpTheorems : Array SimpTheorems := #[]
for a in #[`minimal_theory, `bitvec_rules] do
for a in #[`minimal_theory, `bitvec_rules, `bv_toNat] do
let some ext ← (getSimpExtension? a)
| throwError m!"[simp_mem] Internal error: simp attribute {a} not found!"
simpTheorems := simpTheorems.push (← ext.getTheorems)
Expand Down
2 changes: 2 additions & 0 deletions Proofs/Popcount32.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -70,6 +70,7 @@ def popcount32_program : Program :=

#genStepEqTheorems popcount32_program

set_option trace.simp_mem.info true in
theorem popcount32_sym_meets_spec (s0 sf : ArmState)
(h_s0_pc : read_pc s0 = 0x4005b4#64)
(h_s0_program : s0.program = popcount32_program)
Expand Down Expand Up @@ -104,6 +105,7 @@ theorem popcount32_sym_meets_spec (s0 sf : ArmState)
intro n addr h_separate
simp only [memory_rules] at *
repeat (simp_mem (config := { useOmegaToClose := false }); sym_aggregate)

done

/--
Expand Down
Loading