L40->L50 stmt

Config.v

@@ -7,7 +7,7 @@ Class VyperConfig := {
   string_set_impl: FSet.class String.string_dec string_set;
   string_map: Type -> Type;
   string_map_impl: forall t: Type, Map.class String.string_dec t (string_map t);
-  world_state: Type;
+  world_state: Type; (* includes memory *)
   uint256: Type;
   Z_of_uint256: uint256 -> Z;
   uint256_of_Z: Z -> uint256;
@@ -18,6 +18,9 @@ Class VyperConfig := {
   memory: Type;
   memory_impl: OpenArray.class (uint256_of_Z 0%Z) memory;
   string_hash: string -> uint256;
+  mload: world_state -> uint256 -> uint256;
+  world_except_memory: Type;
+  get_world_except_memory: world_state -> world_except_memory;
 }.
 
 Lemma two_to_256_ne_0: (2^256 <> 0)%Z.
@@ -39,17 +42,21 @@ Definition sample_config
       string_set_impl := FSet.string_avl_set_impl;
       string_map := Map.string_avl_map;
       string_map_impl := Map.string_avl_map_impl;
-      world_state := Map.string_avl_map Z;
+      world_state := Map.string_avl_map Z * list Z;
       uint256 := Z;
       Z_of_uint256 u := (u mod 2^256)%Z;
       uint256_of_Z z := (z mod 2^256)%Z;
       uint256_ok z := Z.mod_mod _ _ two_to_256_ne_0;
       uint256_range u := Z.mod_pos_bound _ _ two_to_256_pos;
-      storage_lookup := let _ := Map.string_avl_map_impl in Map.lookup;
-      storage_insert := let _ := Map.string_avl_map_impl in Map.insert;
+      storage_lookup w := let _ := Map.string_avl_map_impl in Map.lookup (fst w);
+      storage_insert w key val := (let _ := Map.string_avl_map_impl in Map.insert (fst w) key val,
+                                   snd w);
       memory := list Z;
       memory_impl := OpenArray.list_inst 0%Z;
       string_hash := fun s => (Z.of_N (keccak_256_N_of_string s))%Z;
+      mload w addr := List.nth (Z.to_nat (addr mod 2^256)) (snd w) 0%Z;
+      world_except_memory := Map.string_avl_map Z;
+      get_world_except_memory := fst
    |}.
 
 Definition zero256 {C: VyperConfig} := uint256_of_Z 0%Z.

From40To50/Builtins.v

@@ -0,0 +1,49 @@
+From Coq Require Import String NArith ZArith DecimalString List Lia.
+
+From Vyper Require Import Config NaryFun.
+From Vyper.CheckArith Require Import Builtins.
+From Vyper.L10 Require Import Base.
+From Vyper.L40 Require AST.
+From Vyper.L50 Require AST.
+From Vyper.L50 Require Import Types Expr.
+
+From Vyper.L40Metered Require Import Interpret.
+
+From Vyper.From40To50 Require Import Translate Proto.
+
+(* We need to wrap L50 builtins into L40 versions
+   that perform the same typechecks that the L50 interpreter does.
+
+   This is not really necessary with the default list of builtins which is all u256-typed
+   (address is not a Yul type and is not typechecked).
+ *)
+
+(**
+  Typecheck each argument of a [nary_fun].
+  Equivalent to running [L50.Builtins.mass_typecheck] before calling
+  except no length check on input_types is performed.
+ *)
+Fixpoint embed_typechecks {C: VyperConfig}
+                          {arity: nat}
+                          {ReturnType: Type}
+                          (f: NaryFun.nary_fun uint256 arity (world_state * expr_result ReturnType))
+                          (input_types: list yul_type)
+                          (world: world_state)
+: NaryFun.nary_fun uint256 arity (world_state * expr_result ReturnType)
+:= match arity, f with
+   | 0, result  => result
+   | S arity', g =>
+      match input_types with
+      | nil => g
+      | (head_type :: tail_types)%list =>
+          fun arg =>
+            embed_typechecks 
+      end
+   end.
+
+(*
+L10.Base.builtin
+L50.Builtins.yul_builtin
+L10.Base.call_builtin
+L50.Builtins.call_builtin
+*)

From40To50/Expr.v

@@ -52,37 +52,6 @@ refine (local_vars_agree_weaken _ Ok).
 lia.
 Qed.
 
