Implement a decision procedure for memory reads/write via omega

[bollu]

This reduces goals about memory to goals about natural numbers, with the hope of allowing the use of omega to dispatch such goals.

[bollu]

Hmm, by writing the "naive" definitions of getLsb_read_mem_bytes, getLsb_write_mem_bytes, I get the fairly horrific goal state:

⊢ (decide (↑i < 16 * 8) &&
    if src_addr + ↑↑i / 8 < dest_addr then (s0.mem (src_addr + ↑↑i / 8)).getLsb (↑i % 8)
    else
      if (src_addr + ↑↑i / 8).toNat ≥ dest_addr.toNat + 16 then (s0.mem (src_addr + ↑↑i / 8)).getLsb (↑i % 8)
      else (blah.extractLsB (src_addr + ↑↑i / 8 - dest_addr).toNat).getLsb (↑i % 8)) =
  (decide (↑i < 16 * 8) && (s0.mem (src_addr + ↑↑i / 8)).getLsb (↑i % 8))

which is not immediately omega able for sure.

[bollu]

n0 : Nat
src_addr dest_addr : BitVec 64
blah : BitVec (16 * 8)
s0 : ArmState
h_n0 : n0 ≠ 0
h_s0_src_dest_separate : mem_separate src_addr (src_addr + (↑(n0 <<< 4) - 1)) dest_addr (dest_addr + (↑(n0 <<< 4) - 1)) = true
h_no_wrap_dest_region : dest_addr.toNat ≤ (dest_addr.toNat + (18446744073709551615 + n0 <<< 4)) % 18446744073709551616
h_no_wrap_src_region : src_addr.toNat ≤ (src_addr.toNat + (18446744073709551615 + n0 <<< 4)) % 18446744073709551616
i : Fin (16 * 8)
h₁ : ¬src_addr + ↑↑i / 8 < dest_addr
h₂ : ¬(src_addr + ↑↑i / 8).toNat ≥ dest_addr.toNat + 16
⊢ False

we exfalso to get a proof state where we know we gotta prove false. See that the proof state says that dest is in between src_addr + i/8 and src+addr + i/8 + 16. But this cannot happen, because we have a mem_separate clause. While indeed the conditions look terrible, that's more an artefact of how stuff is phrased. I think we can actually see this through!

[bollu]

set_option trace.simp_mem true in
set_option trace.simp_mem.info  true in
theorem mem_automation_test
  (h_s0_src_dest_separate : mem_separate' src_addr  16 dest_addr 16) :
  read_mem_bytes 16 src_addr (write_mem_bytes 16 dest_addr blah s0) =
  read_mem_bytes 16 src_addr s0 := by
  -- ⊢ read_mem_bytes 16 src_addr (write_mem_bytes 16 dest_addr blah s0) = read_mem_bytes 16 src_addr s0
  simp_mem
  -- ⊢ read_mem_bytes 16 src_addr s0 = read_mem_bytes 16 src_addr s0
  rfl

/-- info: 'mem_automation_test' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in #print axioms mem_automation_test

We can now automate this away.

[bollu]

I now have the right theorems to hook into automation:

• mem_subset_refl+ mem_subset_trans to propagate subset information
• mem_separate'_of_mem_separate'_of_mem_subset' to produce disjointedness information from subset information.
• read_mem_bytes_write_mem_bytes_eq_read_mem_bytes_of_mem_separate': to establish reads of non-interfering writes
• read_mem_bytes_write_mem_bytes_eq_extract_LsB_of_mem_subset: to establish results of reads of interfering writes.

This gives us the core theorems we need to write automation on top of. Along with the refactor to use (base pointer + length), life should be good from now ^^

[bollu]

@alexkeizer @shigoel A careful review of the description of the proposed automation would be much appreciated. All previous comments addressed, files are ready for review!

[bollu]

theorem sha512_block_armv8_prelude_sym_ctx_access (s0 : ArmState)
 ...
  :
  read_mem_bytes 16 (ctx_addr s0 + 48#64) s0 = SHA2.h0_512.toBitVec.extractLsBytes 48 16 := by
  simp [memory_rules]
  rw [read_mem_bytes_eq_extractLsBytes_of_subset_of_read_mem_bytes
    (hread := h_s0_ctx)]
  -- ⊢ SHA2.h0_512.toBitVec.extractLsBytes ((ctx_addr s0 + 48#64).toNat - (ctx_addr s0).toNat) 16 =
  --  SHA2.h0_512.toBitVec.extractLsBytes 48 16
  congr
  · -- ⊢ (ctx_addr s0 + 48#64).toNat - (ctx_addr s0).toNat = 48
    -- this will be done by the user, maybe we can do this as well as part of address normalizatio.
    bv_omega'
  · -- this part should be done by the tactic to establish:
    -- mem_subset' (ctx_addr s0 + 48#64) 16 (ctx_addr s0) (63 + 1)
    constructor
    · bv_omega'
    · assumption
    · bv_omega'
    · bv_omega'

In the proof script, we can see that we are able to simplify the read of known read pattern. The tactic should automatically establish mem_subset', which I'll be automating now.

[bollu]

@shigoel all comments addressed!

[bollu]

Aha, indeed, thanks for the -1 catch, I just pulled it in.

[bollu]

@shigoel I pushed a new version that fixes all the bounds.