🔥 Carbonated_map.v

Proofs

See code, Gitlab , OCaml

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

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

Require Import TezosOfOCaml.Proto_alpha.Environment.Proofs.List.
Require Import TezosOfOCaml.Proto_alpha.Environment.Proofs.Map.

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. We will write our lemmas as if we were in the functor, with access to the [FArgs] parameters.

Module Make.
  Import Proto_alpha.Carbonated_map.Make.

  Module Valid.

A map is valid when its [size] field is its actual size.

    Definition t `{FArgs} {a : Set} (map : Carbonated_map.Make.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 :
    letP? '(v, _) := find (A := A) ctxt k map in
    v = M.(Map.S.find) k map.(t.map).
  Proof.
    unfold find.
    destruct Alpha_context.Gas.consume; simpl; auto.
  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? '(updated_map, _) := update ctxt k f map in
    Valid.t updated_map.
  Proof.
    intros Hv.
    unfold Valid.t in Hv.
    unfold update.
    destruct Alpha_context.Gas.consume; simpl; auto.
    destruct map; simpl in ×.
    destruct f eqn:G; try exact I.
    simpl.
    destruct p.
    destruct Make.find eqn:G0.
    { destruct o;
      destruct Alpha_context.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
          map0 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 Alpha_context.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? '(v', _) := f_with_cost ctxt v in
      v' = f v
    ) →
    letP? '(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 Alpha_context.Gas.consume; try exact I.
    simpl.
    destruct f_with_cost eqn:G.
    { simpl.
      destruct p.
      simpl.
      unfold M; simpl.
      destruct (Make.find k) eqn:G0.
      { destruct o;
        destruct Alpha_context.Gas.consume; try exact I.
        { simpl.
          pose (Hf t0 (Some a)) as Hf2.
          rewrite G in Hf2.
          simpl in Hf2.
          unfold Make.update.
          destruct map; simpl in ×.
          rewrite G0.
          rewrite <- Hf2; auto.
        }
        { simpl.
          unfold Make.update.
          destruct map; simpl in ×.
          rewrite G0.
          pose (Hf t0 (Some a)) as Hf2.
          rewrite G in Hf2; simpl in Hf2.
          rewrite <- Hf2; auto.
        }
      }
      { destruct o.
        { destruct Alpha_context.Gas.consume; try exact I.
          simpl.
          destruct map; simpl in ×.
          unfold Make.update.
          rewrite G0.
          pose (Hf t0 None) as Hf2.
          rewrite G in Hf2; simpl in Hf2.
          rewrite <- Hf2; auto.
        }
        { destruct map; simpl in ×.
          unfold Make.update.
          rewrite G0.
          pose (Hf t0 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? '(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 Alpha_context.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? '(added_map, _) := add ctxt merge_overlap k v map in
    Valid.t added_map.
  Proof.
    intro Hv.
    unfold add; simpl.
    do 2 (destruct Alpha_context.Gas.consume; try exact I; simpl).
    destruct map; unfold Valid.t in *; simpl in ×.
    destruct 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? '(v, _) := merge_overlap_with_cost ctxt v1 v2 in
      v = merge_overlap v1 v2
    ) →
    letP? '(added_map, _) := add ctxt merge_overlap_with_cost k v map in
    let f old_value :=
      match old_value with
      | Some old_value ⇒ merge_overlap old_value v
      | None ⇒ v
      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 Alpha_context.Gas.consume; simpl; try exact I).
    destruct map; simpl.
    destruct Make.find eqn:G.
    { destruct merge_overlap_with_cost eqn:G0; simpl; try auto.
      destruct p; simpl.
      pose proof (H0 t1 a v)
        as Hmo.
      rewrite G0 in Hmo.
      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? '(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.
    destruct a1, a2, b.
    pose proof (add_is_valid c0 merge_overlap t3 a t1 H1).
    rewrite H2 in H3; auto.
  Qed.

The [of_list] operator produces a valid map.

  Lemma of_list_is_valid `{FArgs} {A : Set} ctxt merge_overlap key_values :
    letP? '(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? '(merged_map, _) := merge (A := A) ctxt merge_overlap map1 map2 in
    Valid.t merged_map.
  Proof.
    unfold merge.
    intro Hv.
    destruct Alpha_context.Gas.consume;
      [simpl|exact I].
    unfold Make.fold_e.
    destruct map2.
    generalize Hv.
    generalize map1.
    generalize t0.
    clear Hv; clear map1; clear t0.
    induction map0; [auto|].
    simpl; intros.
    Tactics.destruct_pairs.
    destruct add eqn:?.
    unfold Error_monad.ok in ×.
    destruct p.
    { eapply IHmap0.
      epose proof (add_is_valid t0 merge_overlap
        k a map1 Hv) as Hadd.
      unfold Make.key, Make.Ord in ×.
      rewrite Heqt1 in Hadd; auto.
    }
    { clear IHmap0.
      induction map0.
      { exact I. }
      { simpl.
        Tactics.destruct_pairs.
        apply IHmap0.
      }
    }
  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? ' (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
    (@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? '(v, _) := merge_overlap_with_cost ctxt v1 v2 in
      v = merge_overlap v1 v2
    ) →
    letP? '(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 v2 ⇒ Some (merge_overlap v1 v2)
      | Some v1, None ⇒ Some v1
      | None, Some v2 ⇒ Some 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 Alpha_context.Gas.consume; [|discriminate].
      simpl in ×.
      unfold Make.fold_e in Heqt0.
      pose (S := fun (em : M? (t A × Alpha_context.context)) ⇒
        letP? '(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 Alpha_context.Gas.consume;
          [|discriminate].
        simpl in Hadd.
        destruct Alpha_context.Gas.consume;
          [|discriminate].
        simpl in Hadd.
        destruct 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 H1) as [|[|]].
        { destruct H2 as [c1 [c2 [a1 [a2 [Ha1 [Ha2 Ha3]]]]]].
          eapply Make_merge_In3; eauto.
          epose (H0 _ _ _).
          rewrite Ha1 in b.
          simpl in b; 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 H2 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 H0.
          }
        }
      }
    }
  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 :
    (∀ ctxt acc k v,
      letP? '(result, _) := f_with_cost ctxt acc k v in
      result = f k v acc
    ) →
    letP? '(result, _) := fold (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.
    simpl.
    unfold Make.fold_e.
    destruct Alpha_context.Gas.consume;
      [|exact I].
    destruct map; simpl.
    generalize acc.
    generalize t0.
    induction map0.
    { reflexivity. }
    { simpl.
      Tactics.destruct_pairs.
      intros.
      destruct Make.fold eqn:?;
        [simpl|exact I].
      Tactics.destruct_pairs.
      pose proof (H0 t0 acc0 k b).
      destruct f_with_cost eqn:?.
      { Tactics.destruct_pairs.
        simpl in ×.
        pose (IHmap0 c0 a0) as IH.
        unfold Error_monad.ok in IH.
        unfold Alpha_context.context in ×.
        unfold Alpha_context.t in ×.
        unfold Raw_context.t in ×.
        rewrite Heqy in IH.
        simpl in ×.
        clear H1.
        pose proof (H0 t1 acc0 k b).
        rewrite Heqr in H1.
        simpl in ×.
        congruence.
      }
      { cut False; [tauto|].
        clear H0.
        clear IHmap0.
        induction map0.
        { discriminate. }
        { simpl in ×.
          Tactics.destruct_pairs; auto.
        }
      }
    }
  Qed.

  Lemma fold_conditional_preservation_lemma `{Make.FArgs} {A B : Set}
    (E : B → Make.t A → B → Prop)
    (D : Make.t A → B → Prop) (* disjoint *)
    (S : Make.t A → Prop) (* strictly incr *)
    (f : Make.key → A → M? B → M? B)
    (f_pres_error : (∀ (t : trace _error) (k : 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? b2 := eb2 in
      D ((k,a):: m) b2 →
      letP? 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? 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 →
        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
  (@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? '(new_m, _) := map (A := A) (B := B) ctxt f m in
    Valid.t new_m.
  Proof.
    intros.
    unfold map.
    unfold fold; simpl.
    unfold Make.fold_e.
    destruct Alpha_context.Gas.consume;
      [|exact I].
    simpl.
    destruct m; simpl.
    destruct Make.fold eqn:?;
      [|exact I].
    destruct p.
    simpl.
    unfold Valid.t in ×.
    simpl.
    pose (E := fun
     (x : (M.(S.t) B × Alpha_context.context))
     (y : M.(S.t) A)
     (z : (M.(S.t) B × Alpha_context.context)) ⇒
      (Make.cardinal (fst x) = Make.cardinal y +i Make.cardinal (fst z))%Z
    ).
    simpl in H0.
    rewrite <- H0.
    cut
      (E (t1,c)
         map0 (Make.empty, t0)).
    { unfold E; intro.
      unfold Make.cardinal at 3 in H2.
      simpl in H2.
      rewrite H2.
      apply Pervasives.Int.Valid.int_plus_0_r_eq.
      apply length_is_valid.
    }
    pose (D := fun
      (m1 : M.(S.t) A)
      (m2 : (M.(S.t) B × Alpha_context.context)) ⇒
       disj (List.map fst m1) (List.map fst (fst m2))).
    pose (S := fun (m1 : M.(S.t) A) ⇒ StrictlySorted.t (List.map fst m1)).
    eapply (fold_conditional_preservation_lemma E D S).
    9:{ exact Heqy. }
    { 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 Alpha_context.Gas.consume;
        [|exact I].
      simpl; intros.
      unfold E in ×.
      unfold D in ×.
      destruct b1; simpl in ×.
      simpl.
      rewrite cardinal_add_find_None in H3.
      { simpl.
        unfold Make.cardinal in ×.
        simpl.
        rewrite H3.
        rewrite Pervasives.int_add_assoc; lia.
      }
      { apply find_not_In; auto.
        intro.
        eapply H2; eauto.
        left; reflexivity.
      }
    }
    { intros.
      simpl.
      destruct b.
      destruct f eqn:?; [|exact I].
      destruct p; simpl.
      destruct Alpha_context.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 H4.
        rewrite <- H6 in *; clear H6.
        unfold S in H2.
        simpl in H2.
        epose proof (StrictlySorted.strictly_sorted_lb_correct
          _ _ Hv H2 _ Hx1).
        rewrite (Compare.Valid.refl Hv) in H5; auto.
        lia.
      }
      { elim (H3 x).
        { right; auto. }
        { assert (x = fst (x,y)) by auto.
          rewrite H5.
          apply in_map; auto.
        }
      }
    }
    { intros.
      unfold S in ×.
      eapply StrictlySorted.ss_tail.
      exact H2.
    }
    { reflexivity. }
    { exact H1. }
    { 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? '(result, _) := f_with_cost ctxt k v in
      result = f k v
    ) →
    letP? '(new_m, _) := map (A := A) (B := B) ctxt f_with_cost m in
    new_m.(t.map) =
    Make.fold (fun k v ⇒ Make.add k (f k v)) m.(t.map) M.(S.empty).
  Proof.
    intros.
    unfold map.
    unfold fold.
    destruct Alpha_context.Gas.consume;
      [|exact I].
    simpl.
    unfold Make.fold_e.
    destruct m; simpl in ×.
    assert (∀ xs c,
    letP? ' (new_m, _)
:= (let? ' (map1, ctxt0)
    := Make.fold
         (fun (k : Make.key) (v : A)
            (acc : result (M.(S.t) B × Alpha_context.context) (trace _error))
          ⇒
          let? ' (acc_value, ctxt0) := acc
          in let? ' (value_value, ctxt1) := f_with_cost ctxt0 k v
             in let? ' ctxt2
                := Alpha_context.Gas.consume ctxt1 (update_cost k size)
                in return? (Make.add k value_value acc_value, ctxt2)) map0
         (return? (xs, c))
    in return? ({| t.map := map1; t.size := size |}, ctxt0))
in new_m.(t.map) =
   Make.fold (fun (k : Make.key) (v : A) ⇒ Make.add k (f k v)) map0
     xs) as Haux.
    { induction map0.
      { intros; reflexivity. }
      { intros; simpl.
        destruct a; simpl in ×.
        destruct f_with_cost eqn:fwc.
        { destruct p; simpl.
          destruct Alpha_context.Gas.consume;
            simpl.
          { pose proof (IHmap0 (Make.add k b xs)
            t1) as IH.
            destruct Make.fold eqn:?;
              [|exact I].
            destruct p; simpl in ×.
            rewrite IH. repeat f_equal.
            pose proof (H0 c k a) as Hf.
            rewrite fwc in Hf.
            exact Hf.
          }
          { rewrite Make_fold_shortcircuit; simpl; auto. }
        }
        { simpl. 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
  (@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? '(result, _) := f_with_cost ctxt k v in
      result = f k v
    ) →
    letP? '(new_m, _) := map (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 H1).
    destruct map; [|exact I].
    destruct p; simpl in ×.
    rewrite H2.
    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 _ _ _ _ _ H3) as
          [ [] | [z [Hz1 Hz2]] ].
        rewrite <- Hz2.
        apply In_mapi; auto.
      }
      { destruct (In_mapi_invert H3) as [a [Ha1 Ha2]].
        rewrite <- Ha2.
        apply In_to_In_fold; auto.
        { exact I. }
        { exact (fun x _ e ⇒ e). }
      }
    }
  Qed.
End Make.