SHA512 symbolic simulation effort that leverages presimplified block …

…semantics

Arm/Memory/Common.lean

@@ -255,7 +255,7 @@ def TacticM.withTraceNode'
     [MonadRef m]
     [AddMessageContext m]
     [MonadOptions m]
-    [always : MonadAlwaysExcept ε m]
+    [_always : MonadAlwaysExcept ε m]
     [MonadLiftT BaseIO m]
     (header : MessageData) (k : m α)
     (collapsed : Bool := false)
@@ -272,7 +272,7 @@ def TacticM.traceLargeMsg
     [MonadRef m]
     [AddMessageContext m]
     [MonadOptions m]
-    [always : MonadAlwaysExcept ε m]
+    [_always : MonadAlwaysExcept ε m]
     [MonadLiftT BaseIO m]
     (header : MessageData)
     (msg : MessageData) : m Unit := do

Proofs/AES-GCM/GCMInitV8Sym.lean

@@ -30,7 +30,7 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState)
     (h_s0_pc : read_pc s0 = gcm_init_v8_program.min)
     (h_s0_sp_aligned : CheckSPAlignment s0)
     (h_run : sf = run gcm_init_v8_program.length s0)
-    (h_mem : Memory.Region.pairwiseSeparate
+    (_h_mem : Memory.Region.pairwiseSeparate
       [ ⟨(H_addr s0), 128⟩,
         ⟨(Htable_addr s0), 2048⟩ ])
     : -- effects

Proofs/Experiments/Max/MaxTandem.lean

@@ -637,7 +637,7 @@ theorem partial_correctness :
 
       -- 2/15
       name h_s1_run : s2 := run 1 s1
-      obtain ⟨h_s2_cut, h_s2_pc, h_s2_err, h_s2_program, h_s2_read_sp_8, h_s2_read_sp_12, h_s2_x0, h_s2_x1, h_s2_sp, h_s2_sp_aligned⟩ :=
+      obtain ⟨h_s2_cut, h_s2_pc, h_s2_err, h_s2_program, _h_s2_read_sp_8, h_s2_read_sp_12, h_s2_x0, h_s2_x1, h_s2_sp, h_s2_sp_aligned⟩ :=
         program.stepi_0x898_cut s1 s2 h_s1_program h_s1_pc h_s1_err h_s1_sp_aligned (by mem_omega) h_s1_run.symm
       rw [Correctness.snd_cassert_of_not_cut h_s2_cut]; -- try rw [Correctness.snd_cassert_of_cut h_cut];
       simp [show Sys.next s2 = run 1 s2 by rfl]

Proofs/Experiments/MemoryAliasing.lean

@@ -333,8 +333,8 @@ theorem mem_automation_test_2_conv
 
 theorem mem_automation_test_2_conv_focus
   (h_n0 : n0 ≠ 0)
-  (h_no_wrap_src_region : mem_legal' src_addr (n0 <<< 4))
-  (h_no_wrap_dest_region : mem_legal' dest_addr (n0 <<< 4))
+  (_h_no_wrap_src_region : mem_legal' src_addr (n0 <<< 4))
+  (_h_no_wrap_dest_region : mem_legal' dest_addr (n0 <<< 4))
   (h_s0_src_dest_separate :
     mem_separate' src_addr  (n0 <<< 4)
                   dest_addr (n0 <<< 4)) :
@@ -369,7 +369,7 @@ theorem mem_automation_test_3
 interleaved write `[ignore_addr..ignore_addr+ignore_n)`
 -/
 theorem mem_automation_test_3_conv
-  (h_no_wrap_src_region : mem_legal' src_addr 16)
+  (_h_no_wrap_src_region : mem_legal' src_addr 16)
   (h_s0_src_ignore_disjoint :
     mem_separate' src_addr  16
                   ignore_addr ignore_n) :
@@ -645,7 +645,7 @@ namespace SimpMemConv
 
 #time
 theorem irrelvant_hyps
-  (h_irrelevant: mem_subset' src_addr 10 src_addr 30)
+  (_h_irrelevant: mem_subset' src_addr 10 src_addr 30)
   (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

Proofs/SHA512/SHA512_block_armv8_rules.lean

@@ -58,6 +58,17 @@ private theorem extractLsb'_high_64_from_setWidth_128_or (x y : BitVec 64) :
   extractLsb' 64 64 ((setWidth 128 x) ||| (setWidth 128 y <<< 64)) = y := by
   bv_decide
 
+theorem sha512h_rule (a0 a1 b0 b1 c0 c1 d0 d1 e0 e1 : BitVec 64) :
+  (DPSFP.sha512h (a1 ++ a0) (b1 ++ b0) (c1 + (d1 + e1) ++ (c0 + (d0 + e0)))) =
+  let hi64_spec := compression_update_t1 b1 a0 a1 c1 d1 e1
+  let lo64_spec := compression_update_t1 (b0 + hi64_spec) b1 a0 c0 d0 e0
+  hi64_spec ++ lo64_spec
+  := by
+  simp [DPSFP.sha512h, compression_update_t1]
+  repeat rw [extractLsb'_append_left, extractLsb'_append_right]
+  ac_rfl
+  done
+
 -- This lemma takes ~5min with bv_decide and the generated LRAT
 -- file is ~207MB. It turns out this this theorem is not a good candidate for
 -- proof via bit-blasting. As Bruno Dutertre says:
@@ -118,19 +129,32 @@ theorem binary_vector_op_aux_add_128_simp (x y result : BitVec 128) :
   bv_decide
   done
 
-/-
-DPSFP.sha512h2 (r (StateField.SFP 0x1#5) s) (r (StateField.SFP 0x0#5) s)
-    (DPSFP.sha512h (extractLsb' 64 128 (r (StateField.SFP 0x3#5) s ++ r (StateField.SFP 0x2#5) s))
-      (extractLsb' 64 128 (r (StateField.SFP 0x2#5) s ++ r (StateField.SFP 0x1#5) s))
-      (DPSFP.binary_vector_op_aux 0 2 64 BitVec.add (r (StateField.SFP 0x3#5) s)
-        (extractLsb' 64 128
-          (DPSFP.binary_vector_op_aux 0 2 64 BitVec.add (Memory.read_bytes 16 (r (StateField.GPR 0x3#5) s) s.mem)
-              (r (StateField.SFP 0x10#5) s) 0x0#128 ++
-            DPSFP.binary_vector_op_aux 0 2 64 BitVec.add (Memory.read_bytes 16 (r (StateField.GPR 0x3#5) s) s.mem)
-              (r (StateField.SFP 0x10#5) s) 0x0#128))
-        0x0#128))
--/
+theorem sha512h_and_sha512h2_rule :
+  let x0 := extractLsb'  0 64 x
+  let y0 := extractLsb'  0 64 y
+  let y1 := extractLsb' 64 64 y
+  let hi64_spec_1 := compression_update_t1 b1 a0 a1 c1 d1 e1
+  let hi64_spec_2 := compression_update_t2 y0 x0 y1
+  let lo64_spec_1 := compression_update_t1 (b0 + hi64_spec_1) b1 a0 c0 d0 e0
+  let lo64_spec_2 := compression_update_t2 (hi64_spec_2 + hi64_spec_1) y0 y1
+  (DPSFP.sha512h2 x y
+      (DPSFP.sha512h (a1 ++ a0) (b1 ++ b0)
+                     (c1 + (d1 + e1) ++ (c0 + (d0 + e0))))) =
+  (hi64_spec_1 + hi64_spec_2) ++ (lo64_spec_1 + lo64_spec_2) := by
+  simp [sha512h2_rule, sha512h]
+  generalize extractLsb'  0 64 x = x0
+  -- generalize extractLsb' 64 64 x = x1
+  generalize extractLsb'  0 64 y = y0
+  generalize extractLsb' 64 64 y = y1
+  repeat rw [BitVec.extractLsb'_append_left, BitVec.extractLsb'_append_right]
+  simp [compression_update_t1]
+  generalize compression_update_t2 y0 x0 y1 = p0
+  generalize ch b1 a0 a1 = p1
+  generalize sigma_big_1 b1 = p2
+  ac_rfl
+  done
 
+/-
 theorem sha512h_and_sha512h2_rule_1 :
   let elements := 2
   let esize := 64
@@ -172,6 +196,7 @@ theorem sha512h_and_sha512h2_rule_1 :
   generalize extractLsb' 64 64 y = y1
   rw [BitVec.extractLsb'_append_left, BitVec.extractLsb'_append_right]
   ac_rfl
+-/
 
 -- set_option maxHeartbeats 0 in
 -- This lemma takes 2min with bv_decide and the generated LRAT

Specs/AESV8.lean

@@ -111,7 +111,7 @@ def AESHWCtr32EncryptBlocks_helper {Param : AESArm.KBR} (in_blocks : BitVec m)
   if i >= len then acc
   else
     let lo := m - (i + 1) * 128
-    let hi := lo + 127
+    let _hi := lo + 127
     let curr_block : BitVec 128 := BitVec.extractLsb' lo 128 in_blocks
     have h4 : 128 = Param.block_size := by
       cases h3

Specs/SHA512.lean

@@ -165,6 +165,25 @@ def processBlocks (message_schedule : List (BitVec 64) → List (BitVec 64))
     let hash' := add_hash hash work_vars
     processBlocks message_schedule j hash' k rest
 
+def compression_alt (i max : Nat) (wv : Hash) (k m : List (BitVec 64)) : Hash :=
+  if i < max then
+    let ki := List.get! k i
+    let wi := message_schedule_word i m
+    let wv' := compression_update wv ki wi
+    compression_alt (i + 1) max wv' k m
+  else
+    wv
+  termination_by max - i
+
+def processBlocks_alt (j : Nat) (hash : Hash)
+  (k : List (BitVec 64)) (ms : List (List (BitVec 64))) : Hash :=
+  match ms with
+  | [] => hash
+  | m :: rest =>
+    let work_vars := compression_alt 0 j hash k m
+    let hash' := add_hash hash work_vars
+    processBlocks_alt j hash' k rest
+
 def j_512 : Nat := 80
 
 def h0_512 : Hash :=

Tactics/Attr.lean

@@ -16,6 +16,11 @@ initialize
   -- theorem's conclusion
   registerTraceClass `Tactic.prune_updates.answer
 
+  registerOption `Tactic.prune_updates.only_answer {
+  defValue := false
+  descr := "Print the pruned updates and exit"
+  }
+
   registerOption `Tactic.prune_updates.validate {
     defValue := false
     descr := "enable/disable type-checking of internal state during execution \

Tactics/PruneUpdates.lean

@@ -285,11 +285,10 @@ def toContextExpr (s : ToArmExpr.Context) : MetaM Lean.Expr :=
 abbrev mkAuxDecl := Lean.Elab.Tactic.BVDecide.Frontend.mkAuxDecl
 
 -- (FIXME) Better formatting; change into code action, etc.!
-def toArmMessageData (e : Expr) (s : ToArmExpr.Context) : MessageData :=
-  let curr_state := s.stateVars[e.curr_state]!
-  let prev_state := s.stateVars[e.prev_state]!
-  let writes := go e.writes prev_state s 0
-  m!"{curr_state} = {writes}"
+def toArmMessageData (prev_state : StateVar) (updates : Updates) (s : ToArmExpr.Context) : MessageData :=
+  let prev_state := s.stateVars[prev_state]!
+  let writes := go updates prev_state s 0
+  m!"{writes}"
   where go (us : Updates) (prev_state : Lean.Expr)
            (s : ToArmExpr.Context) (paren_count : Nat) :=
     match us with
@@ -416,6 +415,10 @@ def ArmExprPruned? (refl_proof_name : Name) (e : Lean.Expr) :
   let_expr Eq _ lhs rhs := e | return none
   let ((lhs_writes, lhs_s0), state) ←
     ToArmExpr.run (ToArmExpr.toArmUpdatesAndStateVar lhs []) {}
+  let ctx := ToArmExpr.mkContextFromState state
+  trace[Tactic.prune_updates.answer] "Pruned Updates: {toArmMessageData lhs_s0 lhs_writes.prune ctx}"
+  if ←(getBoolOption `Tactic.prune_updates.only_answer) then
+    return none
   let ((rhs_writes, rhs_s0), state) ←
     ToArmExpr.run (ToArmExpr.toArmUpdatesAndStateVar rhs []) state
   trace[Tactic.prune_updates] "LHS writes: {lhs_writes}"
@@ -429,7 +432,6 @@ def ArmExprPruned? (refl_proof_name : Name) (e : Lean.Expr) :
   --  let arm_expr_pruned := lhs_arm_expr.prune
   --  trace[Tactic.prune_updates] "Pruned Arm Expr: {arm_expr_pruned}"
   --
-  let ctx := ToArmExpr.mkContextFromState state
   withAbstractAtoms ctx fun ctx' => do
     if lhs_s0 = rhs_s0 then
       return some (← ArmExprBuildProofTerm ctx'
@@ -504,12 +506,80 @@ fun {s1} {x0} {x1} {s0} h_s1 =>
 #guard_msgs in
 #print example1
 
+/-
+
+set_option trace.Tactic.prune_updates.answer true in
+theorem timeout_example (test : Bool)
+  (h_step : s' = w (StateField.GPR 0x1#5)
+                  (if (AddWithCarry (r (StateField.GPR 0x2#5) s) 0xffffffffffffffff#64 0x1#1).snd.z = 0#1 then
+                   (AddWithCarry (r (StateField.GPR 0x2#5) s) 0xffffffffffffffff#64 0x1#1).fst
+                  else
+                   (AddWithCarry (r (StateField.GPR 0x2#5) s) 0#64 0x1#1).fst)
+                  (w StateField.PC 0x126520#64
+                    (w (StateField.SFP 0x1d#5) (r (StateField.SFP 0x3#5) s) s))) :
+  s' =  (w .PC (1205536#64)
+              (w (.GPR 0x01#5)
+                  (if (AddWithCarry (r (StateField.GPR 0x2#5) s) 0xffffffffffffffff#64 0x1#1).snd.z = 0#1 then
+                    (AddWithCarry (r (StateField.GPR 0x2#5) s) 0xffffffffffffffff#64 0x1#1).fst
+                  else
+                    (AddWithCarry (r (StateField.GPR 0x2#5) s) 0#64 0x1#1).fst)
+                  (w (.SFP 0x1d#5) (r (StateField.SFP 3#5) s)  s)))  := by
+  rw [h_step]
+  prune_updates
+
+-- set_option allowUnsafeReducibility true
+seal AddWithCarry
+-- seal Prod.snd
+-- seal PState.z
+-- seal PFlag.Z
+
 #time
+-- set_option trace.Tactic.prune_updates.answer true in
 set_option diagnostics true in
 set_option diagnostics.threshold 5 in
-set_option trace.Tactic.prune_updates true in
+-- set_option trace.Tactic.prune_updates true in
 set_option maxRecDepth 2000 in
-theorem timeout_example
+theorem timeout_example1
+  (h_step : s' = w (StateField.FLAG PFlag.Z)
+                   (AddWithCarry (r (StateField.GPR 0x2#5) s) 0xff#64 0x1#1).snd.z
+                  (w StateField.PC 0x126520#64
+                    (w (StateField.SFP 0x1d#5) (r (StateField.SFP 0x3#5) s) s))) :
+  s' = (w .PC (1205536#64)  (w (.SFP 0x1d#5) (r (StateField.SFP 3#5)
+      s)  (w (.FLAG PFlag.Z) (AddWithCarry (r (StateField.GPR 0x2#5) s) 0xff#64 0x1#1).snd.z s)))  := by
+  rw [h_step]
+  prune_updates
+
+
+seal AddWithCarry
+set_option allowUnsafeReducibility true in
+seal Prod.snd
+
+-- #time
+-- set_option diagnostics true in
+-- set_option diagnostics.threshold 5 in
+-- -- set_option trace.Tactic.prune_updates true in
+-- set_option trace.Tactic.prune_updates.answer true in
+-- set_option maxRecDepth 2000 in
+-- theorem timeout_example2
+--   (h_step : s' = w (StateField.GPR 0x1#5)
+--     (if ¬(AddWithCarry (r (StateField.GPR 0x2#5) s) 0xffffffffffffffff#64 0x1#1).snd.z = 0x1#1 then
+--       r (StateField.GPR 0x1#5) s
+--     else r (StateField.GPR 0x1#5) s - 0x80#64)
+--     (w StateField.PC 0x126520#64
+--       (w (StateField.SFP 0x1d#5) (r (StateField.SFP 0x3#5) s) s))) :
+--   s' =  (w .PC (1205536#64)  (w (.GPR 0x01#5) (if
+--         ¬(AddWithCarry (r (StateField.GPR 2#5) s) 0xffffffffffffffff#64 1#1).snd.z = 1#1 then r (StateField.GPR 1#5) s
+--     else r (StateField.GPR 1#5) s - 128#64)  (w (.SFP 0x1d#5) (r (StateField.SFP 3#5) s)  s)))  := by
+--   rw [h_step]
+--   prune_updates
+
+/-
+#time
+-- set_option diagnostics true in
+-- set_option diagnostics.threshold 5 in
+-- set_option trace.Tactic.prune_updates true in
+-- set_option maxRecDepth 2000 in
+theorem timeout_example2
   (h_step : s' = w (StateField.GPR 0x1#5)
     (if ¬(AddWithCarry (r (StateField.GPR 0x2#5) s) 0xffff#64 0x1#1).snd.z = 0x1#1 then
       r (StateField.GPR 0x1#5) s
@@ -555,6 +625,6 @@ theorem timeout_example
                       (w (.FLAG PFlag.V) ((AddWithCarry (r (StateField.GPR 2#5) s) 0x0#64 1#1).snd.v) s)))))))))))))) := by
     rw [h_step]
     prune_updates
-
-
+-/
+-/
 end Tests

Tactics/SymBlock.lean

@@ -168,8 +168,7 @@ elab "sym_block" n:num
         return (mkNatLit size))
       let size_terms ← size_exprs.mapM (fun e => do
           let some val ← Lean.Meta.getNatValue? e | throwError ""
-          return val)
-      dbg_trace s!"size_terms: {size_terms}"
+          return val)      
       pure size_terms.toList
   |  _ =>
       -- (FIXME)

Tests/SHA2/SHA512SpecTest.lean

@@ -59,6 +59,10 @@ def ans_one_blk_mem : IO SHA2.Hash := do
 example : SHA2.sha512 ms_mem ms_one_block = expected := by
   native_decide
 
+-- #time
+-- example : SHA2.processBlocks_alt SHA2.j_512 SHA2.h0_512 SHA2.k_512 ms_one_block =
+--           expected := by native_decide
+
 -- Lazy version
 def ms_lazy := (SHA2.message_schedule_lazy SHA2.j_512)