Move contract states into environment

Remove it from the contract's perspective for now.

theories/Blockchain.v

@@ -73,7 +73,6 @@ Record Chain :=
     current_slot : nat;
     finalized_height : nat;
     account_balance : Address -> Amount;
-    contract_state : Address -> option SerializedValue;
   }.
 
 (* Two chains are said to be equivalent if they are extensionally equal.
@@ -85,7 +84,6 @@ Record ChainEquiv (c1 c2 : Chain) : Prop :=
     current_slot_eq : current_slot c1 = current_slot c2;
     finalized_height_eq : finalized_height c1 = finalized_height c2;
     account_balance_eq : forall addr, account_balance c1 addr = account_balance c2 addr;
-    contract_state_eq : forall addr, contract_state c1 addr = contract_state c2 addr;
   }.
 
 Global Program Instance chain_equiv_equivalence : Equivalence ChainEquiv.
@@ -105,9 +103,6 @@ Proof. repeat intro; auto using finalized_height_eq. Qed.
 Global Instance chain_equiv_account_balance_proper :
   Proper (ChainEquiv ==> eq ==> eq) account_balance.
 Proof. repeat intro; subst; auto using account_balance_eq. Qed.
-Global Instance chain_equiv_contract_state_proper :
-  Proper (ChainEquiv ==> eq ==> eq) contract_state.
-Proof. repeat intro; subst; auto using contract_state_eq. Qed.
 
 Record ContractCallContext :=
   build_ctx {
@@ -270,37 +265,31 @@ Definition create_deployment
 (* The contract interface is the main mechanism allowing a deployed
 contract to interact with another deployed contract. This hides
 the ugly details of everything being SerializedValue away from contracts. *)
-Record ContractInterface {Msg State : Type} :=
+Record ContractInterface {Msg : Type} :=
   build_contract_interface {
     (* The address of the contract being interfaced with *)
     contract_address : Address;
-    (* Obtain the state at some point of time *)
-    get_state : Chain -> option State;
     (* Make an action sending money and optionally a message to the contract *)
     send : Amount -> option Msg -> ActionBody;
   }.
 
-Arguments ContractInterface _ _ : clear implicits.
+Arguments ContractInterface _ : clear implicits.
 
 Definition get_contract_interface
-          (chain : Chain)
-          (addr : Address)
-          (Msg State : Type)
-          `{Serializable Msg}
-          `{Serializable State}
-  : option (ContractInterface Msg State) :=
-  let ifc_get_state chain := contract_state chain addr >>= deserialize in
+          (chain : Chain) (addr : Address)
+          (Msg : Type) `{Serializable Msg}
+  : option (ContractInterface Msg) :=
   let ifc_send amount msg :=
       match msg with
       | None => act_transfer addr amount
       | Some msg => act_call addr amount (serialize msg)
       end in
-  Some {| contract_address := addr; get_state := ifc_get_state; send := ifc_send; |}.
+  Some {| contract_address := addr; send := ifc_send; |}.
 
 Section Semantics.
 Instance chain_settable : Settable _ :=
-  settable! build_chain <chain_height; current_slot; finalized_height;
-                         account_balance; contract_state>.
+  settable! build_chain
+  <chain_height; current_slot; finalized_height; account_balance>.
 
 Definition add_balance (addr : Address) (amount : Amount) (map : Address -> Amount) :
   Address -> Amount :=
@@ -320,6 +309,7 @@ Record Environment :=
   build_env {
     env_chain :> Chain;
     env_contracts : Address -> option WeakContract;
+    env_contract_states : Address -> option SerializedValue;
   }.
 
 (* Furthermore we define extensional equality for such environments. *)
@@ -327,6 +317,7 @@ Record EnvironmentEquiv (e1 e2 : Environment) : Prop :=
   build_env_equiv {
     chain_equiv : ChainEquiv e1 e2;
     contracts_eq : forall a, env_contracts e1 a = env_contracts e2 a;
+    contract_states_eq : forall addr, env_contract_states e1 addr = env_contract_states e2 addr;
   }.
 
 Global Program Instance environment_equiv_equivalence : Equivalence EnvironmentEquiv.
@@ -345,12 +336,16 @@ Global Instance environment_equiv_contracts_proper :
   Proper (EnvironmentEquiv ==> eq ==> eq) env_contracts.
 Proof. repeat intro; subst; apply contracts_eq; assumption. Qed.
 
+Global Instance environment_equiv_contract_states_proper :
+  Proper (EnvironmentEquiv ==> eq ==> eq) env_contract_states.
+Proof. repeat intro; subst; apply contract_states_eq; assumption. Qed.
+
 Global Instance environment_equiv_chain_equiv_proper :
   Proper (EnvironmentEquiv ==> ChainEquiv) env_chain.
 Proof. repeat intro; apply chain_equiv; assumption. Qed.
 
 Instance env_settable : Settable _ :=
-  settable! build_env <env_chain; env_contracts>.
+  settable! build_env <env_chain; env_contracts; env_contract_states>.
 
 Definition transfer_balance (from to : Address) (amount : Amount) (env : Environment) :=
   env<|env_chain; account_balance ::= add_balance to amount|>
@@ -366,7 +361,7 @@ Definition add_contract (addr : Address) (contract : WeakContract) (env : Enviro
 
 Definition set_contract_state
            (addr : Address) (state : SerializedValue) (env : Environment) :=
-  env<|env_chain; contract_state ::= set_chain_contract_state addr state|>.
+  env<|env_contract_states ::= set_chain_contract_state addr state|>.
 
 Ltac rewrite_environment_equiv :=
   match goal with
@@ -375,7 +370,7 @@ Ltac rewrite_environment_equiv :=
 
 Ltac solve_proper :=
   apply build_env_equiv;
-  [apply build_chain_equiv|];
+  [apply build_chain_equiv| |];
   cbn;
   repeat intro;
   repeat rewrite_environment_equiv;
@@ -463,7 +458,7 @@ Inductive ActionEvaluation :
              (resp_acts : list ActionBody),
       amount <= account_balance pre from ->
       env_contracts pre to = Some wc ->
-      contract_state pre to = Some prev_state ->
+      env_contract_states pre to = Some prev_state ->
       act = build_act from (match msg with
                             | None => act_transfer to amount
                             | Some msg => act_call to amount msg
@@ -652,8 +647,8 @@ Definition empty_state : ChainState :=
             {| chain_height := 0;
                current_slot := 0;
                finalized_height := 0;
-               account_balance a := 0%Z;
-               contract_state a := None; |};
+               account_balance a := 0%Z; |};
+          env_contract_states a := None;
           env_contracts a := None; |};
      chain_state_queue := [] |}.
 
@@ -936,7 +931,7 @@ End Blockchain.
 Arguments init {_ _ _ _ _ _ _}.
 Arguments receive {_ _ _ _ _ _ _}.
 Arguments build_contract {_ _ _ _ _ _ _}.
-Arguments ContractInterface {_} _ _.
+Arguments ContractInterface {_} _.
 Arguments build_contract_interface {_ _ _ _}.
 
 Ltac destruct_chain_step :=

theories/Congress.v

@@ -388,8 +388,8 @@ Definition num_acts_created_in_proposals (txs : list Tx) :=
 Definition num_cacts_in_raw_state state :=
   sumnat (fun '(k, v) => length (actions v)) (FMap.elements (proposals state)).
 
-Definition num_cacts_in_state chain address :=
-  match contract_state chain address >>= deserialize with
+Definition num_cacts_in_state env address :=
+  match env_contract_states env address >>= deserialize with
   | Some state => num_cacts_in_raw_state state
   | None => 0
   end.
@@ -402,12 +402,10 @@ Definition num_outgoing_acts l address :=
   sumnat extract l.
 
 Instance num_cacts_in_state_proper :
-  Proper (ChainEquiv ==> eq ==> eq) num_cacts_in_state.
+  Proper (EnvironmentEquiv ==> eq ==> eq) num_cacts_in_state.
 Proof.
   now repeat intro; subst; unfold num_cacts_in_state;
-    match goal with
-    | [H: ChainEquiv _ _ |- _] => rewrite H
-    end.
+    rewrite_environment_equiv.
 Qed.
 
 Lemma num_outgoing_acts_app q1 q2 address :
@@ -613,7 +611,7 @@ Lemma wc_receive_state_well_behaved
       from contract amount prev state ctx msg new_state resp_acts
       (trace : ChainTrace empty_state prev) :
   let with_tx := transfer_balance from contract amount prev in
-  contract_state prev contract = Some state ->
+  env_contract_states prev contract = Some state ->
   wc_receive
     Congress.contract
     with_tx
@@ -643,7 +641,7 @@ Proof.
   cbn.
   unfold set_chain_contract_state.
   rewrite address_eq_refl.
-  replace (contract_state _ contract) with (Some state) by auto.
+  replace (env_contract_states _ contract) with (Some state) by auto.
   cbn.
   rewrite deserialize_state, deserialize_serialize.
   fold (num_acts_created_in_proposals (incoming_txs trace contract)).
@@ -694,6 +692,7 @@ Local Ltac solve_single :=
   solve [
       repeat (progress subst; cbn in *; auto);
       unfold add_balance, num_cacts_in_state, num_acts_created_in_proposals, num_outgoing_acts;
+      cbn;
       unfold set_chain_contract_state;
       cbn;
       try rewrite address_eq_refl;
@@ -802,7 +801,7 @@ Proof.
         destruct (address_eqb_spec from contract);
           simpl_goal_invariant;
           simpl_hyp_invariant;
-        cbn; lia.
+          cbn; lia.
       * (* This is deployment of this contract *)
         replace wc with (Congress.contract : WeakContract) in * by congruence.
         (* State starts at 0 *)
@@ -837,7 +836,7 @@ Proof.
         subst to.
         match goal with
         | [H1: wc_receive _ _ _ _ _ = Some _,
-           H2: contract_state _ _ = Some _ |- _] =>
+           H2: env_contract_states _ _ = Some _ |- _] =>
           generalize (wc_receive_state_well_behaved _ _ _ _ _ _ _ _ _ steps H2 H1)
         end.
         simpl_goal_invariant.

theories/LocalBlockchain.v

@@ -51,9 +51,9 @@ Definition lc_to_env (lc : LocalChain) : Environment :=
         {| chain_height := lc_height lc;
            current_slot := lc_slot lc;
            finalized_height := lc_fin_height lc;
-           account_balance a := with_default 0%Z (FMap.find a (lc_account_balances lc));
-           contract_state a := FMap.find a (lc_contract_state lc); |};
-      env_contracts a := FMap.find a (lc_contracts lc); |}.
+           account_balance a := with_default 0%Z (FMap.find a (lc_account_balances lc)); |};
+     env_contract_states a := FMap.find a (lc_contract_state lc);
+     env_contracts a := FMap.find a (lc_contracts lc); |}.
 
 Global Coercion lc_to_env : LocalChain >-> Environment.
 
@@ -98,7 +98,7 @@ Section ExecuteActions.
         | Some msg => None
       end
     | Some wc =>
-      do state <- contract_state lc to;
+      do state <- env_contract_states lc to;
       let lc := transfer_balance from to amount lc in
       let ctx := build_ctx from to amount in
       do '(new_state, new_actions) <- wc_receive wc  lc ctx state msg;
@@ -234,7 +234,7 @@ Section ExecuteActions.
       [cbn in *; congruence|].
     destruct (FMap.find to (lc_contracts lc_before)) as [wc|] eqn:to_contract.
     - (* there is a contract at destination, so do call *)
-      destruct (contract_state _ _) as [prev_state|] eqn:prev_state_eq;
+      destruct (env_contract_states _ _) as [prev_state|] eqn:prev_state_eq;
         [|cbn in *; congruence].
       cbn -[lc_to_env] in *.
       destruct (wc_receive wc _ _ _ _) eqn:receive;

theories/LocalBlockchainTests.v

@@ -5,6 +5,7 @@ From SmartContracts Require Import Congress.
 From SmartContracts Require Import Containers.
 From SmartContracts Require Import BoundedN.
 From SmartContracts Require Import Extras.
+From SmartContracts Require Import Serializable.
 From RecordUpdate Require Import RecordUpdate.
 From Coq Require Import List.
 From Coq Require Import ZArith.
@@ -75,23 +76,19 @@ Section LocalBlockchainTests.
   Compute (account_balance chain4 creator).
   Compute (account_balance chain4 congress_1).
 
-  Definition congress_ifc
-    : ContractInterface Congress.Msg Congress.State :=
-    match get_contract_interface
-            chain4 congress_1
-            Congress.Msg Congress.State with
+  Definition congress_ifc : ContractInterface Congress.Msg :=
+    match get_contract_interface chain4 congress_1 Congress.Msg with
     | Some x => x
     (* Using unpack_option here is extremely slow *)
     | None =>
       @build_contract_interface
-        _ _ _
+        _ _
         creator
-        (fun c => None)
         (fun a m => deploy_congress)
     end.
 
-  Definition congress_state chain : Congress.State :=
-    match congress_ifc.(get_state) chain with
+  Definition congress_state lc : Congress.State :=
+    match env_contract_states lc congress_1 >>= deserialize with
     | Some s => s
     (* And also here *)
     | None => {| owner := creator;
@@ -101,7 +98,7 @@ Section LocalBlockchainTests.
                  members := FMap.empty |}
     end.
 
-  Compute (congress_ifc.(get_state) chain4).
+  Compute (congress_state chain4).
   Compute (FMap.elements (congress_state chain4).(members)).
 
   (* person_1 adds person_1 and person_2 as members of congress *)