Skip to main content

🔥 Carbonated_map.v

Proofs

See code, Gitlab , OCaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V7.
Require TezosOfOCaml.Proto_alpha.Carbonated_map.

Require Import TezosOfOCaml.Environment.V7.Proofs.List.
Require Import TezosOfOCaml.Environment.V7.Proofs.Map.
Require Import TezosOfOCaml.Environment.V7.Proofs.Option.

Module COMPARABLE.
Translation to the standard [Compare.COMPARABLE] signature.
  Definition to_Compare {t : Set} (C : Carbonated_map.COMPARABLE (t := t)) :
    Compare.COMPARABLE (t := t) :=
    {|
      Compare.COMPARABLE.compare := C.(Carbonated_map.COMPARABLE.compare);
    |}.
End COMPARABLE.

We will show here many properties about the [Make] functor inside the [Make_builder] functor. We will write our lemmas as if we were in the functor, with access to the [FArgs] parameters.
Module Make_builder. Module Make.
  Import Proto_alpha.Carbonated_map.Make_builder.
  Import Proto_alpha.Carbonated_map.Make_builder.Make.

  Module Valid.
A map is valid when its [size] field is its actual size.
    Definition t `{FArgs} {a : Set} (map : t a) : Prop :=
      M.(Map.S.cardinal) map.(t.map) = map.(t.size).
  End Valid.

The [empty] operator is a valid map.
  Lemma empty_is_valid `{FArgs} {A : Set} : Valid.t (empty (A := A)).
  Proof.
    reflexivity.
  Qed.

The [empty] operator behaves as on standard maps.
  Lemma empty_eq `{FArgs} {A : Set} :
    (empty (A := A)).(t.map) = M.(Map.S.empty).
  Proof.
    reflexivity.
  Qed.

The [singleton] operator produces a valid map.
  Lemma singleton_is_valid `{FArgs} {A : Set} k v :
    Valid.t (singleton (A := A) k v).
  Proof.
    reflexivity.
  Qed.

The [singleton] operator behaves as on standard maps.
  Lemma singleton_eq `{FArgs} {A : Set} k v :
    (singleton (A := A) k v).(t.map) = M.(Map.S.singleton) k v.
  Proof.
    reflexivity.
  Qed.

The [find] operator behaves as on standard maps.
  Lemma find_eq `{FArgs} {A : Set} ctxt k (map : t A) :
    letP?relaxed '(v, _) := find (A := A) ctxt k map in
    v = M.(Map.S.find) k map.(t.map).
  Proof.
    unfold find.
    destruct (_.(Carbonated_map.GAS.consume)); simpl; trivial.
  Qed.

  #[local] Transparent Map.Make.

The [update] operator produces a valid map.
  Lemma update_is_valid `{FArgs} {A : Set} ctxt k f (map : t A) :
    Valid.t map
    letP?relaxed '(updated_map, _) := update ctxt k f map in
    Valid.t updated_map.
  Proof.
    intros Hv.
    unfold Valid.t in Hv.
    unfold update.
    destruct (_.(Carbonated_map.GAS.consume)); simpl; auto.
    destruct map; simpl in ×.
    destruct f eqn:G; try exact I.
    simpl.
    destruct p.
    destruct Map.Make.find eqn:G0.
    { destruct o;
      destruct (_.(Carbonated_map.GAS.consume)); try exact I.
      { unfold Valid.t; simpl.
        rewrite <- Hv.
        eapply cardinal_add_find_Some; eauto.
      }
      { unfold Valid.t; simpl.
        rewrite <- Hv.
        unfold Make.cardinal.
        repeat rewrite length_eq.
        rewrite <- (length_remove_find_Some
          map k a); auto.
        assert ( x, normalize_int x =
          normalize_int (BinInt.Z.succ x) -i 1)
          as Hnorm by (unfold "-i", normalize_int; lia).
        rewrite Hnorm.
        rewrite Nat2Z.inj_succ.
        reflexivity.
      }
    }
    { destruct o; auto.
      destruct (_.(Carbonated_map.GAS.consume)); try exact I.
      unfold Valid.t; simpl.
      rewrite <- Hv.
      eapply cardinal_add_find_None; eauto.
    }
  Qed.

The [update] operator behaves as on standard maps.
  Lemma update_eq `{FArgs} {A : Set} ctxt k f f_with_cost (map : t A) :
    ( ctxt v,
      letP?relaxed '(v', _) := f_with_cost ctxt v in
      v' = f v
    )
    letP?relaxed '(updated_map, _) := update ctxt k f_with_cost map in
    updated_map.(t.map) = M.(Map.S.update) k f map.(t.map).
  Proof.
    intro Hf.
    unfold update.
    destruct (_.(Carbonated_map.GAS.consume)); try exact I.
    simpl.
    destruct f_with_cost eqn:G.
    { simpl.
      destruct p.
      destruct Map.Make.find eqn:H_find.
      { destruct o;
          destruct (_.(Carbonated_map.GAS.consume)); try exact I;
          simpl.
        { pose (Hf g (Some a)) as Hf2.
          rewrite G in Hf2.
          simpl in Hf2.
          unfold Map.Make.update.
          destruct map; simpl in ×.
          rewrite H_find.
          now rewrite <- Hf2.
        }
        { unfold Map.Make.update.
          destruct map; simpl in ×.
          rewrite H_find.
          pose (Hf g (Some a)) as Hf2.
          rewrite G in Hf2; simpl in Hf2.
          now rewrite <- Hf2.
        }
      }
      { destruct o.
        { destruct (_.(Carbonated_map.GAS.consume)); try exact I.
          simpl.
          destruct map; simpl in ×.
          unfold Map.Make.update.
          rewrite H_find.
          pose (Hf g None) as Hf2.
          rewrite G in Hf2; simpl in Hf2.
          rewrite <- Hf2; auto.
        }
        { destruct map; simpl in ×.
          unfold Map.Make.update.
          rewrite H_find.
          pose (Hf g None) as Hf2.
          rewrite G in Hf2; simpl in Hf2.
          rewrite <- Hf2.
          symmetry.
          apply remove_find_none; auto.
        }
      }
    }
    { exact I. }
  Qed.

