🍬 Script_string.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Script_string.
Require TezosOfOCaml.Environment.V8.Proofs.Compare.
Require TezosOfOCaml.Environment.V8.Proofs.String.
Require Import TezosOfOCaml.Environment.V8.Proofs.Pervasives.
Module PrintableChar.
Module Valid.
Definition t c :=
match c with
("010" % char | " " % char | "!" % char | """" % char | "" % char |
"$" % char | "%" % char | "&" % char | "'" % char | "(" % char |
")" % char | "*" % char | "+" % char | "," % char | "-" % char |
"." % char | "/" % char | "0" % char | "1" % char | "2" % char |
"3" % char | "4" % char | "5" % char | "6" % char | "7" % char |
"8" % char | "9" % char | ":" % char | ";" % char | "<" % char |
"=" % char | ">" % char | "?" % char | "@" % char | "A" % char |
"B" % char | "C" % char | "D" % char | "E" % char | "F" % char |
"G" % char | "H" % char | "I" % char | "J" % char | "K" % char |
"L" % char | "M" % char | "N" % char | "O" % char | "P" % char |
"Q" % char | "R" % char | "S" % char | "T" % char | "U" % char |
"V" % char | "W" % char | "X" % char | "Y" % char | "Z" % char |
"[" % char | "\" % char | "]" % char | "^" % char | "_" % char |
"`" % char | "a" % char | "b" % char | "c" % char | "d" % char |
"e" % char | "f" % char | "g" % char | "h" % char | "i" % char |
"j" % char | "k" % char | "l" % char | "m" % char | "n" % char |
"o" % char | "p" % char | "q" % char | "r" % char | "s" % char |
"t" % char | "u" % char | "v" % char | "w" % char | "x" % char |
"y" % char | "z" % char | "{" % char | "|" % char | "}" % char |
"~" % char) ⇒ True
| _ ⇒ False
end.
End Valid.
End PrintableChar.
Module Valid.
Import Script_string.
Fixpoint valid_string s : Prop :=
match s with
| EmptyString ⇒ True
| String.String c tail ⇒ PrintableChar.Valid.t c ∧ valid_string tail
end.
Definition t (x : Script_string.t) : Prop :=
let 'String_tag s := x in
valid_string s.
End Valid.
#[bypass_check(guard=yes)]
Definition check_printable_ascii : string → int → M? string.
intro s.
set (x := Script_string.of_string s).
cbv beta delta [Script_string.of_string] in x.
intros. hauto l: on.
Defined.
Lemma List_Forall_chars_are_valid : ∀ (s : string),
Valid.valid_string s →
List.Forall PrintableChar.Valid.t (list_ascii_of_string s).
intros.
unfold Valid.t in H.
induction s.
{ simpl. apply Forall_nil. }
{ destruct H. simpl.
apply Forall_cons; [easy|].
now apply IHs. }
Qed.
(* @TODO This one depends on proving that of_string terminates *)
Axiom of_string_identity : ∀ t,
Valid.t t →
let 'Script_string.String_tag s := t in
Script_string.of_string s = return? t.
Lemma compare_is_valid :
Compare.Valid.t (fun _ ⇒ True) id Script_string.compare.
Proof.
apply (Compare.equality (
let proj '(Script_string.String_tag s) := s in
Compare.projection proj String.compare
)); [sauto lq: on|].
eapply Compare.implies.
{ eapply Compare.projection_is_valid.
apply Compare.string_is_valid.
}
all: sauto q: on.
Qed.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Script_string.
Require TezosOfOCaml.Environment.V8.Proofs.Compare.
Require TezosOfOCaml.Environment.V8.Proofs.String.
Require Import TezosOfOCaml.Environment.V8.Proofs.Pervasives.
Module PrintableChar.
Module Valid.
Definition t c :=
match c with
("010" % char | " " % char | "!" % char | """" % char | "" % char |
"$" % char | "%" % char | "&" % char | "'" % char | "(" % char |
")" % char | "*" % char | "+" % char | "," % char | "-" % char |
"." % char | "/" % char | "0" % char | "1" % char | "2" % char |
"3" % char | "4" % char | "5" % char | "6" % char | "7" % char |
"8" % char | "9" % char | ":" % char | ";" % char | "<" % char |
"=" % char | ">" % char | "?" % char | "@" % char | "A" % char |
"B" % char | "C" % char | "D" % char | "E" % char | "F" % char |
"G" % char | "H" % char | "I" % char | "J" % char | "K" % char |
"L" % char | "M" % char | "N" % char | "O" % char | "P" % char |
"Q" % char | "R" % char | "S" % char | "T" % char | "U" % char |
"V" % char | "W" % char | "X" % char | "Y" % char | "Z" % char |
"[" % char | "\" % char | "]" % char | "^" % char | "_" % char |
"`" % char | "a" % char | "b" % char | "c" % char | "d" % char |
"e" % char | "f" % char | "g" % char | "h" % char | "i" % char |
"j" % char | "k" % char | "l" % char | "m" % char | "n" % char |
"o" % char | "p" % char | "q" % char | "r" % char | "s" % char |
"t" % char | "u" % char | "v" % char | "w" % char | "x" % char |
"y" % char | "z" % char | "{" % char | "|" % char | "}" % char |
"~" % char) ⇒ True
| _ ⇒ False
end.
End Valid.
End PrintableChar.
Module Valid.
Import Script_string.
Fixpoint valid_string s : Prop :=
match s with
| EmptyString ⇒ True
| String.String c tail ⇒ PrintableChar.Valid.t c ∧ valid_string tail
end.
Definition t (x : Script_string.t) : Prop :=
let 'String_tag s := x in
valid_string s.
End Valid.
#[bypass_check(guard=yes)]
Definition check_printable_ascii : string → int → M? string.
intro s.
set (x := Script_string.of_string s).
cbv beta delta [Script_string.of_string] in x.
intros. hauto l: on.
Defined.
Lemma List_Forall_chars_are_valid : ∀ (s : string),
Valid.valid_string s →
List.Forall PrintableChar.Valid.t (list_ascii_of_string s).
intros.
unfold Valid.t in H.
induction s.
{ simpl. apply Forall_nil. }
{ destruct H. simpl.
apply Forall_cons; [easy|].
now apply IHs. }
Qed.
(* @TODO This one depends on proving that of_string terminates *)
Axiom of_string_identity : ∀ t,
Valid.t t →
let 'Script_string.String_tag s := t in
Script_string.of_string s = return? t.
Lemma compare_is_valid :
Compare.Valid.t (fun _ ⇒ True) id Script_string.compare.
Proof.
apply (Compare.equality (
let proj '(Script_string.String_tag s) := s in
Compare.projection proj String.compare
)); [sauto lq: on|].
eapply Compare.implies.
{ eapply Compare.projection_is_valid.
apply Compare.string_is_valid.
}
all: sauto q: on.
Qed.
Concatenation of pairs preserves the validity
Lemma concat_pair_is_valid : ∀ t1 t2,
Valid.t t1 →
Valid.t t2 →
Valid.t (Script_string.concat_pair t1 t2).
intros.
unfold Script_string.concat_pair, op_caret.
destruct t1 as [t1], t2 as [t2].
induction t1, t2; try easy.
assert (Happnil : ∀ s, s ++ "" = s).
{ induction s; [easy|]. now (simpl; rewrite IHs). }
{ simpl. rewrite Happnil; apply H. }
{ simpl in ×. destruct H; split; [easy|]. now apply IHt1. }
Qed.
Lemma concat_string_pair_is_valid : ∀ s1 s2,
Valid.valid_string s1 →
Valid.valid_string s2 →
Valid.valid_string (s1 ++ s2).
intros.
induction s1; [hauto lq: on rew: off|].
sfirstorder.
Qed.
Valid.t t1 →
Valid.t t2 →
Valid.t (Script_string.concat_pair t1 t2).
intros.
unfold Script_string.concat_pair, op_caret.
destruct t1 as [t1], t2 as [t2].
induction t1, t2; try easy.
assert (Happnil : ∀ s, s ++ "" = s).
{ induction s; [easy|]. now (simpl; rewrite IHs). }
{ simpl. rewrite Happnil; apply H. }
{ simpl in ×. destruct H; split; [easy|]. now apply IHt1. }
Qed.
Lemma concat_string_pair_is_valid : ∀ s1 s2,
Valid.valid_string s1 →
Valid.valid_string s2 →
Valid.valid_string (s1 ++ s2).
intros.
induction s1; [hauto lq: on rew: off|].
sfirstorder.
Qed.
Contatenation preserves the validity
Lemma concat_is_valid : ∀ {l : list Script_string.t},
Forall Valid.t l →
Valid.t (Script_string.concat l).
intros.
assert (Happnil : ∀ s', s' ++ "" = s')
by (induction s'; [easy|]; simpl; now rewrite IHs').
induction l; [easy|].
unfold Script_string.concat in ×. simpl.
destruct a.
rewrite Happnil.
destruct (List.map) as [|repr lmap]; [sauto|].
apply concat_string_pair_is_valid; sauto l: on.
Qed.
Forall Valid.t l →
Valid.t (Script_string.concat l).
intros.
assert (Happnil : ∀ s', s' ++ "" = s')
by (induction s'; [easy|]; simpl; now rewrite IHs').
induction l; [easy|].
unfold Script_string.concat in ×. simpl.
destruct a.
rewrite Happnil.
destruct (List.map) as [|repr lmap]; [sauto|].
apply concat_string_pair_is_valid; sauto l: on.
Qed.
Helper for sub_is_valid
Lemma substring_0_n_s_is_valid : ∀ s n,
Valid.valid_string s →
Valid.valid_string (substring 0 n s).
induction s, n; sfirstorder.
Qed.
Valid.valid_string s →
Valid.valid_string (substring 0 n s).
induction s, n; sfirstorder.
Qed.
Helper for sub_is_valid
Lemma substring_n_Sn0_s_is_valid : ∀ s n n0,
Valid.valid_string s →
Valid.valid_string (substring n (Datatypes.S n0) s).
induction s, n, n0; sauto l: on.
Qed.
Valid.valid_string s →
Valid.valid_string (substring n (Datatypes.S n0) s).
induction s, n, n0; sauto l: on.
Qed.
Sub-strings preverves validity
Lemma sub_is_valid : ∀ t' offset length,
Valid.t t' →
Valid.t (Script_string.sub t' offset length).
intros.
unfold Script_string.sub.
destruct t' as [s].
induction s, offset, length; simpl in *;
try rewrite String.sub_empty_eq;
try (rewrite String.sub_length_0_eq; [|lia]);
try easy; simpl in *;
cbn; repeat destruct (Pos.to_nat _); try easy; simpl;
intuition;
try (rewrite String.sub_length_0_eq'; easy);
try (apply substring_0_n_s_is_valid; easy);
try (apply substring_n_Sn0_s_is_valid; easy).
Qed.
Valid.t t' →
Valid.t (Script_string.sub t' offset length).
intros.
unfold Script_string.sub.
destruct t' as [s].
induction s, offset, length; simpl in *;
try rewrite String.sub_empty_eq;
try (rewrite String.sub_length_0_eq; [|lia]);
try easy; simpl in *;
cbn; repeat destruct (Pos.to_nat _); try easy; simpl;
intuition;
try (rewrite String.sub_length_0_eq'; easy);
try (apply substring_0_n_s_is_valid; easy);
try (apply substring_n_Sn0_s_is_valid; easy).
Qed.
The function [of_string] is free of internal errors
and the identity on valid inputs.
Lemma of_string_identity' (str : Script_string.repr) :
Script_string.Valid.t (Script_string.String_tag str) →
letP? res := Script_string.of_string str in
res = Script_string.String_tag str.
Proof.
intro Hstr.
now rewrite (Script_string.of_string_identity _ Hstr).
Qed.
Script_string.Valid.t (Script_string.String_tag str) →
letP? res := Script_string.of_string str in
res = Script_string.String_tag str.
Proof.
intro Hstr.
now rewrite (Script_string.of_string_identity _ Hstr).
Qed.