Work on adapting LocalBlockchain

src/Blockchain.v

@@ -9,13 +9,13 @@ From SmartContracts Require Import Extras.
 From SmartContracts Require Import Automation.
 Import ListNotations.
 
-Definition Address := positive.
+Definition Address := N.
 Delimit Scope address_scope with address.
 Bind Scope address_scope with Address.
 
 Module Address.
-  Definition eqb := Pos.eqb.
-  Definition eq_dec := Pos.eq_dec.
+  Definition eqb := N.eqb.
+  Definition eq_dec := N.eq_dec.
 End Address.
 
 Infix "=?" := Address.eqb (at level 70) : address_scope.
@@ -83,12 +83,14 @@ Class ChainType :=
 
     valid_address : Address -> Prop;
 
+    (*
     no_incoming_txs
       (t : chain_type) (a : Address) : ~valid_address a -> incoming_txs t a = [];
     no_outgoing_txs
       (t : chain_type) (a : Address) : ~valid_address a -> outgoing_txs t a = [];
     no_contract_state
       (t : chain_type) (a : Address) : ~valid_address a -> contract_state t a = None;
+*)
   }.
 
 Coercion chain_type : ChainType >-> Sortclass.
@@ -97,6 +99,14 @@ Coercion chain_type : ChainType >-> Sortclass.
 Context {Chain : ChainType}.
 Local Open Scope Z.
 
+(* Define chains with finite address spaces *)
+Class FiniteAddressSpace :=
+  {
+    valid_addresses : list Address;
+    valid_addresses_set : NoDup valid_addresses;
+    valid_addresses_all : forall a, valid_address a -> In a valid_addresses;
+  }.
+
 Definition account_balance (chain : Chain) (addr : Address)
   : Amount :=
   let sum_amounts txs := sumZ tx_amount txs in
@@ -429,10 +439,13 @@ Definition IntActReflectsExtAct
     | iact_empty, act_transfer ext_to ext_amount
     | iact_call None, act_transfer ext_to ext_amount =>
       iact_to = ext_to /\ iact_amount = ext_amount
+
     | iact_deploy iact_wc iact_setup, act_deploy ext_amount ext_wc ext_setup =>
       iact_amount = ext_amount /\ iact_wc = ext_wc /\ iact_setup = ext_setup
+
     | iact_call (Some iact_msg), act_call ext_to ext_amount ext_msg =>
       ext_to = iact_to /\ ext_amount = iact_amount /\ ext_msg = iact_msg
+
     | _, _ => False
   end.
 
@@ -514,7 +527,9 @@ Inductive ChainTrace : Environment -> Environment -> Prop :=
       ChainTrace block_added post ->
       ChainTrace pre post.
 
-(* todo: soundness *)
+(* todo: this is meant to model whether one trace is an extension with the
+specified parameters of another. This is used to model soundness of
+builder_add_block below. *)
 Inductive IsTraceExtension
           {pre mid post : Environment}
           (extension : ChainTrace pre post)
@@ -564,8 +579,15 @@ Class ChainBuilderType :=
 Coercion builder_type : ChainBuilderType >-> Sortclass.
 End Blockchain.
 
+Hint Resolve valid_addresses_set valid_addresses_all.
+
+Arguments FiniteAddressSpace : clear implicits.
 Arguments Transfer {_} _ _ _.
 Arguments EmptyTransfer {_} _ _ _.
 Arguments CallTransfer {_} _ _ _.
 Arguments DeployTransfer {_} _ _ _.
 Arguments BlockTransfer {_} _ _ _.
+Arguments version {_ _ _ _ _ _ _} contract : rename.
+Arguments init {_ _ _ _ _ _ _} contract ctx setup : rename.
+Arguments receive {_ _ _ _ _ _ _} contract ctx state msg : rename.
+Arguments build_contract {_ _ _ _ _ _ _}.

src/Circulation.v

