Skip to content

Commit

Permalink
Better bitvec reduction (#89)
Browse files Browse the repository at this point in the history
### Description:

Relatively minor PR: adds some existing lemmas to the `minimal_theory`
and `bitvec_rules` to get nicer normal forms.
In particular:
- `BitVec.zero` now becomes `0#_`, and
- `truncate` now becomes `zeroExtend`, since the latter has simprocs for
better reduction

Various tests have been changed accordingly

### Testing:

`make all` ran locally

### License:

By submitting this pull request, I confirm that my contribution is
made under the terms of the Apache 2.0 license.

---------

Co-authored-by: Shilpi Goel <[email protected]>
  • Loading branch information
alexkeizer and shigoel authored Aug 15, 2024
1 parent 31575ac commit 60156d5
Show file tree
Hide file tree
Showing 6 changed files with 8 additions and 11 deletions.
2 changes: 2 additions & 0 deletions Arm/BitVec.lean
Original file line number Diff line number Diff line change
Expand Up @@ -159,6 +159,8 @@ attribute [bitvec_rules] BitVec.getLsb_rotateRight
attribute [bitvec_rules] BitVec.ofBool_true
attribute [bitvec_rules] BitVec.ofBool_false
attribute [bitvec_rules] BitVec.ofNat_eq_ofNat
attribute [bitvec_rules] BitVec.zero_eq
attribute [bitvec_rules] BitVec.truncate_eq_zeroExtend

-- BitVec Simproc rules:
-- See Lean/Meta/Tactic/Simp/BuiltinSimprocs for the built-in
Expand Down
2 changes: 2 additions & 0 deletions Arm/MinTheory.lean
Original file line number Diff line number Diff line change
Expand Up @@ -88,6 +88,8 @@ attribute [minimal_theory] bne_self_eq_false
attribute [minimal_theory] bne_self_eq_false'
attribute [minimal_theory] decide_False
attribute [minimal_theory] decide_True
attribute [minimal_theory] decide_eq_false_iff_not
attribute [minimal_theory] decide_eq_true_iff
attribute [minimal_theory] bne_iff_ne
attribute [minimal_theory] Bool.false_eq
attribute [minimal_theory] Bool.and_eq_false_imp
Expand Down
3 changes: 1 addition & 2 deletions Proofs/Experiments/AbsVCG.lean
Original file line number Diff line number Diff line change
Expand Up @@ -271,8 +271,7 @@ theorem program_effects_lemma (h_pre : abs_pre s0)
BitVec.truncate 64 4294967295#32) &&&
BitVec.truncate 64 1#32)) := by
simp (config := {decide := true}) only [h_step_4, h_step_3, h_step_2, h_step_1,
state_simp_rules]
rfl
state_simp_rules, bitvec_rules]

have h_sf_s4 : sf = s4 := by
simp only [h_run, h_s4, h_s3, h_s2, h_s1, run]
Expand Down
6 changes: 1 addition & 5 deletions Proofs/Popcount32.lean
Original file line number Diff line number Diff line change
Expand Up @@ -136,11 +136,7 @@ info: popcount32_program.stepi_0x4005c0 (s sn : ArmState) (h_program : s.program
(sn =
w StateField.PC (4195780#64)
(w (StateField.GPR 0#5)
(truncate 64 (BitVec.zero 32) &&& truncate 64 2147483648#32 |||
(truncate 64 (BitVec.zero 32) &&& 0#64 |||
truncate 64 ((zeroExtend 32 (r (StateField.GPR 0#5) s)).rotateRight 1) &&&
truncate 64 4294967295#32) &&&
truncate 64 2147483647#32)
(zeroExtend 64 ((zeroExtend 32 (r (StateField.GPR 0#5) s)).rotateRight 1) &&& 4294967295#64 &&& 2147483647#64)
s))
-/
#guard_msgs in #check popcount32_program.stepi_0x4005c0
Expand Down
2 changes: 1 addition & 1 deletion Proofs/SHA512/Sha512DecodeExecLemmas.lean
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,7 @@ info: sha512_program.exec_0x126c90 (s : ArmState) :
(ArmInst.BR (BranchInst.Compare_branch { sf := 1#1, _fixed := 26#5, op := 1#1, imm19 := 523804#19, Rt := 2#5 }))
s =
w StateField.PC
(if decide (r (StateField.GPR 2#5) s = BitVec.zero 64) = false then r StateField.PC s + 18446744073709549680#64
(if ¬r (StateField.GPR 2#5) s = 0#64 then r StateField.PC s + 18446744073709549680#64
else r StateField.PC s + 4#64)
s
-/
Expand Down
4 changes: 1 addition & 3 deletions Proofs/SHA512/Sha512StepLemmas.lean
Original file line number Diff line number Diff line change
Expand Up @@ -11,9 +11,7 @@ set_option maxHeartbeats 2000000 in
/--
info: sha512_program.stepi_0x126c90 (s sn : ArmState) (h_program : s.program = sha512_program)
(h_pc : r StateField.PC s = 1207440#64) (h_err : r StateField.ERR s = StateError.None) :
(sn = stepi s) =
(sn =
w StateField.PC (if decide (r (StateField.GPR 2#5) s = BitVec.zero 64) = false then 1205504#64 else 1207444#64) s)
(sn = stepi s) = (sn = w StateField.PC (if ¬r (StateField.GPR 2#5) s = 0#64 then 1205504#64 else 1207444#64) s)
-/
#guard_msgs in
#check sha512_program.stepi_0x126c90

0 comments on commit 60156d5

Please sign in to comment.