Move common theories to venom/ for shared use across passes

venom/passes/phi_elimination/execEquivScript.sml → venom/execEquivScript.sml

@@ -113,6 +113,28 @@ Proof
     (* PHI case - prev_bb is same in both states *)
     TRY (`s1.vs_prev_bb = s2.vs_prev_bb` by fs[state_equiv_def] >> gvs[] >>
          irule update_var_state_equiv >> simp[] >> NO_TAC) >>
+    (* MSIZE case - memory is same in both states *)
+    TRY (`s1.vs_memory = s2.vs_memory` by fs[state_equiv_def] >> gvs[] >>
+         irule update_var_state_equiv >> simp[] >> NO_TAC) >>
+    (* Environment opcodes - contexts are same in both states *)
+    TRY (`s1.vs_call_ctx = s2.vs_call_ctx` by fs[state_equiv_def] >> gvs[] >>
+         irule update_var_state_equiv >> simp[] >> NO_TAC) >>
+    TRY (`s1.vs_tx_ctx = s2.vs_tx_ctx` by fs[state_equiv_def] >> gvs[] >>
+         irule update_var_state_equiv >> simp[] >> NO_TAC) >>
+    TRY (`s1.vs_block_ctx = s2.vs_block_ctx` by fs[state_equiv_def] >> gvs[] >>
+         irule update_var_state_equiv >> simp[] >> NO_TAC) >>
+    TRY (`s1.vs_accounts = s2.vs_accounts /\ s1.vs_call_ctx = s2.vs_call_ctx`
+         by fs[state_equiv_def] >> gvs[] >>
+         irule update_var_state_equiv >> simp[] >> NO_TAC) >>
+    TRY (`s1.vs_returndata = s2.vs_returndata` by fs[state_equiv_def] >> gvs[] >>
+         irule update_var_state_equiv >> simp[] >> NO_TAC) >>
+    (* Memory write operations with expansion *)
+    TRY (`s1.vs_call_ctx = s2.vs_call_ctx /\ s1.vs_memory = s2.vs_memory`
+         by fs[state_equiv_def] >> gvs[] >>
+         irule write_memory_with_expansion_state_equiv >> simp[] >> NO_TAC) >>
+    TRY (`s1.vs_returndata = s2.vs_returndata /\ s1.vs_memory = s2.vs_memory`
+         by fs[state_equiv_def] >> gvs[] >>
+         irule write_memory_with_expansion_state_equiv >> simp[] >> NO_TAC) >>
     simp[state_equiv_refl]
   ]
 QED
@@ -272,6 +294,14 @@ Proof
   TRY (
     simp[result_equiv_def] >> irule revert_state_state_equiv >> simp[] >> NO_TAC
   ) >>
+  (* ASSERT and ASSERT_UNREACHABLE *)
+  TRY (
+    drule eval_operand_state_equiv >> strip_tac >>
+    rpt CASE_TAC >> gvs[result_equiv_def] >>
+    TRY (irule halt_state_state_equiv >> simp[] >> NO_TAC) >>
+    TRY (irule revert_state_state_equiv >> simp[] >> NO_TAC) >>
+    simp[state_equiv_refl] >> NO_TAC
+  ) >>
   (* PHI *)
   TRY (
     `s1.vs_prev_bb = s2.vs_prev_bb` by fs[state_equiv_def] >>
@@ -290,6 +320,70 @@ Proof
     Cases_on `eval_operand h s1` >> simp[result_equiv_def] >>
     irule update_var_state_equiv >> simp[] >> NO_TAC
   ) >>