The [to_list] operator behaves as on standard maps.
  Lemma to_list_eq `{FArgs} {A : Set} ctxt map :
    letP?relaxed '(l, _) := to_list (A := A) ctxt map in
    l = M.(Map.S.bindings) map.(t.map).
  Proof.
    unfold M, Map.Make; simpl.
    destruct map; simpl.
    unfold to_list.
    destruct (_.(Carbonated_map.GAS.consume)); simpl; auto.
  Qed.

The [add] operator produces a valid map.
  Lemma add_is_valid `{FArgs} {A : Set} ctxt merge_overlap k v (map : t A) :
    Valid.t map
    letP?relaxed '(added_map, _) := add ctxt merge_overlap k v map in
    Valid.t added_map.
  Proof.
    intro Hv.
    unfold add; simpl.
    do 2 (destruct (_.(Carbonated_map.GAS.consume)); try exact I; simpl).
    destruct map; unfold Valid.t in *; simpl in ×.
    destruct Map.Make.find eqn:G; simpl.
    { destruct merge_overlap eqn:G0; try exact I.
      destruct p; simpl.
      erewrite cardinal_add_find_Some; eauto.
    }
    { erewrite cardinal_add_find_None; eauto.
      congruence.
    }
  Qed.

The [add] operator behaves as on standard maps.
  Lemma add_eq `{FArgs} {A : Set} ctxt merge_overlap merge_overlap_with_cost k v
    (map : t A) :
    ( ctxt v1 v2,
      letP?relaxed '(v, _) := merge_overlap_with_cost ctxt v1 v2 in
      v = merge_overlap v1 v2
    )
    letP?relaxed '(added_map, _) := add ctxt merge_overlap_with_cost k v map in
    let f old_value :=
      match old_value with
      | Some old_valuemerge_overlap old_value v
      | Nonev
      end in
    added_map.(t.map) = M.(Map.S.add) k
      (f (M.(Map.S.find) k map.(t.map)))
      map.(t.map).
  Proof.
    intros.
    simpl.
    unfold add.
    do 2 (destruct (_.(Carbonated_map.GAS.consume)); simpl; try exact I).
    destruct map; simpl.
    destruct Map.Make.find eqn:G.
    { destruct merge_overlap_with_cost eqn:G0; simpl; try auto.
      pose proof (H1 g0 a v) as Hmo.
      rewrite G0 in Hmo.
      destruct p; simpl.
      congruence.
    }
    { reflexivity. }
  Qed.

The [add_key_values_to_map] operator produces a valid map.
  Lemma add_key_values_to_map_is_valid `{FArgs} {A : Set}
    ctxt merge_overlap (map : t A) key_values :
    Valid.t map
    letP?relaxed '(added_map, _) :=
      add_key_values_to_map ctxt merge_overlap map key_values in
    Valid.t added_map.
  Proof.
    intro.
    unfold add_key_values_to_map.
    destruct fold_left_e eqn:G;
      [|exact I].
    Tactics.destruct_pairs.
    simpl.
    epose fold_left_e_lemma; eauto.
    epose (P := fun '(map, _)
      Valid.t map).
    cut (P (t0, c)); auto.
    eapply p.
    2:{ exact G. }
    2:{ auto. }
    intros; simpl.
    unfold P in ×.
    destruct a1, a2, b.
    pose proof (add_is_valid c0 merge_overlap t3 a t1 H2) as H_add_valid.
    now rewrite H3 in H_add_valid.
  Qed.

