Commit 5e814944 authored by Jakob Botsch Nielsen's avatar Jakob Botsch Nielsen
Browse files

Refactor finite map/finite sets and prove map-list/set-list equality

* Pull the functionality we need into a Containers.v file that takes
  care of including the proper implementations of fmaps and fsets.
  Additionally, this file defines notation/new names.
* Stop using map/set notation for operations. This conflicts with
  lists/record-set and is generally a head-ache.
* Switch to lists instead of AVL trees for the sets and maps. This
  allows us to prove (assuming proof irrelevance) what we need:
  FSet.of_list (FSet.elements x) = x. Prove this and the equivalent for
  fin maps.
* Do not use program instances in Oak.v. We can do with instances which
  generate a lot less bloat.
parent 11c14413
Pipeline #11256 failed with stage
in 3 minutes and 13 seconds
-R src SmartContracts
src/Blockchain.v
src/Congress.v
src/Containers.v
src/Extras.v
src/LocalBlockchain.v
src/LocalBlockchainTests.v
......
From Coq Require Import String.
From Coq Require OrderedTypeEx.
From Coq Require Import List.
From SmartContracts Require Import Oak.
From SmartContracts Require Import Monads.
......@@ -17,7 +15,6 @@ Infix "=?" := Address.eqb (at level 70) : address_scope.
Definition Amount := nat.
Definition BlockId := nat.
Definition BlockHash := string.
Definition Version := nat.
Record ContractDeployment :=
......
From Coq Require Import String.
From Coq Require Import ZArith.
From Coq Require Import Program.Basics.
From Containers Require Import OrderedTypeEx.
From Containers Require Import MapInterface.
From Containers Require Import SetInterface.
From Containers Require MapAVL.
From Containers Require SetAVL.
From SmartContracts Require Import Blockchain.
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 MapNotations.
Import ListNotations.
Import RecordSetNotations.
......@@ -29,7 +24,7 @@ Inductive CongressAction :=
Record Proposal :=
build_proposal {
actions : list CongressAction;
votes : Map[Address, Z];
votes : FMap Address Z;
vote_result : Z;
proposed_in : BlockId;
}.
......@@ -68,9 +63,9 @@ Record State :=
build_state {
owner : Address;
state_rules : Rules;
proposals : Map[nat, Proposal];
proposals : FMap nat Proposal;
next_proposal_id : ProposalId;
members : SetInterface.set Address;
members : FSet Address;
}.
Instance eta_state : Settable _ :=
......@@ -94,9 +89,9 @@ Definition init (ctx : ContractCallContext) (setup : Setup) : option State :=
if validate_rules setup.(setup_rules) then
Some {| owner := ctx.(ctx_from);
state_rules := setup.(setup_rules);
proposals := []%map;
proposals := FMap.empty;
next_proposal_id := 1%nat;
members := {}%set |}
members := FSet.empty |}
else
None.
......@@ -104,10 +99,10 @@ Definition add_proposal (actions : list CongressAction) (chain : Chain) (state :
let id := state.(next_proposal_id) in
let head_block := chain.(head_block) in
let proposal := {| actions := actions;
votes := []%map;
votes := FMap.empty;
vote_result := 0;
proposed_in := head_block.(block_header).(block_number) |} in
let new_proposals := state.(proposals)[id <- proposal]%map in
let new_proposals := FMap.add id proposal state.(proposals) in
state[[proposals := new_proposals]][[next_proposal_id := (id + 1)%nat]].
Definition vote_on_proposal
......@@ -116,27 +111,27 @@ Definition vote_on_proposal
(vote : Z)
(state : State)
: option State :=
do proposal <- state.(proposals)[pid]%map;
let old_vote := match proposal.(votes)[voter]%map with
do proposal <- FMap.find pid state.(proposals);
let old_vote := match FMap.find voter proposal.(votes) with
| Some old => old
| None => 0
end in
let new_votes := proposal.(votes)[voter <- vote]%map in
let new_votes := FMap.add voter vote proposal.(votes) in
let new_vote_result := proposal.(vote_result) - old_vote + vote in
let new_proposal := proposal[[votes := new_votes]][[vote_result := new_vote_result]] in
Some (state[[proposals ::= MapInterface.add pid new_proposal]]).
Some (state[[proposals ::= FMap.add pid new_proposal]]).
Definition do_retract_vote
(voter : Address)
(pid : ProposalId)
(state : State)
: option State :=
do proposal <- state.(proposals)[pid]%map;
do old_vote <- proposal.(votes)[voter]%map;
let new_votes := MapInterface.remove voter proposal.(votes) in
do proposal <- FMap.find pid state.(proposals);
do old_vote <- FMap.find voter proposal.(votes);
let new_votes := FMap.remove voter proposal.(votes) in
let new_vote_result := proposal.(vote_result) - old_vote in
let new_proposal := proposal[[votes := new_votes]][[vote_result := new_vote_result]] in
Some (state[[proposals ::= MapInterface.add pid new_proposal]]).
Some (state[[proposals ::= FMap.add pid new_proposal]]).
Definition congress_action_to_chain_action (act : CongressAction) : ChainAction :=
match act with
......@@ -149,16 +144,16 @@ Definition do_finish_proposal
(state : State)
(chain : Chain)
: option (State * list ChainAction) :=
do proposal <- state.(proposals)[pid]%map;
do proposal <- FMap.find pid state.(proposals);
let rules := state.(state_rules) in
let debate_end := (Z.of_nat proposal.(proposed_in)) + rules.(debating_period_in_blocks) in
let cur_block := chain.(head_block) in
if (Z.of_nat cur_block.(block_header).(block_number)) <? debate_end then
None
else
let new_state := state[[proposals ::= MapInterface.remove pid]] in
let total_votes_for_proposal := Z.of_nat (MapInterface.cardinal proposal.(votes)) in
let total_members := Z.of_nat (SetInterface.cardinal state.(members)) in
let new_state := state[[proposals ::= FMap.remove pid]] in
let total_votes_for_proposal := Z.of_nat (FMap.size proposal.(votes)) in
let total_members := Z.of_nat (FSet.size state.(members)) in
let aye_votes := (proposal.(vote_result) + total_votes_for_proposal) / 2 in
let vote_count_permille := total_votes_for_proposal * 1000 / total_members in
let aye_permille := aye_votes * 1000 / total_votes_for_proposal in
......@@ -167,7 +162,7 @@ Definition do_finish_proposal
let response_acts :=
if (enough_voters && enough_ayes)%bool
then proposal.(actions)
else [ ] in
else [] in
let response_chain_acts := map congress_action_to_chain_action response_acts in
Some (new_state, response_chain_acts).
......@@ -179,8 +174,8 @@ Definition receive
let chain := ctx.(ctx_chain) in
let sender := ctx.(ctx_from) in
let is_from_owner := (sender =? state.(owner))%address in
let is_from_member := (sender \in state.(members))%set in
let without_actions := option_map (fun new_state => (new_state, [ ])) in
let is_from_member := FSet.mem sender state.(members) in
let without_actions := option_map (fun new_state => (new_state, [])) in
match is_from_owner, is_from_member, maybe_msg with
| true, _, Some (transfer_ownership new_owner) =>
Some (state[[owner := new_owner]], [ ])
......@@ -192,10 +187,10 @@ Definition receive
None
| true, _, Some (add_member new_member) =>
Some (state[[members ::= SetInterface.add new_member]], [ ])
Some (state[[members ::= FSet.add new_member]], [ ])
| true, _, Some (remove_member old_member) =>
Some (state[[members ::= SetInterface.remove old_member]], [ ])
Some (state[[members ::= FSet.remove old_member]], [ ])
| _, true, Some (create_proposal actions) =>
Some (add_proposal actions chain state, [ ])
......
From Coq Require Import ProofIrrelevance.
From Containers Require Export OrderedType.
From Containers Require OrderedTypeEx.
From Containers Require SetListInstance.
From Containers Require MapListInstance.
From Containers Require MapFacts.
From Containers Require SetProperties.
From Coq Require Import List.
Import ListNotations.
Notation FSet := SetInterface.set.
Module FSet.
Notation empty := SetInterface.empty.
Notation add := SetInterface.add.
Notation mem := SetInterface.mem.
Notation remove := SetInterface.remove.
Notation elements := SetInterface.elements.
Notation size := SetInterface.cardinal.
Notation of_list := SetProperties.of_list.
(*
Section Forwarders.
Context {A : Type} {H : OrderedType A} {impl : @SetInterface.FSet A H}.
Definition empty : FSet A :=
SetInterface.empty.
Definition add (elem : A) (s : FSet A) : FSet A :=
SetInterface.add elem s.
Definition mem (elem : A) (s : FSet A) :=
SetInterface.mem elem s.
Definition remove (elem : A) (s : FSet A) : FSet A :=
SetInterface.remove elem s.
Definition elements (s : FSet A) : list A :=
SetInterface.elements s.
Definition of_list {spec : SetInterface.FSetSpecs impl} (l : list A) :=
SetProperties.of_list l.
End Forwarders.
*)
(* TODO: We should really use setoids instead of this hacky crap... *)
Proposition of_elements_eq
{A : Type}
{a_order : OrderedType A}
(s : FSet A)
: of_list (elements s) = s.
Proof.
destruct s as [l l_sorted].
unfold SetProperties.of_list.
Transparent SetInterface.empty.
Transparent SetInterface.elements.
unfold SetInterface.empty.
unfold SetListInstance.SetList_FSet.
unfold SetList.empty.
unfold SetList.S.empty.
simpl.
induction l as [| hd tl IHl].
- simpl.
assert (SetList.S.empty_sort a_order = l_sorted) by apply proof_irrelevance.
subst; reflexivity.
- assert (decomposable: forall s1 s2 : SetList.set A, SetList.this s1 = SetList.this s2 -> s1 = s2).
+ intros [l1 l1_sorted] [l2 l2_sorted].
simpl.
intros l1_eq_l2.
subst.
replace l2_sorted with l1_sorted by apply proof_irrelevance.
reflexivity.
+ apply decomposable.
inversion l_sorted as [| a b tl_sorted hd_sorted]; subst.
simpl in *.
rewrite IHl with (l_sorted := tl_sorted).
Transparent SetInterface.add.
unfold SetInterface.add.
unfold SetList.add.
simpl.
unfold SetList.S.add.
destruct tl as [| hd' tl_tl].
* reflexivity.
* inversion hd_sorted as [|? ? k_k'_lt]; subst.
destruct (OrderedType.compare_dec hd hd').
-- reflexivity.
-- order.
-- order.
Qed.
End FSet.
Notation FMap := MapInterface.dict.
Module FMap.
Notation empty := MapInterface.empty.
Arguments empty {_ _ _ _}.
Notation add := MapInterface.add.
Notation find := MapInterface.find.
Notation mem := MapInterface.mem.
Notation remove := MapInterface.remove.
Notation elements := MapInterface.elements.
Notation size := MapInterface.cardinal.
Notation of_list := MapFacts.of_list.
(*
Section Forwarders.
Context {K V : Type} {H : OrderedType K} {impl : @MapInterface.FMap K H}.
Definition empty : FMap K V :=
@MapInterface.empty K H impl V.
Definition add (k : K) (v : V) (m : FMap K V) : FMap K V :=
MapInterface.add k v m.
Definition mem (k : K) (m : FMap K V) :=
MapInterface.mem k m.
Definition remove (k : K) (m : FMap K V) : FMap K V :=
MapInterface.remove k m.
Definition elements (m : FMap K V) : list (K * V) :=
MapInterface.elements m.
Definition of_list (l : list (K * V)) : FMap K V :=
MapFacts.of_list l.
End Forwarders.
*)
Proposition of_elements_eq
{A B : Type}
{_ : OrderedType A}
(m : FMap A B)
: of_list (elements m) = m.
Proof.
destruct m as [l l_sorted].
unfold MapList.M.dict in *.
unfold MapFacts.of_list.
Transparent MapInterface.empty.
Transparent MapInterface.elements.
unfold MapInterface.empty.
unfold MapListInstance.MapList_FMap.
unfold MapList.empty.
unfold MapList.M.empty.
simpl.
induction l as [| hd tl IHl].
- simpl.
assert (MapList.M.empty_sorted B = l_sorted) by apply proof_irrelevance.
subst; reflexivity.
- assert (decomposable: forall m1 m2 : MapList.dict A B, MapList.this m1 = MapList.this m2 -> m1 = m2).
+ intros [l1 l1_sorted] [l2 l2_sorted].
simpl.
intros l1_eq_l2.
subst.
replace l2_sorted with l1_sorted by apply proof_irrelevance.
reflexivity.
+ apply decomposable.
simpl.
inversion l_sorted as [| a b tl_sorted hd_sorted].
subst.
rewrite IHl with (l_sorted := tl_sorted).
Transparent MapInterface.add.
unfold MapInterface.add.
unfold MapList.add.
simpl.
unfold MapList.M.add.
destruct hd as [k v].
simpl.
destruct tl as [| [k' v'] tl_tl].
* reflexivity.
* inversion hd_sorted as [|? ? k_k'_lt]; subst.
unfold MapList.M.K.ltk in k_k'_lt.
simpl in *.
destruct (compare_dec k k').
-- reflexivity.
-- order.
-- order.
Qed.
End FMap.
......@@ -2,20 +2,18 @@ From Coq Require Import ZArith.
From SmartContracts Require Import Blockchain.
From SmartContracts Require Import Oak.
From SmartContracts Require Import Monads.
From SmartContracts Require Import Containers.
From SmartContracts Require Import Extras.
From RecordUpdate Require Import RecordUpdate.
From Containers Require Import Maps.
From Coq Require Import List.
From SmartContracts Require Import Extras.
Import RecordSetNotations.
Import ListNotations.
(* Note that [ ] or nil is needed for the empty list
in this file as [] parses an empty map *)
Local Record ChainUpdate :=
build_chain_update {
(* Contracts that had their states updated and the new state *)
upd_contracts : Map[Address, OakValue];
upd_contracts : FMap Address OakValue;
(* All transactions caused by update, including internal txs
(due to contract execution) *)
upd_txs : list Tx;
......@@ -57,14 +55,14 @@ Instance eta_local_chain_environment : Settable _ :=
Definition genesis_block : Block :=
{| block_header := {| block_number := 0; |};
block_txs := nil |}.
block_txs := [] |}.
Definition initial_chain : LocalChainEnvironment :=
{| lce_lc := {| lc_blocks := [genesis_block];
lc_updates :=
[{| upd_contracts := []%map;
upd_txs := nil |}] |};
lce_contracts := nil;
[{| upd_contracts := FMap.empty;
upd_txs := [] |}] |};
lce_contracts := [];
|}.
Definition lc_chain_at (lc : LocalChain) (bid : BlockId) : option LocalChain :=
......@@ -76,7 +74,7 @@ Definition lc_chain_at (lc : LocalChain) (bid : BlockId) : option LocalChain :=
| hd :: _ => if hd.(block_header).(block_number) =? bid
then Some {| lc_blocks := at_blocks; lc_updates := at_updates; |}
else None
| nil => None
| [] => None
end.
Definition lc_block_at (lc : LocalChain) (bid : BlockId) : option Block :=
......@@ -86,7 +84,7 @@ Definition lc_block_at (lc : LocalChain) (bid : BlockId) : option Block :=
Definition lc_head_block (lc : LocalChain) : Block :=
match lc.(lc_blocks) with
| hd :: _ => hd
| nil => genesis_block
| [] => genesis_block
end.
Definition lc_incoming_txs (lc : LocalChain) (addr : Address) : list Tx :=
......@@ -101,7 +99,7 @@ Definition lc_outgoing_txs (lc : LocalChain) (addr : Address) : list Tx :=
Definition lc_contract_state (lc : LocalChain) (addr : Address)
: option OakValue :=
find_first (fun u => u.(upd_contracts)[addr]%map) lc.(lc_updates).
find_first (fun u => FMap.find addr u.(upd_contracts)) lc.(lc_updates).
Definition lc_interface : ChainInterface :=
{| ci_chain_type := LocalChain;
......@@ -182,7 +180,7 @@ Section ExecuteActions.
tx_amount := amount;
tx_body := tx_deploy contract_deployment |} in
let new_cu :=
ec.(new_update)[[upd_contracts ::= MapInterface.add contract_addr state]]
ec.(new_update)[[upd_contracts ::= FMap.add contract_addr state]]
[[upd_txs ::= cons new_tx]] in
let new_contract := (contract_addr, wc) in
let new_ec :=
......@@ -221,13 +219,13 @@ Section ExecuteActions.
ctx_amount := amount |} in
do '(new_state, resp_actions) <- recv ctx state msg_opt;
let new_cu :=
ec.(new_update)[[upd_contracts ::= MapInterface.add to new_state]]
ec.(new_update)[[upd_contracts ::= FMap.add to new_state]]
[[upd_txs ::= cons new_tx]] in
let new_ec := ec[[new_update := new_cu]] in
let new_ec := if record then new_ec[[block_txs ::= cons new_tx]] else new_ec in
let fix go acts cur_ec :=
match acts with
| nil => Some cur_ec
| [] => Some cur_ec
| hd :: tl =>
do cur_ec <- execute_action (contract_addr, hd) cur_ec gas false;
go tl cur_ec
......@@ -249,15 +247,15 @@ Section ExecuteActions.
: option LocalChainEnvironment :=
let fix go acts ec :=
match acts with
| nil => Some ec
| [] => Some ec
| hd :: tl =>
do ec <- execute_action hd ec gas true;
go tl ec
end in
let empty_ec := {| block_txs := [coinbase];
new_update := {| upd_contracts := []%map;
new_update := {| upd_contracts := FMap.empty;
upd_txs := [coinbase] |};
new_contracts := nil |} in
new_contracts := [] |} in
do ec <- go actions empty_ec;
let new_lce := make_acc_lce ec in
let recorded_txs := ec.(block_txs) in
......
......@@ -3,7 +3,7 @@ From SmartContracts Require Import Blockchain.
From SmartContracts Require Import LocalBlockchain.
From SmartContracts Require Import Congress.
From SmartContracts Require Import Oak.
From Containers Require SetInterface MapInterface OrderedTypeEx.
From SmartContracts Require Import Containers.
From Coq Require Import List.
From Coq Require Import ZArith.
Import ListNotations.
......@@ -82,13 +82,13 @@ Section LocalBlockchainTests.
| Some s => s
| None => {| owner := 0;
state_rules := setup_rules;
proposals := MapInterface.empty Proposal;
proposals := FMap.empty;
next_proposal_id := 0;
members := SetInterface.empty |}
members := FSet.empty |}
end.
Compute (congress_ifc.(get_state) chain4).
Compute (SetInterface.elements (congress_state chain4).(members)).
Compute (FSet.elements (congress_state chain4).(members)).
(* person_1 adds person_1 and person_2 as members of congress *)
Let add_person p :=
......@@ -97,7 +97,7 @@ Section LocalBlockchainTests.
Let chain5 := otry (LocalBlockchain.add_block baker [(person_1, add_person person_1) ;
(person_1, add_person person_2)] chain4).
Compute (SetInterface.elements (congress_state chain4).(members)).
Compute (FSet.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
......@@ -106,7 +106,7 @@ Section LocalBlockchainTests.
congress_ifc.(call) 0 (create_proposal [cact_transfer person_3 3]).
Let chain6 := otry (LocalBlockchain.add_block baker [(person_1, create_proposal_call)] chain5).
Compute (MapInterface.elements (congress_state chain6).(proposals)).
Compute (FMap.elements (congress_state chain6).(proposals)).
(* person_1 and person_2 votes for the proposal *)
Let vote_proposal :=
......@@ -114,7 +114,7 @@ Section LocalBlockchainTests.
Let chain7 := otry (LocalBlockchain.add_block baker [(person_1, vote_proposal);
(person_2, vote_proposal)] chain6).
Compute (MapInterface.elements (congress_state chain7).(proposals)).
Compute (FMap.elements (congress_state chain7).(proposals)).
(* Finish the proposal *)
Let finish_proposal :=
......
From Coq Require Import ZArith.
From Containers Require Import Sets Maps.
From Containers Require SetProperties.
From SmartContracts Require Import Monads.
From SmartContracts Require Import Containers.
From Coq Require Import List.
From Coq Require Import Setoid.
Import ListNotations.
Inductive OakType :=
| oak_empty : OakType
......@@ -27,7 +27,7 @@ Proof.
Qed.
Program Instance empty_set_strict_order
: OrderedType.StrictOrder (fun (_ _ : Empty_set) => False) (@eq Empty_set).
: StrictOrder (fun (_ _ : Empty_set) => False) (@eq Empty_set).
Solve Obligations with contradiction.
Program Instance empty_set_ordered_type : UsualOrderedType Empty_set.
Solve Obligations with contradiction.
......@@ -58,11 +58,11 @@ Local Fixpoint interp_type_with_ordering (t : OakType) : OakInterpretation :=
build_interpretation (list aT) _
| oak_set a =>
let (aT, _) := interp_type_with_ordering a in
build_interpretation (set aT) _
build_interpretation (FSet aT) _
| oak_map a b =>
let (aT, _) := interp_type_with_ordering a in
let (bT, _) := interp_type_with_ordering b in
build_interpretation Map[aT, bT] _
build_interpretation (FMap aT bT) _
end.
Definition interp_type (t : OakType) : Type :=
......@@ -116,22 +116,24 @@ Instance oak_int_equivalence : OakTypeEquivalence Z :=
Instance oak_bool_equivalence : OakTypeEquivalence bool :=
make_trivial_equiv oak_bool.
Program Instance oak_nat_equivalence : OakTypeEquivalence nat :=
Instance oak_nat_equivalence : OakTypeEquivalence nat :=
{| serialize n := serialize (Z.of_nat n);
deserialize z := do z' <- deserialize z; Some (Z.to_nat z'); |}.
Next Obligation.
Proof.
intros x.
rewrite ote_equivalence.
simpl.
rewrite Nat2Z.id.
reflexivity.
Qed.
Defined.
Program Instance oak_value_equivalence : OakTypeEquivalence OakValue :=
Instance oak_value_equivalence : OakTypeEquivalence OakValue :=
{| serialize v := v;
deserialize v := Some v; |}.
deserialize v := Some v;
ote_equivalence x := eq_refl (Some x); |}.
Generalizable Variables A B.
Program Instance oak_sum_equivalence
Instance oak_sum_equivalence
`{e_a : OakTypeEquivalence A}
`{e_b : OakTypeEquivalence B}
: OakTypeEquivalence (A + B)%type :=
......@@ -151,19 +153,12 @@ Program Instance oak_sum_equivalence
else do b <- @deserialize _ e_b (build_oak_value v val);
Some (inr b)
| _ => None
end;
|}.
Next Obligation.
destruct x as [a | b]; rewrite ote_equivalence; reflexivity.
(*
- change ({| oak_value_type := oak_value_type (serialize a);
oak_value := oak_value (serialize a) |}) with (serialize a).
rewrite ote_equivalence.
*)
Qed.
end; |}.
Proof.
intros [a | b]; simpl; rewrite ote_equivalence; reflexivity.
Defined.
Program Instance oak_pair_equivalence
Instance oak_pair_equivalence