🐾 Path_encoding.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Path_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.Hex.
Module S.
Module Valid.
Record t {t : Set} {P : Path_encoding.S (t := t)} : Prop := {
to_path_postfix v postfix :
P.(Path_encoding.S.to_path) v postfix =
List.app (P.(Path_encoding.S.to_path) v []) postfix;
of_path_to_path v :
P.(Path_encoding.S.of_path) (P.(Path_encoding.S.to_path) v []) =
return? Some v;
to_path_of_path path :
letP? p := P.(Path_encoding.S.of_path) path in
match p with
| Some v ⇒ P.(Path_encoding.S.to_path) v [] = path
| None ⇒ True
end;
to_path_path_length v :
letP? path_length := P.(Path_encoding.S.path_length) in
List.length (P.(Path_encoding.S.to_path) v []) = path_length;
}.
Arguments t {_}.
End Valid.
End S.
Module ENCODING.
Module Valid.
Record t {t : Set} {E : Path_encoding.ENCODING (t := t)} : Prop := {
of_bytes_opt_to_bytes v :
E.(Path_encoding.ENCODING.of_bytes_opt)
(E.(Path_encoding.ENCODING.to_bytes) v) =
Some v;
to_bytes_of_bytes_opt bytes :
match E.(Path_encoding.ENCODING.of_bytes_opt) bytes with
| Some v ⇒ E.(Path_encoding.ENCODING.to_bytes) v = bytes
| None ⇒ True
end;
}.
Arguments t {_}.
End Valid.
End ENCODING.
Lemma Make_hex_is_valid : ∀ {t : Set}
(E : Path_encoding.ENCODING (t := t)),
Path_encoding.ENCODING.Valid.t E →
Path_encoding.S.Valid.t (Path_encoding.Make_hex E).
Proof.
intros t E H; constructor; intros; cbv - [List.app List.length].
{ now destruct (Hex.of_bytes _ _). }
{ destruct (Hex.of_bytes _ _) eqn:H_eq.
rewrite <- H_eq.
rewrite Hex.to_bytes_of_bytes.
now rewrite H.(Path_encoding.ENCODING.Valid.of_bytes_opt_to_bytes).
}
{ destruct path as [|bytes[]]; trivial.
assert (H_hex := Hex.of_bytes_to_bytes (Hex.Hex bytes)).
destruct (Hex.to_bytes _) as [bytes'|]; trivial.
assert (H_bytes :=
H.(Path_encoding.ENCODING.Valid.to_bytes_of_bytes_opt) bytes'
).
destruct (E.(Path_encoding.ENCODING.of_bytes_opt) _); trivial.
cbv in ×.
now rewrite H_bytes; rewrite H_hex.
}
{ now destruct (Hex.of_bytes _ _). }
Qed.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Path_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.Hex.
Module S.
Module Valid.
Record t {t : Set} {P : Path_encoding.S (t := t)} : Prop := {
to_path_postfix v postfix :
P.(Path_encoding.S.to_path) v postfix =
List.app (P.(Path_encoding.S.to_path) v []) postfix;
of_path_to_path v :
P.(Path_encoding.S.of_path) (P.(Path_encoding.S.to_path) v []) =
return? Some v;
to_path_of_path path :
letP? p := P.(Path_encoding.S.of_path) path in
match p with
| Some v ⇒ P.(Path_encoding.S.to_path) v [] = path
| None ⇒ True
end;
to_path_path_length v :
letP? path_length := P.(Path_encoding.S.path_length) in
List.length (P.(Path_encoding.S.to_path) v []) = path_length;
}.
Arguments t {_}.
End Valid.
End S.
Module ENCODING.
Module Valid.
Record t {t : Set} {E : Path_encoding.ENCODING (t := t)} : Prop := {
of_bytes_opt_to_bytes v :
E.(Path_encoding.ENCODING.of_bytes_opt)
(E.(Path_encoding.ENCODING.to_bytes) v) =
Some v;
to_bytes_of_bytes_opt bytes :
match E.(Path_encoding.ENCODING.of_bytes_opt) bytes with
| Some v ⇒ E.(Path_encoding.ENCODING.to_bytes) v = bytes
| None ⇒ True
end;
}.
Arguments t {_}.
End Valid.
End ENCODING.
Lemma Make_hex_is_valid : ∀ {t : Set}
(E : Path_encoding.ENCODING (t := t)),
Path_encoding.ENCODING.Valid.t E →
Path_encoding.S.Valid.t (Path_encoding.Make_hex E).
Proof.
intros t E H; constructor; intros; cbv - [List.app List.length].
{ now destruct (Hex.of_bytes _ _). }
{ destruct (Hex.of_bytes _ _) eqn:H_eq.
rewrite <- H_eq.
rewrite Hex.to_bytes_of_bytes.
now rewrite H.(Path_encoding.ENCODING.Valid.of_bytes_opt_to_bytes).
}
{ destruct path as [|bytes[]]; trivial.
assert (H_hex := Hex.of_bytes_to_bytes (Hex.Hex bytes)).
destruct (Hex.to_bytes _) as [bytes'|]; trivial.
assert (H_bytes :=
H.(Path_encoding.ENCODING.Valid.to_bytes_of_bytes_opt) bytes'
).
destruct (E.(Path_encoding.ENCODING.of_bytes_opt) _); trivial.
cbv in ×.
now rewrite H_bytes; rewrite H_hex.
}
{ now destruct (Hex.of_bytes _ _). }
Qed.