🍬 Script_string.v

Proofs

See code, Gitlab , OCaml

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.

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.

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.

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.

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.

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.

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.