Lots of work and some things work again

src/Blockchain.v

@@ -17,6 +17,8 @@ Definition Version := nat.
 
 Definition Amount := Z.
 
+Bind Scope Z_scope with Amount.
+
 Class ChainBaseTypes :=
   build_chain_base_types {
     Address : Type;
@@ -335,7 +337,6 @@ Definition create_deployment
           (setup : setup_ty) : ActionBody :=
   act_deploy amount contract (serialize setup).
 
-(*
 (* 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 OakValue away from contracts. *)
@@ -348,7 +349,7 @@ Record ContractInterface {setup_ty msg_ty state_ty : Type} :=
     (* The setup that was passed when the contract was deployed *)
     contract_setup : setup_ty;
     (* Obtain the state at some point of time *)
-    get_state : forall (Chain : ChainType), Chain -> option state_ty;
+    get_state : Chain -> option state_ty;
     (* Make an action transferring money to the contract without
       a message *)
     transfer : Amount -> ActionBody;
@@ -378,7 +379,6 @@ Definition get_contract_interface
           get_state := ifc_get_state;
           transfer := ifc_transfer;
           call := ifc_call; |}.
-*)
 
 End Blockchain.
 
@@ -756,3 +756,4 @@ Arguments version {_ _ _ _ _ _ _}.
 Arguments init {_ _ _ _ _ _ _}.
 Arguments receive {_ _ _ _ _ _ _}.
 Arguments build_contract {_ _ _ _ _ _ _}.
+Arguments ContractInterface {_} _ _ _.

src/BoundedN.v

 From Coq Require Import NArith ZArith.
 From SmartContracts Require Import Monads.
-From SmartContracts Require Import Oak.
 From SmartContracts Require Import Finite.
 From SmartContracts Require Import Extras.
 From SmartContracts Require Import Automation.
@@ -12,11 +11,17 @@ Import ListNotations.
 
 Local Open Scope N.
 
-Definition BoundedN (bound : N) := { n : N | n < bound }.
+Inductive BoundedN (bound : N) :=
+  | bounded (n : N) (_ : n < bound) : BoundedN bound.
+
+Arguments bounded {_}.
 
 Module BoundedN.
+  Definition to_N {bound : N} (n : BoundedN bound) : N :=
+    let (val, _) := n in val.
+
   Definition eqb {bound : N} (a b : BoundedN bound) : bool :=
-    N.eqb (proj1_sig a) (proj1_sig b).
+    N.eqb (to_N a) (to_N b).
 
   Definition eq_dec {bound : N} (a b : BoundedN bound) :
     {a = b} + {a <> b}.
@@ -38,13 +43,10 @@ Module BoundedN.
   Local Lemma Z_lt_dec (a b : Z) : ({a < b} + {~(a < b)})%Z.
   Proof. unfold "<"%Z. decide equality. Defined.
 
-  Definition to_N {bound : N} (n : BoundedN bound) : N :=
-    proj1_sig n.
-
   Definition of_N {bound : N} (n : N) : option (BoundedN bound).
   Proof.
     destruct (N_lt_dec n bound).
-    - exact (Some (exist _ n l)).
+    - exact (Some (bounded n l)).
     - exact None.
   Defined.
 
@@ -88,7 +90,7 @@ Module BoundedN.
     Bool.reflect (a = b) (eqb a b).
   Proof.
     unfold eqb.
-    destruct (N.eqb_spec (proj1_sig a) (proj1_sig b)) as [eq | neq].
+    destruct (N.eqb_spec (to_N a) (to_N b)) as [eq | neq].
     - constructor.
       auto.
     - constructor.
@@ -216,7 +218,7 @@ Module BoundedN.
 
     Global Instance BoundedNCountable {bound : N} : Countable (BoundedN bound).
     Proof.
