🔥 Carbonated_map.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Carbonated_map.
Require Import TezosOfOCaml.Environment.V8.Proofs.List.
Require Import TezosOfOCaml.Environment.V8.Proofs.Map.
Require Import TezosOfOCaml.Environment.V8.Proofs.Option.
Module COMPARABLE.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Carbonated_map.
Require Import TezosOfOCaml.Environment.V8.Proofs.List.
Require Import TezosOfOCaml.Environment.V8.Proofs.Map.
Require Import TezosOfOCaml.Environment.V8.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.
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.
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.
M.(Map.S.cardinal) map.(t.map) = map.(t.size).
End Valid.
The [empty] operator is a valid map.
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.
(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.
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.
(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.
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.
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.
(∀ 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.
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.
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_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 (_.(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.
(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_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 (_.(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.
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.
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.
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 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 (_.(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.
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 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 (_.(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.
(∀ 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 v ⇒ Map.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.
(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 v ⇒ Map.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.
}
{ apply In_mapi_invert in H4.
destruct H4 as [a [Ha1 Ha2]].
rewrite <- Ha2.
apply In_to_In_fold; auto.
{ exact I. }
{ exact (fun x _ e ⇒ e). }
}
}
Qed.
End Make. End Make_builder.
Module Make.
Module Valid.
@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.
}
{ apply In_mapi_invert in H4.
destruct H4 as [a [Ha1 Ha2]].
rewrite <- Ha2.
apply In_to_In_fold; auto.
{ exact I. }
{ exact (fun x _ e ⇒ e). }
}
}
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).
{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.
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.
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).
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.
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.
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.
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.
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.
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.
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 :
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) ≠ [] →
(∀ 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.
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.