From 277f9e133153eb7d18ee3c80eec9a415add73735 Mon Sep 17 00:00:00 2001 From: Igor Zhirkov Date: Wed, 29 Nov 2023 15:19:53 +0100 Subject: [PATCH] fix missing files --- src/ABI/FarRetABI.v | 11 +- src/ABI/ForwardPageTypesABI.v | 4 +- src/lib/Arith_ext.v | 36 ++++++ src/lib/Decidability.v | 46 +++++++ src/lib/PArith_ext.v | 52 ++++++++ src/lib/PMap_ext.v | 15 +++ src/lib/ZArith_ext.v | 128 +++++++++++++++++++ src/lib/ZMod.v | 229 ++++++++++++++++++++++++++++++++++ src/lib/ZModTests.v | 13 ++ src/memory/Depot.v | 153 +++++++++++++++++++++++ src/memory/PageTypes.v | 159 +++++++++++++++++++++++ src/memory/Pages.v | 88 +++++++++++++ src/sem/Farcall.v | 3 +- 13 files changed, 929 insertions(+), 8 deletions(-) create mode 100644 src/lib/Arith_ext.v create mode 100644 src/lib/Decidability.v create mode 100644 src/lib/PArith_ext.v create mode 100644 src/lib/PMap_ext.v create mode 100644 src/lib/ZArith_ext.v create mode 100644 src/lib/ZMod.v create mode 100644 src/lib/ZModTests.v create mode 100644 src/memory/Depot.v create mode 100644 src/memory/PageTypes.v create mode 100644 src/memory/Pages.v diff --git a/src/ABI/FarRetABI.v b/src/ABI/FarRetABI.v index 810a88a..2b5b57e 100644 --- a/src/ABI/FarRetABI.v +++ b/src/ABI/FarRetABI.v @@ -79,12 +79,12 @@ End BinaryCoder. Section LayoutCoder. - Definition encode_layout: @encoder params_layout params := + Definition encode_layout: @encoder params_layout params := fun params => match params with | mk_params (ForwardExistingFatPointer fptr) => match FatPointerABI.encode_layout fptr with - | Some ptr_layout => + | Some ptr_layout => Some {| raw_memory_forwarding_type_enum := FarCallForwardPageType.ForwardFatPointer; @@ -115,9 +115,9 @@ fun params => end end . - Theorem layout_coding_revertible: revertible decode_layout encode_layout. - unfold revertible. +Proof. + unfold revertible. unfold revertible, decode_layout, encode_layout, fwd_memory_adapter. move => [fwd_memory encoded]. case_eq fwd_memory. @@ -144,7 +144,8 @@ fun params => repeat f_equal =>//=; by destruct s. } } - Qed. + Qed. + Definition coder_layout := mk_coder decode_layout encode_layout layout_coding_revertible. diff --git a/src/ABI/ForwardPageTypesABI.v b/src/ABI/ForwardPageTypesABI.v index 5c816f1..a0fcab8 100644 --- a/src/ABI/ForwardPageTypesABI.v +++ b/src/ABI/ForwardPageTypesABI.v @@ -18,8 +18,8 @@ Definition data_page_type_to_u8 (t:data_page_type) : u8 := Definition span_of (fp: fat_ptr_layout) : option span := if fp.(offset) == zero32 - then None - else Some (mk_span fp.(start) fp.(length)) + then Some (mk_span fp.(start) fp.(length)) + else None . Definition fwd_memory_adapter (fwd_type: u8) (raw_fat_ptr_layout: fat_ptr_layout) : option MemoryManagement.fwd_memory:= diff --git a/src/lib/Arith_ext.v b/src/lib/Arith_ext.v new file mode 100644 index 0000000..18fe0e1 --- /dev/null +++ b/src/lib/Arith_ext.v @@ -0,0 +1,36 @@ +Require Lia ZArith. + +(** * Additional properties of natural numbers *) + +Section PowerTwo. + Import Coq.ZArith.Zpower. + Import Coq.ZArith.BinIntDef. + Import BinNums. + + + Open Scope Z_scope. + + Theorem two_power_nat_0 : + two_power_nat 0 = 1%Z. + Proof. + reflexivity. + Qed. + + Theorem two_power_nat_gt_0: + forall n : nat, BinInt.Z.gt (two_power_nat n) 0%Z. + Proof. + induction n. + - rewrite two_power_nat_0. + reflexivity. + - rewrite two_power_nat_S. + Lia.lia. + Qed. + + + (* Lemma two_power_nat_two_p: *) + (* forall x, two_power_nat x = two_p (Z.of_nat x). *) + (* Proof. *) + (* induction x. auto. *) + (* rewrite two_power_nat_S. rewrite Nat2Z.inj_succ. rewrite two_p_S. Lia.lia. Lia.lia. *) + (* Qed. *) +End PowerTwo. diff --git a/src/lib/Decidability.v b/src/lib/Decidability.v new file mode 100644 index 0000000..cf5e1d0 --- /dev/null +++ b/src/lib/Decidability.v @@ -0,0 +1,46 @@ +From Coq.Logic Require Decidable. + +Import Decidable. + +Section Decidability. + + Definition dec(A: Prop) := { A } + { ~ A }. + + Lemma dec_decidable : + forall P, dec P -> decidable P. + Proof. unfold dec, decidable. intros ? []; tauto. Qed. + + + Theorem dec_conj: + forall A B: Prop, + dec A -> + dec B -> + dec (A /\ B). + Proof. unfold dec. intros; tauto. Qed. + + Theorem dec_not : forall A:Prop, dec A -> dec (~ A). + Proof. unfold dec. tauto. Qed. + + Theorem dec_not_not : forall P:Prop, dec P -> ~ ~ P -> P. + Proof. unfold dec; tauto. Qed. + + Theorem not_not : forall P: Prop, + dec P -> ~ ~ P -> P. + Proof. unfold dec; tauto. Qed. + + Theorem dec_or: + forall A B: Prop, + dec A -> + dec B -> + dec (A \/ B). + Proof. unfold dec; intros; tauto. Qed. + + Definition eq_dec (T:Type) := forall x1 x2: T, dec (x1 = x2). + +End Decidability. + +Ltac decide_equality := + unfold eq_dec, dec in *; + repeat decide equality; + unfold eq_dec, dec in *; + eauto with decidable_prop. diff --git a/src/lib/PArith_ext.v b/src/lib/PArith_ext.v new file mode 100644 index 0000000..a369bc2 --- /dev/null +++ b/src/lib/PArith_ext.v @@ -0,0 +1,52 @@ +Require BinNums BinInt ZArith Arith_ext. + +(** * Additional properties of positive numbers *) + + +(** ** Power *) +Section ModuloPowerOfTwo. +Import Arith_ext BinNums BinInt ZArith Lia. + +Open Scope Z_scope. + + +Fixpoint mod_pow2 (p: positive) (n: nat) {struct n} : Z := + match n, p with + | O, _ => 0 + | S m, xH => 1 + | S m, xO tail => Z.double (mod_pow2 tail m) + | S m, xI tail => Z.succ_double (mod_pow2 tail m) + end. + +Theorem mod_pow2_ge_0: + forall p n, mod_pow2 p n >= 0. +Proof. + induction p; destruct n; simpl; auto with zarith. + - rewrite Z.succ_double_spec. + apply Z.le_ge. + apply Z.add_nonneg_nonneg; auto with zarith. + replace 0 with ( 0 * mod_pow2 p n); [|auto with zarith]. + eapply Zmult_le_compat_r; [auto with zarith|]. + apply Z.ge_le. + apply IHp. + - rewrite Z.double_spec. + replace 0 with ( 0 * mod_pow2 p n); [|auto with zarith]. + eapply Zmult_ge_compat_r; [auto with zarith|]. + apply IHp. +Qed. + +Lemma mod_pow2_limit: + forall p n, mod_pow2 p n < two_power_nat n. +Proof. + intros p n; revert p. + induction n; simpl; intros. + - rewrite Arith_ext.two_power_nat_0. lia. + - rewrite two_power_nat_S. destruct p. + + pose (IHn p). rewrite Z.succ_double_spec. lia. + + pose (IHn p). rewrite Z.double_spec. lia. + + pose (two_power_nat_gt_0 n). lia. +Qed. + + +Close Scope Z_scope. +End ModuloPowerOfTwo. diff --git a/src/lib/PMap_ext.v b/src/lib/PMap_ext.v new file mode 100644 index 0000000..1ea4cc3 --- /dev/null +++ b/src/lib/PMap_ext.v @@ -0,0 +1,15 @@ +Require FMapPositive. + +Import FMapPositive.PositiveMap BinPos. + +Definition pmap_slice {V} (m:t V) (from_incl to_excl:positive ) : t V := + let leb x y := negb (Pos.ltb y x) in + let in_range k := andb (leb from_incl k) (Pos.ltb k to_excl) in + let f k cell accmap := + if in_range k + then + add k cell accmap + else + accmap + in + fold f m (empty _). diff --git a/src/lib/ZArith_ext.v b/src/lib/ZArith_ext.v new file mode 100644 index 0000000..6879f21 --- /dev/null +++ b/src/lib/ZArith_ext.v @@ -0,0 +1,128 @@ +Require Coq.Logic.Decidable. +Require Decidability. +Require PArith. +Require PArith_ext. +Require ZArith. +Require Lia. + +(** * Properties of Z *) + +Section Decidability. + (** ** Decidability *) + Import Decidability ZArith. + + Lemma eq_dec : eq_dec BinNums.Z. + decide_equality. + Defined. + + Open Scope Z_scope. + Definition lt_dec: forall (x y: Z), {x < y} + {x >= y}. + Proof. + unfold Z.lt, Z.ge. + intros x y; destruct (Z.compare x y); auto; right; intro H; inversion H. + Defined. + + Definition gt_dec: forall (x y: Z), {x > y} + {x <= y}. + Proof. + unfold Z.gt, Z.le. + intros x y; destruct (Z.compare x y); auto; right; intro H; inversion H. + Defined. + +End Decidability. + + +Section ModuloPowerOfTwo. + Import ZArith. + Import PArith_ext. + Open Scope Z. + + Definition mod_pow2 (z: Z) (n: nat) : Z := + match z with + | Z0 => 0 + | Zpos p => mod_pow2 p n + | Zneg p => let r := mod_pow2 p n in + if ZArith_ext.eq_dec r 0%Z + then 0 + else ZArith.Zpower.two_power_nat n - r + end. + + + Theorem mod_pow2_ge_0: + forall z n, mod_pow2 z n >= 0. + Proof. + intros. unfold mod_pow2. pose ( Arith_ext.two_power_nat_gt_0 n) as Hpos. + destruct z. + - auto with zarith. + - exact (PArith_ext.mod_pow2_ge_0 p n). + - destruct (eq_dec _ 0) . + + auto with zarith. + + pose (PArith_ext.mod_pow2_ge_0 p n). + pose (PArith_ext.mod_pow2_limit p n). + Lia.lia. + Qed. + + Theorem mod_pow2_limit: + forall z n, mod_pow2 z n < two_power_nat n. + Proof. + intros. unfold mod_pow2. pose ( Arith_ext.two_power_nat_gt_0 n) as Hpos. + destruct z. + - auto with zarith. + - pose (PArith_ext.mod_pow2_limit p n). auto with zarith. + - destruct (eq_dec _ 0) . + + auto with zarith. + + pose (PArith_ext.mod_pow2_ge_0 p n). + pose (PArith_ext.mod_pow2_limit p n). + Lia.lia. + Qed. + + Theorem mod_pow2_range: + forall z n, 0 <= mod_pow2 z n < two_power_nat n. + Proof. + split. + - apply Z.ge_le. apply mod_pow2_ge_0. + - apply mod_pow2_limit. + Qed. + + (* Lemma mod_modulus_range: *) + (* forall x, 0 <= Z_mod_modulus x < characteristic. *) + (* Proof (Z_mod_two_p_range bits). *) + + (* Lemma Z_mod_modulus_range': *) + (* forall x, -1 < Z_mod_modulus x < modulus. *) + (* Proof. *) + + (* Lemma Z_mod_modulus_eq: *) + (* forall x, Z_mod_modulus x = x mod modulus. *) + (* Proof (Z_mod_two_p_eq wordsize). *) + + + Close Scope Z_scope. +End ModuloPowerOfTwo. + +Section Range. +Import ZArith. +Definition in_range (x y z:Z) : bool := + if Z_le_dec x y then + if Z_lt_dec y z then true + else false + else false. + +Theorem in_range_spec_l: + forall x y z, (x <= y < z)%Z -> in_range x y z = true. +Proof. +unfold in_range; intros x y z [H H']. +destruct (Z_le_dec _ _); auto. +destruct (Z_lt_dec _ _); auto. +Qed. + +Theorem in_range_spec_r: + forall x y z, in_range x y z = true -> (x <= y < z)%Z. +Proof. + unfold in_range. + intros x y z H. + destruct (Z_le_dec _ _); try destruct (Z_lt_dec _ _); auto; try discriminate. +Qed. + +End Range. +#[export] + Hint Resolve eq_dec gt_dec lt_dec: decidable_prop. diff --git a/src/lib/ZMod.v b/src/lib/ZMod.v new file mode 100644 index 0000000..eb52ce0 --- /dev/null +++ b/src/lib/ZMod.v @@ -0,0 +1,229 @@ +Require ZArith ZArith_ext ZBits. + +Import BinInt ZArith ZArith_ext BinIntDef.Z. + + + +(** * Machine integers modulo 2^N. + Integers are encoded in binary form (see [%BinNums.positive]), therefore we are able to + efficiently reason about wide numbers e.g. 256-bit. *) +Section Def. + + (** [%bits] is an implicit parameter passed to all definitions in this section + that use it. After the Section end, all definitions will be rewritten so that + [%bits] is passed to them explicitly. *) + Variable bits: nat. + + (** [%bits_nz] is an implicit proof passed to all definitions in this section + that use it. It forbids constructing integers modulo 1. After the Section end, + all definitions will be rewritten so that [%bits] is passed to them explicitly. *) + Hypothesis bits_nz: (bits <> 0)%nat. + + + (* [%Let] is a keyword for section-local definitions, to be inlined. *) + Let zbits: Z := Z.of_nat bits. + Let characteristic: Z := 2 ^ zbits. + + + (** An integer modulo 2^N. It carries a proof [%int_range] of representability + with no more than [%bits] binary digits. *) + Record int_mod: Type := mk_int_mod { + int_val: Z; + int_range: in_range 0 int_val characteristic = true + }. + + (** ## Equality *) + + Lemma eq_values: forall (x y: int_mod), + x = y <-> int_val x = int_val y. + Proof. + intros x y; split. + - intros; subst; reflexivity. + - destruct x,y. + simpl in *. + intros ?; subst. + f_equal. + destruct (in_range 0 int_val1 characteristic); [|discriminate]. + rewrite (Eqdep_dec.UIP_refl_bool _ int_range1). + rewrite (Eqdep_dec.UIP_refl_bool _ int_range0). + reflexivity. + Qed. + + Theorem eq_dec : Decidability.eq_dec int_mod. + Proof. + intros [x xp] [y yp]. + destruct (Z.eq_dec x y); subst. + - left. + apply eq_values. reflexivity. + - right. + intro H. subst. apply eq_values in H. contradiction. + Qed. + + (** ** Conversions *) + + (** Interpreting [%int_mod] as an unsigned integer modulo 2^N. *) + Definition as_unsigned (n: int_mod) : Z := int_val n. + + (** Interpreting [%int_mod] as a signed [%Z], where the leftmost bit encodes the + sign. *) + Definition as_signed (n: int_mod) : Z := + (let x := as_unsigned n in + if lt_dec x (characteristic/2) then x else x - characteristic)%Z. + + (** Minimal unsigned value. *) + Definition unsigned_min: Z := 0. + (** Maximal unsigned value. *) + Definition unsigned_max : Z := characteristic - 1. + (** Minimal signed value. *) + Definition signed_min : Z := - (characteristic / 2). + (** Maximal signed value. *) + Definition signed_max : Z := (characteristic / 2) - 1. + + + (** An integer modulo 2^N falls in range between 0 inclusive and 2^N exclusive. *) + Theorem int_mod_range: + forall z : Z, (0 <= mod_pow2 z bits < characteristic)%Z. + Proof. + intros z. + unfold characteristic, zbits. + rewrite <-two_power_nat_equiv. + apply mod_pow2_range. + Qed. + + (** Ensure an integer is representable with N bits, truncating it if necessary. *) + Definition int_mod_of (z: Z) : int_mod. + pose (truncated := ZArith_ext.mod_pow2 z bits). + refine (mk_int_mod truncated _). + apply in_range_spec_l. + apply (int_mod_range z). + Defined. + + (** ## Operations + Addition, subtraction, multiplication, division, shifts, modulo operations. +### Comparison *) + Definition beq (x y: int_mod) : bool := if eq_dec x y then true else false. + Definition lt_signed (x y: int_mod) : bool := if lt_dec (as_signed x) (as_signed y) then true else false. + Definition lt_unsigned (x y: int_mod) : bool := if lt_dec (as_unsigned x) (as_unsigned y) then true else false. + Definition gt_unsigned := Basics.flip lt_unsigned. + + Definition le_unsigned (x y: int_mod) : bool := (lt_unsigned x y) || beq x y. + Definition ge_unsigned := Basics.flip le_unsigned. + + Definition liftZ (f:Z->Z->Z) x y := int_mod_of (f x.(int_val) y.(int_val)). + + Definition min := liftZ BinIntDef.Z.min. + Definition max := liftZ BinIntDef.Z.max. + + Definition carry (z:Z) : bool := if gt_dec z unsigned_max then true else false. + + Definition uadd_overflow (x y: int_mod) : int_mod * bool := + let result := (as_unsigned x + as_unsigned y)%Z in + (int_mod_of result, carry result). + + Definition uinc_overflow (x: int_mod) : int_mod * bool := + uadd_overflow x (int_mod_of 1). + + Definition usub_overflow (x y: int_mod) : int_mod * bool := + let a := as_unsigned x in + let b := as_unsigned y in + (int_mod_of (a-b)%Z, if gt_dec b a then true else false). + + Definition is_overflowing (res: int_mod * bool) := snd res. + + Definition umul_overflow (x y: int_mod) : int_mod * bool := + let result := (as_unsigned x * as_unsigned y)%Z in + (int_mod_of result, carry result). + + Definition add_wrap (x y: int_mod) : int_mod := + match uadd_overflow x y with + | (z, _) => z + end. + Definition sub_wrap (x y: int_mod) : int_mod := + match usub_overflow x y with + | (z, _) => z + end. + (** ## Shifts +### Logical shifts *) + Definition shiftl_nat (x: int_mod) (bits: nat) : int_mod := + int_mod_of (Z.shiftl (int_val x) (Z.of_nat bits)). + + Definition shiftl (x: int_mod) (bits: int_mod) : int_mod := + int_mod_of (Z.shiftl (int_val x) (int_val bits)). + + Definition shiftr_nat (x: int_mod) (bits: nat): int_mod := + int_mod_of (Z.shiftr (int_val x) (Z.of_nat bits)). + + Definition shiftr (x: int_mod) (bits: int_mod) : int_mod := + int_mod_of (Z.shiftr (int_val x) (int_val bits)). + + (** ### Circular shifts *) + Definition rol (x: int_mod) (shift: int_mod): int_mod := + let shift := Z.modulo shift.(int_val) zbits in + let x := int_val x in + let low := Z.shiftl x shift in + let high := Z.shiftr x (zbits - shift) in + int_mod_of (Z.lor low high). + + Definition ror (x: int_mod) (shift: int_mod): int_mod := + let shift := Z.modulo shift.(int_val) zbits in + let x := int_val x in + let low := Z.shiftr x shift in + let high := Z.shiftl x (zbits - shift) in + int_mod_of (Z.lor low high). + +End Def. + + +Definition beq_op {n:nat} (x y: int_mod n) : bool := beq n x y. +Definition bneq_op {n:nat} (x y: int_mod n) : bool := negb (beq n x y). + +Declare Scope ZMod_scope. +Infix "==" := beq_op (at level 70, no associativity): ZMod_scope. +Infix "!=" := bneq_op (at level 70, no associativity): ZMod_scope. +Infix "+" := (uadd_overflow _) : ZMod_scope. +Infix "-" := (usub_overflow _) : ZMod_scope. +Infix "*" := (umul_overflow _) : ZMod_scope. + +Infix "<" := (lt_unsigned _) : ZMod_scope. +Infix ">" := (gt_unsigned _) : ZMod_scope. +Infix "<=" := (le_unsigned _) : ZMod_scope. +Infix ">=" := (ge_unsigned _) : ZMod_scope. + +Bind Scope ZMod_scope with int_mod. +Definition bitwise_op (f:Z->Z->Z) (bits:nat) (x y: int_mod bits) : int_mod bits := + int_mod_of _ (f (int_val _ x) (int_val _ y)). + +Definition bitwise_xor := bitwise_op lxor. +Definition bitwise_or := bitwise_op lor. +Definition bitwise_and := bitwise_op land. + + +Definition resize (sz1 sz2:nat) (x: int_mod sz1) : int_mod sz2 := + int_mod_of sz2 (int_val sz1 x). + +Definition mix_lower n (source: int_mod (n+n) ) (mix: int_mod n) : int_mod (n+n) := + let p := Z.of_nat n in + let hi := shiftr_nat _ source n in + bitwise_or _ (shiftl_nat (n+n) hi n) (resize n (n+n) mix). + +Fixpoint extract_digits (w:Z) (bits_per_digit: nat) (units:nat) : list Z := + let truncate x := ZArith_ext.mod_pow2 x bits_per_digit in + match units with + | O => truncate w :: nil + | S m => + let h := truncate w in + let new_w := Z.shiftr w (Z.of_nat bits_per_digit) in + let tail := extract_digits new_w bits_per_digit m in + h:: tail + + end. + +Section ConcatBytes. + Variable bits: nat. + + Definition concat_z z1 z2 : Z:= + ((Z.shiftl z1 (Z.of_nat bits)) + z2)%Z. + + Definition concat_bytes_Z (ls: list Z) : Z := + @List.fold_left Z Z concat_z ls 0%Z. +End ConcatBytes. diff --git a/src/lib/ZModTests.v b/src/lib/ZModTests.v new file mode 100644 index 0000000..886dda1 --- /dev/null +++ b/src/lib/ZModTests.v @@ -0,0 +1,13 @@ +Require ZMod. + +Import ZMod ZArith List ListNotations. + +Let test_rols seed := List.map (fun i => int_val _ (rol _ (int_mod_of 4 seed) (int_mod_of _ i) ) ). +Open Scope Z. +Check eq_refl: test_rols 1 [1;2;3;4;5] = [2; 4; 8; 1; 2]. +Check eq_refl: test_rols 3 [1;2;3;4;5] = [6; 12; 9; 3; 6]. + +Compute rol _ (int_mod_of 4 4%Z) (int_mod_of 4 1%Z). +Compute rol _ (int_mod_of 4 4%Z) (int_mod_of 4 3%Z). + +Check eq_refl: (1027%Z = int_val _ ( mix_lower _ (int_mod_of _ 1025) (int_mod_of 8 3))). diff --git a/src/memory/Depot.v b/src/memory/Depot.v new file mode 100644 index 0000000..73dd691 --- /dev/null +++ b/src/memory/Depot.v @@ -0,0 +1,153 @@ +Require Core PrimitiveValue MemoryBase. + +Import Common Core MemoryBase BinInt PrimitiveValue. + +Section Depot. + (** +# Storage of a contract + +A **storage** is a persistent linear mapping from $2^{256}$ addresses to words. + +Therefore, given a storage, each word storage is addressed through a 256-bit +address. + +In storage, individual bytes inside a word can not be addressed directly: a load +or a store happen on a word level. + +Both word address in storage and word width are 256 bits. + +All words in a storage are zero-initialized on genesis. +Therefore, reading storage word prior to writing yields zero. It is a +well-defined behavior. *) + + Definition storage_params := {| + addressable_block := word; + address_bits := 256; + default_value := word0; + writable := true + |}. + + Definition storage_address := BITS (address_bits storage_params). + Definition storage: Type := mem_parameterized storage_params. + + (** Storage start blanks. *) + Definition storage_empty : storage := empty storage_params. + + (** Storage does not hold contract code, it is a responsibility of decommittment +processor [%decommitter]. + +Storage is a part of a [%shard], which is a part of [%depot]. + +One storage is selected as an active storage, it is the storage corresponding to +the [%current_shard] and [%current_contract]. + +Use the instruction [%OpSStore] to write to the active storage, [%OpSLoad] to +read from the active storage. + +## Instructions + +Instruction [%OpSLoad] implements reading from storage; instruction [%OpSStore] +implements writing to storage. + +## Memory model + +Storage has a sequentially-consistent, strong memory model. +All writes are atomic and immediately visible; reads are guaranteed to return +the last value written. + + +# Shards and contracts + +A **contract** is uniquely identified by its 160-bit address [%contract_address]. +In future, the address could be seamlessly extended to up to 256 bits. + +A **shard** is a mapping of contract addresses to storages. + +Therefore, every contract is associated with as many storages as there are +shards. *) + + Definition shard_params := {| + addressable_block := storage; + address_bits := 160; + default_value := storage_empty; + writable := true + |}. + + Definition contract_address := address shard_params. + Definition contract_address_bits := address_bits shard_params. + Definition shard := mem_parameterized shard_params. + + (** Contracts are also associated with code. The association is global per depot +and implemented by [%Decommitter]. Therefore, the contract code is the same for +all shards, but the storages of a contract in different shards differ. + +Unlike in Ethereum, there is only type of accounts capable of both transacting +coins and executing contracts. + +Contracts with addresses in range from 0 (inclusive) to [%KERNEL_MODE_MAXADDR] +(exclusive) are **system contracts**; they are allowed to execute all +instructions. + +# Depot + +**Depot** is a collection of shards. +Depot is the global storage of storages of all contracts. + + *) + Definition depot_params := + {| + addressable_block := shard; + address_bits := 8; + default_value := empty _; + writable := true + |}. + + Definition depot := mem_parameterized depot_params. + + Definition shard_id := BITS (address_bits depot_params). + (** There are currently two shards: one for zkRollup, one for zkPorter. *) + + Inductive shard_exists: shard_id -> Prop := + | se_rollup: shard_exists (fromZ 0) + | se_porter: shard_exists (fromZ 1) + . + + + (** The **fully qualified address** of a word in depot is a triple: + + +$(\texttt{shard\_id}, \texttt{contract\_id} , \texttt{key})$ + +It is formalized by [%fqa_key]. + *) + + Record fqa_storage := mk_fqa_storage { + k_shard: shard_id; + k_contract: contract_address; + }. + Record fqa_key := mk_fqa_key { + k_storage :> fqa_storage; + k_key: storage_address + }. + + Inductive storage_get (d: depot): fqa_storage -> storage -> Prop := + | sg_apply: forall storage shard s c st, + shard_exists s -> + MemoryBase.load_result depot_params s d shard -> + MemoryBase.load_result shard_params c shard storage -> + storage_get d (mk_fqa_storage s c) st . + + Inductive storage_read (d: depot): fqa_key -> word -> Prop := + | sr_apply: forall storage sk c w, + storage_get d sk storage -> + storage_read d (mk_fqa_key sk c) w. + + Inductive storage_write (d: depot): fqa_key -> word -> depot -> Prop := + | sw_apply: forall storage shard sk s c k w shard' depot' storage', + storage_get d sk storage -> + MemoryBase.store_result storage_params k storage w storage' -> + MemoryBase.store_result shard_params c shard storage' shard' -> + MemoryBase.store_result depot_params s d shard' depot' -> + storage_write d (mk_fqa_key sk k) w depot'. + +End Depot. diff --git a/src/memory/PageTypes.v b/src/memory/PageTypes.v new file mode 100644 index 0000000..b7bea04 --- /dev/null +++ b/src/memory/PageTypes.v @@ -0,0 +1,159 @@ +Require List Core MemoryBase. +Import Common Core MemoryBase List. + +Section Memory. + + (** ### Data pages + +A **data page** contains individually addressable bytes. Each data page holds +$2^{32}$ bytes. *) + + Definition data_page_params := {| + addressable_block := u8; + address_bits := 32; + default_value := zero8; + writable := true + |}. + Definition mem_address := address data_page_params. + Definition mem_address_zero: mem_address := zero32. + Definition mem_address_bits := data_page_params.(address_bits). + + Definition data_page := mem_parameterized data_page_params. + + (** There are currently two types of data pages: + +- [%Heap] +- [%AuxHeap]. + + We call both of them **heap variants** for brevity, as in almost all cases + they are handled in a similar way. *) + Inductive data_page_type := Heap | AuxHeap. + Definition page_bound := prod data_page_type mem_address. + + Local Open Scope ZMod_scope. + Definition growth (current_bound: mem_address) (query_bound: mem_address) + : mem_address := + if query_bound < current_bound then zero32 else + snd (query_bound - current_bound) + . + (** + +Note: only selected few instructions can access data pages: + +- [%OpLoad]/[%OpLoadInc] +- [%OpStore]/[%OpStoreInc] +- [%OpLoadPointer]/[%OpLoadPointerInc] + +Every byte on data pages has an address, but these instructions read or store 32-byte words. + +----- + +Fat pointers [%fat_ptr] define slices of data pages and allow passing them +between contracts. + +### Stack pages + +A **stack page** contains $2^{16}$ primitive values (see [%primitive_value]). +Reminder: primitive values are tagged words. + + *) + Context {primitive_value: Type} (pv0: primitive_value). + Definition stack_page_params := {| + addressable_block := primitive_value; + address_bits := 16; + default_value := pv0; + writable := true + |}. + + Definition stack_address := address stack_page_params. + Definition stack_address_bits := stack_page_params.(address_bits). + Definition stack_address_zero: stack_address := zero16. + + Definition stack_page := mem_parameterized stack_page_params. + + (** #### Data stack in EraVM + +There are two stacks in EraVM: call stack to support the execution of functions +and contracts, and data stack to facilitate computations. This section details +the data stack. + +At each moment of execution, one stack page is active; it is associated with the +topmost of external frames, which belongs to the contract currently being +executed. See [%active_extframe], its field [%ecf_mem_ctx] and subfield +[%ctx_stack_page_id]. + +Each contract instance has an independent stack on a separate page. +Instead of zero, stack pointer on new stack pages start with a value +[%INITIAL_SP_ON_FAR_CALL]. Stack addresses in range [0; [%INITIAL_SP_ON_FAR_CALL]) can be used as a scratch space. + +Topmost frame of the callstack, whether internal or external, contains the stack +pointer (SP) value [%cf_sp]; which points to the address after the topmost element of +the stack. That means that the topmost element of the stack is located in word +number $(\mathit{SP}-1)$ on the associated stack page. + +Data stack grows towards greater addresses. +In other words, pushing to stack increases stack pointer value, and popping +elements decreases stack pointer. + +### Const pages + +A **const page** contains $2^{16}$ non tagged [%word]s. +They are not writable. + +Implementation may put constants and code on the same pages. +In this case, the bytes on the same virtual page can be addressed in two ways: + +- For instructions [%OpJump] and [%OpNearCall], the code addressing will be + used: consecutive addresses correspond to 8-bytes instructions. +- For instructions like [%OpAdd] with [%CodeAddr] addressing mode, the const + data addressing will be used: consecutive addresses correspond to 32-bytes + words. + +For example, [%OpJump 0], [%OpJump 1], [%OpJump 2], [%OpJump 3] will refer to +the first four instructions on the page; their binary representations, put +together, can be fetched by addressing the const page's 0-th word e.g. +[%OpAdd (CodeAddr R0 zero_16 ) (Reg R0) (Reg R1)]. + *) + Definition const_address_bits := 16. + + Definition const_page_params := {| + addressable_block := word; + address_bits := const_address_bits; + default_value := word0; + writable := false + |}. + Definition const_address := address const_page_params. + Definition const_page := mem_parameterized const_page_params. + + (** ### Code pages + +A **code page** contains $2^{16}$ instructions. +They are not writable. + +On genesis, code pages are filled as follows: + +- The contract code is places starting from the address 0. +- The rest is filled with a value guaranteed to decode as [%invalid] instruction. + +Const pages can coincide with code pages. *) + + Context {ins_type: Type} (invalid_ins: ins_type). + + (* Implementation note: [%code_address] should be [%address code_page_params] but we don't want to introduce + dependency between code_address and instruction type *) + Definition code_address_bits := 16. + Definition code_address := BITS code_address_bits. + Definition code_address_zero: stack_address := zero16. + + Definition code_page_params := {| + addressable_block := ins_type; + address_bits := code_address_bits; + default_value := invalid_ins; + writable := false + |}. + Record code_page := mk_code_page { + cp_insns:> mem_parameterized code_page_params; + }. + Definition code_length := code_address. + +End Memory. diff --git a/src/memory/Pages.v b/src/memory/Pages.v new file mode 100644 index 0000000..f570c2e --- /dev/null +++ b/src/memory/Pages.v @@ -0,0 +1,88 @@ +Require Common MemoryBase. +Import Common MemoryBase. + +Section Pages. + (** # Main memory (transient) +## Memory structure + +Contract execution routinely uses **main memory** to hold instructions, stack, +heaps, and constants. + +When the execution of a contract starts, new pages are allocated for: + +- contract code: [%code_page], fetched by decommitter; see [%Decommitter] and + [%FarCallDefinitions]); +- data stack: [%stack_page]; +- heap: [%data_page]; +- aux_heap: [%data_page]; +- constants: [%const_page], implementation may chose to allocate code and + constants on the same page. + +Therefore, the types of pages are: data pages, stack pages, constant data pages, +and code pages. **) + + Context {code_page const_page data_page stack_page: Type}. + + Inductive page_type := + | DataPage : data_page -> page_type + | StackPage : stack_page -> page_type + | ConstPage : const_page -> page_type + | CodePage : code_page -> page_type + . + + Record page := mk_page { + type:> page_type + }. + (** **Memory** is a collection of pages [%memory], each page is attributed a + unique identifier [%page_id]. Pages persist for as long as they can be read + by some code; in presence of [%FatPointer] the page lifetime may exceed the + lifetime of the frame that created it. *) + + Definition page_id := nat. + Definition pages := list (page_id * page). + Record memory := mk_pages { + mem_pages:> pages; + }. + + Inductive page_has_id : memory -> page_id -> page -> Prop := + | mpid_select : forall mm id page, + List.In (id, page) mm -> + page_has_id (mk_pages mm) id page. + + (** The set of identifiers has a complete linear order, ordering the pages + by the time of creation. The ability to distinguish older pages from newer + is necessary to prevent returning fat pointers to pages from older frames. + See e.g. [% step_RetExt_ForwardFatPointer]. *) + Section Order. + Definition page_ordering := Nat.leb. + Definition page_eq x y := page_ordering x y && page_ordering y x. + Definition page_neq x y := negb (page_eq x y). + Definition page_older (id1 id2: page_id) : bool := + page_ordering id1 id2. + End Order. + + (** Predicate [%page_replace] describes a relation between two memories + [%m1] and [%m2], where [%m2] is a copy of [%m1] but a page with it [%id] is + replaced + by another page [%p].*) + Inductive page_replace_list (id:page_id) (p:page): pages -> pages -> Prop := + | mm_replace_base: forall oldpage newpage tail, + page_replace_list id p ((id, oldpage)::tail) ((id,newpage)::tail) + | mm_replace_ind: forall oldpage not_id tail tail', + page_replace_list id p tail tail' -> + id <> not_id -> + page_replace_list id p ((not_id,oldpage)::tail) ((not_id,oldpage)::tail'). + + Inductive page_replace (id:page_id) (p:page): memory -> memory -> Prop := + | prl_apply: forall ls ls', + page_replace_list id p ls ls' -> + page_replace id p (mk_pages ls) (mk_pages ls'). + + (** Function [%page_alloc] creates a new page in memory. *) + Definition page_alloc (p:page) (m: memory) : memory := + let new_id := length (mem_pages m) in + match m with + | mk_pages mem_pages => mk_pages (cons (new_id, p) mem_pages) + end. + +End Pages. diff --git a/src/sem/Farcall.v b/src/sem/Farcall.v index 912d0d5..3408e39 100644 --- a/src/sem/Farcall.v +++ b/src/sem/Farcall.v @@ -53,7 +53,7 @@ Import Import Addressing.Coercions. Local Coercion Z.b2z: bool >-> Z. - +Section FarCalls. (** # Far calls Far calls are calls to the code outside the current contract space. @@ -701,3 +701,4 @@ Inductive step_farcall : instruction -> smallstep := step_transient_only ts1 ts2 s1 s2 -> step_farcall (OpDelegateCall (Some pv_abi) (mk_pv __ dest) handler call_shard call_as_static) s1 s2 . +End FarCalls.