search

leanprover / LNSym

Armv8 Native Code Symbolic Simulator in Lean
Apache License 2.0
51 stars 13 forks source link

feat: Proof automation for simplifying reads of known reads [3/3] #90

Closed bollu closed 3 weeks ago

bollu commented 1 month ago

This PR is stacked on top of #56

The first example extracted by Shilpi tries to simplify a read of a known read. 

theorem sha512_block_armv8_prelude_sym_ctx_access
  ...
  (h_s0_ctx : read_mem_bytes 64 (ctx_addr s0) s0 = SHA2.h0_512.toBitVec)
  :
  read_mem_bytes 16 (ctx_addr s0 + 48#64) s0 = xxxx := by
  ....

here, we can exploit the fact that we know s0.mem[ctx_addr...ctx_addr+64] = SHA2.h0_512.toBitVec to compute the value of s0.mem[ctx_addr+48...ctx_addr+(48+16)]. To perform this, we will first show that the read in the goal state is a subset of the hypothesis, and then exploit to simplify the read away.

shigoel commented 3 weeks ago

LGTM in general, teeny tiny comments.

bollu commented 3 weeks ago

@shigoel all comments addressed :) Please hit merge!

bollu commented 3 weeks ago

@shigoel resolved for realsies!