Small refactoring to ChainBuilderType and some proofs

theories/Blockchain.v

@@ -74,6 +74,9 @@ Record BlockHeader :=
     finalized_height : nat;
   }.
 
+Global Instance block_header_settable : Settable _ :=
+  settable! build_block_header <block_height; slot_number; finalized_height>.
+
 (* This represents the view of the blockchain that a contract
 can access and interact with. *)
 Record Chain :=
@@ -898,15 +901,14 @@ Class ChainBuilderType :=
     builder_env : builder_type -> Environment;
 
     builder_add_block
-      (b : builder_type)
+      (builder : builder_type)
       (baker : Address)
-      (actions : list Action)
-      (slot_number : nat)
-      (finalized_height : nat) :
+      (header : BlockHeader)
+      (actions : list Action) :
       option builder_type;
 
-    builder_trace (b : builder_type) :
-      ChainTrace empty_state (build_chain_state (builder_env b) []);
+    builder_trace (builder : builder_type) :
+      ChainTrace empty_state (build_chain_state (builder_env builder) []);
   }.
 
 Global Coercion builder_type : ChainBuilderType >-> Sortclass.

theories/Congress.v

@@ -601,10 +601,7 @@ Proof.
     end; cbn in *; try congruence.
     inversion receive.
     rewrite <- (remove_proposal_cacts _ _ _ found), map_length.
-    match goal with
-    | [|- context[if ?large_annoying_expression_i_should_refactor then _ else _]] =>
-      destruct large_annoying_expression_i_should_refactor
-    end; cbn.
+    destruct (proposal_passed _ _); cbn.
     + (* I wonder why these asserts are necessary... *)
       assert (forall a b, a + b <= a + b + 0) by (intros; lia); auto.
     + assert (forall a b, a + 0 <= a + b + 0) by (intros; lia); auto.
@@ -682,7 +679,6 @@ Proof.
            _ _ trace is_contract no_contract_prev) as all.
   rewrite queue_eq in *.
   inversion all.
-  cbn in *.
   destruct_address_eq; congruence.
 Qed.
 Hint Resolve undeployed_contract_no_out_queue_count : core.
@@ -856,17 +852,14 @@ Proof.
           lia.
   - (* Permute queue *)
     unfold num_outgoing_acts.
-    match goal with
-    | [Hperm: Permutation _ _ |- _] => rewrite <- Hperm
-    end.
     cbn.
-    rewrite <- prev_new in *; auto.
+    rewrite <- perm, prev_new in *; auto.
 Qed.
 
 Corollary congress_txs_after_block
           {ChainBuilder : ChainBuilderType}
-          prev baker acts slot finalization_height new :
-  builder_add_block prev baker acts slot finalization_height = Some new ->
+          prev baker header acts new :
+  builder_add_block prev baker header acts = Some new ->
   forall addr,
     env_contracts new addr = Some (Congress.contract : WeakContract) ->
     length (outgoing_txs (builder_trace new) addr) <=

theories/Congress_Buggy.v

@@ -446,9 +446,13 @@ Section Theories.
   Definition exploit_example : option (Address * LocalChainBuilderDepthFirst) :=
     let chain := builder_initial in
     let baker := BoundedN.of_Z_const AddrSize 10 in
-    let next_num chain := S (block_height (block_header chain)) in
+    let add_block (chain : LocalChainBuilderDepthFirst) act_bodies :=
+        let next_header :=
+            (block_header chain)<|block_height ::= S|><|slot_number ::= S|> in
+        let acts := map (build_act baker) act_bodies in
+        builder_add_block chain baker next_header acts in
     (* Get some money on the baker *)
-    do chain <- builder_add_block chain baker [] (next_num chain) 0;
+    do chain <- add_block chain [];
     (* Deploy congress and exploit contracts *)
     let rules :=
         {| min_vote_count_permille := 200;
@@ -456,9 +460,7 @@ Section Theories.
            debating_period_in_blocks := 0; |} in
     let dep_congress := create_deployment 50 contract {| setup_rules := rules |} in
     let dep_exploit := create_deployment 0 exploit_contract () in
