Add ASSERT_UNREACHABLE and environment opcode semantics

.github/workflows/build.yml

@@ -5,6 +5,7 @@ on:
   push:
     paths:
     - '**'
+  pull_request:
 
 jobs:
   build:

venom/Holmakefile

@@ -1,2 +1,3 @@
 # Include paths to verifereum theories (vfmTypes, vfmState, etc.)
-INCLUDES = $(VFMDIR)/util $(VFMDIR)/spec
+# Also include Keccak for SHA3 implementation
+INCLUDES = $(VFMDIR)/util $(VFMDIR)/spec $(HOLDIR)/examples/Crypto/Keccak

venom/venomSemScript.sml

@@ -7,7 +7,7 @@
 
 Theory venomSem
 Ancestors
-  venomState venomInst
+  venomState venomInst keccak
 
 (* --------------------------------------------------------------------------
    Effects System
@@ -334,6 +334,27 @@ Definition step_inst_def:
     | REVERT => Revert (revert_state s)
     | SINK => Halt (halt_state s)
 
+    (* Assertions *)
+    | ASSERT =>
+        (case inst.inst_operands of
+          [cond_op] =>
+            (case eval_operand cond_op s of
+              SOME cond =>
+                if cond = 0w then Revert (revert_state s)
+                else OK s
+            | NONE => Error "undefined operand")
+        | _ => Error "assert requires 1 operand")
+
+    | ASSERT_UNREACHABLE =>
+        (case inst.inst_operands of
+          [cond_op] =>
+            (case eval_operand cond_op s of
+              SOME cond =>
+                if cond <> 0w then Halt (halt_state s)
+                else OK s
+            | NONE => Error "undefined operand")
+        | _ => Error "assert_unreachable requires 1 operand")
+
     (* SSA - PHI node *)
     | PHI =>
         (case inst.inst_outputs of
@@ -361,6 +382,208 @@ Definition step_inst_def:
     (* NOP *)
     | NOP => OK s
 
+    (* Environment - Call context *)
+    | CALLER =>
+        (case inst.inst_outputs of
+          [out] => OK (update_var out (w2w s.vs_call_ctx.cc_caller) s)
+        | _ => Error "caller requires single output")
+
+    | ADDRESS =>
+        (case inst.inst_outputs of
+          [out] => OK (update_var out (w2w s.vs_call_ctx.cc_address) s)
+        | _ => Error "address requires single output")
+
+    | CALLVALUE =>
+        (case inst.inst_outputs of
+          [out] => OK (update_var out s.vs_call_ctx.cc_callvalue s)
+        | _ => Error "callvalue requires single output")
+
+    | GAS =>
+        (case inst.inst_outputs of
+          [out] => OK (update_var out (n2w s.vs_call_ctx.cc_gas) s)
+        | _ => Error "gas requires single output")
+
+    (* Environment - Transaction context *)
+    | ORIGIN =>
+        (case inst.inst_outputs of
+          [out] => OK (update_var out (w2w s.vs_tx_ctx.tc_origin) s)
+        | _ => Error "origin requires single output")
+
+    | GASPRICE =>
+        (case inst.inst_outputs of
+          [out] => OK (update_var out s.vs_tx_ctx.tc_gasprice s)
+        | _ => Error "gasprice requires single output")
+
+    | CHAINID =>
+        (case inst.inst_outputs of
+          [out] => OK (update_var out s.vs_tx_ctx.tc_chainid s)
+        | _ => Error "chainid requires single output")
+
+    (* Environment - Block context *)
+    | COINBASE =>
+        (case inst.inst_outputs of
+          [out] => OK (update_var out (w2w s.vs_block_ctx.bc_coinbase) s)
+        | _ => Error "coinbase requires single output")
+
+    | TIMESTAMP =>
+        (case inst.inst_outputs of
+          [out] => OK (update_var out s.vs_block_ctx.bc_timestamp s)
+        | _ => Error "timestamp requires single output")
+
+    | NUMBER =>
+        (case inst.inst_outputs of
+          [out] => OK (update_var out s.vs_block_ctx.bc_number s)
+        | _ => Error "number requires single output")
+
+    | PREVRANDAO =>
+        (case inst.inst_outputs of
+          [out] => OK (update_var out s.vs_block_ctx.bc_prevrandao s)
+        | _ => Error "prevrandao requires single output")
+
+    | GASLIMIT =>
+        (case inst.inst_outputs of
+          [out] => OK (update_var out s.vs_block_ctx.bc_gaslimit s)
+        | _ => Error "gaslimit requires single output")
+
+    | BASEFEE =>
+        (case inst.inst_outputs of
+          [out] => OK (update_var out s.vs_block_ctx.bc_basefee s)
+        | _ => Error "basefee requires single output")
+
+    | BLOBBASEFEE =>
+        (case inst.inst_outputs of
+          [out] => OK (update_var out s.vs_block_ctx.bc_blobbasefee s)
+        | _ => Error "blobbasefee requires single output")
+
+    | BLOCKHASH =>
+        (case inst.inst_operands of
+          [op1] =>
+            (case eval_operand op1 s of
+              SOME blocknum =>
+                (case inst.inst_outputs of
+                  [out] => OK (update_var out (s.vs_block_ctx.bc_blockhash (w2n blocknum)) s)
+                | _ => Error "blockhash requires single output")
+            | NONE => Error "undefined operand")
+        | _ => Error "blockhash requires 1 operand")
+
+    (* Environment - Balance *)
+    | BALANCE =>
+        (case inst.inst_operands of
+          [op1] =>
+            (case eval_operand op1 s of
+              SOME addr =>
+                (case inst.inst_outputs of
+                  [out] =>
+                    let acct = lookup_account (w2w addr) s.vs_accounts in
+                    OK (update_var out (n2w acct.balance) s)
+                | _ => Error "balance requires single output")
+            | NONE => Error "undefined operand")
+        | _ => Error "balance requires 1 operand")
+
+    | SELFBALANCE =>
+        (case inst.inst_outputs of
+          [out] =>
+            let acct = lookup_account s.vs_call_ctx.cc_address s.vs_accounts in
+            OK (update_var out (n2w acct.balance) s)
+        | _ => Error "selfbalance requires single output")
+
+    (* Calldata *)
+    | CALLDATASIZE =>
+        (case inst.inst_outputs of
+          [out] => OK (update_var out (n2w (LENGTH s.vs_call_ctx.cc_calldata)) s)
+        | _ => Error "calldatasize requires single output")
+
+    | CALLDATALOAD =>
+        (case inst.inst_operands of
+          [op1] =>
+            (case eval_operand op1 s of
+              SOME offset =>
+                (case inst.inst_outputs of
+                  [out] =>
+                    let data = s.vs_call_ctx.cc_calldata in
+                    let bytes = TAKE 32 (DROP (w2n offset) data ++ REPLICATE 32 0w) in
+                    OK (update_var out (word_of_bytes T (0w:bytes32) bytes) s)
+                | _ => Error "calldataload requires single output")
+            | NONE => Error "undefined operand")
+        | _ => Error "calldataload requires 1 operand")
+
+    | CALLDATACOPY =>
+        (case inst.inst_operands of
+          [op_size; op_offset; op_destOffset] =>
+            (case (eval_operand op_size s, eval_operand op_offset s, eval_operand op_destOffset s) of
+              (SOME size_val, SOME offset, SOME destOffset) =>
+                let data = s.vs_call_ctx.cc_calldata in
+                let size = w2n size_val in
+                let src_offset = w2n offset in
+                let bytes = TAKE size (DROP src_offset data ++ REPLICATE size 0w) in
+                OK (write_memory_with_expansion (w2n destOffset) bytes s)
+            | _ => Error "undefined operand")
+        | _ => Error "calldatacopy requires 3 operands")
+
+    (* Return data *)
+    | RETURNDATASIZE =>
+        (case inst.inst_outputs of
+          [out] => OK (update_var out (n2w (LENGTH s.vs_returndata)) s)
+        | _ => Error "returndatasize requires single output")
+
+    | RETURNDATACOPY =>
+        (case inst.inst_operands of
+          [op_size; op_offset; op_destOffset] =>
+            (case (eval_operand op_size s, eval_operand op_offset s, eval_operand op_destOffset s) of
+              (SOME size_val, SOME offset, SOME destOffset) =>
+                let size = w2n size_val in
+                let src_offset = w2n offset in
+                (* Check for out-of-bounds access *)
+                if src_offset + size > LENGTH s.vs_returndata then
+                  Revert (revert_state s)
+                else
+                  let bytes = TAKE size (DROP src_offset s.vs_returndata) in
+                  OK (write_memory_with_expansion (w2n destOffset) bytes s)
+            | _ => Error "undefined operand")
+        | _ => Error "returndatacopy requires 3 operands")
+
+    (* Memory size *)
+    | MSIZE =>
+        (case inst.inst_outputs of
+          [out] =>
+            (* MSIZE returns memory size rounded up to 32-byte words *)
+            let size = LENGTH s.vs_memory in
+            let words = (size + 31) DIV 32 in
+            OK (update_var out (n2w (words * 32)) s)
+        | _ => Error "msize requires single output")
+
+    (* Hashing - using Keccak256 like EVM *)
+    | SHA3 =>
+        (case inst.inst_operands of
+          [op_size; op_offset] =>
+            (case (eval_operand op_size s, eval_operand op_offset s) of
+              (SOME size_val, SOME offset) =>
+                (case inst.inst_outputs of
+                  [out] =>
+                    let size = w2n size_val in
+                    let off = w2n offset in
+                    let data = TAKE size (DROP off s.vs_memory ++ REPLICATE size 0w) in
+                    let hash = word_of_bytes T (0w:bytes32) (Keccak_256_w64 data) in
+                    OK (update_var out hash s)
+                | _ => Error "sha3 requires single output")
+            | _ => Error "undefined operand")
+        | _ => Error "sha3 requires 2 operands")
+
+    | SHA3_64 =>
+        (* SHA3_64 is a Vyper optimization: hash exactly 64 bytes (two words) *)
+        (case inst.inst_operands of
+          [op2; op1] =>
+            (case (eval_operand op1 s, eval_operand op2 s) of
+              (SOME v1, SOME v2) =>
+                (case inst.inst_outputs of
+                  [out] =>
+                    let data = word_to_bytes v1 T ++ word_to_bytes v2 T in
+                    let hash = word_of_bytes T (0w:bytes32) (Keccak_256_w64 data) in
+                    OK (update_var out hash s)
+                | _ => Error "sha3_64 requires single output")
+            | _ => Error "undefined operand")
+        | _ => Error "sha3_64 requires 2 operands")
+
     (* Default - unimplemented *)
     | _ => Error "unimplemented opcode"
 End
@@ -379,7 +602,8 @@ Proof
   gvs[AllCaseEqs(), is_terminator_def] >>
   fs[exec_binop_def, exec_unop_def, exec_modop_def] >>
   gvs[AllCaseEqs()] >>
-  fs[update_var_def, mstore_def, sstore_def, tstore_def]
+  fs[update_var_def, mstore_def, sstore_def, tstore_def,
+     write_memory_with_expansion_def]
 QED
 
 (* Step within a basic block - returns (result, is_terminator) *)

venom/venomStateScript.sml

@@ -21,6 +21,44 @@ Ancestors
 (* Variable environment maps variable names to 256-bit values *)
 Type var_env = ``:string |-> bytes32``
 
+(* --------------------------------------------------------------------------
+   Execution Context (from EVM environment)
+
+   This provides the environmental information needed for opcodes like
+   CALLER, CALLVALUE, ADDRESS, etc.
+   -------------------------------------------------------------------------- *)
+
+Datatype:
+  call_context = <|
+    cc_caller : address;           (* Caller address (CALLER) *)
+    cc_address : address;          (* Current contract address (ADDRESS) *)
+    cc_callvalue : bytes32;        (* Value sent with call (CALLVALUE) *)
+    cc_calldata : byte list;       (* Call data (CALLDATALOAD, etc.) *)
+    cc_gas : num                   (* Remaining gas (GAS) *)
+  |>
+End
+
+Datatype:
+  tx_context = <|
+    tc_origin : address;           (* Transaction origin (ORIGIN) *)
+    tc_gasprice : bytes32;         (* Gas price (GASPRICE) *)
+    tc_chainid : bytes32           (* Chain ID (CHAINID) *)
+  |>
+End
+
+Datatype:
+  block_context = <|
+    bc_coinbase : address;         (* Block coinbase (COINBASE) *)
+    bc_timestamp : bytes32;        (* Block timestamp (TIMESTAMP) *)
+    bc_number : bytes32;           (* Block number (NUMBER) *)
+    bc_prevrandao : bytes32;       (* Previous randao (PREVRANDAO) *)
+    bc_gaslimit : bytes32;         (* Block gas limit (GASLIMIT) *)
+    bc_basefee : bytes32;          (* Base fee (BASEFEE) *)
+    bc_blobbasefee : bytes32;      (* Blob base fee (BLOBBASEFEE) *)
+    bc_blockhash : num -> bytes32  (* Block hash lookup (BLOCKHASH) *)
+  |>
+End
+
 (* --------------------------------------------------------------------------
    Operands - values that can be used as instruction arguments
    -------------------------------------------------------------------------- *)
@@ -52,7 +90,43 @@ Datatype:
     vs_inst_idx : num;               (* Instruction index within block *)
     vs_returndata : byte list;       (* Return data buffer *)
     vs_halted : bool;                (* Execution halted? *)
-    vs_reverted : bool               (* Execution reverted? *)
+    vs_reverted : bool;              (* Execution reverted? *)
+    vs_accounts : evm_accounts;      (* Account states for BALANCE, etc. *)
+    vs_call_ctx : call_context;      (* Call context *)
+    vs_tx_ctx : tx_context;          (* Transaction context *)
+    vs_block_ctx : block_context     (* Block context *)
+  |>
+End
+
+(* Default context values *)
+Definition empty_call_context_def:
+  empty_call_context = <|
+    cc_caller := 0w;
+    cc_address := 0w;
+    cc_callvalue := 0w;
+    cc_calldata := [];
+    cc_gas := 0
+  |>
+End
+
+Definition empty_tx_context_def:
+  empty_tx_context = <|
+    tc_origin := 0w;
+    tc_gasprice := 0w;
+    tc_chainid := 0w
+  |>
+End
+
+Definition empty_block_context_def:
+  empty_block_context = <|
+    bc_coinbase := 0w;
+    bc_timestamp := 0w;
+    bc_number := 0w;
+    bc_prevrandao := 0w;
+    bc_gaslimit := 0w;
+    bc_basefee := 0w;
+    bc_blobbasefee := 0w;
+    bc_blockhash := K 0w
   |>
 End
 
@@ -68,7 +142,11 @@ Definition init_venom_state_def:
     vs_inst_idx := 0;
     vs_returndata := [];
     vs_halted := F;
-    vs_reverted := F
+    vs_reverted := F;
+    vs_accounts := empty_accounts;
+    vs_call_ctx := empty_call_context;
+    vs_tx_ctx := empty_tx_context;
+    vs_block_ctx := empty_block_context
   |>
 End
 
@@ -103,6 +181,17 @@ Definition expand_memory_def:
     s with vs_memory := s.vs_memory ++ REPLICATE n 0w
 End
 
+(* Expand memory if needed, then write bytes at offset *)
+Definition write_memory_with_expansion_def:
+  write_memory_with_expansion offset bytes s =
+    let mem = s.vs_memory in
+    let size = LENGTH bytes in
+    let needed = (offset + size) - LENGTH mem in
+    let expanded = if needed > 0 then mem ++ REPLICATE needed 0w else mem in
+    let newmem = TAKE offset expanded ++ bytes ++ DROP (offset + size) expanded in
+    s with vs_memory := newmem
+End
+
 (* Load a 32-byte word from memory (big-endian) *)
 Definition mload_def:
   mload offset s =