@@ -2,27 +2,19 @@
 chain implementing a chain type. More specifically, we show that the circulation
 does not change during execution of blocks. This is proven under the (implicit)
 assumption that the address space is finite. *)
-From Coq Require Import List Permutation.
+From Coq Require Import List Permutation ZArith.
 From SmartContracts Require Import Automation Blockchain Extras.
 Import ListNotations.
 
 Section Circulation.
 Context {Chain : ChainType}.
+Context `{!FiniteAddressSpace Chain}.
 
-(* First, we must define the circulation. We will define it as a finite
-sum of the balance over all valid addresses. This is where the assumption
-about finite address space comes into play. With some work this result could
-be improved to assume only that the set of addresses which has seen transactions
-is finite. *)
-Definition IsSetOfAllAddresses (addrs : list Address) : Prop :=
-  NoDup addrs /\ forall a, valid_address a -> In a addrs.
-
-Context {addrs : list Address} (all_addrs : IsSetOfAllAddresses addrs).
-
-Definition circulation (chain : Chain) := sumZ (account_balance chain) addrs.
+Definition circulation (chain : Chain) :=
+  sumZ (account_balance chain) valid_addresses.
 
 (* We then prove that over any single step, the circulation is preserved.
-The idea behind this proof is that all_addrs contain from and to so
+The idea behind this proof is that addrs contain from and to so
 we can move them to the beginning of the sum and it easily follows that
 the sum of their balances is the same as before. For the rest of the
 list the total balance will then not be affected which follows by induction. *)
@@ -30,13 +22,12 @@ Lemma transfer_reorganize
       {pre post : Environment}
       {act : InternalAction}
       (transfer : Transfer act pre post)
-  : exists suf, Permutation ([iact_from act; iact_to act] ++ suf) addrs.
+  : exists suf, Permutation ([iact_from act; iact_to act] ++ suf) valid_addresses.
 Proof.
   pose proof (valid_address_from transfer).
   pose proof (valid_address_to transfer).
   pose proof (from_neq_to transfer).
-  unfold IsSetOfAllAddresses in *.
-  apply (NoDup_incl_reorganize _ ([iact_from act; iact_to act]));
+  apply (NoDup_incl_reorganize _ [iact_from act; iact_to act]);
     repeat constructor; unfold incl; prove.
 Qed.
 
@@ -54,8 +45,7 @@ Proof.
   rewrite (account_balance_to_pre_post transfer).
   enough (sumZ (account_balance pre) suf = sumZ (account_balance post) suf) by prove.
 
-  destruct all_addrs as [addrs_set all_addrs_in].
-  pose proof (Permutation_NoDup perm addrs_set) as perm_set.
+  pose proof (Permutation_NoDup perm valid_addresses_set) as perm_set.
   assert (from_not_in_suf: ~In (iact_from act) suf).
   { apply (in_NoDup_app _ [iact_from act; iact_to act] _); prove. }
   assert (to_not_in_suf: ~In (iact_to act) suf).

src/Congress.v

@@ -7,13 +7,15 @@ From SmartContracts Require Import Oak.
 From SmartContracts Require Import Monads.
 From SmartContracts Require Import Containers.
 From RecordUpdate Require Import RecordUpdate.
-(* This is included last to default things to list rather than map/set *)
 From Coq Require Import List.
 
 Import ListNotations.
 Import RecordSetNotations.
 
-Open Scope Z.
+Section Congress.
+Context {Chain : ChainType}.
+
+Local Open Scope Z.
 Set Primitive Projections.
 
 Definition ProposalId := nat.

src/Extras.v

@@ -3,6 +3,7 @@ From Coq Require Import List.
 From Coq Require Import Permutation.
 From Coq Require Import Morphisms.
 From Coq Require Import Psatz.
+From Coq Require Import Eqdep_dec.
 From SmartContracts Require Import Automation.
 Import ListNotations.
 
@@ -92,3 +93,21 @@ Proof.
   rewrite app_assoc in nodup_l_app_m.
   generalize in_or_app; prove.
 Qed.
+
+Section N.
+  Local Open Scope N.
+
+  Lemma N_lt_dec (p1 p2 : N) :
+    {p1 < p2} + {~(p1 < p2)}.
+  Proof.
+    unfold "<".
+    decide equality.
+  Qed.
+
+  Lemma N_lt_proofirrelevant (p1 p2 : N) (pf1 pf2 : p1 < p2) :
+    pf1 = pf2.
+  Proof.
+    apply UIP_dec.
+    decide equality.
+  Qed.
+End N.

src/LocalBlockchain.v

@@ -4,12 +4,52 @@ From SmartContracts Require Import Oak.
 From SmartContracts Require Import Monads.
 From SmartContracts Require Import Containers.
 From SmartContracts Require Import Extras.
+From SmartContracts Require Import Automation.
 From RecordUpdate Require Import RecordUpdate.
 From Coq Require Import List.
+From stdpp Require countable.
 
 Import RecordSetNotations.
 Import ListNotations.
 
+(*
+(* Very important we use < here because it is defined as a decidable equality. *)
+Definition LCAddress := { n : N | n < 2^128 }%N.
+
+Module LCAddressCountable.
+  Import countable.
+
+  Instance LCAddress_countable : Countable LCAddress.
+  Proof.
+    refine {| encode n := encode (proj1_sig n);
+              decode n :=
+                do n' <- (decode n : option N);
+                _; |}.
+    Unshelve. all: cycle 1.
+    - destruct (N_lt_dec n' (2^128)%N).
+      + exact (Some (exist _ n' l)).
+      + exact None.
+    - intros x.
+      rewrite decode_encode.
+      destruct x as [x lt].
+      simpl.
+      destruct (N_lt_dec x (N.pos (2^128))).
+      + rewrite (N_lt_proofirrelevant _ _ lt l).
+        reflexivity.
+      + contradiction.
+  Qed.
+End LCAddressCountable.
+
+Definition lc_addr (n : N) : (if (n <? 2^128)%N then LCAddress else unit).
+Proof.
+  unfold "<?"%N.
+  destruct (n ?= 2^128)%N eqn:n_comp.
+  - exact tt.
+  - exact (exist _ n n_comp).
+  - exact tt.
+Qed.
+*)
+
 Record ChainUpdate :=
   build_chain_update {
     (* Contracts that had their states updated and the new state *)
@@ -36,35 +76,16 @@ Record LocalChain :=
     lc_updates : list ChainUpdate;
   }.
 
+Definition genesis_block : Block :=
+  {| block_header := {| block_number := 0;
+                        block_coinbase := 0%N; |};
+     block_txs := [] |}.
+
 Instance eta_local_chain : Settable _ :=
   mkSettable
     ((constructor build_local_chain) <*> lc_blocks
                                      <*> lc_updates)%settable.
 
-(* Contains full information about a chain, including contracts *)
-Record LocalChainBuilder :=
-  build_local_chain_builder {
-    lcb_lc : LocalChain;
-    lcb_ftxs : list (BlockId * FullTx);
-  }.
-
-Instance eta_local_chain_builder : Settable _ :=
-  mkSettable
-    ((constructor build_local_chain_builder) <*> lcb_lc
-                                             <*> lcb_ftxs)%settable.
-
-Definition genesis_block : Block :=
-  {| block_header := {| block_number := 0; |};
-     block_txs := [] |}.
-
-Definition initial_chain_builder : LocalChainBuilder :=
-  {| lcb_lc := {| lc_blocks := [genesis_block];
-                  lc_updates :=
-                    [{| upd_contracts := FMap.empty;
-                        upd_txs := [] |}] |};
-     lcb_ftxs := [];
-  |}.
-
 Definition lc_chain_at (lc : LocalChain) (bid : BlockId) : option LocalChain :=
   let is_old '(b, u) := b.(block_header).(block_number) <=? bid in
   let zipped := rev (combine (rev lc.(lc_blocks)) (rev lc.(lc_updates))) in
@@ -101,113 +122,138 @@ Definition lc_contract_state (lc : LocalChain) (addr : Address)
   : option OakValue :=
   find_first (fun u => FMap.find addr u.(upd_contracts)) lc.(lc_updates).
 
-Definition lc_interface : ChainInterface :=
-  {| ci_type := LocalChain;
-     ci_chain_at := lc_chain_at;
-     ci_head_block := lc_head_block;
-     ci_incoming_txs := lc_incoming_txs;
-     ci_outgoing_txs := lc_outgoing_txs;
-     ci_contract_state := lc_contract_state;
+Instance lc_type : ChainType :=
+  {| chain_type := LocalChain;
+     chain_at := lc_chain_at;
+     head_block := lc_head_block;
+     incoming_txs := lc_incoming_txs;
+     outgoing_txs := lc_outgoing_txs;
+     contract_state := lc_contract_state;
+     valid_address a := True;
   |}.
 
+Definition lc_initial_chain : LocalChain :=
+  {| lc_blocks := [genesis_block];
+     lc_updates :=
+       [{| upd_contracts := FMap.empty;
+           upd_txs := [] |}] |}.
+
+(* Contains full information about a chain, including contracts *)
+Record LocalChainBuilder :=
+  build_local_chain_builder {
+    lcb_lc : LocalChain;
+    lcb_contracts : FMap Address WeakContract;
+    (*
+    lcb_trace : ChainTrace
+                  (build_env lc_initial_chain (fun a => None))
+                  (build_env lcb_lc lcb_contracts);
+*)
+  }.
+
+Definition initial_chain_builder : LocalChainBuilder :=
+  {| lcb_lc := lc_initial_chain;
+     lcb_contracts := FMap.empty |}.
+
+Instance eta_local_chain_builder : Settable _ :=
+  mkSettable
+    ((constructor build_local_chain_builder) <*> lcb_lc
+                                             <*> lcb_contracts)%settable.
 
 Section ExecuteActions.
   Context (initial_lcb : LocalChainBuilder).
 
+  Local Coercion lcb_lc : LocalChainBuilder >-> LocalChain.
+
   Record ExecutionContext :=
     build_execution_context {
-      new_ftxs : list FullTx;
+      new_iacts : list InternalAction;
       new_update : ChainUpdate;
+      recorded_iacts : list InternalAction;
     }.
 
   Instance eta_execution_context : Settable _ :=
     mkSettable
-      ((constructor build_execution_context) <*> new_ftxs
-                                             <*> new_update)%settable.
+      ((constructor build_execution_context) <*> new_iacts
+                                             <*> new_update
+                                             <*> recorded_iacts)%settable.
+
+  Definition merge_contracts (m : FMap Address WeakContract) (l : list InternalAction)
+    : FMap Address WeakContract :=
+    let go (iact : InternalAction)
+           (m : FMap Address WeakContract) : FMap Address WeakContract :=
+        match iact.(iact_body) with
+          | iact_deploy wc _ => FMap.add iact.(iact_to) wc m
+          | _ => m
+        end in
+    fold_right go m l.
 
-  Let make_acc_lcb (ec : ExecutionContext) : LocalChainBuilder :=
+  Definition make_acc (ec : ExecutionContext) : LocalChainBuilder :=
     let new_lc := (initial_lcb.(lcb_lc))[[lc_updates ::= cons ec.(new_update)]] in
     let new_bid := new_lc.(lc_head_block).(block_header).(block_number) + 1 in
-    let new_bftxs := map (fun t => (new_bid, t)) ec.(new_ftxs) in
-    {| lcb_lc := new_lc; lcb_ftxs := new_bftxs ++ initial_lcb.(lcb_ftxs) |}.
-
-  Let make_acc_c (lcb : LocalChainBuilder) : Chain :=
-    build_chain lc_interface lcb.(lcb_lc).
+    let new_biacts := map (fun t => (new_bid, t)) ec.(new_iacts) in
+    let new_contracts := merge_contracts initial_lcb.(lcb_contracts) ec.(new_iacts) in
+    {| lcb_lc := new_lc; lcb_contracts := new_contracts |}.
 
-  Let verify_amount (c : Chain) (addr : Address) (amt : Amount)
+  Definition verify_amount (c : LocalChain) (addr : Address) (amt : Amount)
     : option unit :=
-    if (amt <=? account_balance c addr)%nat
+    if (amt <=? account_balance c addr)%Z
     then Some tt
     else None.
 
-  Let find_contract (addr : Address) (lcb : LocalChainBuilder)
-    : option WeakContract :=
-    let to_wc (t : BlockId * FullTx) : option WeakContract :=
-        let (bid, ft) := t in
-        if ft.(ftx_to) =? addr then
-          match ft.(ftx_body) with
-          | ftx_deploy wc _ => Some wc
-          | _ => None
-          end
-        else
-          None in
-    find_first to_wc lcb.(lcb_ftxs).
-
-  Let count_contract_deployments (lcb : LocalChainBuilder) : nat :=
-    let is_deployment (t : BlockId * FullTx) : bool :=
-        match (snd t).(ftx_body) with
-        | ftx_deploy _ _ => true
-        | _ => false
-        end in
-    length (filter is_deployment lcb.(lcb_ftxs)).
+  Definition count_contract_deployments (lcb : LocalChainBuilder) : nat :=
+    FMap.size lcb.(lcb_contracts).
 
-  Let verify_no_txs (addr : Address) (lcb : LocalChainBuilder) : option unit :=
-    match incoming_txs (make_acc_c lcb) addr with
+  Let verify_no_txs (addr : Address) (c : LocalChain) : option unit :=
+    match incoming_txs c addr with
     | _ :: _ => None
     | [] => Some tt
     end.
 
+  Axiom b : False.
+  Notation todo := (False_rect _ b).
   Fixpoint execute_action
           (act : Address (*from*) * ChainAction)
           (ec : ExecutionContext)
           (gas : nat)
-          (is_internal : bool)
+          (record : bool)
           {struct gas}
     : option ExecutionContext :=
     match gas, act with
     | 0, _ => None
     | S gas, (from, act) =>
-      let acc_lcb := make_acc_lcb ec in
-      let acc_c := make_acc_c acc_lcb in
+      let acc_lcb := make_acc ec in
       let deploy_contract amount (wc : WeakContract) setup :=
-          do verify_amount acc_c from amount;
-          let contract_addr := 1 + count_contract_deployments acc_lcb in (* todo *)
+          do verify_amount acc_lcb from amount;
+          let contract_addr := N.of_nat (1 + count_contract_deployments acc_lcb) in (* todo *)
           do verify_no_txs contract_addr acc_lcb;
-          let ctx := {| ctx_chain := acc_c;
+          let ctx := {| ctx_chain := acc_lcb;
                         ctx_from := from;
                         ctx_contract_address := contract_addr;
                         ctx_amount := amount |} in
           let (ver, init, recv) := wc in
           do state <- init ctx setup;
-          let new_ftx := {| ftx_from := from;
-                            ftx_to := contract_addr;
-                            ftx_amount := amount;
-                            ftx_body := ftx_deploy wc setup;
-                            ftx_is_internal := is_internal; |} in
+          let new_iact := {|
+                iact_from := from;
+                iact_to := contract_addr;
+                iact_amount := amount;
+                iact_body := iact_deploy wc setup; |} in
           let new_cu :=
               ec.(new_update)[[upd_contracts ::= FMap.add contract_addr state]]
-                             [[upd_txs ::= cons (new_ftx : Tx)]] in
+                             [[upd_txs ::= cons (new_iact : Tx)]] in
           let new_ec :=
               ec[[new_update := new_cu]]
-                [[new_ftxs ::= cons new_ftx]] in
+                [[new_iacts ::= cons new_iact]]
+                [[recorded_iacts ::= if record then cons new_iact else id]] in
           Some new_ec in