From 33def2a21421e10b89a7b550173f011558750415 Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Thu, 1 Aug 2024 10:06:00 -0500 Subject: [PATCH 1/8] chore: make ArmState fields private --- Arm/Cosim.lean | 6 +-- Arm/Memory.lean | 124 ------------------------------------------ Arm/State.lean | 139 +++++++++++++++++++++++++++++++++++++++++++++--- 3 files changed, 136 insertions(+), 133 deletions(-) diff --git a/Arm/Cosim.lean b/Arm/Cosim.lean index fa392091..757230f3 100644 --- a/Arm/Cosim.lean +++ b/Arm/Cosim.lean @@ -73,7 +73,7 @@ def init_flags (flags : BitVec 4) (s : ArmState) : ArmState := Id.run do /-- Initialize an ArmState for cosimulation from a given regState. -/ def regState_to_armState (r : regState) : ArmState := let s := init_gprs r.gpr (init_flags r.nzcv (init_sfps r.sfp init_cosim_state)) - let s := { s with program := def_program [(0x0#64, r.inst)] } + let s := set_program s (def_program [(0x0#64, r.inst)]) s def bitvec_to_hex (x : BitVec n) : String := @@ -128,7 +128,7 @@ bitvector values.-/ def gpr_list (s : ArmState) : List (BitVec 64) := Id.run do let mut acc := [] for i in [0:31] do - acc := acc ++ [(s.gpr (BitVec.ofNat 5 i))] + acc := acc ++ [read_gpr 64 (BitVec.ofNat 5 i) s] pure acc /-- Get the SIMD/FP registers in an ArmState as a list of bitvector @@ -136,7 +136,7 @@ values.-/ def sfp_list (s : ArmState) : List (BitVec 64) := Id.run do let mut acc := [] for i in [0:32] do - let reg := s.sfp (BitVec.ofNat 5 i) + let reg := read_sfp 64 (BitVec.ofNat 5 i) s acc := acc ++ [(extractLsb 63 0 reg), (extractLsb 127 64 reg)] pure acc diff --git a/Arm/Memory.lean b/Arm/Memory.lean index 93bff238..a6077163 100644 --- a/Arm/Memory.lean +++ b/Arm/Memory.lean @@ -8,127 +8,3 @@ import Arm.Separate section Memory open BitVec - ----------------------------------------------------------------------- - ----- Memory accessors and updaters ---- - --- We don't add the simp attribute to read/write_mem_bytes. Instead, --- we prove and export properties about their (non)interference. - --- (FIXME) Make read_mem private. --- We export read_mem_bytes, not read_mem. -def read_mem (addr : BitVec 64) (s : ArmState) : BitVec 8 := - read_store addr s.mem - -def read_mem_bytes (n : Nat) (addr : BitVec 64) (s : ArmState) : BitVec (n * 8) := - match n with - | 0 => 0#0 - | n' + 1 => - let byte := read_mem addr s - let rest := read_mem_bytes n' (addr + 1#64) s - have h: n' * 8 + 8 = (n' + 1) * 8 := by simp_arith - BitVec.cast h (rest ++ byte) - --- (FIXME) Make write_mem private. --- We export write_mem_bytes, not write_mem. -def write_mem (addr : BitVec 64) (val : BitVec 8) (s : ArmState) : ArmState := - let new_mem := write_store addr val s.mem - { s with mem := new_mem } - -def write_mem_bytes (n : Nat) (addr : BitVec 64) (val : BitVec (n * 8)) (s : ArmState) : ArmState := - match n with - | 0 => s - | n' + 1 => - let byte := extractLsb 7 0 val - let s := write_mem addr byte s - let val_rest := BitVec.zeroExtend (n' * 8) (val >>> 8) - write_mem_bytes n' (addr + 1#64) val_rest s - ----- RoW/WoW lemmas about memory and other fields ---- - -theorem r_of_write_mem : r fld (write_mem addr val s) = r fld s := by - unfold r - unfold read_base_gpr read_base_sfp read_base_pc - unfold read_base_flag read_base_error - unfold write_mem - split <;> simp - -@[state_simp_rules] -theorem r_of_write_mem_bytes : - r fld (write_mem_bytes n addr val s) = r fld s := by - induction n generalizing addr s - case succ => - rename_i n n_ih - unfold write_mem_bytes; simp only - rw [n_ih, r_of_write_mem] - case zero => rfl - done - -theorem fetch_inst_of_write_mem : - fetch_inst addr1 (write_mem addr2 val s) = fetch_inst addr1 s := by - unfold fetch_inst write_mem - simp - -@[state_simp_rules] -theorem fetch_inst_of_write_mem_bytes : - fetch_inst addr1 (write_mem_bytes n addr2 val s) = fetch_inst addr1 s := by - induction n generalizing addr2 s - case zero => rfl - case succ => - rename_i n n_ih - unfold write_mem_bytes; simp only - rw [n_ih, fetch_inst_of_write_mem] - done - -theorem read_mem_of_w : - read_mem addr (w fld v s) = read_mem addr s := by - unfold read_mem - unfold w write_base_gpr write_base_sfp - unfold write_base_pc write_base_flag write_base_error - split <;> simp - -@[state_simp_rules] -theorem read_mem_bytes_of_w : - read_mem_bytes n addr (w fld v s) = read_mem_bytes n addr s := by - induction n generalizing addr s - case zero => rfl - case succ => - rename_i n n_ih - unfold read_mem_bytes; simp only [read_mem_of_w] - rw [n_ih] - done - -@[state_simp_rules] -theorem write_mem_bytes_program {n : Nat} (addr : BitVec 64) (bytes : BitVec (n * 8)): - (write_mem_bytes n addr bytes s).program = s.program := by - intros - induction n generalizing addr s - · simp [write_mem_bytes] - · rename_i n h_n - simp only [write_mem_bytes] - rw [h_n] - simp only [write_mem] - ----- Memory RoW/WoW lemmas ---- - -theorem read_mem_of_write_mem_same : - read_mem addr (write_mem addr v s) = v := by - unfold read_mem write_mem; simp [store_read_over_write_same] - -theorem read_mem_of_write_mem_different (h : addr1 ≠ addr2) : - read_mem addr1 (write_mem addr2 v s) = read_mem addr1 s := by - unfold read_mem write_mem; simp - rw [store_read_over_write_different]; trivial - -theorem write_mem_of_write_mem_shadow : - write_mem addr val2 (write_mem addr val1 s) = write_mem addr val2 s := by - simp [write_mem]; unfold write_store; simp_all; done - -theorem write_mem_irrelevant : - write_mem addr (read_mem addr s) s = s := by - simp [read_mem, write_mem, store_write_irrelevant] - -end Memory - ----------------------------------------------------------------------- diff --git a/Arm/State.lean b/Arm/State.lean index 656a9577..99103bf4 100644 --- a/Arm/State.lean +++ b/Arm/State.lean @@ -118,15 +118,15 @@ deriving DecidableEq, Repr @[ext] structure ArmState where -- General-purpose registers: register 31 is the stack pointer. - gpr : Store (BitVec 5) (BitVec 64) + private gpr : Store (BitVec 5) (BitVec 64) -- SIMD/floating-point registers - sfp : Store (BitVec 5) (BitVec 128) + private sfp : Store (BitVec 5) (BitVec 128) -- Program Counter - pc : BitVec 64 + private pc : BitVec 64 -- PState - pstate : PState + private pstate : PState -- Memory: maps 64-bit addresses to bytes - mem : Store (BitVec 64) (BitVec 8) + private mem : Store (BitVec 64) (BitVec 8) -- Program: maps 64-bit addresses to 32-bit instructions. -- Note that we have the following assumption baked into our machine model: -- the program is always disjoint from the rest of the memory. @@ -136,7 +136,7 @@ structure ArmState where -- non-None value when some irrecoverable error is encountered -- (e.g., an unimplemented instruction is hit). Any reasoning or -- execution based off an erroneous state is invalid. - error : StateError + private error : StateError deriving Repr ---- Basic State Accessors and Updaters (except memory) ---- @@ -204,6 +204,9 @@ def write_base_flag (flag : PFlag) (val : BitVec 1) (s : ArmState) : ArmState := -- Program -- +def set_program (s : ArmState) (program : Program) : ArmState := + { s with program := program } + -- Fetch the instruction at address addr. @[irreducible] def fetch_inst (addr : BitVec 64) (s : ArmState) : Option (BitVec 32) := @@ -507,4 +510,128 @@ example : end State +section Memory +---------------------------------------------------------------------- + +-- (FIXME) Make read_mem private. +-- We export read_mem_bytes, not read_mem. +private def read_mem (addr : BitVec 64) (s : ArmState) : BitVec 8 := + read_store addr s.mem + +-- We don't add the simp attribute to read/write_mem_bytes. Instead, +-- we prove and export properties about their (non)interference. + +def read_mem_bytes (n : Nat) (addr : BitVec 64) (s : ArmState) : BitVec (n * 8) := + match n with + | 0 => 0#0 + | n' + 1 => + let byte := read_mem addr s + let rest := read_mem_bytes n' (addr + 1#64) s + have h: n' * 8 + 8 = (n' + 1) * 8 := by simp_arith + BitVec.cast h (rest ++ byte) + +-- (FIXME) Make write_mem private. +-- We export write_mem_bytes, not write_mem. +private def write_mem (addr : BitVec 64) (val : BitVec 8) (s : ArmState) : ArmState := + let new_mem := write_store addr val s.mem + { s with mem := new_mem } + +def write_mem_bytes (n : Nat) (addr : BitVec 64) (val : BitVec (n * 8)) (s : ArmState) : ArmState := + match n with + | 0 => s + | n' + 1 => + let byte := BitVec.extractLsb 7 0 val + let s := write_mem addr byte s + let val_rest := BitVec.zeroExtend (n' * 8) (val >>> 8) + write_mem_bytes n' (addr + 1#64) val_rest s +---------------------------------------------------------------------- + +---- Memory accessors and updaters ---- + +---- RoW/WoW lemmas about memory and other fields ---- + +theorem r_of_write_mem : r fld (write_mem addr val s) = r fld s := by + unfold r + unfold read_base_gpr read_base_sfp read_base_pc + unfold read_base_flag read_base_error + unfold write_mem + split <;> simp + +@[state_simp_rules] +theorem r_of_write_mem_bytes : + r fld (write_mem_bytes n addr val s) = r fld s := by + induction n generalizing addr s + case succ => + rename_i n n_ih + unfold write_mem_bytes; simp only + rw [n_ih, r_of_write_mem] + case zero => rfl + done + +theorem fetch_inst_of_write_mem : + fetch_inst addr1 (write_mem addr2 val s) = fetch_inst addr1 s := by + unfold fetch_inst write_mem + simp + +@[state_simp_rules] +theorem fetch_inst_of_write_mem_bytes : + fetch_inst addr1 (write_mem_bytes n addr2 val s) = fetch_inst addr1 s := by + induction n generalizing addr2 s + case zero => rfl + case succ => + rename_i n n_ih + unfold write_mem_bytes; simp only + rw [n_ih, fetch_inst_of_write_mem] + done + +theorem read_mem_of_w : + read_mem addr (w fld v s) = read_mem addr s := by + unfold read_mem + unfold w write_base_gpr write_base_sfp + unfold write_base_pc write_base_flag write_base_error + split <;> simp + +@[state_simp_rules] +theorem read_mem_bytes_of_w : + read_mem_bytes n addr (w fld v s) = read_mem_bytes n addr s := by + induction n generalizing addr s + case zero => rfl + case succ => + rename_i n n_ih + unfold read_mem_bytes; simp only [read_mem_of_w] + rw [n_ih] + done + +@[state_simp_rules] +theorem write_mem_bytes_program {n : Nat} (addr : BitVec 64) (bytes : BitVec (n * 8)): + (write_mem_bytes n addr bytes s).program = s.program := by + intros + induction n generalizing addr s + · simp [write_mem_bytes] + · rename_i n h_n + simp only [write_mem_bytes] + rw [h_n] + simp only [write_mem] + +---- Memory RoW/WoW lemmas ---- + +theorem read_mem_of_write_mem_same : + read_mem addr (write_mem addr v s) = v := by + unfold read_mem write_mem; simp [store_read_over_write_same] + +theorem read_mem_of_write_mem_different (h : addr1 ≠ addr2) : + read_mem addr1 (write_mem addr2 v s) = read_mem addr1 s := by + unfold read_mem write_mem; simp + rw [store_read_over_write_different]; trivial + +theorem write_mem_of_write_mem_shadow : + write_mem addr val2 (write_mem addr val1 s) = write_mem addr val2 s := by + simp [write_mem]; unfold write_store; simp_all; done + +theorem write_mem_irrelevant : + write_mem addr (read_mem addr s) s = s := by + simp [read_mem, write_mem, store_write_irrelevant] + +end Memory + ---------------------------------------------------------------------- From 9e0ec16c880330452fd8df530b886d2941d75c2d Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Thu, 1 Aug 2024 10:08:38 -0500 Subject: [PATCH 2/8] chore: delete Arm.Memory --- Arm/Decode.lean | 1 - Arm/Exec.lean | 1 - Arm/Insts/BR/Compare_branch.lean | 2 +- Arm/Insts/BR/Cond_branch_imm.lean | 2 +- Arm/Insts/BR/Uncond_branch_imm.lean | 2 +- Arm/Insts/BR/Uncond_branch_reg.lean | 2 +- Arm/Insts/Common.lean | 2 +- Arm/Insts/DPI/PC_rel_addressing.lean | 2 +- Arm/Insts/DPR/Conditional_select.lean | 2 +- Arm/Insts/DPSFP/Advanced_simd_extract.lean | 2 +- Arm/Insts/DPSFP/Advanced_simd_three_different.lean | 2 +- Arm/Insts/DPSFP/Advanced_simd_three_same.lean | 2 +- Arm/Insts/DPSFP/Advanced_simd_two_reg_misc.lean | 2 +- Arm/Insts/DPSFP/Crypto_four_reg.lean | 2 +- Arm/Insts/DPSFP/Crypto_three_reg_sha512.lean | 2 +- Arm/Memory.lean | 10 ---------- Arm/SeparateProofs.lean | 2 +- Arm/State.lean | 4 +--- Arm/StateEq.lean | 2 -- Proofs/Experiments/MemoryAliasing.lean | 1 + 20 files changed, 16 insertions(+), 31 deletions(-) delete mode 100644 Arm/Memory.lean diff --git a/Arm/Decode.lean b/Arm/Decode.lean index 0e58797a..52871d61 100644 --- a/Arm/Decode.lean +++ b/Arm/Decode.lean @@ -3,7 +3,6 @@ Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved. Released under Apache 2.0 license as described in the file LICENSE. Author(s): Shilpi Goel -/ -import Arm.Memory import Arm.Decode.DPI import Arm.Decode.DPR import Arm.Decode.BR diff --git a/Arm/Exec.lean b/Arm/Exec.lean index 6e5ffc50..cfbffa11 100644 --- a/Arm/Exec.lean +++ b/Arm/Exec.lean @@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE. Author(s): Shilpi Goel -/ import Arm.BitVec -import Arm.Memory import Arm.Decode import Arm.Insts diff --git a/Arm/Insts/BR/Compare_branch.lean b/Arm/Insts/BR/Compare_branch.lean index 41eae29f..b15d551d 100644 --- a/Arm/Insts/BR/Compare_branch.lean +++ b/Arm/Insts/BR/Compare_branch.lean @@ -7,7 +7,7 @@ Author(s): Shilpi Goel -- CBZ, CBNZ -- 32 and 64-bit variants import Arm.Decode -import Arm.Memory +import Arm.State import Arm.Insts.Common import Arm.BitVec diff --git a/Arm/Insts/BR/Cond_branch_imm.lean b/Arm/Insts/BR/Cond_branch_imm.lean index f523140d..d15aa16b 100644 --- a/Arm/Insts/BR/Cond_branch_imm.lean +++ b/Arm/Insts/BR/Cond_branch_imm.lean @@ -7,7 +7,7 @@ Author(s): Yan Peng -- B.cond import Arm.Decode -import Arm.Memory +import Arm.State import Arm.Insts.Common import Arm.BitVec diff --git a/Arm/Insts/BR/Uncond_branch_imm.lean b/Arm/Insts/BR/Uncond_branch_imm.lean index d2623ca0..1313a4d3 100644 --- a/Arm/Insts/BR/Uncond_branch_imm.lean +++ b/Arm/Insts/BR/Uncond_branch_imm.lean @@ -7,7 +7,7 @@ Author(s): Shilpi Goel -- B, BL import Arm.Decode -import Arm.Memory +import Arm.State import Arm.Insts.Common import Arm.BitVec diff --git a/Arm/Insts/BR/Uncond_branch_reg.lean b/Arm/Insts/BR/Uncond_branch_reg.lean index 710d44b1..1e3cbb97 100644 --- a/Arm/Insts/BR/Uncond_branch_reg.lean +++ b/Arm/Insts/BR/Uncond_branch_reg.lean @@ -7,7 +7,7 @@ Author(s): Shilpi Goel -- RET import Arm.Decode -import Arm.Memory +import Arm.State import Arm.Insts.Common import Arm.BitVec diff --git a/Arm/Insts/Common.lean b/Arm/Insts/Common.lean index 794121b5..f2547044 100644 --- a/Arm/Insts/Common.lean +++ b/Arm/Insts/Common.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author(s): Shilpi Goel, Yan Peng -/ import Arm.BitVec -import Arm.Memory +import Arm.State section Common diff --git a/Arm/Insts/DPI/PC_rel_addressing.lean b/Arm/Insts/DPI/PC_rel_addressing.lean index 76bf345f..82f63a35 100644 --- a/Arm/Insts/DPI/PC_rel_addressing.lean +++ b/Arm/Insts/DPI/PC_rel_addressing.lean @@ -6,7 +6,7 @@ Author(s): Shilpi Goel -- ADR, ADRP import Arm.Decode -import Arm.Memory +import Arm.State import Arm.Insts.Common import Arm.BitVec diff --git a/Arm/Insts/DPR/Conditional_select.lean b/Arm/Insts/DPR/Conditional_select.lean index 23939220..547f8ebd 100644 --- a/Arm/Insts/DPR/Conditional_select.lean +++ b/Arm/Insts/DPR/Conditional_select.lean @@ -6,7 +6,7 @@ Author(s): Shilpi Goel -- CSEL, CSINC, CSINV, CSNEG: 32- and 64-bit versions import Arm.Decode -import Arm.Memory +import Arm.State import Arm.Insts.Common import Arm.BitVec diff --git a/Arm/Insts/DPSFP/Advanced_simd_extract.lean b/Arm/Insts/DPSFP/Advanced_simd_extract.lean index abfa13ed..19e9ead5 100644 --- a/Arm/Insts/DPSFP/Advanced_simd_extract.lean +++ b/Arm/Insts/DPSFP/Advanced_simd_extract.lean @@ -6,7 +6,7 @@ Author(s): Shilpi Goel -- EXT import Arm.Decode -import Arm.Memory +import Arm.State import Arm.Insts.Common import Arm.BitVec diff --git a/Arm/Insts/DPSFP/Advanced_simd_three_different.lean b/Arm/Insts/DPSFP/Advanced_simd_three_different.lean index ed311369..2d18e935 100644 --- a/Arm/Insts/DPSFP/Advanced_simd_three_different.lean +++ b/Arm/Insts/DPSFP/Advanced_simd_three_different.lean @@ -7,7 +7,7 @@ Author(s): Yan Peng -- Polynomial arithmetic over {0,1}: https://tiny.amazon.com/5h01fjm6/devearmdocuddi0cApplApplPoly import Arm.Decode -import Arm.Memory +import Arm.State import Arm.Insts.Common ---------------------------------------------------------------------- diff --git a/Arm/Insts/DPSFP/Advanced_simd_three_same.lean b/Arm/Insts/DPSFP/Advanced_simd_three_same.lean index ca4ad97f..616ecd5e 100644 --- a/Arm/Insts/DPSFP/Advanced_simd_three_same.lean +++ b/Arm/Insts/DPSFP/Advanced_simd_three_same.lean @@ -6,7 +6,7 @@ Author(s): Shilpi Goel, Yan Peng -- ADD, ORR, AND, BIC, ORR, ORN, EOR, BSL, BIT, BIF (vector) import Arm.Decode -import Arm.Memory +import Arm.State import Arm.Insts.Common import Arm.BitVec diff --git a/Arm/Insts/DPSFP/Advanced_simd_two_reg_misc.lean b/Arm/Insts/DPSFP/Advanced_simd_two_reg_misc.lean index 7fc90ad5..2d68feaf 100644 --- a/Arm/Insts/DPSFP/Advanced_simd_two_reg_misc.lean +++ b/Arm/Insts/DPSFP/Advanced_simd_two_reg_misc.lean @@ -6,7 +6,7 @@ Author(s): Shilpi Goel -- REV64 import Arm.Decode -import Arm.Memory +import Arm.State import Arm.Insts.Common import Arm.BitVec diff --git a/Arm/Insts/DPSFP/Crypto_four_reg.lean b/Arm/Insts/DPSFP/Crypto_four_reg.lean index a0ac299d..a08cede0 100644 --- a/Arm/Insts/DPSFP/Crypto_four_reg.lean +++ b/Arm/Insts/DPSFP/Crypto_four_reg.lean @@ -6,7 +6,7 @@ Author(s): Shilpi Goel, Nevine Ebeid -- EOR3 import Arm.Decode -import Arm.Memory +import Arm.State import Arm.Insts.Common import Arm.BitVec diff --git a/Arm/Insts/DPSFP/Crypto_three_reg_sha512.lean b/Arm/Insts/DPSFP/Crypto_three_reg_sha512.lean index 3e8a2f7f..c25d02d8 100644 --- a/Arm/Insts/DPSFP/Crypto_three_reg_sha512.lean +++ b/Arm/Insts/DPSFP/Crypto_three_reg_sha512.lean @@ -6,7 +6,7 @@ Author(s): Shilpi Goel -- SHA512H, SHA512H2, SHA512SU1 import Arm.Decode -import Arm.Memory +import Arm.State import Arm.Insts.Common import Arm.BitVec import Specs.SHA512Common diff --git a/Arm/Memory.lean b/Arm/Memory.lean deleted file mode 100644 index a6077163..00000000 --- a/Arm/Memory.lean +++ /dev/null @@ -1,10 +0,0 @@ -/- -Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Author(s): Shilpi Goel --/ -import Arm.Separate - -section Memory - -open BitVec diff --git a/Arm/SeparateProofs.lean b/Arm/SeparateProofs.lean index ddb58552..3776f7e6 100644 --- a/Arm/SeparateProofs.lean +++ b/Arm/SeparateProofs.lean @@ -3,7 +3,7 @@ Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. Released under Apache 2.0 license as described in the file LICENSE. Author(s): Shilpi Goel -/ -import Arm.Memory +import Arm.State import LeanSAT ---------------------------------------------------------------------- diff --git a/Arm/State.lean b/Arm/State.lean index 99103bf4..af77a3e4 100644 --- a/Arm/State.lean +++ b/Arm/State.lean @@ -513,14 +513,12 @@ end State section Memory ---------------------------------------------------------------------- --- (FIXME) Make read_mem private. -- We export read_mem_bytes, not read_mem. private def read_mem (addr : BitVec 64) (s : ArmState) : BitVec 8 := read_store addr s.mem -- We don't add the simp attribute to read/write_mem_bytes. Instead, -- we prove and export properties about their (non)interference. - def read_mem_bytes (n : Nat) (addr : BitVec 64) (s : ArmState) : BitVec (n * 8) := match n with | 0 => 0#0 @@ -530,7 +528,6 @@ def read_mem_bytes (n : Nat) (addr : BitVec 64) (s : ArmState) : BitVec (n * 8) have h: n' * 8 + 8 = (n' + 1) * 8 := by simp_arith BitVec.cast h (rest ++ byte) --- (FIXME) Make write_mem private. -- We export write_mem_bytes, not write_mem. private def write_mem (addr : BitVec 64) (val : BitVec 8) (s : ArmState) : ArmState := let new_mem := write_store addr val s.mem @@ -544,6 +541,7 @@ def write_mem_bytes (n : Nat) (addr : BitVec 64) (val : BitVec (n * 8)) (s : Arm let s := write_mem addr byte s let val_rest := BitVec.zeroExtend (n' * 8) (val >>> 8) write_mem_bytes n' (addr + 1#64) val_rest s + ---------------------------------------------------------------------- ---- Memory accessors and updaters ---- diff --git a/Arm/StateEq.lean b/Arm/StateEq.lean index ee3cb3e8..e3f685c5 100644 --- a/Arm/StateEq.lean +++ b/Arm/StateEq.lean @@ -4,8 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE. Author(s): Shilpi Goel -/ import Arm.State -import Arm.Memory - section StateEq open BitVec diff --git a/Proofs/Experiments/MemoryAliasing.lean b/Proofs/Experiments/MemoryAliasing.lean index 471d613a..9c42afeb 100644 --- a/Proofs/Experiments/MemoryAliasing.lean +++ b/Proofs/Experiments/MemoryAliasing.lean @@ -7,6 +7,7 @@ The goal is to eliminate the sorry, and to simplify the proof to a tactic invoca -/ import Arm -- TODO(@bollu): make this visible from 'Arm'. +import Arm.State import Arm.MemoryProofs theorem mem_automation_test From 1d826251c7363e6e0e58ff895222b306de0a3d81 Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Thu, 1 Aug 2024 10:12:33 -0500 Subject: [PATCH 3/8] chore: update comments to use doc syntax --- Arm/State.lean | 24 +++++++++++------------- 1 file changed, 11 insertions(+), 13 deletions(-) diff --git a/Arm/State.lean b/Arm/State.lean index af77a3e4..96e31fb5 100644 --- a/Arm/State.lean +++ b/Arm/State.lean @@ -510,25 +510,26 @@ example : end State +/-! # Memory operations on State. -/ section Memory ----------------------------------------------------------------------- --- We export read_mem_bytes, not read_mem. +/-- We export read_mem_bytes, not read_mem. -/ private def read_mem (addr : BitVec 64) (s : ArmState) : BitVec 8 := read_store addr s.mem --- We don't add the simp attribute to read/write_mem_bytes. Instead, --- we prove and export properties about their (non)interference. +/-- +We don't add the simp attribute to read/write_mem_bytes. Instead, +we prove and export properties about their (non)interference. +-/ def read_mem_bytes (n : Nat) (addr : BitVec 64) (s : ArmState) : BitVec (n * 8) := match n with | 0 => 0#0 | n' + 1 => let byte := read_mem addr s let rest := read_mem_bytes n' (addr + 1#64) s - have h: n' * 8 + 8 = (n' + 1) * 8 := by simp_arith - BitVec.cast h (rest ++ byte) + (rest ++ byte).cast (by omega) --- We export write_mem_bytes, not write_mem. +/-- We export write_mem_bytes, not write_mem. -/ private def write_mem (addr : BitVec 64) (val : BitVec 8) (s : ArmState) : ArmState := let new_mem := write_store addr val s.mem { s with mem := new_mem } @@ -542,11 +543,10 @@ def write_mem_bytes (n : Nat) (addr : BitVec 64) (val : BitVec (n * 8)) (s : Arm let val_rest := BitVec.zeroExtend (n' * 8) (val >>> 8) write_mem_bytes n' (addr + 1#64) val_rest s ----------------------------------------------------------------------- ----- Memory accessors and updaters ---- +/-! # Memory accessors and updaters -/ ----- RoW/WoW lemmas about memory and other fields ---- +/-! ### RoW/WoW lemmas about memory and other fields -/ theorem r_of_write_mem : r fld (write_mem addr val s) = r fld s := by unfold r @@ -611,7 +611,7 @@ theorem write_mem_bytes_program {n : Nat} (addr : BitVec 64) (bytes : BitVec (n rw [h_n] simp only [write_mem] ----- Memory RoW/WoW lemmas ---- +/-! ### Memory RoW/WoW lemmas -/ theorem read_mem_of_write_mem_same : read_mem addr (write_mem addr v s) = v := by @@ -631,5 +631,3 @@ theorem write_mem_irrelevant : simp [read_mem, write_mem, store_write_irrelevant] end Memory - ----------------------------------------------------------------------- From 9e8e198277b291cd7c5de0cbc10a67a2a917e897 Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Thu, 1 Aug 2024 10:14:17 -0500 Subject: [PATCH 4/8] chore: update comment syntax for Arm/State.lean --- Arm/State.lean | 31 ++++++++++++++------------ Proofs/Experiments/MemoryAliasing.lean | 2 -- 2 files changed, 17 insertions(+), 16 deletions(-) diff --git a/Arm/State.lean b/Arm/State.lean index 96e31fb5..97367356 100644 --- a/Arm/State.lean +++ b/Arm/State.lean @@ -117,25 +117,28 @@ deriving DecidableEq, Repr @[ext] structure ArmState where - -- General-purpose registers: register 31 is the stack pointer. + /-- General-purpose registers: register 31 is the stack pointer. -/ private gpr : Store (BitVec 5) (BitVec 64) - -- SIMD/floating-point registers + /-- SIMD/floating-point registers -/ private sfp : Store (BitVec 5) (BitVec 128) - -- Program Counter + /-- Program Counter -/ private pc : BitVec 64 - -- PState + /-- PState -/ private pstate : PState - -- Memory: maps 64-bit addresses to bytes + /-- Memory: maps 64-bit addresses to bytes -/ private mem : Store (BitVec 64) (BitVec 8) - -- Program: maps 64-bit addresses to 32-bit instructions. - -- Note that we have the following assumption baked into our machine model: - -- the program is always disjoint from the rest of the memory. - program : Program - - -- The error field is an artifact of this model; it is set to a - -- non-None value when some irrecoverable error is encountered - -- (e.g., an unimplemented instruction is hit). Any reasoning or - -- execution based off an erroneous state is invalid. + /-- + Program: maps 64-bit addresses to 32-bit instructions. + Note that we have the following assumption baked into our machine model: + the program is always disjoint from the rest of the memory. + -/ + program : Program + /-- + The error field is an artifact of this model; it is set to a + non-None value when some irrecoverable error is encountered + (e.g., an unimplemented instruction is hit). Any reasoning or + execution based off an erroneous state is invalid. + -/ private error : StateError deriving Repr diff --git a/Proofs/Experiments/MemoryAliasing.lean b/Proofs/Experiments/MemoryAliasing.lean index 9c42afeb..ea78859d 100644 --- a/Proofs/Experiments/MemoryAliasing.lean +++ b/Proofs/Experiments/MemoryAliasing.lean @@ -6,8 +6,6 @@ Author(s): Shilpi Goel, Siddharth Bhat The goal is to eliminate the sorry, and to simplify the proof to a tactic invocation. -/ import Arm --- TODO(@bollu): make this visible from 'Arm'. -import Arm.State import Arm.MemoryProofs theorem mem_automation_test From 24a0e8cc685a1d70f86a0b5c26d4f474bec3c68b Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Thu, 1 Aug 2024 11:04:18 -0500 Subject: [PATCH 5/8] chore: fixup read_err and read_pc in tests --- Arm/MemoryProofs.lean | 5 +++- Arm/SeparateProofs.lean | 1 + Arm/State.lean | 16 ++++++++--- Tests/AES-GCM/AESGCMProgramTests.lean | 12 ++++----- Tests/AES-GCM/AESV8ProgramTests.lean | 38 +++++++++++++-------------- Tests/AES-GCM/GCMProgramTests.lean | 16 +++++------ Tests/LDSTTest.lean | 6 ++--- Tests/SHA2/SHA512ProgramTest.lean | 2 +- 8 files changed, 54 insertions(+), 42 deletions(-) diff --git a/Arm/MemoryProofs.lean b/Arm/MemoryProofs.lean index 66c83e56..e9590724 100644 --- a/Arm/MemoryProofs.lean +++ b/Arm/MemoryProofs.lean @@ -5,6 +5,9 @@ Author(s): Shilpi Goel -/ import Arm.SeparateProofs import Arm.FromMathlib +import Arm.State +import Arm.Separate +import Arm.SeparateProofs -- In this file, we have memory (non-)interference proofs. @@ -690,7 +693,7 @@ theorem read_mem_of_write_mem_bytes_subset -- disable simproc for 2^64. simp only [mod_lt_conc, read_mem_of_write_mem_bytes_subset_helper_5] - have h_tmp : (2 ^ 64 - 1 + a) = (a + 2 ^ 64 - 1) := by + have h_tmp : (2 ^ 64 - 1 + a) = (a + 2 ^ 64 - 1) := by apply Nat.add_comm simp only [h_tmp] apply read_mem_of_write_mem_bytes_subset_helper_4 v a n' h_v_size h_a_base h_a_size diff --git a/Arm/SeparateProofs.lean b/Arm/SeparateProofs.lean index 3776f7e6..6e193465 100644 --- a/Arm/SeparateProofs.lean +++ b/Arm/SeparateProofs.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author(s): Shilpi Goel -/ import Arm.State +import Arm.Separate import LeanSAT ---------------------------------------------------------------------- diff --git a/Arm/State.lean b/Arm/State.lean index 97367356..3b645a3d 100644 --- a/Arm/State.lean +++ b/Arm/State.lean @@ -514,10 +514,18 @@ example : end State /-! # Memory operations on State. -/ + section Memory -/-- We export read_mem_bytes, not read_mem. -/ -private def read_mem (addr : BitVec 64) (s : ArmState) : BitVec 8 := +/-! +Ideally, `read_mem` and `write_mem` ought to be private, and we ought to only +expose `read_mem_bytes` and `write_mem_bytes` to the outside world. +However, due to layering violations with `Arm/MemoryProofs.lean`, we currently keep them public. +-/ + + +/-- We export read_mem_bytes, not read_mem. FIXME: make private. -/ +def read_mem (addr : BitVec 64) (s : ArmState) : BitVec 8 := read_store addr s.mem /-- @@ -532,8 +540,8 @@ def read_mem_bytes (n : Nat) (addr : BitVec 64) (s : ArmState) : BitVec (n * 8) let rest := read_mem_bytes n' (addr + 1#64) s (rest ++ byte).cast (by omega) -/-- We export write_mem_bytes, not write_mem. -/ -private def write_mem (addr : BitVec 64) (val : BitVec 8) (s : ArmState) : ArmState := +/-- We export write_mem_bytes, not write_mem. FIXME: make private. -/ +def write_mem (addr : BitVec 64) (val : BitVec 8) (s : ArmState) : ArmState := let new_mem := write_store addr val s.mem { s with mem := new_mem } diff --git a/Tests/AES-GCM/AESGCMProgramTests.lean b/Tests/AES-GCM/AESGCMProgramTests.lean index a9462458..892db542 100644 --- a/Tests/AES-GCM/AESGCMProgramTests.lean +++ b/Tests/AES-GCM/AESGCMProgramTests.lean @@ -216,7 +216,7 @@ def final_ciphertext : BitVec 4096 := read_mem_bytes 512 out_address final_state def final_hash : BitVec 128 := read_mem_bytes 16 Xi_address final_state def final_ivec : BitVec 128 := read_mem_bytes 16 ivec_address final_state -example : final_state.error = StateError.None := by native_decide +example : read_err final_state = StateError.None := by native_decide example : final_hash = revflat Xi_res := by native_decide example : final_ciphertext = revflat ciphertext := by native_decide example : final_ivec = revflat ivec_res := by native_decide @@ -234,7 +234,7 @@ def final_ciphertext : BitVec 4096 := read_mem_bytes 512 out_address final_state def final_hash : BitVec 128 := read_mem_bytes 16 Xi_address final_state def final_ivec : BitVec 128 := read_mem_bytes 16 ivec_address final_state -example : final_state.error = StateError.None := by native_decide +example : read_err final_state = StateError.None := by native_decide example : final_hash = revflat Xi_res := by native_decide set_option maxRecDepth 2100 in example : final_ciphertext = revflat in_blocks := by native_decide @@ -317,7 +317,7 @@ def final_ciphertext : BitVec 4096 := read_mem_bytes 512 out_address final_state def final_hash : BitVec 128 := read_mem_bytes 16 Xi_address final_state def final_ivec : BitVec 128 := read_mem_bytes 16 ivec_address final_state -example : final_state.error = StateError.None := by native_decide +example : read_err final_state = StateError.None := by native_decide example : final_hash = revflat Xi_res := by native_decide example : final_ciphertext = (revflat ciphertext) := by native_decide example : final_ivec = (revflat ivec_res) := by native_decide @@ -335,7 +335,7 @@ def final_ciphertext : BitVec 4096 := read_mem_bytes 512 out_address final_state def final_hash : BitVec 128 := read_mem_bytes 16 Xi_address final_state def final_ivec : BitVec 128 := read_mem_bytes 16 ivec_address final_state -example : final_state.error = StateError.None := by native_decide +example : read_err final_state = StateError.None := by native_decide example : final_hash = revflat Xi_res := by native_decide set_option maxRecDepth 2100 in example : final_ciphertext = revflat in_blocks := by native_decide @@ -421,7 +421,7 @@ def final_ciphertext : BitVec 4096 := read_mem_bytes 512 out_address final_state def final_hash : BitVec 128 := read_mem_bytes 16 Xi_address final_state def final_ivec : BitVec 128 := read_mem_bytes 16 ivec_address final_state -example : final_state.error = StateError.None := by native_decide +example : read_err final_state = StateError.None := by native_decide example : final_hash = revflat Xi_res := by native_decide example : final_ciphertext = revflat ciphertext := by native_decide example : final_ivec = (revflat ivec_res) := by native_decide @@ -439,7 +439,7 @@ def final_ciphertext : BitVec 4096 := read_mem_bytes 512 out_address final_state def final_hash : BitVec 128 := read_mem_bytes 16 Xi_address final_state def final_ivec : BitVec 128 := read_mem_bytes 16 ivec_address final_state -example : final_state.error = StateError.None := by native_decide +example : read_err final_state = StateError.None := by native_decide example : final_hash = revflat Xi_res := by native_decide set_option maxRecDepth 2100 in example : final_ciphertext = revflat in_blocks := by native_decide diff --git a/Tests/AES-GCM/AESV8ProgramTests.lean b/Tests/AES-GCM/AESV8ProgramTests.lean index 39dbb1e6..80dd2462 100644 --- a/Tests/AES-GCM/AESV8ProgramTests.lean +++ b/Tests/AES-GCM/AESV8ProgramTests.lean @@ -28,20 +28,20 @@ open BitVec -- Run test: -- 1. aws-lc-build/crypto/crypto_test --gtest_filter="AESTest.ABI" -/- +/- How to get the number of steps to run for a program? - When a program finishes, ArmState.pc would be set to 0x0#64 and ArmState.error + When a program finishes, ArmState.pc would be set to 0x0#64 read_err and ArmState will be `StateError.None`. If a program hasn't reached the last instruction, its ArmState.pc will be some number other than 0x0#64. This is based on an assumption that programs don't typically start at pc 0x0#64. - If a program runs past the last instruction, its ArmState.error will be: + If a program runs past the last instruction, read_err its ArmState will be: StateError.NotFound "No instruction found at PC 0x0000000000000000#64!" Based on above information, we could do a binary search for the number of steps - to run a program and the stopping criterion is that ArmState.pc = 0x0#64 and - ArmState.error = StateError.None. This sounds awfully programmable, but for + to run a program and the stopping criterion is that ArmState.pc = 0x0#64 anread_err d + ArmState = StateError.None. This sounds awfully programmable, but for now we reply on this comment. -/ @@ -113,7 +113,7 @@ def final_state : ArmState := aes_hw_set_encrypt_key_test 167 key_bits def final_rd_key : BitVec 1408 := read_mem_bytes 176 key_address final_state def final_rounds : BitVec 64 := read_mem_bytes 8 (key_address + 240) final_state -example : final_state.error = StateError.None := by native_decide +example : read_err final_state = StateError.None := by native_decide example : final_rd_key = revflat rd_key := by native_decide example : final_rounds = rounds := by native_decide @@ -143,7 +143,7 @@ def final_state : ArmState := aes_hw_set_encrypt_key_test 195 key_bits def final_rd_key : BitVec 1664 := read_mem_bytes 208 key_address final_state def final_rounds : BitVec 64 := read_mem_bytes 8 (key_address + 240) final_state -example : final_state.error = StateError.None := by native_decide +example : read_err final_state = StateError.None := by native_decide example : final_rd_key = revflat rd_key := by native_decide example : final_rounds = rounds := by native_decide @@ -175,7 +175,7 @@ def final_state : ArmState := aes_hw_set_encrypt_key_test 198 key_bits def final_rd_key : BitVec 1920 := read_mem_bytes 240 key_address final_state def final_rounds : BitVec 64 := read_mem_bytes 8 (key_address + 240) final_state -example : final_state.error = StateError.None := by native_decide +example : read_err final_state = StateError.None := by native_decide example : final_rd_key = revflat rd_key := by native_decide example : final_rounds = rounds := by native_decide @@ -231,7 +231,7 @@ def final_state : ArmState := aes_hw_encrypt_test 44 (revflat in_block) rounds (revflat key_schedule) def final_ciphertext : BitVec 128 := read_mem_bytes 16 out_address final_state -example : final_state.error = StateError.None := by native_decide +example : read_err final_state = StateError.None := by native_decide example : final_ciphertext = revflat out_block := by native_decide end AES128 @@ -254,7 +254,7 @@ def final_state : ArmState := aes_hw_encrypt_test 52 (revflat in_block) rounds (revflat key_schedule) def final_ciphertext : BitVec 128 := read_mem_bytes 16 out_address final_state -example : final_state.error = StateError.None := by native_decide +example : read_err final_state = StateError.None := by native_decide example : final_ciphertext = revflat out_block := by native_decide @@ -276,7 +276,7 @@ def final_state : ArmState := aes_hw_encrypt_test 60 (revflat in_block) rounds (revflat key_schedule) def final_ciphertext : BitVec 128 := read_mem_bytes 16 out_address final_state -example : final_state.error = StateError.None := by native_decide +example : read_err final_state = StateError.None := by native_decide example : final_ciphertext = revflat out_block := by native_decide @@ -355,42 +355,42 @@ def buf_res_128 : List (BitVec 8) := def final_state0 : ArmState := aes_hw_ctr32_encrypt_blocks_test 83 0 in_block rounds key_schedule ivec def final_buf0 : BitVec 640 := read_mem_bytes 80 out_address final_state0 -example : final_state0.error = StateError.None := by native_decide +example : read_err final_state0 = StateError.None := by native_decide example: final_buf0 = (BitVec.zero 384) ++ (extractLsb 255 0 (revflat buf_res_128)) := by native_decide -- len = 1 def final_state1 : ArmState := aes_hw_ctr32_encrypt_blocks_test 82 1 in_block rounds key_schedule ivec def final_buf1 : BitVec 640 := read_mem_bytes 80 out_address final_state1 -example : final_state1.error = StateError.None := by native_decide +example : read_err final_state1 = StateError.None := by native_decide example: final_buf1 = (BitVec.zero 512) ++ (extractLsb 127 0 (revflat buf_res_128)) := by native_decide -- -- len = 2 def final_state2 : ArmState := aes_hw_ctr32_encrypt_blocks_test 82 2 in_block rounds key_schedule ivec def final_buf2 : BitVec 640 := read_mem_bytes 80 out_address final_state2 -example : final_state2.error = StateError.None := by native_decide +example : read_err final_state2 = StateError.None := by native_decide example: final_buf2 = (BitVec.zero 384) ++ (extractLsb 255 0 (revflat buf_res_128)) := by native_decide -- len = 3 def final_state3 : ArmState := aes_hw_ctr32_encrypt_blocks_test 129 3 in_block rounds key_schedule ivec def final_buf3 : BitVec 640 := read_mem_bytes 80 out_address final_state3 -example : final_state3.error = StateError.None := by native_decide +example : read_err final_state3 = StateError.None := by native_decide example: final_buf3 = (BitVec.zero 256) ++ (extractLsb 383 0 (revflat buf_res_128)) := by native_decide -- len = 4 def final_state4 : ArmState := aes_hw_ctr32_encrypt_blocks_test 187 4 in_block rounds key_schedule ivec def final_buf4 : BitVec 640 := read_mem_bytes 80 out_address final_state4 -example : final_state4.error = StateError.None := by native_decide +example : read_err final_state4 = StateError.None := by native_decide example: final_buf4 = (BitVec.zero 127) ++ (extractLsb 512 0 (revflat buf_res_128)) := by native_decide -- len = 5 def final_state5 : ArmState := aes_hw_ctr32_encrypt_blocks_test 188 5 in_block rounds key_schedule ivec def final_buf5 : BitVec 640 := read_mem_bytes 80 out_address final_state5 -example : final_state5.error = StateError.None := by native_decide +example : read_err final_state5 = StateError.None := by native_decide example: final_buf5 = revflat buf_res_128 := by native_decide end AES128Ctr32 @@ -416,7 +416,7 @@ def buf_res_192 : List (BitVec 8) := def final_state : ArmState := aes_hw_ctr32_encrypt_blocks_test 216 5 in_block rounds key_schedule ivec def final_buf : BitVec 640 := read_mem_bytes 80 out_address final_state -example : final_state.error = StateError.None := by native_decide +example : read_err final_state = StateError.None := by native_decide example: final_buf = revflat buf_res_192 := by native_decide end AES192Ctr32 @@ -442,7 +442,7 @@ def buf_res_256 : List (BitVec 8) := def final_state : ArmState := aes_hw_ctr32_encrypt_blocks_test 244 5 in_block rounds key_schedule ivec def final_buf : BitVec 640 := read_mem_bytes 80 out_address final_state -example : final_state.error = StateError.None := by native_decide +example : read_err final_state = StateError.None := by native_decide example: final_buf = revflat buf_res_256 := by native_decide end AES256Ctr32 diff --git a/Tests/AES-GCM/GCMProgramTests.lean b/Tests/AES-GCM/GCMProgramTests.lean index 01347cf8..8d93b6ee 100644 --- a/Tests/AES-GCM/GCMProgramTests.lean +++ b/Tests/AES-GCM/GCMProgramTests.lean @@ -130,10 +130,10 @@ def init_gcm_init_test : ArmState := s def final_state : ArmState := run GCMInitV8Program.gcm_init_v8_program.length init_gcm_init_test -def final_pc : BitVec 64 := final_state.pc +def final_pc : BitVec 64 := read_pc final_state def final_table : BitVec 2048 := read_mem_bytes 256 Htable_address final_state example : final_table = revflat Htable := by native_decide -example : final_state.error = StateError.None := by native_decide +example : read_err final_state = StateError.None := by native_decide end GCMInitV8ProgramTest @@ -171,7 +171,7 @@ def gcm_gmult_final_state : ArmState := def final_hash : BitVec 128 := read_mem_bytes 16 x_address gcm_gmult_final_state example : final_hash = revflat X_after := by native_decide -example : gcm_gmult_final_state.error = StateError.None := by native_decide +example : read_err gcm_gmult_final_state = StateError.None := by native_decide end GCMGmultV8ProgramTest @@ -218,7 +218,7 @@ def final_state : ArmState := def final_hash : BitVec 128 := read_mem_bytes 16 x_address final_state example : final_hash = revflat X_after := by native_decide -example : final_state.error = StateError.None := by native_decide +example : read_err final_state = StateError.None := by native_decide end block2 @@ -234,7 +234,7 @@ def final_state : ArmState := def final_hash : BitVec 128 := read_mem_bytes 16 x_address final_state example : final_hash = revflat X_after := by native_decide -example : final_state.error = StateError.None := by native_decide +example : read_err final_state = StateError.None := by native_decide end block4 @@ -250,7 +250,7 @@ def final_state : ArmState := def final_hash : BitVec 128 := read_mem_bytes 16 x_address final_state example : final_hash = revflat X_after := by native_decide -example : final_state.error = StateError.None := by native_decide +example : read_err final_state = StateError.None := by native_decide end block5 @@ -266,7 +266,7 @@ def final_state : ArmState := def final_hash : BitVec 128 := read_mem_bytes 16 x_address final_state example : final_hash = revflat X_after := by native_decide -example : final_state.error = StateError.None := by native_decide +example : read_err final_state = StateError.None := by native_decide end block6 @@ -282,7 +282,7 @@ def final_state : ArmState := def final_hash : BitVec 128 := read_mem_bytes 16 x_address final_state example : final_hash = revflat X_after := by native_decide -example : final_state.error = StateError.None := by native_decide +example : read_err final_state = StateError.None := by native_decide end block7 diff --git a/Tests/LDSTTest.lean b/Tests/LDSTTest.lean index c036584a..d60a829a 100644 --- a/Tests/LDSTTest.lean +++ b/Tests/LDSTTest.lean @@ -38,7 +38,7 @@ def ldr_gpr_unsigned_offset_state : ArmState := def ldr_gpr_unsigned_offset_final_state : ArmState := run 1 ldr_gpr_unsigned_offset_state example : (read_gpr 64 0#5 ldr_gpr_unsigned_offset_final_state) = 20#64 := by native_decide -example : ldr_gpr_unsigned_offset_final_state.pc = 4#64 := by native_decide +example : read_pc ldr_gpr_unsigned_offset_final_state = 4#64 := by native_decide ---------------------------------------------------------------------- -- test str, 64-bit gpr, post-index @@ -56,7 +56,7 @@ def str_gpr_post_index_final_state : ArmState := run 1 str_gpr_post_index_state example : (read_gpr 64 1#5 str_gpr_post_index_final_state) = 3#64 := by native_decide example : (read_mem_bytes 8 0#64 str_gpr_post_index_final_state) = 20#64 := by native_decide -example : str_gpr_post_index_final_state.pc = 4#64 := by native_decide +example : read_pc str_gpr_post_index_final_state = 4#64 := by native_decide ---------------------------------------------------------------------- -- test ldr, 64-bit sfp, post-index @@ -94,7 +94,7 @@ def ldrb_unsigned_offset : Program := def ldrb_unsigned_offset_state: ArmState := let s := set_init_state ldrb_unsigned_offset write_mem_bytes 1 4#64 20#8 s - + def ldrb_unsigned_offset_final_state : ArmState := run 1 ldrb_unsigned_offset_state example : (read_gpr 64 0#5 ldrb_unsigned_offset_final_state) = 20#64 := by native_decide diff --git a/Tests/SHA2/SHA512ProgramTest.lean b/Tests/SHA2/SHA512ProgramTest.lean index c22b626d..e37b921d 100644 --- a/Tests/SHA2/SHA512ProgramTest.lean +++ b/Tests/SHA2/SHA512ProgramTest.lean @@ -609,7 +609,7 @@ def init_sha512_test : ArmState := -- #eval (log_run "Tests/SHA512_PC.log" pc_trace 503 init_sha512_test) def final_sha512_state : ArmState := run 503 init_sha512_test -def final_sha512_pc : BitVec 64 := final_sha512_state.pc +def final_sha512_pc : BitVec 64 := read_pc final_sha512_state -- read_mem_bytes below with (512/8) as the first arg. causes a -- "maximum recursion depth has been reached" error, but that worked From 3ad266bbc67580810b540b6f7d9b23ba0e822077 Mon Sep 17 00:00:00 2001 From: Siddharth Date: Fri, 2 Aug 2024 07:29:29 -0500 Subject: [PATCH 6/8] Apply suggestions from code review Co-authored-by: Shilpi Goel --- Tests/AES-GCM/AESV8ProgramTests.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Tests/AES-GCM/AESV8ProgramTests.lean b/Tests/AES-GCM/AESV8ProgramTests.lean index 4e659bd0..ff45f3eb 100644 --- a/Tests/AES-GCM/AESV8ProgramTests.lean +++ b/Tests/AES-GCM/AESV8ProgramTests.lean @@ -35,12 +35,12 @@ open BitVec will be `StateError.None`. If a program hasn't reached the last instruction, its ArmState.pc will be some number other than 0x0#64. This is based on an assumption that programs don't typically start at pc 0x0#64. - If a program runs past the last instruction, read_err its ArmState will be: + If a program runs past the last instruction, (read_err ArmState) will be: StateError.NotFound "No instruction found at PC 0x0000000000000000#64!" Based on above information, we could do a binary search for the number of steps - to run a program and the stopping criterion is that ArmState.pc = 0x0#64 anread_err d + to run a program and the stopping criterion is that ArmState.pc = 0x0#64 and read_err ArmState = StateError.None. This sounds awfully programmable, but for now we reply on this comment. From d3918e50283aa73a05db5b1a1f7d8f1e6c3029d4 Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Fri, 2 Aug 2024 09:18:01 -0500 Subject: [PATCH 7/8] chore: remove redundant import --- Arm/MemoryProofs.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Arm/MemoryProofs.lean b/Arm/MemoryProofs.lean index e9590724..ed70ca51 100644 --- a/Arm/MemoryProofs.lean +++ b/Arm/MemoryProofs.lean @@ -3,7 +3,6 @@ Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. Released under Apache 2.0 license as described in the file LICENSE. Author(s): Shilpi Goel -/ -import Arm.SeparateProofs import Arm.FromMathlib import Arm.State import Arm.Separate From 64b9230dcd3272bc366dddf5c5926dfb1bb394a6 Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Fri, 2 Aug 2024 09:19:49 -0500 Subject: [PATCH 8/8] chore: fixup comments in AESV8ProgramTests --- Tests/AES-GCM/AESV8ProgramTests.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Tests/AES-GCM/AESV8ProgramTests.lean b/Tests/AES-GCM/AESV8ProgramTests.lean index ff45f3eb..a60f6ba2 100644 --- a/Tests/AES-GCM/AESV8ProgramTests.lean +++ b/Tests/AES-GCM/AESV8ProgramTests.lean @@ -31,17 +31,17 @@ open BitVec /- How to get the number of steps to run for a program? - When a program finishes, ArmState.pc would be set to 0x0#64 read_err and ArmState + When a program finishes, ArmState.pc would be set to 0x0#64 and `read_err ArmState` will be `StateError.None`. If a program hasn't reached the last instruction, its ArmState.pc will be some number other than 0x0#64. This is based on an assumption that programs don't typically start at pc 0x0#64. - If a program runs past the last instruction, (read_err ArmState) will be: + If a program runs past the last instruction, `(read_err ArmState)` will be: StateError.NotFound "No instruction found at PC 0x0000000000000000#64!" Based on above information, we could do a binary search for the number of steps - to run a program and the stopping criterion is that ArmState.pc = 0x0#64 and read_err - ArmState = StateError.None. This sounds awfully programmable, but for + to run a program and the stopping criterion is that ArmState.pc = 0x0#64 and + `read_err ArmState = StateError.None`. This sounds awfully programmable, but for now we reply on this comment. -/