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.

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

Add reference implementation of prune_updates #246

Merged
merged 29 commits into from
Nov 13, 2024
Merged
Changes from 1 commit
Commits
Show all changes
29 commits
Select commit Hold shift + click to select a range
bcec32b
Experimental method to aggregate state effects
shigoel Oct 14, 2024
5ac43cc
Merge branch 'main' into aggr_dsl
shigoel Oct 14, 2024
1f8df56
Fix comments
shigoel Oct 14, 2024
7687069
Merge branch 'main' into aggr_dsl
shigoel Oct 14, 2024
85ea0e6
Update Tactics/ArmConstr.lean
shigoel Oct 14, 2024
c67f1ca
Add a test for 30 steps
shigoel Oct 14, 2024
a16325c
Add a python script to generate theorems for ArmConstr method
shigoel Oct 14, 2024
61fa5c3
chore: cleanup to use stdlib API
bollu Oct 14, 2024
7de7f7b
Cherry-pick @bollu's commit 7947bbf (https://github.com/leanprover/LN…
shigoel Oct 15, 2024
e61e5d6
Minor edits
shigoel Oct 15, 2024
cf0d8a6
Sort the updates when doing the aggregation
shigoel Oct 15, 2024
ad449b0
Add note about why decide doesn't do a complete reduction (thanks, @a…
shigoel Oct 15, 2024
f002039
Merge branch 'main' into aggr_dsl
shigoel Oct 17, 2024
c23db62
Prove Expr.eq_true_of_denote
shigoel Oct 21, 2024
8ab5f2a
Merge branch 'main' into aggr_dsl
shigoel Oct 21, 2024
421b76a
Minor comments
shigoel Oct 21, 2024
8295aa5
Add sym_block; manually aggregate basic blocks for SHA512; simulate S…
shigoel Oct 23, 2024
45f4742
Clean up sym_block; account for blockSize in some Sym/Context functions
shigoel Oct 24, 2024
9f83f49
Merge branch 'main' into aggr_dsl
shigoel Oct 30, 2024
d4429bb
prune_updates ready for GPR writes
shigoel Nov 5, 2024
b7a71b3
Merge branch 'main' into aggr_dsl
shigoel Nov 5, 2024
1488732
Merge branch 'aggr_dsl' into more_preprocessing
shigoel Nov 5, 2024
67df45d
Merge branch 'aggr_dsl' into more_preprocessing
shigoel Nov 5, 2024
156c712
Finished reference implementation of prune_updates
shigoel Nov 8, 2024
32619ab
Merge branch 'main' into more_preprocessing
shigoel Nov 12, 2024
c59a393
Add missing copyright header
shigoel Nov 12, 2024
dd971b2
Fix a bug in the application of mkNeProofOfNotMemAndMem
shigoel Nov 12, 2024
b477dc5
Add capability to sym_block to specify a list of possibly different b…
shigoel Nov 13, 2024
b1378c4
Add an example where prune_updates times out
shigoel Nov 13, 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
Prev Previous commit
Next Next commit
prune_updates ready for GPR writes
  • Loading branch information
shigoel committed Nov 5, 2024
commit d4429bbfa9b7137c0b484ff609fafc9f8a6f2c51
22 changes: 22 additions & 0 deletions Arm/State.lean
Original file line number Diff line number Diff line change
@@ -55,6 +55,15 @@ theorem store_write_irrelevant [DecidableEq α]
unfold write_store read_store
simp

@[local simp]
theorem write_store_commute [DecidableEq α] (store : Store α β)
(h : i ≠ j) :
write_store i x (write_store j y store) =
write_store j y (write_store i x store) := by
apply funext; intro idx
simp [write_store]
split <;> simp_all

instance [Repr β]: Repr (Store (BitVec n) β) where
reprPrec store _ :=
let rec helper (a : Nat) (acc : Lean.Format) :=
@@ -451,6 +460,19 @@ theorem w_irrelevant : w fld (r fld s) s = s := by
unfold read_base_error write_base_error
repeat (split <;> simp_all)

theorem w_of_w_commute (h : fld1 ≠ fld2) :
w fld1 v1 (w fld2 v2 s) = w fld2 v2 (w fld1 v1 s) := by
unfold w
unfold write_base_gpr
unfold write_base_sfp
unfold write_base_pc
unfold write_base_flag
unfold write_base_error
split <;> split <;> (simp_all; try rwa [write_store_commute])
rename_i fld1 t1 i1 v1 fld2 t2 i2 v2
cases i1 <;> (cases i2 <;> (split <;> simp_all))
done

@[state_simp_rules]
theorem fetch_inst_of_w : fetch_inst addr (w fld val s) = fetch_inst addr s := by
unfold fetch_inst w
Loading