-(** Value agreement between L40 and L50.
-    [n]: expected length of [e50]
-    The tricky part here is that L50 might have no value where L40 sees zero. 
- *)
-Definition ExprResultsAgree {C: VyperConfig}
-                            (e40: expr_result uint256)
-                            (e50: expr_result (list dynamic_value))
-                            (n: N)
-:= match e40, e50 with
-   | ExprAbort a40, ExprAbort a50               =>  a40 = a50
-   | ExprSuccess v40, ExprSuccess nil           =>  Z_of_uint256 v40 = 0%Z /\ n = 0%N
-   | ExprSuccess v40, ExprSuccess (v50 :: nil)  =>  (* v40 = uint256_of_dynamic_value v50 *)
-                                                    v50 = (existT _ U256 (yul_uint256 v40)) /\ n = 1%N
-   | _, _ => False
-   end.
-
-
-(** Value agreement between L40 and L50, a variant with u256 list on the L50 side.
-    [n]: expected length of [e50]
-    The tricky part here is that L50 might have no value where L40 sees zero.
- *)
-Definition ExprResultsAgree256 {C: VyperConfig}
-                               (e40: expr_result uint256)
-                               (e50: expr_result (list uint256))
-                               (n: N)
-:= match e40, e50 with
-   | ExprAbort a40, ExprAbort a50               =>  a40 = a50
-   | ExprSuccess v40, ExprSuccess nil           =>  Z_of_uint256 v40 = 0%Z /\ n = 0%N
-   | ExprSuccess v40, ExprSuccess (v50 :: nil)  =>  v40 = v50 /\ n = 1%N
-   | _, _ => False
-   end.
 
 (** Same as [ExprResultsAgree] but lifted to [world_state * option]. *)
 Definition ResultsAgree {C: VyperConfig}
@@ -154,41 +123,6 @@ Definition LoopCursorsAgree {C: VyperConfig}
      end.
 
 
-Definition BuiltinsAgree {C: VyperConfig}
-                         (b40: builtin)
-                         (b50: L50.Builtins.yul_builtin)
-                         (B50InputsU256:   L50.Builtins.all_are_u256 (L50.Builtins.b_input_types  b50) = true)
-                         (B50OutputssU256: L50.Builtins.all_are_u256 (L50.Builtins.b_output_types b50) = true)
-:= let '(existT _ arity f40) := b40 in
-       arity = List.length (L50.Builtins.b_input_types b50)
-        /\
-       forall (world: world_state) (args: list uint256)
-              (LenOk40: arity =? List.length args = true)
-              (LenOk50: List.length (Builtins.b_input_types b50) = List.length args),
-         let (w40, e40) := (call_builtin args LenOk40 (f40 world)) in
-         let (w50, e50) := (call_builtin_u256 b50 world args LenOk50) in
-         w40 = w50  /\  ExprResultsAgree256 e40 e50 
-                                            (N.of_nat (List.length (L50.Builtins.b_output_types b50))).
-
-Definition AllBuiltinsAgreeIfU256 {C: VyperConfig}
-                                  (builtins40: string -> option builtin)
-                                  (builtins50: string -> option L50.Builtins.yul_builtin)
-:= forall name: string,
-     match builtins50 name with
-     | None => True
-     | Some b50 =>
-        (if L50.Builtins.all_are_u256 (L50.Builtins.b_input_types b50) as z return _ = z -> _
-         then 
-           fun i256 =>
-            (if L50.Builtins.all_are_u256 (L50.Builtins.b_output_types b50) as z return _ = z -> _
-              then fun o256 =>
-                   match builtins40 name with
-                   | None => False
-                   | Some b40 => BuiltinsAgree b40 b50 i256 o256
-                   end
-              else fun _ => True) eq_refl
-         else fun _ => True) eq_refl
-     end.
 
 Lemma if_yes_prop cond yes no
                   (E: cond = true):

From40To50/Mangle.v

