Dev v1.4.1

docseq

@@ -7,11 +7,16 @@ doc/EraVM.State.html
 doc/EraVM.GPR.html
 doc/EraVM.Flags.html
 doc/EraVM.Predication.html
-doc/EraVM.Memory.html
+doc/EraVM.TransientMemory.html
+doc/EraVM.memory.Depot.html
+doc/EraVM.memory.Pages.html
+doc/EraVM.memory.PageTypes.html
 doc/EraVM.Pointer.html
 doc/EraVM.Slice.html
 doc/EraVM.CallStack.html
 doc/EraVM.MemoryContext.html
+doc/EraVM.PointerErasure.html
+doc/EraVM.Binding.html
 
 doc/EraVM.History.html
 doc/EraVM.Event.html

src/ABI.v

@@ -1,7 +1,7 @@
-Require Coder Ergs Pointer GPR MemoryManagement lib.BitsExt.
+Require Coder Ergs Pointer GPR MemoryManagement TransientMemory lib.BitsExt.
 
 Import ssreflect ssreflect.ssrfun ssreflect.ssrbool ssreflect.eqtype ssreflect.tuple zmodp.
-Import Core Common Coder Bool GPR Ergs Memory MemoryManagement Pointer.
+Import Core Common Coder Bool GPR Ergs MemoryManagement TransientMemory Pointer.
 
 
 (** # Application binary interface (ABI)

src/ABI/FarCallABI.v

@@ -1,7 +1,7 @@
-Require Coder Ergs MemoryManagement Pointer lib.BitsExt ABI.FatPointerABI ABI.ForwardPageTypesABI.
+Require Coder Ergs memory.Depot MemoryManagement Pointer lib.BitsExt ABI.FatPointerABI ABI.ForwardPageTypesABI.
 
 Import ssreflect ssreflect.ssrfun ssreflect.eqtype ssreflect.tuple.
-Import Arith Core Common Coder Ergs Memory MemoryManagement Pointer lib.BitsExt FatPointerABI ForwardPageTypesABI.
+Import Arith Core Common Coder Ergs memory.Depot MemoryManagement Pointer TransientMemory lib.BitsExt FatPointerABI ForwardPageTypesABI.
 
 Section FarCallABI.
   (** This record describes all the parameters that [%FarCalls] can use. *)

src/ABI/FarRetABI.v

@@ -1,7 +1,7 @@
 Require Coder Ergs MemoryManagement Pointer lib.BitsExt ABI.FatPointerABI ABI.ForwardPageTypesABI.
 
 Import ssreflect ssreflect.ssrfun ssreflect.eqtype ssreflect.tuple.
-Import Arith Core Common Coder Ergs Memory MemoryManagement Pointer lib.BitsExt FatPointerABI ForwardPageTypesABI.
+Import Arith Core Common Coder Ergs MemoryManagement Pointer TransientMemory lib.BitsExt FatPointerABI ForwardPageTypesABI.
 
 
   (** This record describes all the parameters that far returns can use. *)

src/ABI/ForwardPageTypesABI.v

@@ -1,7 +1,7 @@
-Require Coder Ergs MemoryManagement Pointer lib.BitsExt ABI.FatPointerABI.
+Require Coder Ergs MemoryManagement Pointer TransientMemory lib.BitsExt ABI.FatPointerABI.
 
 Import ssreflect ssreflect.ssrfun ssreflect.eqtype ssreflect.tuple.
-Import Arith Core Common Coder Ergs Memory MemoryManagement Pointer lib.BitsExt FatPointerABI.
+Import Arith Core Common Coder Ergs MemoryManagement Pointer TransientMemory lib.BitsExt FatPointerABI.
 
 Module FarCallForwardPageType.
   Definition UseHeap : u8 := # 0.

src/ABI/MetaParametersABI.v

@@ -1,7 +1,7 @@
-Require Coder Ergs MemoryManagement Pointer lib.BitsExt.
+Require Coder Ergs memory.Depot MemoryManagement Pointer TransientMemory lib.BitsExt.
 
 Import ssreflect ssreflect.ssrfun ssreflect.eqtype ssreflect.tuple.
-Import Arith Core Common Coder Ergs Memory MemoryManagement Pointer lib.BitsExt.
+Import Arith Core Common Coder Ergs memory.Depot TransientMemory MemoryManagement Pointer lib.BitsExt.
 
 Section MetaParametersABI.
 

src/ABI/NearCallABI.v

@@ -1,7 +1,7 @@
-Require Coder Ergs Memory.
+Require Coder Ergs TransientMemory.
 
 Import ssreflect.
-Import Types Core Coder Ergs Memory.
+Import Types Core Coder Ergs TransientMemory.
 
 Section NearCallABI.
 

src/ABI/PrecompileParametersABI.v

@@ -1,7 +1,7 @@
-Require Coder Memory lib.BitsExt.
+Require Coder TransientMemory lib.BitsExt.
 
 Import ssreflect ssreflect.ssrfun ssreflect.eqtype ssreflect.tuple.
-Import Core Common Coder Memory lib.BitsExt.
+Import Core Common Coder TransientMemory lib.BitsExt.
 
 Section PrecompileParametersABI.
 

src/Addressing.v

@@ -1,6 +1,6 @@
-Require Common Memory GPR.
+Require Common TransientMemory GPR.
 
-Import Common Memory GPR.
+Import Common TransientMemory GPR.
 
 Section Addressing.
   (** # Addressing modes
@@ -245,12 +245,13 @@ and memory locations.
      add r3, r0, stack+=[r1+42]
      ```
 
-   **WARNING: KNOWN DIVERGENCE** current implementation diverges from the described spec:
+   **WARNING: KNOWN DIVERGENCE (in versions prior to v1.4.1)** implementation
+     of earlier versions diverged from the described spec:
 
      - Implementation: the write happens to the new SP address
      - Specification: the write happens to the old SP address
 
-     The implementation will be adjusted to conform to the spec in later versions.
+     Since v 1.4.1 the implementation conforms to the spec.
    *)
   Inductive stack_out_only : Type :=
   | RelSpPush (reg:reg_name) (offset: stack_address)

src/Binding.v

@@ -9,6 +9,7 @@ Require
     GPR
     isa.CoreSet
     Pointer
+    PointerErasure
     PrimitiveValue
     State.
 Import
@@ -23,6 +24,7 @@ Import
     isa.CoreSet
     MemoryOps
     Pointer
+    PointerErasure
     PrimitiveValue
     State
     Types.
@@ -43,44 +45,67 @@ decoded for small step relations, e.g. [%step_ptradd] for [%OpPtrAdd].
    *)
   #[global]
     Canonical Structure bound: descr :=
-  let pv := @primitive_value word in
   {|
-    src_pv := pv;
+    src_pv := @primitive_value Core.word;
     src_fat_ptr := option (@primitive_value (u128 * fat_ptr_nullable));
     src_heap_ptr := option (@primitive_value (u224 * heap_ptr));
     src_farcall_params := option (@primitive_value FarCallABI.params);
     src_nearcall_params := option (@primitive_value (u224 * NearCallABI.params));
     src_ret_params := option (@primitive_value FarRetABI.params);
     src_precompile_params := option (@primitive_value PrecompileParametersABI.params);
-    dest_pv := pv;
+    dest_pv := @primitive_value Core.word;
     dest_heap_ptr := option (@primitive_value (u224 * heap_ptr) );
     dest_fat_ptr := option (@primitive_value (u128 * fat_ptr_nullable) );
     dest_meta_params := option (@primitive_value (MetaParametersABI.params ));
   |}
   .
 
   (**
-Knowing the call stack, memory pages and registers are enough to bind any value appearing in [%CoreInstructionSet].
+Knowing the call stack, memory pages and registers are enough to bind any value appearing in [%CoreInstructionSet]; additionally, kernel mode affects it: pointer erasure only happens in user mode.
    *)
   Record binding_state := mk_bind_st {
+                              bs_is_kernel_mode: bool;
                               bs_cs: State.callstack;
                               bs_regs: regs_state;
                               bs_mem: State.memory;
                             }.
 
+  Inductive bind_any_src: binding_state -> binding_state -> in_any -> @primitive_value word -> Prop :=
+  | bind_any_src_apply: forall regs (mem:State.memory) (cs cs':State.callstack) (op:in_any) (v:@primitive_value word) (is_k: bool),
+      load _ regs cs mem op (cs', v) ->
+      bind_any_src (mk_bind_st is_k cs regs mem) (mk_bind_st is_k cs' regs mem) op v.
+
   (** To bind a [%src_pv] type of instruction operand, load its
-  value and apply the effects of [%RelSpPop] addressing mode. *)
+  value and apply the effects of [%RelSpPop] addressing mode.
+  Additionally, if the instruction expects an integer, but gets a pointer with a
+  tag, the pointer erasure happens (since v.1.4.1).
+   *)
+
   Inductive bind_src: binding_state -> binding_state -> in_any -> @primitive_value word -> Prop :=
-  | bind_src_apply: forall regs (mem:State.memory) (cs cs':State.callstack) (op:in_any) (v:@primitive_value word),
-      load _ regs cs mem op (cs', v) ->
-      bind_src (mk_bind_st cs regs mem) (mk_bind_st cs' regs mem) op v.
+  | bind_src_int_apply: forall regs (mem:State.memory) (cs cs':State.callstack) (op:in_any) (v:word) (is_k: bool),
+      bind_any_src (mk_bind_st is_k cs regs mem) (mk_bind_st is_k cs' regs mem) op (IntValue v) ->
+      bind_src (mk_bind_st is_k cs regs mem) (mk_bind_st is_k cs' regs mem) op (IntValue v)
+
+  | bind_src_ptr_apply: forall regs (mem:State.memory) (cs cs':State.callstack) (op:in_any) (v v':word)
+                          (decoded decoded_erased: fat_ptr_nullable)
+                          (encoded_erased high128: u128)
+                          (is_k: bool),
+      bind_any_src (mk_bind_st is_k cs regs mem) (mk_bind_st is_k cs' regs mem) op (PtrValue v) ->
+
+      Some (high128, decoded) = decode_fat_ptr_word v ->
+      decoded_erased = fat_ptr_nullable_erase is_k decoded ->
+      Some encoded_erased = encode_fat_ptr decoded ->
+      v' = high128 ## encoded_erased ->
+
+      bind_src (mk_bind_st is_k cs regs mem) (mk_bind_st is_k cs' regs mem) op (IntValue v')
+  .
 
   (** To bind a [%dest_pv] type of instruction operand, store its
   value and apply the effects of [%RelSpPush] addressing mode. *)
   Inductive bind_dest: binding_state -> binding_state -> out_any -> primitive_value  -> Prop :=
-  | bind_dest_apply: forall regs mem cs regs' mem' cs' op val,
+  | bind_dest_apply: forall regs mem cs regs' mem' cs' op val is_k,
       store _ regs cs mem op val (regs', mem', cs') ->
-      bind_dest (mk_bind_st cs regs mem) (mk_bind_st cs' regs' mem') op val.
+      bind_dest (mk_bind_st is_k cs regs mem) (mk_bind_st is_k cs' regs' mem') op val.
 
   (** To bind [%src_fat_ptr] or any other compound value encoded in a binary form,  bind both the encoded and decoded value. *)
   Inductive bind_fat_ptr: binding_state -> binding_state -> in_any -> option (@primitive_value (u128 * fat_ptr_nullable)) -> Prop :=
@@ -159,25 +184,30 @@ Knowing the call stack, memory pages and registers are enough to bind any value
       mf_dest_meta_params := bind_dest_meta_params;
     |}.
 
+
   #[local]
-  Definition get_binding_state (s: state) : binding_state :=
+  Definition get_binding_state_ts (s: transient_state) : binding_state :=
     {|
+      bs_is_kernel_mode := in_kernel_mode (gs_callstack s);
       bs_regs := gs_regs s;
       bs_mem  := gs_pages s;
       bs_cs   := gs_callstack s;
     |}.
 
+  #[local]
+  Definition get_binding_state (s: state) : binding_state := get_binding_state_ts s.
+
   Inductive relate_transient_states (P: binding_state -> binding_state -> Prop): transient_state -> transient_state -> Prop :=
   | rts_apply:
-    forall r1 r2 m1 m2 c1 c2 ctx flags status,
-      P (mk_bind_st c1 r1 m1 ) (mk_bind_st c1 r1 m1) ->
-      relate_transient_states P (mk_transient_state flags r1 m1 c1 ctx status) (mk_transient_state flags r2 m2 c2 ctx status).
+    forall ts1 ts2,
+      P (get_binding_state_ts ts1) (get_binding_state_ts ts2)->
+      relate_transient_states P ts1 ts2.
 
   #[local]
   Definition merge_binding_transient_state: binding_state -> transient_state -> transient_state :=
     fun bs s1 =>
       match bs with
-      | mk_bind_st cs regs gmem => s1
+      | mk_bind_st _ cs regs gmem => s1
                                    <| gs_regs      := regs |>
                                    <| gs_pages     := gmem |>
                                    <| gs_callstack := cs   |>
@@ -187,7 +217,7 @@ Knowing the call stack, memory pages and registers are enough to bind any value
   Definition merge_binding_state : state -> binding_state -> state :=
     fun s1 bs =>
       match bs with
-      | mk_bind_st cs regs gmem => s1 <| gs_transient ::= merge_binding_transient_state bs |>
+      | mk_bind_st _ cs regs gmem => s1 <| gs_transient ::= merge_binding_transient_state bs |>
       end.
 
   #[local]

src/Bootloader.v

@@ -1,5 +1,5 @@
-Require Memory.
-Import Memory.
+Require memory.Depot.
+Import memory.Depot.
 
 Section Bootloader.
   Import ZArith spec.

src/CallStack.v

@@ -1,8 +1,8 @@
 From RecordUpdate Require Import RecordSet.
 Import RecordSetNotations.
-Require Common Ergs Memory MemoryContext.
+Require Common Ergs KernelMode memory.Depot TransientMemory MemoryContext.
 
-Import Common Ergs MemoryContext Memory List ListNotations.
+Import Common Ergs KernelMode memory.Depot TransientMemory MemoryContext List ListNotations.
 
 Section Callstack.
 
@@ -455,4 +455,10 @@ Executing any instruction $I$ changes the topmost frame:
     End ActivePages.
 
   End ActiveMemory.
+
+
+  Definition in_kernel_mode (ef:callstack) : bool :=
+    let ef := active_extframe ef in
+    addr_is_kernel ef.(ecf_this_address).
+
 End Callstack.

src/Decommitter.v

@@ -1,6 +1,6 @@
-Require Common ABI lib.Decidability History MemoryOps VersionedHash.
+Require Common ABI lib.Decidability History memory.Depot MemoryOps VersionedHash.
 
-Import Coder Core History VersionedHash Common Decidability Ergs Memory MemoryBase ZArith ABI bits.
+Import Coder Core History VersionedHash Common Decidability Ergs MemoryBase memory.Depot TransientMemory ZArith ABI bits.
 
 
 Section Decommitter.
@@ -26,7 +26,7 @@ Note: storage with the same contract address may differ between shards.
 
   Definition DEPLOYER_SYSTEM_CONTRACT_ADDRESS : contract_address := fromZ ((2^15) + 2).
 
-  Definition code_hash_location (for_contract: contract_address) (sid:Memory.shard_id): fqa_key :=
+  Definition code_hash_location (for_contract: contract_address) (sid:Depot.shard_id): fqa_key :=
     mk_fqa_key (mk_fqa_storage sid DEPLOYER_SYSTEM_CONTRACT_ADDRESS) (widen word_bits for_contract).
 
   Context {ins_type: Type} (invalid_ins: ins_type) (code_page := code_page invalid_ins)
@@ -67,7 +67,7 @@ Decommitting warm code is free. *)
     is_first_access cm vhash = false ->
     decommitment_cost cm vhash code_length_in_words zero32.
 
-  Inductive code_fetch_hash (d:depot) (cs: code_storage) (sid: Memory.shard_id) (contract_addr: contract_address) :
+  Inductive code_fetch_hash (d:depot) (cs: code_storage) (sid: Depot.shard_id) (contract_addr: contract_address) :
     option (versioned_hash * code_length) -> Prop :=
   |cfh_found: forall hash_enc code_length_in_words extra_marker partial_hash,
       storage_read d (code_hash_location contract_addr sid) hash_enc ->
@@ -92,9 +92,9 @@ VM does not mask the code for system contracts; see [%sem.FarCall.step].
 
 [%DEFAULT_AA_CODE] is the decommitter's answer to the query [%DEFAULT_AA_VHASH]. *)
 
-  Parameter DEFAULT_AA_CODE: (Memory.code_page invalid_ins * const_page).
+  Parameter DEFAULT_AA_CODE: (code_page* const_page).
 
-  Inductive code_fetch  (d:depot) (cs: code_storage) (sid: Memory.shard_id) (contract_addr: contract_address) :
+  Inductive code_fetch  (d:depot) (cs: code_storage) (sid: Depot.shard_id) (contract_addr: contract_address) :
     bool -> (versioned_hash * (code_page * const_page) * code_length) -> Prop :=
   | cfnm_no_masking: forall vhash (code_storage:code_storage) code_length_in_words pages0 masking,
       code_fetch_hash d cs sid contract_addr (Some (vhash, code_length_in_words)) ->

src/Ergs.v

@@ -1,5 +1,5 @@
-Require Common isa.Assembly Memory.
-Import Common Assembly Memory ZArith.
+Require Common isa.Assembly TransientMemory.
+Import Common Assembly TransientMemory ZArith.
 
 Section Ergs.
 Open Scope Z_scope.

src/Event.v

@@ -1,6 +1,6 @@
 From mathcomp Require ssreflect ssrfun ssrbool eqtype tuple zmodp.
-Require Core Memory.
-Import Core Memory.
+Require Core memory.Depot TransientMemory.
+Import Core memory.Depot TransientMemory.
 
 Section Events.
   Import ssreflect ssreflect.tuple ssreflect.eqtype ssrbool.

src/GPR.v

@@ -1,11 +1,11 @@
 From RecordUpdate Require Import RecordSet.
 Require Core List PrimitiveValue.
 
-Import Core PrimitiveValue .
+Import Core PrimitiveValue.
 
 Section Registers.
   Import RecordSetNotations.
-  Context (pv := @primitive_value word).
+  Context (pv := @primitive_value Core.word).
 
   (** # GPR (General Purpose Registers)
 
@@ -39,7 +39,7 @@ evaluates to [%IntValue 0], that is, an untagged integer 0.
                           }.
 
   (* begin hide *)
-  Definition reg_zero := IntValue word0.
+  Definition reg_zero := pv0.
   Definition reserved := reg_zero.
   Definition regs_state_zero := let z := reg_zero in
                                 mk_regs z z z z z z z z z z z z z z z.

src/Introduction.v

@@ -1,4 +1,4 @@
-(** This is the specification of the instruction set of EraVM 1.4.0, a language
+(** This is the specification of the instruction set of EraVM 1.4.1, a language
 virtual machine for zkSync Era. It describes the virtual machine's architecture,
 instruction syntax and semantics, and some elements of system protocol.
 

src/KernelMode.v

@@ -1,6 +1,6 @@
-Require isa.CoreSet.
+Require isa.CoreSet memory.Depot.
 
-Import CoreSet Memory.
+Import CoreSet TransientMemory memory.Depot.
 
 Section KernelMode.
   Import ZArith Arith spec.