-    do chain <-
-       builder_add_block
-         chain baker (map (build_act baker) [dep_congress; dep_exploit]) (next_num chain) 0;
+    do chain <- add_block chain [dep_congress; dep_exploit];
     let contracts := map fst (FMap.elements (lc_contracts (lcb_lc chain))) in
     let exploit := nth 0 contracts baker in
     let congress := nth 1 contracts baker in
@@ -468,10 +470,10 @@ Section Theories.
     let create_proposal := create_proposal [cact_transfer exploit 1] in
     let vote_proposal := vote_for_proposal 1 in
     let exec_proposal := finish_proposal 1 in
-    let acts :=
-        map (fun msg => build_act baker (act_call congress 0 (serialize msg)))
+    let act_bodies :=
+        map (fun m => act_call congress 0 (serialize m))
             [add_baker; create_proposal; vote_proposal; exec_proposal] in
-    do chain <- builder_add_block chain baker acts (next_num chain) 0;
+    do chain <- add_block chain act_bodies;
     Some (congress, chain).
 
   Definition unpacked_exploit_example : Address * LocalChainBuilderDepthFirst :=

theories/LocalBlockchain.v

@@ -439,20 +439,14 @@ Definition add_block
            (depth_first : bool)
            (lcb : LocalChainBuilder)
            (baker : Address)
-           (actions : list Action)
-           (slot_number : nat)
-           (finalized_height : nat)
-  : option LocalChainBuilder.
+           (header : BlockHeader)
+           (actions : list Action) : option LocalChainBuilder.
 Proof.
   set (lcopt :=
          let lc := lcb_lc lcb in
-         let new_header :=
-             {| block_height := S (block_height (lc_header lc));
-                slot_number := slot_number;
-                finalized_height := finalized_height; |} in
-         do validate_header new_header (lc_header lc);
+         do validate_header header (lc_header lc);
          do validate_actions actions;
-         let lc := add_new_block new_header baker lc in
+         let lc := add_new_block header baker lc in
          execute_actions 1000 actions lc depth_first).
 
   destruct lcopt as [lc|] eqn:exec; [|exact None].

theories/LocalBlockchainTests.v

@@ -5,6 +5,8 @@ From SmartContracts Require Import Congress.
 From SmartContracts Require Import Oak.
 From SmartContracts Require Import Containers.
 From SmartContracts Require Import BoundedN.
+From SmartContracts Require Import Extras.
+From RecordUpdate Require Import RecordUpdate.
 From Coq Require Import List.
 From Coq Require Import ZArith.
 Import ListNotations.
@@ -27,31 +29,23 @@ Section LocalBlockchainTests.
 
   Definition chain1 : ChainBuilder := builder_initial.
 
-  Definition unpack_option {A : Type} (a : option A) :=
-    match a return match a with
-                   | Some _ => A
-                   | None => unit
-                   end with
-    | Some x => x
-    | None => tt
-    end.
-
   Compute (block_header chain1).
 
+  Definition add_block (chain : ChainBuilder) acts : option ChainBuilder :=
+    let header :=
+        (block_header chain)<|block_height ::= S|><|slot_number ::= S|> in
+    builder_add_block chain baker header acts.
+
   (* Baker mines an empty block (and gets some coins) *)
   Definition chain2 : ChainBuilder :=
-    unpack_option (chain1.(builder_add_block) baker [] 2 0).
+    unpack_option (add_block chain1 []).
 
   Compute (account_balance chain2 person_1).
   Compute (account_balance chain2 baker).
 
   (* Baker transfers 10 coins to person_1 *)
   Definition chain3 : ChainBuilder :=
-    unpack_option (
-        chain2.(builder_add_block)
-                 baker
-                 [build_act baker (act_transfer person_1 10)]
-                 3 0).
+    unpack_option (add_block chain2 [build_act baker (act_transfer person_1 10)]).
 
   Compute (account_balance chain3 person_1).
   Compute (account_balance chain3 baker).
@@ -68,11 +62,7 @@ Section LocalBlockchainTests.
     create_deployment 5 Congress.contract setup.
 
   Definition chain4 : ChainBuilder :=