The [of_list] operator produces a valid map.
  Lemma of_list_is_valid `{FArgs} {A : Set} ctxt merge_overlap key_values :
    letP?relaxed '(map, _) := of_list (A := A) ctxt merge_overlap key_values in
    Valid.t map.
  Proof.
    apply add_key_values_to_map_is_valid.
    apply empty_is_valid.
  Qed.

The [merge] operator produces a valid map.
  Lemma merge_is_valid `{FArgs} {A : Set} ctxt merge_overlap map1 map2 :
    Valid.t map1
    letP?relaxed '(merged_map, _) := merge (A := A) ctxt merge_overlap map1 map2 in
    Valid.t merged_map.
  Proof.
    unfold merge.
    intro Hv.
    destruct (_.(Carbonated_map.GAS.consume));
      [simpl|exact I].
    unfold Map.Make.fold_e.
    destruct map2.
    generalize Hv.
    generalize map1.
    generalize g.
    clear Hv; clear map1; clear g.
    induction map; [auto|].
    simpl; intros.
    Tactics.destruct_pairs.
    destruct add eqn:?.
    unfold Error_monad.ok in ×.
    destruct p.
    { eapply IHmap.
      epose proof (add_is_valid g merge_overlap
        k a map1 Hv) as Hadd.
      unfold Map.Make.key, Map.Make.Ord in ×.
      rewrite Heqt0 in Hadd; auto.
    }
    { clear IHmap.
      induction map.
      { exact I. }
      { simpl.
        Tactics.destruct_pairs.
        apply IHmap.
      }
    }
  Qed.

  Lemma merge_In1 `{FArgs} {A : Set} ctxt ctxt' merge_overlap_with_cost :
     k a1 a2 a3 (m1 m2 m3 : t.record A),
    StrictlySorted.t (List.map fst (m2.(t.map)))
    In (k, a1) m1.(t.map)
    In (k, a2) m2.(t.map)
    merge ctxt merge_overlap_with_cost m1 m2 =
        Pervasives.Ok (m3, ctxt')
    ( ctxt', letP?relaxed ' (a4, _)
     := merge_overlap_with_cost ctxt' a1 a2
     in a4 = a3)
    In (k, a3) m3.(t.map).
  Proof.
    intros.
    unfold merge in H2.
  Admitted.

  Lemma merge_In2 `{FArgs} {A : Set} ctxt ctxt' merge_overlap_with_cost :
     k a (m1 m2 m3 : t.record A),
    StrictlySorted.t (List.map fst (m2.(t.map)))
    In (k, a) m1.(t.map)
    ¬ In k (List.map fst m2.(t.map))
    merge ctxt merge_overlap_with_cost m1 m2 =
        Pervasives.Ok (m3, ctxt')
    In (k, a) m3.(t.map).
  Proof.
  Admitted.

  Lemma merge_In3 `{FArgs} {A : Set} ctxt ctxt' merge_overlap_with_cost :
     k a (m1 m2 m3 : t.record A),
    StrictlySorted.t (List.map fst (m2.(t.map)))
    In (k, a) m2.(t.map)
    ¬ In k (List.map fst m1.(t.map))
    merge ctxt merge_overlap_with_cost m1 m2 =
        Pervasives.Ok (m3, ctxt')
    In (k, a) m3.(t.map).
  Proof.
  Admitted.

  Lemma merge_In_inversion `{FArgs} {A : Set}
    : {m1 m2 m3 : t A} {merge_overlap c1 c2},
    merge c1 merge_overlap m1 m2 = Pervasives.Ok (m3, c2)
     {k v}, In (k, v) m3.(t.map)
      ( ctxt ctxt' a1 a2, merge_overlap ctxt a1 a2 =
           Pervasives.Ok (v, ctxt')
         In (k, a1) m1.(t.map)
         In (k, a2) m2.(t.map))
      (In (k, v) m1.(t.map) ¬ In k (List.map fst m2.(t.map)))
      (In (k, v) m2.(t.map) ¬ In k (List.map fst m1.(t.map))).
    Proof.
    Admitted.

The [merge] operator behaves as on standard maps.
  Lemma merge_eq `{FArgs} {A : Set} ctxt merge_overlap merge_overlap_with_cost
    map1 map2 :
    @Map.Valid.t C_t
    (@Map.Make.Build_FArgs C_t
      (COMPARABLE.Build_signature C_t
        (@Carbonated_map.COMPARABLE.compare
          _ (@C _ H))))
    StrictlySorted.t
      (List.map fst map1.(t.map))
    StrictlySorted.t
      (List.map fst map2.(t.map))
    ( ctxt v1 v2,
      letP?relaxed '(v, _) := merge_overlap_with_cost ctxt v1 v2 in
      v = merge_overlap v1 v2
    )
    letP?relaxed '(merged_map, _) :=
      merge (A := A) ctxt merge_overlap_with_cost map1 map2 in
    merged_map.(t.map) =
    let generalized_merge k v1 v2 :=
      match v1, v2 with
      | Some v1, Some v2Some (merge_overlap v1 v2)
      | Some v1, NoneSome v1
      | None, Some v2Some v2
      | _, _None
      end in
    M.(Map.S.merge) generalized_merge map1.(t.map) map2.(t.map).
  Proof.
    intros Hv Hm1 Hm2 ?.
    destruct merge eqn:?; [|exact I].
    Tactics.destruct_pairs.
    simpl.
    apply StrictlySorted.map_extensional; auto.
    { unfold merge in Heqt0.
      destruct (_.(Carbonated_map.GAS.consume)); [|discriminate].
      simpl in ×.
      unfold Map.Make.fold_e in Heqt0.
      pose (S := fun (em : M? (t A × G.(Carbonated_map.GAS.context))) ⇒
        letP?relaxed '(m,_) := em in StrictlySorted.t (List.map fst (m.(t.map)))).
      cut (S (Pervasives.Ok (t0, c))); auto.
      rewrite <- Heqt0.
      apply Make_fold_lemma.
      { unfold S; intros.
        destruct b; [|exact I].
        Tactics.destruct_pairs; simpl in ×.
        destruct add eqn:Hadd; [|exact I].
        Tactics.destruct_pairs; simpl in ×.
        unfold add in Hadd.
        destruct (_.(Carbonated_map.GAS.consume));
          [|discriminate].
        simpl in Hadd.
        destruct (_.(Carbonated_map.GAS.consume));
          [|discriminate].
        simpl in Hadd.
        destruct Map.Make.find eqn:?; simpl in Hadd.
        { destruct merge_overlap_with_cost eqn:?;
            simpl in Hadd; [|discriminate].
          destruct p; simpl in Hadd.
          inversion Hadd.
          simpl.
          apply StrictlySorted.add_preserves_sorting; auto.
        }
        { inversion Hadd.
          simpl.
          apply StrictlySorted.add_preserves_sorting; auto.
        }
      }
      { unfold S; simpl; auto.
      }
    }
    { simpl.
      apply StrictlySorted.merge_ss; auto.
    }
    { intros [k v]; split.
      { intro.
        destruct (merge_In_inversion Heqt0 H2) as [|[|]].
        { destruct H3 as [c1 [c2 [a1 [a2 [Ha1 [Ha2 Ha3]]]]]].
          eapply Make_merge_In3; eauto.
          epose (H1 _ _ _) as H_merge_overlap_eq.
          rewrite Ha1 in H_merge_overlap_eq.
          simpl in H_merge_overlap_eq; congruence.
        }
        { eapply Make_merge_In1; try tauto; tauto. }
        { eapply Make_merge_In2; try tauto; tauto. }
      }
      { intro Hin.
        destruct (Make_merge_In_inversion Hin) as
          [ [a [Ha1 [Ha2 Ha3]]] |
          [ [b [Hb1 [Hb2 Hb3]]] |
            [a [b [Hab1 [Hab2 Hab3]]]]
]]; try discriminate.
        { eapply merge_In2.
          { exact Hm2. }
          { inversion Ha3.
            rewrite H3 in Ha1.
            exact Ha1.
          }
          { exact Ha2. }
          { exact Heqt0. }
        }
        { eapply merge_In3.
          { exact Hm2. }
          { inversion Hb3.
            congruence.
          }
          { exact Hb2. }
          { exact Heqt0. }
        }
        { eapply merge_In1.
          { exact Hm2. }
          { exact Hab1. }
          { exact Hab2. }
          { exact Heqt0. }
          { inversion Hab3.
            intro; apply H1.
          }
        }
      }
    }
  Unshelve.
  all: auto.
  Qed.

The [fold] operator behaves as on standard maps.
  Lemma fold_eq `{FArgs} {A B : Set} ctxt f f_with_cost acc (map : t B) :
    ( ctxt acc k v,
      letP?relaxed '(result, _) := f_with_cost ctxt acc k v in
      result = f k v acc
    )
    letP?relaxed '(result, _) := fold_es (A := A) (B := B) ctxt f_with_cost acc map in
    result = M.(Map.S.fold) f map.(t.map) acc.
  Proof.
    intros.
    simpl.
    unfold fold_es.
    simpl.
    unfold Make.fold_e.
    destruct (_.(Carbonated_map.GAS.consume));
      [|exact I].
    destruct map; simpl.
    generalize acc.
    generalize g.
    induction map.
    { reflexivity. }
    { simpl.
      Tactics.destruct_pairs.
      intros.
      destruct Map.Make.fold_es eqn:?;
        [simpl|exact I].
      Tactics.destruct_pairs.
      pose proof (H1 g acc0 k b).
      destruct f_with_cost eqn:H_f_with_cost.
      { Tactics.destruct_pairs.
        simpl in ×.
        pose (IHmap c0 a0) as IH.
        unfold Error_monad.ok in IH.
  Admitted.
  (* @TODO fix this proof *)
(*      rewrite Heqr in IH.
        simpl in *.
        pose proof (H1 g0 acc0 k b) as H_f_eq.
        rewrite H_f_with_cost in H_f_eq.
        simpl in *.
        congruence.
      }
      { cut False; [tauto|].
        clear H1.
        clear IHmap0.
        induction map0.
        { discriminate. }
        { simpl in *.
          Tactics.destruct_pairs; auto.
        }
      }
    }
  Qed. *)


  Lemma fold_conditional_preservation_lemma `{Map.Make.FArgs} {A B : Set}
    (E : B Map.Make.t A B Prop)
    (D : Map.Make.t A B Prop) (* disjoint *)
    (S : Map.Make.t A Prop) (* strictly incr *)
    (f : Map.Make.key A M? B M? B)
    (f_pres_error : ( (t : trace _error) (k : Map.Make.key) (x : A),
    f k x (Pervasives.Error t) = Pervasives.Error t))
    (E_nil : b, E b [] b)
    (E_cons : b1 k a m eb2,
      letP?relaxed b2 := eb2 in
      D ((k,a):: m) b2
      letP?relaxed m' := f k a eb2 in
      E b1 m m' E b1 ((k,a)::m) b2)
    (D_cons : b k a m, S ((k,a) :: m)
      D ((k, a) :: m) b
      letP?relaxed b1 := f k a (Pervasives.Ok b) in
      D m b1)
    (S_cons : p m, S (p :: m) S m)
    : (m : Make.t A) (eb : M? B) b m',
        eb = Pervasives.Ok b S m D m b
        Map.Make.fold f m eb = Pervasives.Ok m'
        E m' m b.
  Proof.
    induction m.
    { intros; simpl.
      rewrite H0 in H3.
      simpl in H3.
      inversion H3.
      apply E_nil.
    }
    { intros.
      destruct a; simpl.
      simpl in H3.
      epose proof (E_cons m' k a m eb).
      rewrite H0 in *; simpl in H4.
      destruct f eqn:?.
      { simpl in H4.
        apply H4; auto.
        eapply IHm; eauto; try congruence.
        epose (D_cons b k a m) as HD.
        rewrite Heqt1 in HD.
        simpl in HD.
        apply HD; auto.
      }
      { unfold tzresult in H3.
        rewrite Make_fold_shortcircuit in H3;
        auto;
        discriminate.
      }
    }
  Qed.

The [map] operator produces a valid map.
  Lemma map_is_valid `{FArgs} {A B : Set} ctxt f m
   (Hv : @Map.Valid.t C_t
  (@Map.Make.Build_FArgs C_t
     (COMPARABLE.Build_signature C_t
        (@Carbonated_map.COMPARABLE.compare _
           (@C _ H))))) :
    Valid.t m
    (* this could be weakened to keys are unique *)
    StrictlySorted.t (List.map fst m.(t.map))
    letP?relaxed '(new_m, _) := map_e (A := A) (B := B) ctxt f m in
    Valid.t new_m.
  Proof.
    intros.
    unfold map_e.
    unfold fold; simpl.
    unfold Make.fold_e.
    destruct (_.(Carbonated_map.GAS.consume));
      [|exact I].
    simpl.
    destruct m; simpl.
    destruct Map.Make.fold_e eqn:?;
      [|exact I].
    destruct p.
    simpl.
    unfold Valid.t in ×.
    simpl.
    pose (E := fun
     (x : (M.(Map.S.t) B × G.(Carbonated_map.GAS.context)))
     (y : M.(Map.S.t) A)
     (z : (M.(Map.S.t) B × G.(Carbonated_map.GAS.context))) ⇒
      (Make.cardinal (fst x) = Make.cardinal y +i Make.cardinal (fst z))%Z
    ).
    simpl in H1.
    rewrite <- H1.
    cut
      (E (t0, c)
         map (Map.Make.empty, g)).
    { unfold E; intro.
      unfold Make.cardinal at 3 in H3.
      simpl in H3.
      rewrite H3.
      apply Pervasives.Int.Valid.int_plus_0_r_eq.
      apply length_is_valid.
    }
    pose (D := fun
      (m1 : M.(Map.S.t) A)
      (m2 : (M.(Map.S.t) B × G.(Carbonated_map.GAS.context))) ⇒
       disj (List.map fst m1) (List.map fst (fst m2))).
    pose (S := fun (m1 : M.(Map.S.t) A) ⇒ StrictlySorted.t (List.map fst m1)).
    eapply (fold_conditional_preservation_lemma E D S).
    9:{ exact Heqr. }
    { intros; reflexivity. }
    { intro.
      unfold E.
      unfold Make.cardinal; simpl.
      simpl.
      symmetry; apply Pervasives.normalize_identity.
      apply length_is_valid.
    }
    { intros.
      destruct eb2; [|exact I].
      destruct p; simpl; intros.
      destruct f eqn:?; [|exact I].
      destruct p; simpl.
      destruct (_.(Carbonated_map.GAS.consume));
        [|exact I].
      simpl; intros.
      unfold E in ×.
      unfold D in ×.
      destruct b1; simpl in ×.
      simpl.
      rewrite cardinal_add_find_None in H4.
      { simpl.
        unfold Make.cardinal in ×.
        simpl.
        rewrite H4.
        rewrite Pervasives.int_add_assoc; lia.
      }
      { apply find_not_In; auto.
        intro.
        eapply H3; eauto.
        left; reflexivity.
      }
    }
    { intros.
      simpl.
      destruct b.
      destruct f eqn:?; [|exact I].
      destruct p; simpl.
      destruct (_.(Carbonated_map.GAS.consume)); [|exact I].
      simpl.
      unfold D in *; simpl in ×.
      unfold disj in ×.
      intros x Hx1 Hx2.
      destruct (In_map_invert Hx2) as [[x' y] [Hxy1 Hxy2]].
      simpl in Hxy1; rewrite Hxy1 in *; clear Hxy1.
      destruct (In_add_destruct Hxy2).
      { inversion H5.
        rewrite <- H7 in *; clear H7.
        unfold S in H3.
        simpl in H3.
        epose proof (StrictlySorted.strictly_sorted_lb_correct
          _ _ Hv H3 _ Hx1).
        rewrite (Compare.Valid.refl Hv) in H6; auto.
        lia.
      }
      { elim (H4 x).
        { right; auto. }
        { assert (x = fst (x,y)) by auto.
          rewrite H6.
          apply in_map; auto.
        }
      }
    }
    { intros.
      unfold S in ×.
      eapply StrictlySorted.ss_tail.
      exact H3.
    }
    { reflexivity. }
    { exact H2. }
    { unfold D; simpl.
      unfold disj; simpl; tauto.
    }
  Qed.

  Lemma map_eq_aux `{FArgs} {A B : Set} ctxt f f_with_cost (m : t A) :
    ( ctxt k v,
      letP?relaxed '(result, _) := f_with_cost ctxt k v in
      result = f k v
    )
    letP?relaxed '(new_m, _) := map_e (A := A) (B := B) ctxt f_with_cost m in
    new_m.(t.map) =
    Map.Make.fold (fun k vMap.Make.add k (f k v)) m.(t.map) M.(S.empty).
  Proof.
    intros.
    unfold map_e.
    unfold fold_e.
    destruct (_.(Carbonated_map.GAS.consume));
      [|exact I].
    simpl.
    unfold Map.Make.fold_e.
    destruct m; simpl in ×.
    assert ( xs c,
    letP?relaxed ' (new_m, _)
:= (let? ' (map1, ctxt0)
    := Map.Make.fold
         (fun (k : Make.key) (v : A)
            (acc : tzresult (M.(Map.S.t) B × G.(Carbonated_map.GAS.context)))
          ⇒
          let? ' (acc_value, ctxt0) := acc
          in let? ' (value_value, ctxt1) := f_with_cost ctxt0 k v
             in let? ' ctxt2
                := G.(Carbonated_map.GAS.consume) ctxt1 (update_cost k size)
                in return? (Map.Make.add k value_value acc_value, ctxt2)) map
         (return? (xs, c))
    in return? ({| t.map := map1; t.size := size |}, ctxt0))
in new_m.(t.map) =
   Map.Make.fold (fun (k : Make.key) (v : A) ⇒ Map.Make.add k (f k v)) map
     xs) as Haux.
    { induction map.
      { intros; reflexivity. }
      { intros; simpl.
        destruct a; simpl in ×.
        destruct f_with_cost eqn:fwc.
        { destruct p; simpl.
          destruct (_.(Carbonated_map.GAS.consume)).
            simpl.
          { pose proof (IHmap (Map.Make.add k b xs)
            g0) as IH.
            destruct Map.Make.fold eqn:?;
              [|exact I].
            destruct p; simpl in ×.
            rewrite IH. repeat f_equal.
            pose proof (H1 c k a) as Hf.
            rewrite fwc in Hf.
            exact Hf.
          }
          { simpl; unfold tzresult.
            rewrite Make_fold_shortcircuit; simpl; auto.
          }
        }
        { simpl; unfold tzresult.
          rewrite Make_fold_shortcircuit; simpl; auto.
        }
      }
    }
    { apply Haux. }
  Qed.

The [map] operator behaves as on standard maps.
  Lemma map_eq `{FArgs} {A B : Set} ctxt f f_with_cost (m : t A) :
    @Map.Valid.t C_t
      (@Map.Make.Build_FArgs C_t
         (COMPARABLE.Build_signature C_t
            (@Carbonated_map.COMPARABLE.compare _ (@C _ H))))
    StrictlySorted.t (List.map fst m.(t.map))
    ( ctxt k v,
      letP?relaxed '(result, _) := f_with_cost ctxt k v in
      result = f k v
    )
    letP?relaxed '(new_m, _) := map_e (A := A) (B := B) ctxt f_with_cost m in
    new_m.(t.map) = M.(Map.S.mapi) f m.(t.map).
  Proof.
    intro Hv; intros.
    epose proof (map_eq_aux ctxt f f_with_cost m H2).
    destruct map_e; [|exact I].
    destruct p; simpl in ×.
    rewrite H3.
    destruct m; simpl in ×.
    apply StrictlySorted.map_extensional; auto.
    { apply Make_fold_lemma.
      { intros; apply StrictlySorted.add_preserves_sorting; auto. }
      { exact I. }
    }
    { rewrite mapi_preserves_keys; auto. }
    { intros; split; intro; destruct p.
      { destruct (In_fold _ _ _ _ _ H4) as
          [ [] | [z [Hz1 Hz2]] ].
        rewrite <- Hz2.
        apply In_mapi; auto.
      }
      { destruct (In_mapi_invert H4) as [a [Ha1 Ha2]].
        rewrite <- Ha2.
        apply In_to_In_fold; auto.
        { exact I. }
        { exact (fun x _ ee). }
      }
    }
  Qed.
End Make. End Make_builder.

Module Make.
  Module Valid.
Validity predicate for [t].
    Parameter t : {ctxt k v : Set}
      {G : Carbonated_map.GAS (context := ctxt)}
      {C : Carbonated_map.COMPARABLE (t := k)}
      (P_key : k Prop)
      (P_value : v Prop),
      (Carbonated_map.Make G C).(Carbonated_map.S.t) v
      Prop.
  End Valid.

  Section Make.
    Context
      {context k v : Set}
      {G : Carbonated_map.GAS (context := context)}
      {C : Carbonated_map.COMPARABLE (t := k)}
      (P_key : k Prop)
      (P_value : v Prop)
      (Map := Carbonated_map.Make G C)
      (P_map := Valid.t (G := G) (C := C) P_key P_value).

The function [empty] is valid.
    Lemma empty_is_valid : P_map Map.(Carbonated_map.S.empty).
    Proof.
    Admitted.

The function [singleton] is valid.
    Lemma singleton_is_valid key value :
      P_key key
      P_value value
      P_map (Map.(Carbonated_map.S.singleton) key value).
    Proof.
    Admitted.

The function [size_value] is valid.
    Lemma size_value_is_valid map :
      P_map map
      Pervasives.Int.Valid.t (Map.(Carbonated_map.S.size_value) (a := v) map).
    Proof.
    Admitted.

    Context (P_ctxt : context Prop).

The function [find] is valid.
    Lemma find_is_valid ctxt key map :
      P_ctxt ctxt
      P_key key
      P_map map
      letP? '(value, ctxt) := Map.(Carbonated_map.S.find) ctxt key map in
      Option.Forall P_value value
      P_ctxt ctxt.
    Proof.
    Admitted.

The function [update] is valid.
    Lemma update_is_valid ctxt key f map :
      P_ctxt ctxt
      P_key key
      ( ctxt value,
        P_ctxt ctxt
        Option.Forall P_value value
        letP? '(value, ctxt) := f ctxt value in
        Option.Forall P_value value P_ctxt ctxt
      )
      P_map map
      letP? '(map, ctxt) := Map.(Carbonated_map.S.update) ctxt key f map in
      P_map map P_ctxt ctxt.
    Proof.
    Admitted.

The function [to_list] is valid.
    Lemma to_list_is_valid ctxt map :
      P_ctxt ctxt
      P_map map
      letP? '(list, ctxt) := Map.(Carbonated_map.S.to_list) ctxt map in
      List.Forall (fun '(key, value)P_key key P_value value) list
      P_ctxt ctxt.
    Proof.
    Admitted.

The function [of_list] is valid.
    Lemma of_list_is_valid ctxt merge list :
      P_ctxt ctxt
      ( ctxt value1 value2,
        P_ctxt ctxt
        P_value value1
        P_value value2
        letP? '(value, ctxt) := merge ctxt value1 value2 in
        P_value value P_ctxt ctxt
      )
      letP? '(map, ctxt) := Map.(Carbonated_map.S.of_list) ctxt merge list in
      P_map map P_ctxt ctxt.
    Proof.
    Admitted.

The function [merge] is valid.
    Lemma merge_is_valid ctxt merge map1 map2 :
      P_ctxt ctxt
      ( ctxt value1 value2,
        P_ctxt ctxt
        P_value value1
        P_value value2
        letP? '(value, ctxt) := merge ctxt value1 value2 in
        P_value value P_ctxt ctxt
      )
      P_map map1
      P_map map2
      letP? '(map, ctxt) := Map.(Carbonated_map.S.merge) ctxt merge map1 map2 in
      P_map map P_ctxt ctxt.
    Proof.
    Admitted.

The function [map] is valid.
    Lemma map_is_valid {v' : Set} (P_value' : v' Prop) ctxt f map :
      P_ctxt ctxt
      ( ctxt key value,
        P_ctxt ctxt
        P_key key
        P_value value
        letP? '(value', ctxt) := f ctxt key value in
        P_value' value' P_ctxt ctxt
      )
      letP? '(map, ctxt) := Map.(Carbonated_map.S.map_e) ctxt f map in
      Valid.t (G := G) (C := C) P_key P_value' map P_ctxt ctxt.
    Proof.
    Admitted.

The function [fold] is valid.
    Lemma fold_is_valid {s : Set} (P_state : s Prop) ctxt f state map :
      P_ctxt ctxt
      ( ctxt state key value,
        P_ctxt ctxt
        P_state state
        P_key key
        P_value value
        letP? '(state, ctxt) := f ctxt state key value in
        P_state state P_ctxt ctxt
      )
      P_state state
      P_map map
      letP? '(state, ctxt) := Map.(Carbonated_map.S.fold_es) ctxt f state map in
      P_state state P_ctxt ctxt.
    Proof.
    Admitted.

    Lemma non_empty_fold_is_valid {s : Set} (P_state : s Prop)
    ctxt f state map :
    
@TODO : modify with map non-empty
      P_ctxt ctxt
      ( ctxt state key value,
        P_ctxt ctxt
        P_state state
        P_key key
        P_value value
        letP? '(state, ctxt) := f ctxt state key value in
        P_state state P_ctxt ctxt
      )
      P_state state
      P_map map
      map.(Carbonated_map.Make_builder.t.map) []
non-emptiness
      letP? '(state, ctxt) := Map.(Carbonated_map.S.fold_es) ctxt f state map in
      P_state state P_ctxt ctxt.
    Proof.
      (* Locate Map.Make.  (* TezosOfOCaml.Environment.Structs.V0.Map.Make*)
      Print Compare.COMPARABLE.
      Print COMPARABLE.signature. *)

      (* Arguments COMPARABLE {t}%type_scope
Record signature (t : Set) : Set := Build_signature
  { t := t;  compare : t -> t -> int }. *)

    Admitted.
  End Make.
End Make.

#[global] Opaque Make.