📜 Bounded_history_repr.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require Import TezosOfOCaml.Proto_alpha.Proofs.Error.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.Map.
Require TezosOfOCaml.Proto_alpha.Bounded_history_repr.
Module Make.
Import Bounded_history_repr.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require Import TezosOfOCaml.Proto_alpha.Proofs.Error.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.Map.
Require TezosOfOCaml.Proto_alpha.Bounded_history_repr.
Module Make.
Import Bounded_history_repr.
Assume validity of the key encoding
Axiom key_encoding_id_valid : ∀ {key value : Set}
`{Make.FArgs (Key_t := key) (Value_t := value)},
Data_encoding.Valid.t (fun _ ⇒ True) Make.Key.(KEY.encoding).
#[global] Hint Resolve key_encoding_id_valid : Data_encoding_db.
`{Make.FArgs (Key_t := key) (Value_t := value)},
Data_encoding.Valid.t (fun _ ⇒ True) Make.Key.(KEY.encoding).
#[global] Hint Resolve key_encoding_id_valid : Data_encoding_db.
Assume validity of the value encoding
Axiom value_encoding_id_valid : ∀ {key value : Set}
`{Make.FArgs (Key_t := key) (Value_t := value)},
Data_encoding.Valid.t (fun _ ⇒True) Make.Value.(VALUE.encoding).
#[global] Hint Resolve value_encoding_id_valid : Data_encoding_db.
`{Make.FArgs (Key_t := key) (Value_t := value)},
Data_encoding.Valid.t (fun _ ⇒True) Make.Value.(VALUE.encoding).
#[global] Hint Resolve value_encoding_id_valid : Data_encoding_db.
The validity predicate for [Make.t]
Module Valid.
Record t {key value : Set}
`{Make.FArgs (Key_t := key) (Value_t := value)}
(x : Make.t) : Prop := {
events : Sorted.Sorted (fun '(k1, _) '(k2, _) ⇒
Make.compare_keys k2 k1 = Datatypes.Gt) x.(Make.t.events);
keys : Forall (fun '(k, _) ⇒ Int64.Valid.t k)
(Make.Int64_map.(S.bindings) x.(Make.t.sequence));
capacity : Int64.Valid.t x.(Make.t.capacity);
index : Int64.Valid.t x.(Make.t.next_index);
oldest_index : Int64.Valid.t x.(Make.t.oldest_index);
size : Int64.Valid.t x.(Make.t.size);
sequence : Sorted.Sorted (fun '(k1, _) '(k2, _) ⇒
Int64.compare k1 k2 = -1) x.(Make.t.sequence);
}.
End Valid.
Record t {key value : Set}
`{Make.FArgs (Key_t := key) (Value_t := value)}
(x : Make.t) : Prop := {
events : Sorted.Sorted (fun '(k1, _) '(k2, _) ⇒
Make.compare_keys k2 k1 = Datatypes.Gt) x.(Make.t.events);
keys : Forall (fun '(k, _) ⇒ Int64.Valid.t k)
(Make.Int64_map.(S.bindings) x.(Make.t.sequence));
capacity : Int64.Valid.t x.(Make.t.capacity);
index : Int64.Valid.t x.(Make.t.next_index);
oldest_index : Int64.Valid.t x.(Make.t.oldest_index);
size : Int64.Valid.t x.(Make.t.size);
sequence : Sorted.Sorted (fun '(k1, _) '(k2, _) ⇒
Int64.compare k1 k2 = -1) x.(Make.t.sequence);
}.
End Valid.
[encoding_is_valid]
Lemma encoding_is_valid {key value : Set}
`{Make.FArgs (Key_t := key) (Value_t := value)} :
Data_encoding.Valid.t Valid.t
Bounded_history_repr.Make.encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
intros [x] H_Valid.
repeat match goal with
| |- _ ∧ _ ⇒ split
end; try apply H_Valid; try f_equal.
{ unfold Make.Int64_map, Make.Map in *;
with_strategy transparent [Map.Make] unfold Map.Make in *;
cbn in *; unfold Make.bindings in *;
unfold Map.Make.empty;
destruct H_Valid; cbn in ×.
induction x; [constructor|].
constructor.
{ step; easy. }
{ apply IHx. now inversion events. }
}
{ unfold Make.Int64_map, Make.Map in *;
with_strategy transparent [Map.Make] unfold Map.Make in *;
cbn in *; unfold Make.bindings, Map.Make.empty in *; cbn in ×.
apply Map.add_seq_node_to_seq_node_eq.
apply H_Valid.
}
{ unfold Make.Int64_map, Make.Map in *;
with_strategy transparent [Map.Make] unfold Map.Make in *;
cbn in *; unfold Make.bindings in *;
unfold Map.Make.empty;
destruct H_Valid; cbn in ×.
induction sequence; constructor; fcrush. }
{ epose proof (Map.bindings_of_bindings)
as H_bindings_of_bindings.
unfold Make.Int64_map, Make.Map in *; cbn.
with_strategy transparent [Map.Make] unfold Map.Make in *;
cbn in ×.
rewrite Map.make_bindings_rev_eq.
unfold Make.bindings, Map.of_bindings in ×.
with_strategy transparent [Map.Make] unfold Map.Make in *;
cbn in *; unfold Map.Make.empty in ×.
rewrite <- fold_left_rev_right, <- List.fold_right_eq.
rewrite List.rev_eq, rev_involutive.
match goal with
| |- context [fold_right ?f _ _] ⇒
let t := type of H_bindings_of_bindings in
match t with
| context [fold_right ?f' _ _] ⇒
assert (H_f_ext : f = f')
end
end.
{ do 2 (apply FunctionalExtensionality.functional_extensionality;
intro).
now step.
}
rewrite H_f_ext in ×.
apply Map.bindings_of_bindings.
apply H_Valid.
}
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
`{Make.FArgs (Key_t := key) (Value_t := value)} :
Data_encoding.Valid.t Valid.t
Bounded_history_repr.Make.encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
intros [x] H_Valid.
repeat match goal with
| |- _ ∧ _ ⇒ split
end; try apply H_Valid; try f_equal.
{ unfold Make.Int64_map, Make.Map in *;
with_strategy transparent [Map.Make] unfold Map.Make in *;
cbn in *; unfold Make.bindings in *;
unfold Map.Make.empty;
destruct H_Valid; cbn in ×.
induction x; [constructor|].
constructor.
{ step; easy. }
{ apply IHx. now inversion events. }
}
{ unfold Make.Int64_map, Make.Map in *;
with_strategy transparent [Map.Make] unfold Map.Make in *;
cbn in *; unfold Make.bindings, Map.Make.empty in *; cbn in ×.
apply Map.add_seq_node_to_seq_node_eq.
apply H_Valid.
}
{ unfold Make.Int64_map, Make.Map in *;
with_strategy transparent [Map.Make] unfold Map.Make in *;
cbn in *; unfold Make.bindings in *;
unfold Map.Make.empty;
destruct H_Valid; cbn in ×.
induction sequence; constructor; fcrush. }
{ epose proof (Map.bindings_of_bindings)
as H_bindings_of_bindings.
unfold Make.Int64_map, Make.Map in *; cbn.
with_strategy transparent [Map.Make] unfold Map.Make in *;
cbn in ×.
rewrite Map.make_bindings_rev_eq.
unfold Make.bindings, Map.of_bindings in ×.
with_strategy transparent [Map.Make] unfold Map.Make in *;
cbn in *; unfold Map.Make.empty in ×.
rewrite <- fold_left_rev_right, <- List.fold_right_eq.
rewrite List.rev_eq, rev_involutive.
match goal with
| |- context [fold_right ?f _ _] ⇒
let t := type of H_bindings_of_bindings in
match t with
| context [fold_right ?f' _ _] ⇒
assert (H_f_ext : f = f')
end
end.
{ do 2 (apply FunctionalExtensionality.functional_extensionality;
intro).
now step.
}
rewrite H_f_ext in ×.
apply Map.bindings_of_bindings.
apply H_Valid.
}
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
[Bounded_history_repr.Make.remember] is valid.
Lemma remember_is_valid `{Make.FArgs}
key_value value_value t_value :
letP? res :=
Bounded_history_repr.Make.remember key_value value_value t_value in True.
Proof.
Admitted.
End Make.
key_value value_value t_value :
letP? res :=
Bounded_history_repr.Make.remember key_value value_value t_value in True.
Proof.
Admitted.
End Make.