-    unpack_option (
-        chain3.(builder_add_block)
-                 baker
-                 [build_act person_1 deploy_congress]
-                 4 0).
+    unpack_option (add_block chain3 [build_act person_1 deploy_congress]).
 
   Definition congress_1 : Address :=
     match outgoing_txs (builder_trace chain4) person_1 with
@@ -118,11 +108,9 @@ Section LocalBlockchainTests.
     congress_ifc.(send) 0 (Some (add_member p)).
 
   Definition chain5 : ChainBuilder :=
-    unpack_option
-      (chain4.(builder_add_block)
-                baker
-                [build_act person_1 (add_person person_1); build_act person_1 (add_person person_2)]
-                5 0).
+    let acts := [build_act person_1 (add_person person_1);
+                 build_act person_1 (add_person person_2)] in
+    unpack_option (add_block chain4 acts).
 
   Compute (FMap.elements (congress_state chain5).(members)).
   Compute (account_balance chain5 congress_1).
@@ -133,11 +121,7 @@ Section LocalBlockchainTests.
     congress_ifc.(send) 0 (Some (create_proposal [cact_transfer person_3 3])).
 
   Definition chain6 : ChainBuilder :=
-    unpack_option (
-        chain5.(builder_add_block)
-                 baker
-                 [build_act person_1 create_proposal_call]
-                 6 0).
+    unpack_option (add_block chain5 [build_act person_1 create_proposal_call]).
 
   Compute (FMap.elements (congress_state chain6).(proposals)).
 
@@ -146,11 +130,8 @@ Section LocalBlockchainTests.
     congress_ifc.(send) 0 (Some (vote_for_proposal 1)).
 
   Definition chain7 : ChainBuilder :=
-    unpack_option (
-        chain6.(builder_add_block)
-                 baker
-                 [build_act person_1 vote_proposal; build_act person_2 vote_proposal]
-                 7 0).
+    let acts := [build_act person_1 vote_proposal; build_act person_2 vote_proposal] in
+    unpack_option (add_block chain6 acts).
 
   Compute (FMap.elements (congress_state chain7).(proposals)).
 
@@ -159,11 +140,7 @@ Section LocalBlockchainTests.
     congress_ifc.(send) 0 (Some (finish_proposal 1)).
 
   Definition chain8 : ChainBuilder :=
-    unpack_option (
-        chain7.(builder_add_block)
-                 baker
-                 [build_act person_3 finish_proposal]
-                 8 0).
+    unpack_option (add_block chain7 [build_act person_3 finish_proposal]).
 
   Compute (FMap.elements (congress_state chain8).(proposals)).
   (* Balances before: *)
@@ -178,8 +155,8 @@ End LocalBlockchainTests.
 Hint Resolve congress_txs_after_block : core.
 (* The congress satisfies a property specialized to the local blockchain DFS: *)
 Lemma congress_txs_after_local_chain_block
-          (prev new : LocalChainBuilderDepthFirst) baker acts slot finalization_height :
-  builder_add_block prev baker acts slot finalization_height = Some new ->
+          (prev new : LocalChainBuilderDepthFirst) baker header acts :
+  builder_add_block prev baker header acts = Some new ->
   forall addr,
     env_contracts new addr = Some (Congress.contract : WeakContract) ->
     length (outgoing_txs (builder_trace new) addr) <=
@@ -187,8 +164,8 @@ Lemma congress_txs_after_local_chain_block
 Proof. eauto. Qed.
 (* And of course, it is satisfied for the breadth first chain as well. *)
 Lemma congress_txs_after_local_chain_bf_block
-      (prev new : LocalChainBuilderBreadthFirst) baker acts slot finalization_height :
-  builder_add_block prev baker acts slot finalization_height = Some new ->
+      (prev new : LocalChainBuilderBreadthFirst) baker header acts :
+  builder_add_block prev baker header acts = Some new ->
   forall addr,
     env_contracts new addr = Some (Congress.contract : WeakContract) ->
     length (outgoing_txs (builder_trace new) addr) <=