Switch to finite maps from std++

.gitlab-ci.yml

@@ -12,28 +12,15 @@ stages:
     - opam config list
     - opam repo list
     - opam list
-    - echo "Cloning branch $COQ_CONTAINERS_BRANCH"
-    - git clone --branch $COQ_CONTAINERS_BRANCH https://github.com/jakobbotsch/containers.git dep-coq-containers
-    - cd dep-coq-containers
-    - make -j
-    - make -f Makefile.coq install
-    - cd ..
-    - rm -rf dep-coq-containers
   script:
     - sudo chown -R coq:coq "$CI_PROJECT_DIR"
     - make -j
 
 coq:8.8:
   extends: .build
-  variables:
-    COQ_CONTAINERS_BRANCH: 'v8.8'
 
 coq:8.9:
   extends: .build
-  variables:
-    COQ_CONTAINERS_BRANCH: 'v8.9'
 
 coq:dev:
   extends: .build
-  variables:
-    COQ_CONTAINERS_BRANCH: 'vdev'

README.md

@@ -3,21 +3,11 @@ This repo is a playground for various experiments with embedding Oak contracts
 into Coq and verifying them.
 
 ## Building/Developing
-This repo uses the coq-containers library by Stéphane Lescuyer. This must be
-installed first. For Coq 8.9 follow the following steps:
+This repo uses the std++ library. This must be installed first and can be
+installed via Opam (`opam install coq-stdpp`). For more instructions, see
+[the stdpp readme](https://gitlab.mpi-sws.org/iris/stdpp).
 
-```bash
-git clone https://github.com/coq-contribs/containers
-cd containers
-make -j
-make -f Makefile.coq install
-```
-
-For other versions of Coq you will need to use an appropriate tag of this repo.
-See [.gitlab-ci.yml](.gitlab-ci.yml) for how the CI builds with older versions
-of Coq.
-
-After coq-containers is installed, this repo should build with
+After stdpp is installed, this repo should build with
 ```bash
 make
 ```

src/Congress.v

@@ -65,7 +65,7 @@ Record State :=
     state_rules : Rules;
     proposals : FMap nat Proposal;
     next_proposal_id : ProposalId;
-    members : FSet Address;
+    members : FMap Address unit;
   }.
 
 Instance eta_state : Settable _ :=
@@ -91,7 +91,7 @@ Definition init (ctx : ContractCallContext) (setup : Setup) : option State :=
             state_rules := setup.(setup_rules);
             proposals := FMap.empty;
             next_proposal_id := 1%nat;
-            members := FSet.empty |}
+            members := FMap.empty |}
   else
     None.
 
@@ -153,7 +153,7 @@ Definition do_finish_proposal
   else
     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 total_members := Z.of_nat (FMap.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
@@ -174,7 +174,7 @@ 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 := FSet.mem sender state.(members) in
+  let is_from_member := FMap.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) =>
@@ -187,10 +187,10 @@ Definition receive
             None
 
   | true, _, Some (add_member new_member) =>
-        Some (state[[members ::= FSet.add new_member]], [])
+        Some (state[[members ::= FMap.add new_member tt]], [])
 
   | true, _, Some (remove_member old_member) =>
-        Some (state[[members ::= FSet.remove old_member]], [])
+        Some (state[[members ::= FMap.remove old_member]], [])
 
   | _, true, Some (create_proposal actions) =>
         Some (add_proposal actions chain state, [])
@@ -224,12 +224,23 @@ Program Instance rules_equivalence : OakTypeEquivalence Rules :=
        Some (build_rules a b c); |}.
        not work here? *)
      deserialize := deserialize_rules; |}.
+Next Obligation.
+  intros x. unfold deserialize_rules.
+  rewrite deserialize_serialize.
+  reflexivity.
+Qed.
 
 Program Instance setup_equivalence : OakTypeEquivalence Setup :=
   {| serialize s := serialize s.(setup_rules);
      deserialize or :=
        do rules <- deserialize or;
        Some (build_setup rules); |}.
+Next Obligation.
+  intros x.
+  simpl.
+  rewrite deserialize_serialize.
+  reflexivity.
+Qed.
 
 Definition deserialize_congress_action (v : OakValue) : option CongressAction :=
   do val <- deserialize v;
@@ -247,9 +258,10 @@ Program Instance congress_action_equivalence : OakTypeEquivalence CongressAction
          end;
      deserialize := deserialize_congress_action; |}.
 Next Obligation.
+  intros ca.
   unfold deserialize_congress_action.
-  rewrite ote_equivalence.
-  destruct x; reflexivity.
+  rewrite deserialize_serialize.
+  destruct ca; reflexivity.
 Qed.
 
 Definition deserialize_proposal (v : OakValue) : option Proposal :=