+  (* MSIZE - memory is same in both states *)
+  TRY (
+    `s1.vs_memory = s2.vs_memory` by fs[state_equiv_def] >>
+    rpt CASE_TAC >> gvs[result_equiv_def] >>
+    irule update_var_state_equiv >> simp[] >> NO_TAC
+  ) >>
+  (* Environment opcodes - contexts are same in both states *)
+  TRY (
+    `s1.vs_call_ctx = s2.vs_call_ctx` by fs[state_equiv_def] >>
+    rpt CASE_TAC >> gvs[result_equiv_def] >>
+    irule update_var_state_equiv >> simp[] >> NO_TAC
+  ) >>
+  TRY (
+    `s1.vs_tx_ctx = s2.vs_tx_ctx` by fs[state_equiv_def] >>
+    rpt CASE_TAC >> gvs[result_equiv_def] >>
+    irule update_var_state_equiv >> simp[] >> NO_TAC
+  ) >>
+  TRY (
+    `s1.vs_block_ctx = s2.vs_block_ctx` by fs[state_equiv_def] >>
+    rpt CASE_TAC >> gvs[result_equiv_def] >>
+    irule update_var_state_equiv >> simp[] >> NO_TAC
+  ) >>
+  (* BLOCKHASH - needs eval_operand *)
+  TRY (
+    `s1.vs_block_ctx = s2.vs_block_ctx` by fs[state_equiv_def] >>
+    drule eval_operand_state_equiv >> strip_tac >>
+    rpt CASE_TAC >> gvs[result_equiv_def] >>
+    irule update_var_state_equiv >> simp[] >> NO_TAC
+  ) >>
+  TRY (
+    `s1.vs_accounts = s2.vs_accounts /\ s1.vs_call_ctx = s2.vs_call_ctx`
+    by fs[state_equiv_def] >>
+    drule eval_operand_state_equiv >> strip_tac >>
+    rpt CASE_TAC >> gvs[result_equiv_def] >>
+    irule update_var_state_equiv >> simp[] >> NO_TAC
+  ) >>
+  TRY (
+    `s1.vs_returndata = s2.vs_returndata` by fs[state_equiv_def] >>
+    rpt CASE_TAC >> gvs[result_equiv_def] >>
+    irule update_var_state_equiv >> simp[] >> NO_TAC
+  ) >>
+  (* SHA3 - needs memory and eval_operand *)
+  TRY (
+    `s1.vs_memory = s2.vs_memory` by fs[state_equiv_def] >>
+    drule eval_operand_state_equiv >> strip_tac >>
+    rpt CASE_TAC >> gvs[result_equiv_def] >>
+    irule update_var_state_equiv >> simp[] >> NO_TAC
+  ) >>
+  (* Memory write operations with expansion *)
+  TRY (
+    `s1.vs_call_ctx = s2.vs_call_ctx /\ s1.vs_memory = s2.vs_memory`
+    by fs[state_equiv_def] >>
+    drule eval_operand_state_equiv >> strip_tac >>
+    rpt CASE_TAC >> gvs[result_equiv_def] >>
+    irule write_memory_with_expansion_state_equiv >> simp[] >> NO_TAC
+  ) >>
+  TRY (
+    `s1.vs_returndata = s2.vs_returndata /\ s1.vs_memory = s2.vs_memory`
+    by fs[state_equiv_def] >>
+    drule eval_operand_state_equiv >> strip_tac >>
+    rpt CASE_TAC >> gvs[result_equiv_def] >>
+    TRY (irule revert_state_state_equiv >> simp[] >> NO_TAC) >>
+    irule write_memory_with_expansion_state_equiv >> simp[] >> NO_TAC
+  ) >>
   (* NOP *)
   simp[result_equiv_def, state_equiv_refl]
 QED

venom/passes/phi_elimination/phiBlockScript.sml

@@ -217,7 +217,7 @@ Proof
   Cases_on `inst.inst_opcode` >> simp[is_terminator_def] >>
   simp[exec_binop_def, exec_unop_def, exec_modop_def] >>
   strip_tac >> gvs[AllCaseEqs()] >>
-  gvs[update_var_def, mstore_def, sstore_def, tstore_def]
+  gvs[update_var_def, mstore_def, sstore_def, tstore_def, write_memory_with_expansion_def]
 QED
 
 (* Helper: step_in_block preserves vs_prev_bb for non-terminator steps *)

venom/passes/revert_to_assert/Holmakefile