@@ -0,0 +1,141 @@
+From Coq Require Import Ascii String List NArith DecimalString DecimalN DecimalPos.
+
+From Vyper Require Import Config.
+From Vyper.CheckArith Require Import Builtins.
+From Vyper.L10 Require Import Base.
+
+From Vyper.From40To50 Require Import Translate Proto.
+
+
+Definition starts_with_dollar (s: string)
+: bool
+:= match s with
+   | String "$"%char _ => true
+   | _ => false
+   end.
+
+Lemma starts_with_dollar_eqb (head: ascii) (tail: string):
+  starts_with_dollar (String head tail) = Ascii.eqb head "$"%char.
+Proof.
+cbn.
+destruct head as (b0, b1, b2, b3, b4, b5, b6, b7).
+now destruct b0, b1, b2, b3, b4, b5, b6, b7.
+Qed.
+
+(** [translate_fun_decls] prefixes everything with '$'. *)
+Lemma translated_decls_start_with_dollar {C: VyperConfig}
+                                {B: builtin_names_config}
+                                {protos: string_map proto}
+                                (decls40: string_map L40.AST.decl)
+                                (decls50: string_map L50.AST.fun_decl)
+                                (DeclsOk: translate_fun_decls B protos decls40 = inr decls50)
+                                (name: string)
+                                (Ok: map_lookup decls50 name <> None):
+  starts_with_dollar name = true.
+Proof.
+unfold translate_fun_decls in DeclsOk.
+remember (Map.items decls40) as items40. clear Heqitems40.
+revert decls50 DeclsOk Ok.
+induction items40 as [|(k,v)]; intros; cbn in DeclsOk.
+{
+  inversion DeclsOk. subst. unfold map_lookup in Ok.
+  now rewrite Map.empty_lookup in Ok.
+}
+destruct (translate_fun_decl B protos v). { discriminate. }
+destruct alist_maybe_map_kv. { discriminate. }
+cbn in DeclsOk. inversion DeclsOk. subst. clear DeclsOk.
+unfold map_lookup in Ok. rewrite Map.insert_ok in Ok.
+remember (string_dec (String "$" k) name) as found.
+destruct found. { now subst. }
+unfold map_lookup in IHitems40.
+now refine (IHitems40 _ _ Ok).
+Qed.
+
+(** The same as the previous one but more convenient to use for builtins. *)
+Lemma unmangled_names_are_not_translated {C: VyperConfig}
+                                         {B: builtin_names_config}
+                                         {protos: string_map proto}
+                                         (decls40: string_map L40.AST.decl)
+                                         (decls50: string_map L50.AST.fun_decl)
+                                         (DeclsOk: translate_fun_decls B protos decls40 = inr decls50)
+                                         (name: string)
+                                         (Ok: starts_with_dollar name = false):
+  map_lookup decls50 name = None.
+Proof.
+remember (map_lookup decls50 name) as d. destruct d; trivial.
+assert (NE: map_lookup decls50 name <> None). { rewrite<- Heqd. discriminate. }
+rewrite (translated_decls_start_with_dollar decls40 decls50 DeclsOk name NE) in Ok.
+discriminate.
+Qed.
+
+Lemma mangled_safety_equiv {T} (builtins: string -> option T):
+  (forall x, builtins ("$" ++ x)%string = None)
+   <->
+  (forall x, builtins x <> None -> starts_with_dollar x = false).
+Proof.
+cbn.
+split.
+{
+  intros H x Ok.
+  destruct x as [|head]. { easy. }
+  rewrite starts_with_dollar_eqb.
+  cbn.
+  remember ((head =? "$")%char) as head_is_dollar. destruct head_is_dollar. 2:trivial.
+  symmetry in Heqhead_is_dollar. apply Ascii.eqb_eq in Heqhead_is_dollar.
+  subst. exfalso. exact (Ok (H x)).
+}
+intros H x.
+assert (Ok := H (String "$"%char x)). clear H.
+remember (builtins (String "$" x)) as b. destruct b. 2:trivial.
+clear Heqb. cbn in Ok. exfalso. assert (W: Some t <> None) by discriminate.
+assert (Ok' := Ok W). discriminate.
+Qed.
+
+(***************************************************************************************************)
+
+(* not in standard library? oh well *)
+Lemma string_app_l_inj (a b c: string)
+                       (E: (a ++ b = a ++ c)%string):
+  b = c.
+Proof.
+induction a as [|h]. { easy. }
+cbn in E. inversion E. tauto.
+Qed.
+
+(* why is it not in stdlib? *)
+Lemma to_uint_nonnil (a: N):
+  N.to_uint a <> Decimal.Nil.
+Proof.
+destruct a as [|p]. { easy. }
+cbn. apply Unsigned.to_uint_nonnil.
+Qed.
+
+Lemma string_of_N_inj (a b: N)
+                      (E: NilZero.string_of_uint (N.to_uint a)
+                           =
+                          NilZero.string_of_uint (N.to_uint b)):
+  a = b.
+Proof.
+assert (UsuA := NilZero.usu (N.to_uint a) (to_uint_nonnil a)).
+assert (UsuB := NilZero.usu (N.to_uint b) (to_uint_nonnil b)).
+apply DecimalN.Unsigned.to_uint_inj.
+enough (Q: Some (N.to_uint a) = Some (N.to_uint b)) by now inversion Q.
+rewrite<- UsuA. rewrite<- UsuB.
+now rewrite E.
+Qed.
+
+Lemma make_var_name_inj (prefix: string) (a b: N)
+                        (E: make_var_name prefix a = make_var_name prefix b):
+  a = b.
+Proof.
+cbn in E. inversion E. apply string_of_N_inj.
+apply string_app_l_inj with (a := prefix). assumption.
+Qed.
+
+Lemma make_var_name_inj' (prefix: string) (a b: N)
+                         (NE: a <> b):
+  make_var_name prefix a <> make_var_name prefix b.
+Proof.
+intro E. apply NE.
+exact (make_var_name_inj prefix a b E).
+Qed.