@@ -263,9 +275,10 @@ Program Instance proposal_equivalence : OakTypeEquivalence Proposal :=
      deserialize := deserialize_proposal;
   |}.
 Next Obligation.
+  intros p.
   unfold deserialize_proposal.
-  rewrite ote_equivalence.
-  destruct x; reflexivity.
+  rewrite deserialize_serialize.
+  destruct p; reflexivity.
 Qed.
 
 Definition serialize_msg (m : Msg) : OakValue :=
@@ -300,8 +313,9 @@ Definition deserialize_msg (v : OakValue) : option Msg :=
 Program Instance msg_equivalence : OakTypeEquivalence Msg :=
   {| serialize := serialize_msg; deserialize := deserialize_msg; |}.
 Next Obligation.
+  intros msg.
   unfold serialize_msg, deserialize_msg.
-  destruct x; repeat (simpl; rewrite ote_equivalence); reflexivity.
+  destruct msg; repeat (simpl; rewrite deserialize_serialize); reflexivity.
 Qed.
 
 Definition serialize_state (s : State) : OakValue :=
@@ -316,12 +330,13 @@ Program Instance state_equivalence : OakTypeEquivalence State :=
   {| serialize := serialize_state; deserialize := deserialize_state; |}.
 Next Obligation.
   unfold serialize_state, deserialize_state.
-  destruct x; repeat (simpl; rewrite ote_equivalence); reflexivity.
+  destruct x; repeat (simpl; rewrite deserialize_serialize); reflexivity.
 Qed.
 
 Definition contract : Contract Setup Msg State :=
   build_contract version init receive.
 