@@ -1,3 +1,3 @@
 # Revert-to-assert pass correctness proof
-# Includes venom semantics, verifereum theories, and state equivalence from phi_elimination
-INCLUDES = $(VFMDIR)/util $(VFMDIR)/spec ../.. ../phi_elimination
+# Includes venom semantics and verifereum theories
+INCLUDES = $(VFMDIR)/util $(VFMDIR)/spec ../..

venom/passes/revert_to_assert/revertAssertPropsScript.sml

@@ -33,40 +33,14 @@
 
 Theory revertAssertProps
 Ancestors
-  revertAssertDefs stateEquiv
+  revertAssertDefs stateEquiv venomSemProps
 
 (* ==========================================================================
-   bool_to_word Properties
+   NOTE: bool_to_word properties and basic instruction behavior lemmas
+   (step_iszero_value, step_assert_behavior, step_revert_always_reverts,
+   step_jnz_behavior, step_jmp_behavior) are now in venomSemPropsTheory.
    ========================================================================== *)
 
-(* WHY THIS IS TRUE: By definition, bool_to_word T = 1w, bool_to_word F = 0w.
-   So bool_to_word b = 0w iff b = F iff ~b. *)
-Theorem bool_to_word_eq_0w:
-  !b. (bool_to_word b = 0w) <=> ~b
-Proof
-  cheat
-QED
-
-(* WHY THIS IS TRUE: Contrapositive of above. bool_to_word b <> 0w iff b = T. *)
-Theorem bool_to_word_neq_0w:
-  !b. (bool_to_word b <> 0w) <=> b
-Proof
-  cheat
-QED
-
-(* WHY THIS IS TRUE: Direct evaluation of bool_to_word on T and F. *)
-Theorem bool_to_word_T[simp]:
-  bool_to_word T = 1w
-Proof
-  cheat
-QED
-
-Theorem bool_to_word_F[simp]:
-  bool_to_word F = 0w
-Proof
-  cheat
-QED
-
 (* ==========================================================================
    Operand Evaluation with Variable Updates
    ========================================================================== *)
@@ -96,39 +70,10 @@ Proof
 QED
 
 (* ==========================================================================
-   ISZERO Instruction Behavior
+   ASSERT Instruction Behavior - Special Cases
+   (Base lemma step_assert_behavior is in venomSemPropsTheory)
    ========================================================================== *)
 
-(* WHY THIS IS TRUE: By step_inst_def, ISZERO uses exec_unop with
-   (\x. bool_to_word (x = 0w)). exec_unop evaluates the single operand,
-   applies the function, and updates the output variable. *)
-Theorem step_iszero_value:
-  !s cond cond_op out id.
-    eval_operand cond_op s = SOME cond ==>
-    step_inst <| inst_id := id; inst_opcode := ISZERO;
-                 inst_operands := [cond_op]; inst_outputs := [out] |> s =
-    OK (update_var out (bool_to_word (cond = 0w)) s)
-Proof
-  cheat
-QED
-
-(* ==========================================================================
-   ASSERT Instruction Behavior
-   ========================================================================== *)
-
-(* WHY THIS IS TRUE: By step_inst_def, ASSERT evaluates its operand.
-   If cond = 0w, it returns Revert (revert_state s).
-   If cond <> 0w, it returns OK s. *)
-Theorem step_assert_behavior:
-  !s cond cond_op id.
-    eval_operand cond_op s = SOME cond ==>
-    step_inst <| inst_id := id; inst_opcode := ASSERT;
-                 inst_operands := [cond_op]; inst_outputs := [] |> s =
-    if cond = 0w then Revert (revert_state s) else OK s
-Proof
-  cheat
-QED
-
 (* WHY THIS IS TRUE: Special case of step_assert_behavior with cond = 0w. *)
 Theorem step_assert_zero_reverts:
   !s cond_op id.
@@ -152,38 +97,10 @@ Proof
 QED
 
 (* ==========================================================================
-   REVERT Instruction Behavior
+   JNZ Instruction Behavior - Special Cases
+   (Base lemma step_jnz_behavior is in venomSemPropsTheory)
    ========================================================================== *)
 