-      refine {| encode n := encode (proj1_sig n);
+      refine {| encode n := encode (to_N n);
                 decode n := of_N =<< decode n; |}.
       intros [x lt].
       rewrite decode_encode.
@@ -226,23 +228,9 @@ Module BoundedN.
       - assert (lt = l) by (apply UIP_dec; decide equality).
         congruence.
       - tauto.
-    Qed.
+    Defined.
   End Stdpp.
 
-  Program Instance BoundedN_equivalence {bound : N}
-    : OakTypeEquivalence (BoundedN bound) :=
-    {| serialize bn := serialize (countable.encode bn);
-      deserialize v :=
-        do p <- (deserialize v : option positive);
-        countable.decode p |}.
-  Next Obligation.
-    intros bound x.
-    simpl.
-    rewrite deserialize_serialize.
-    simpl.
-    now rewrite countable.decode_encode.
-  Qed.
-
   Global Instance BoundedN_finite {bound : N} : Finite (BoundedN bound) :=
     {| elements := map_option of_nat (List.seq 0 (N.to_nat bound)) |}.
   Proof.

src/Congress.v

@@ -216,7 +216,7 @@ Definition deserialize_rules (v : OakValue) : option Rules :=
   do '((a, b), c) <- deserialize v;
   Some (build_rules a b c).
 
-Program Instance rules_equivalence : OakTypeEquivalence Rules :=
+Global Program Instance rules_equivalence : OakTypeEquivalence Rules :=
   {| serialize r := let (a, b, c) := r in serialize (a, b, c);
      (* Why does
      deserialize v :=
@@ -230,7 +230,7 @@ Next Obligation.
   reflexivity.
 Qed.
 
-Program Instance setup_equivalence : OakTypeEquivalence Setup :=
+Global Program Instance setup_equivalence : OakTypeEquivalence Setup :=
   {| serialize s := serialize s.(setup_rules);
      deserialize or :=
        do rules <- deserialize or;
@@ -249,7 +249,7 @@ Definition deserialize_congress_action (v : OakValue) : option CongressAction :=
   | inr (to, amount, msg) => cact_call to amount msg
   end).
 
-Program Instance congress_action_equivalence : OakTypeEquivalence CongressAction :=
+Global Program Instance congress_action_equivalence : OakTypeEquivalence CongressAction :=
   {| serialize ca :=
        serialize
          match ca with
@@ -268,7 +268,7 @@ Definition deserialize_proposal (v : OakValue) : option Proposal :=
   do '(a, b, c, d) <- deserialize v;
   Some (build_proposal a b c d).
 
-Program Instance proposal_equivalence : OakTypeEquivalence Proposal :=
+Global Program Instance proposal_equivalence : OakTypeEquivalence Proposal :=
   {| serialize p :=
        let (a, b, c, d) := p in
        serialize (a, b, c, d);
@@ -310,7 +310,7 @@ Definition deserialize_msg (v : OakValue) : option Msg :=
   | _ => None
   end.
 
-Program Instance msg_equivalence : OakTypeEquivalence Msg :=
+Global Program Instance msg_equivalence : OakTypeEquivalence Msg :=
   {| serialize := serialize_msg; deserialize := deserialize_msg; |}.
 Next Obligation.
   intros msg.
@@ -326,7 +326,7 @@ Definition deserialize_state (v : OakValue) : option State :=
   do '(a, b, c, d, e) <- deserialize v;
   Some (build_state a b c d e).
 
-Program Instance state_equivalence : OakTypeEquivalence State :=
+Global Program Instance state_equivalence : OakTypeEquivalence State :=
   {| serialize := serialize_state; deserialize := deserialize_state; |}.
 Next Obligation.
   unfold serialize_state, deserialize_state.

src/LocalBlockchain.v

@@ -371,6 +371,9 @@ Proof.
     end; simpl in *; intuition.
 Qed.
 
+Axiom b : False.
+Notation todo := (False_rect _ b).
+
 (* Adds a block to the chain by executing the specified chain actions.
    Returns the new chain if the execution succeeded (for instance,
    transactions need enough funds, contracts should not reject, etc. *)
@@ -427,7 +430,7 @@ Proof.
   - subst.
     now rewrite FMap.find_partial_alter.
   - now rewrite FMap.find_partial_alter_ne; auto.
-Qed.
+Defined.
 
 Global Instance lcb_chain_builder_type : ChainBuilderType :=
   {| builder_type := LocalChainBuilder;

src/LocalBlockchainTests.v

 From SmartContracts Require Import Monads.
 From SmartContracts Require Import Blockchain.
-From SmartContracts Require LocalBlockchain.
+From SmartContracts Require Import LocalBlockchain.
 From SmartContracts Require Import Congress.
 From SmartContracts Require Import Oak.
 From SmartContracts Require Import Containers.
+From SmartContracts Require Import BoundedN.
 From Coq Require Import List.
 From Coq Require Import ZArith.
 Import ListNotations.
 
 Section LocalBlockchainTests.
   (* Addresses *)
-  Definition congress_1 := 1.
-  Definition baker := 10.
-  Definition person_1 := 11.
-  Definition person_2 := 12.
-  Definition person_3 := 13.
+  Definition congress_1 : Address :=
+    BoundedN.of_Z_const AddrSize 1.
 
-  Definition chain1 :=
-    initial_chain_builder LocalBlockchain.lc_builder_interface.
+  Definition baker : Address :=
+    BoundedN.of_Z_const AddrSize 10.
+
+  Definition person_1 : Address :=
+    BoundedN.of_Z_const AddrSize 11.
+
+  Definition person_2 : Address :=
+    BoundedN.of_Z_const AddrSize 12.
+
+  Definition person_3 : Address :=
+    BoundedN.of_Z_const AddrSize 13.
+
+  Definition ChainBuilder := builder_type.
+
+  Definition chain1 : ChainBuilder := builder_initial.
 
   Definition unpack_option {A : Type} (a : option A) :=
     match a return match a with
@@ -28,16 +39,25 @@ Section LocalBlockchainTests.
     | None => tt
     end.
 
+  Local Coercion to_env (cb : ChainBuilder) : Environment :=
+    builder_env cb.
+
+  Compute (block_header chain1).
+
   (* Baker mines an empty block (and gets some coins) *)
   Definition chain2 : ChainBuilder :=
-    unpack_option (chain1.(add_block) baker []).
+    unpack_option (chain1.(builder_add_block) baker [] 2 0).
 
   Compute (account_balance chain2 person_1).
   Compute (account_balance chain2 baker).
 
   (* Baker transfers 10 coins to person_1 *)
   Definition chain3 : ChainBuilder :=
-    unpack_option (chain2.(add_block) baker [(baker, act_transfer person_1 10)]).
+    unpack_option (
+        chain2.(builder_add_block)
+                 baker
+                 [build_act baker (act_transfer person_1 10)]
+                 3 0).
 
   Compute (account_balance chain3 person_1).
   Compute (account_balance chain3 baker).
@@ -50,30 +70,28 @@ Section LocalBlockchainTests.
 
   Definition setup := Congress.build_setup setup_rules.
 
-  Definition deploy_congress : ChainAction :=
+  Definition deploy_congress : ActionBody :=
     create_deployment 5 Congress.contract setup.
 
   Definition chain4 : ChainBuilder :=
-    unpack_option (chain3.(add_block) baker [(person_1, deploy_congress)]).
+    unpack_option (
+        chain3.(builder_add_block)
+                 baker
+                 [build_act person_1 deploy_congress]
+                 4 0).
 
   Compute (contract_deployment chain4 congress_1).
   Compute (account_balance chain4 person_1).
   Compute (account_balance chain4 baker).
   Compute (account_balance chain4 congress_1).
 
-  Definition congress_ifc :=
+  (*
+  Definition congress_ifc : ContractInterface Congress.Setup Congress.Msg Congress.State :=
     unpack_option
       (get_contract_interface chain4 congress_1 Congress.Setup Congress.Msg Congress.State).
 
-  Definition congress_state chain : Congress.State :=
-    match congress_ifc.(get_state) chain with
-    | Some s => s
-    | None => {| owner := 0;
-                 state_rules := setup_rules;
-                 proposals := FMap.empty;
-                 next_proposal_id := 0;
-                 members := FMap.empty |}
-    end.
+  Definition congress_state chain :=
+    unpack_option (congress_ifc.(get_state) chain).
 
   Compute (congress_ifc.(get_state) chain4).
   Compute (FMap.elements (congress_state chain4).(members)).
@@ -84,11 +102,12 @@ Section LocalBlockchainTests.
 
   Definition chain5 : ChainBuilder :=
     unpack_option
-      (chain4.(add_block)
+      (chain4.(builder_add_block)
                 baker
-                [(person_1, add_person person_1); (person_1, add_person person_2)]).
+                [build_act person_1 (add_person person_1); build_act person_1 (add_person person_2)]
+                5 0).
 
-  Compute (FMap.elements (congress_state chain5).(members)).
+  Eval cbn in (FMap.elements (congress_state chain5).(members)).
   Compute (account_balance chain5 congress_1).
 
   (* person_1 creates a proposal to send 3 coins to person_3 using funds
@@ -97,7 +116,11 @@ Section LocalBlockchainTests.
     congress_ifc.(call) 0 (create_proposal [cact_transfer person_3 3]).
 
   Definition chain6 : ChainBuilder :=
-    unpack_option (chain5.(add_block) baker [(person_1, create_proposal_call)]).
+    unpack_option (
+        chain5.(builder_add_block)
+                 baker
+                 [build_act person_1 create_proposal_call]
+                 6 0).
 
   Compute (FMap.elements (congress_state chain6).(proposals)).
 
@@ -126,4 +149,5 @@ Section LocalBlockchainTests.
   Compute (account_balance chain8 congress_1).
   Compute (account_balance chain8 person_3).
   Print Assumptions chain8.
+*)
 End LocalBlockchainTests.

src/Oak.v

@@ -2,6 +2,7 @@ From Coq Require Import ZArith.
 From SmartContracts Require Import Monads.
 From SmartContracts Require Import Containers.
 From SmartContracts Require Import Automation.
+From SmartContracts Require Import BoundedN.
 From Coq Require Import List.
 
 Import ListNotations.
@@ -135,6 +136,21 @@ Program Instance oak_value_equivalence : OakTypeEquivalence OakValue :=
      deserialize v := Some v; |}.
 Solve Obligations with reflexivity.
 
+Program Instance BoundedN_equivalence {bound : N}
+  : OakTypeEquivalence (BoundedN bound) :=
+  {| serialize bn := serialize (countable.encode bn);
+    deserialize v :=
+      do p <- (deserialize v : option positive);
+      countable.decode p |}.
+Next Obligation.
+  intros bound x.
+  simpl.
+  rewrite deserialize_serialize.
+  simpl.
+  now rewrite countable.decode_encode.
+Qed.
+
+
 (* Program Instance generates an insane amount of obligations for sums,
    so we define it by ourselves. *)
 Section Sum.