+
 (*
 (* This first property states that the Congress will only send out actions
    to be performed if there is a matching CreateProposal somewhere in the

src/Containers.v

 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 ZArith.
+From stdpp Require Import gmap.
 From Coq Require Import List.
+From SmartContracts Require Import Monads.
 Import ListNotations.
 
-Notation FSet := SetInterface.set.
+Notation FMap := gmap.gmap.
 
-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.
+Module FMap.
+  Generalizable All Variables.
+  Notation empty := stdpp.base.empty.
+  Notation add := stdpp.base.insert.
+  Notation find := stdpp.base.lookup.
+  Definition mem `{base.Lookup K V M} (i : K) (m : M) :=
+    match base.lookup i m with
+    | Some _ => true
+    | None => false
+    end.
+
+  Notation remove := stdpp.base.delete.
+  Notation elements := fin_maps.map_to_list.
+  Notation size := stdpp.base.size.
+  Notation of_list := fin_maps.list_to_map.
 
-  (* 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.
+              {A B : Type}
+              `{countable.Countable A}
+              (m : FMap A B)
+              : of_list (elements m) = m.
   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 [|? ? hd_hd'_lt]; subst.
-          destruct (OrderedType.compare_dec hd hd').
-          -- reflexivity.
-          -- order.
-          -- order.
+    apply fin_maps.list_to_map_to_list.
   Qed.
-End FSet.
+End FMap.
 
-Notation FMap := MapInterface.dict.
+Instance empty_set_eq_dec : stdpp.base.EqDecision Empty_set.
+Proof. decidable.solve_decision. Defined.
+Program Instance empty_set_countable : countable.Countable Empty_set :=
+  {| countable.encode e := 1%positive; countable.decode d := None; |}.
+Solve Obligations with contradiction.
 
-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.
+(* The default list countable instance is exponential. For instance,
+   1000%positive takes around 10 bits to describe, but
+   countable.encode [1000%positive] returns a positive taking around
+   1000 bits to describe. This is because it writes everything out
+   in unary. Here is a more efficient implementation that works by
+   duplicating the bits of each element and separating them by
+   1~0. *)
+Remove Hints countable.list_countable : typeclass_instances.
+Section ListCountable.
+  Context `{countable.Countable A}.
+  Open Scope positive.
 
-  Proposition of_elements_eq
-              {A B : Type}
-              {_ : OrderedType A}
-              (m : FMap A B)
-              : of_list (elements m) = m.
+  Fixpoint encode_single (p acc : positive) : positive :=
+    match p with
+    | 1 => acc
+    | p'~0 => encode_single p' (acc~0~0)
+    | p'~1 => encode_single p' (acc~1~1)
+    end.
+
+  Fixpoint encode_list' (l : list A) (acc : positive) : positive :=
+    match l with
+    | [] => acc
+    | hd :: tl => encode_list' tl (encode_single (encode hd) (acc~1~0))
+    end.
+
+  Definition encode_list l := encode_list' l 1.
+
+  Fixpoint decode_list'
+           (p : positive)
+           (acc_l : list A)
+           (acc_elm : positive)
+    : option (list A) :=
+      match p with
+      | 1 => Some acc_l
+      | p'~0~0 => decode_list' p' acc_l (acc_elm~0)
+      | p'~1~1 => decode_list' p' acc_l (acc_elm~1)
+      | p'~1~0 => do elm <- countable.decode acc_elm;
+                  decode_list' p' (elm :: acc_l) 1
+      | _ => None
+      end.
+
+  Definition decode_list (p : positive) : option (list A) :=
+    decode_list' p [] 1.
+
+  Lemma encode_single_app (p acc : positive) :
+    encode_single p acc = acc ++ encode_single p 1.
   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.
+    generalize dependent acc.
+    induction p.
+    - intros acc.
+      simpl.
+      rewrite IHp.
+      rewrite (IHp 7).
+      rewrite Papp_assoc.
+      reflexivity.
+    - intros acc.
+      simpl.
+      rewrite IHp.
+      rewrite (IHp 4).
+      rewrite Papp_assoc.
+      reflexivity.
+    - intros acc.
+      reflexivity.
+  Qed.
+
+  Lemma encode_list'_app (l : list A) (acc : positive) :
+    encode_list' l acc = acc ++ encode_list' l 1.
+  Proof.
+    generalize dependent acc.
     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.
+    - intros acc; reflexivity.
+    - intros acc.
+      simpl.
+      rewrite IHl.
+      rewrite (IHl (encode_single _ _)).
+      rewrite Papp_assoc.
+      rewrite (encode_single_app _ 6).
+      rewrite Papp_assoc.
+      simpl.
+      rewrite <- encode_single_app.
+      reflexivity.
   Qed.
-End FMap.
+
+  Lemma decode_list'_single (p prefix : positive) (l : list A) :
+    decode_list' (prefix ++ encode_single p 1) l 1 = decode_list' prefix l p.
+  Proof.
+    generalize dependent prefix.
+    induction p.
+    - intros.
+      simpl.
+      rewrite encode_single_app.
+      rewrite Papp_assoc.
+      rewrite IHp.
+      reflexivity.
+    - intros.
+      simpl.
+      rewrite encode_single_app.
+      rewrite Papp_assoc.
+      rewrite IHp.
+      reflexivity.
+    - reflexivity.
+  Qed.
+
+  Lemma decode_list'_list (prefix : positive) (l acc : list A) :
+    decode_list' (prefix ++ encode_list' l 1) acc 1 = decode_list' prefix (l ++ acc) 1.
+  Proof.
+    generalize dependent prefix.
+    generalize dependent acc.
+    induction l as [| hd tl IHl].
+    - reflexivity.
+    - intros acc prefix.
+      simpl.
+      rewrite encode_list'_app.
+      rewrite Papp_assoc.
+      rewrite IHl.
+      rewrite encode_single_app.
+      rewrite Papp_assoc.
+      rewrite decode_list'_single.
+      simpl.
+      rewrite decode_encode.
+      reflexivity.
+  Qed.
+
+  Global Program Instance list_countable : countable.Countable (list A) :=
+    {| encode := encode_list; decode := decode_list; |}.
+  Next Obligation.
+    intros l.
+    unfold encode_list, decode_list.
+    replace (encode_list' _ _) with (1 ++ encode_list' l 1) by apply Papp_1_l.
+    rewrite decode_list'_list.
+    simpl.
+    rewrite app_nil_r.
+    reflexivity.
+  Qed.
+End ListCountable.

src/LocalBlockchainTests.v

@@ -82,11 +82,11 @@ Section LocalBlockchainTests.
                  state_rules := setup_rules;
                  proposals := FMap.empty;
                  next_proposal_id := 0;
-                 members := FSet.empty |}
+                 members := FMap.empty |}
     end.
 
   Compute (congress_ifc.(get_state) chain4).
-  Compute (FSet.elements (congress_state chain4).(members)).
+  Compute (FMap.elements (congress_state chain4).(members)).
 
   (* person_1 adds person_1 and person_2 as members of congress *)
   Let add_person p :=
@@ -95,7 +95,7 @@ Section LocalBlockchainTests.
   Let chain5 := otry (chain4.(add_block) baker [(person_1, add_person person_1);
                                                 (person_1, add_person person_2)]).
 
-  Compute (FSet.elements (congress_state chain5).(members)).
+  Compute (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

src/Oak.v

@@ -26,43 +26,40 @@ Proof.
     try simpl; try rewrite IHx; try rewrite IHx1; try rewrite IHx2; reflexivity.
 Qed.
 
-Program Instance empty_set_strict_order
-  : 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.
-
 Set Primitive Projections.
 Record OakInterpretation :=
   build_interpretation {
     oi_ty : Type;
-    oi_order : OrderedType oi_ty;
+    oi_eqdec : stdpp.base.EqDecision oi_ty;
+    oi_countable : countable.Countable oi_ty;
   }.
 
+Arguments build_interpretation _ {_ _}.
+
 Local Fixpoint interp_type_with_ordering (t : OakType) : OakInterpretation :=
   match t with
-  | oak_empty => build_interpretation Empty_set _
-  | oak_unit => build_interpretation unit _
-  | oak_int => build_interpretation Z _
-  | oak_bool => build_interpretation bool _
+  | oak_empty => build_interpretation Empty_set
+  | oak_unit => build_interpretation unit
+  | oak_int => build_interpretation Z
+  | oak_bool => build_interpretation bool
   | oak_sum a b =>
-    let (aT, _) := interp_type_with_ordering a in
-    let (bT, _) := interp_type_with_ordering b in
-    build_interpretation (aT + bT)%type _
+    let (aT, _, _) := interp_type_with_ordering a in
+    let (bT, _, _) := interp_type_with_ordering b in
+    build_interpretation (aT + bT)%type
   | oak_pair a b =>
-    let (aT, _) := interp_type_with_ordering a in
-    let (bT, _) := interp_type_with_ordering b in
-    build_interpretation (aT * bT)%type _
+    let (aT, _, _) := interp_type_with_ordering a in
+    let (bT, _, _) := interp_type_with_ordering b in
+    build_interpretation (aT * bT)%type
   | oak_list a =>
-    let (aT, _) := interp_type_with_ordering a in
-    build_interpretation (list aT) _
+    let (aT, _, _) := interp_type_with_ordering a in
+    build_interpretation (list aT)
   | oak_set a =>
-    let (aT, _) := interp_type_with_ordering a in
-    build_interpretation (FSet aT) _
+    let (aT, _, _) := interp_type_with_ordering a in
+    build_interpretation (FMap aT unit)
   | oak_map a b =>
-    let (aT, _) := interp_type_with_ordering a in
-    let (bT, _) := interp_type_with_ordering b in
-    build_interpretation (FMap aT bT) _
+    let (aT, _, _) := interp_type_with_ordering a in
+    let (bT, _, _) := interp_type_with_ordering b in
+    build_interpretation (FMap aT bT)
   end.
 
 Definition interp_type (t : OakType) : Type :=
@@ -88,173 +85,197 @@ Class OakTypeEquivalence (ty : Type) :=
   {
     serialize : ty -> OakValue;
     deserialize : OakValue -> option ty;
-    ote_equivalence : forall (x : ty), deserialize (serialize x) = Some x;
+    deserialize_serialize : forall (x : ty), deserialize (serialize x) = Some x;
   }.
 
-Global Opaque serialize deserialize ote_equivalence.
 
-Definition make_trivial_equiv (ot : OakType) : OakTypeEquivalence (interp_type ot).
-Proof.
-  refine {| serialize := build_oak_value ot;
-            deserialize := extract_oak_value ot;
-            ote_equivalence := _ |}.
-  intros x.
-  unfold extract_oak_value.
-  rewrite eq_oak_type_dec_refl.
-  reflexivity.
-Defined.
 
-Instance oak_empty_equivalence : OakTypeEquivalence Empty_set :=
-  make_trivial_equiv oak_empty.
+Global Opaque serialize deserialize deserialize_serialize.
+
+Program Instance oak_empty_equivalence : OakTypeEquivalence Empty_set :=
+  {| serialize e := ltac:(contradiction);
+     deserialize v := None; |}.
+Solve Obligations with contradiction.
 
-Instance oak_unit_equivalence : OakTypeEquivalence unit :=
-  make_trivial_equiv oak_unit.
+Program Instance oak_unit_equivalence : OakTypeEquivalence unit :=
+  {| serialize u := build_oak_value oak_unit u;
+     deserialize := extract_oak_value oak_unit; |}.
+Solve Obligations with reflexivity.
 
-Instance oak_int_equivalence : OakTypeEquivalence Z :=
-  make_trivial_equiv oak_int.
+Program Instance oak_int_equivalence : OakTypeEquivalence Z :=
+  {| serialize i := build_oak_value oak_int i;
+     deserialize := extract_oak_value oak_int; |}.
+Solve Obligations with reflexivity.
 
-Instance oak_bool_equivalence : OakTypeEquivalence bool :=
-  make_trivial_equiv oak_bool.
+Program Instance oak_bool_equivalence : OakTypeEquivalence bool :=
+  {| serialize b := build_oak_value oak_bool b;
+     deserialize := extract_oak_value oak_bool; |}.
+Solve Obligations with reflexivity.
 
-Instance oak_nat_equivalence : OakTypeEquivalence nat.
-Proof.
-  refine {| serialize n := serialize (Z.of_nat n);