-(* WHY THIS IS TRUE: By step_inst_def, REVERT unconditionally returns
-   Revert (revert_state s) regardless of operands. *)
-Theorem step_revert_always_reverts:
-  !s id ops.
-    step_inst <| inst_id := id; inst_opcode := REVERT;
-                 inst_operands := ops; inst_outputs := [] |> s =
-    Revert (revert_state s)
-Proof
-  cheat
-QED
-
-(* ==========================================================================
-   JNZ Instruction Behavior
-   ========================================================================== *)
-
-(* WHY THIS IS TRUE: By step_inst_def, JNZ evaluates the condition.
-   If cond <> 0w, it jumps to if_nonzero; else to if_zero. *)
-Theorem step_jnz_behavior:
-  !s cond cond_op if_nonzero if_zero id.
-    eval_operand cond_op s = SOME cond ==>
-    step_inst <| inst_id := id; inst_opcode := JNZ;
-                 inst_operands := [cond_op; Label if_nonzero; Label if_zero];
-                 inst_outputs := [] |> s =
-    if cond <> 0w then OK (jump_to if_nonzero s)
-    else OK (jump_to if_zero s)
-Proof
-  cheat
-QED
-
 (* WHY THIS IS TRUE: Special case when cond <> 0w. *)
 Theorem step_jnz_nonzero_jumps:
   !s cond cond_op if_nonzero if_zero id.
@@ -208,22 +125,9 @@ Proof
   cheat
 QED
 
-(* ==========================================================================
-   JMP Instruction Behavior
-   ========================================================================== *)
-
-(* WHY THIS IS TRUE: By step_inst_def, JMP unconditionally jumps to the label. *)
-Theorem step_jmp_behavior:
-  !s lbl id.
-    step_inst <| inst_id := id; inst_opcode := JMP;
-                 inst_operands := [Label lbl]; inst_outputs := [] |> s =
-    OK (jump_to lbl s)
-Proof
-  cheat
-QED
-
 (* ==========================================================================
    Simple Revert Block Execution
+   (step_jmp_behavior is in venomSemPropsTheory)
    ========================================================================== *)
 
 (* WHY THIS IS TRUE: A block with only [revert 0 0] will:

venom/passes/phi_elimination/stateEquivScript.sml → venom/stateEquivScript.sml

@@ -52,7 +52,12 @@ Definition state_equiv_def:
     s1.vs_inst_idx = s2.vs_inst_idx /\
     s1.vs_prev_bb = s2.vs_prev_bb /\
     s1.vs_halted = s2.vs_halted /\
-    s1.vs_reverted = s2.vs_reverted
+    s1.vs_reverted = s2.vs_reverted /\
+    s1.vs_returndata = s2.vs_returndata /\
+    s1.vs_accounts = s2.vs_accounts /\
+    s1.vs_call_ctx = s2.vs_call_ctx /\
+    s1.vs_tx_ctx = s2.vs_tx_ctx /\
+    s1.vs_block_ctx = s2.vs_block_ctx
 End
 
 (* ==========================================================================
@@ -192,6 +197,15 @@ Proof
   rw[state_equiv_def, var_equiv_def, mstore_def, lookup_var_def]
 QED
 
+Theorem write_memory_with_expansion_state_equiv:
+  !offset bytes s1 s2.
+    state_equiv s1 s2 ==>
+    state_equiv (write_memory_with_expansion offset bytes s1)
+                (write_memory_with_expansion offset bytes s2)
+Proof
+  rw[state_equiv_def, var_equiv_def, write_memory_with_expansion_def, lookup_var_def]
+QED
+
 Theorem sload_state_equiv:
   !key s1 s2.
     state_equiv s1 s2 ==>
@@ -247,4 +261,3 @@ Theorem revert_state_state_equiv:
 Proof
   rw[state_equiv_def, var_equiv_def, revert_state_def, lookup_var_def]
 QED
-