Skip to main content

🍬 Script_list.v

Proofs

See code, Gitlab , OCaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Script_list.
Require TezosOfOCaml.Environment.V8.Proofs.Utils.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_typed_ir.
Require Import TezosOfOCaml.Proto_alpha.Simulations.Script_family.

Module Valid.
The validity predicate for the type [Script_list.t] .
  Definition t {a : Set} (l : Script_list.t a) : Prop :=
    List.length l.(Script_list.t.elements) =
    l.(Script_list.t.length).
End Valid.

The [empty] definition from [Script_list] is valid.
Lemma empty_is_valid {a : Set} : Valid.t (Script_list.empty (a := a)).
  reflexivity.
Qed.

The function [cons_value] is valid.
Lemma cons_value_is_valid {a} {v : Ty.to_Set a} {l}
  : Pervasives.Int.Valid.non_negative
      (l.(Script_list.t.length))%Z
    1 + l.(Script_list.t.length) Pervasives.max_int
    Script_typed_ir.Valid.value a v
    Script_typed_ir.Valid.value (Ty.List a) l
    Script_typed_ir.Valid.value (Ty.List a) (Script_list.cons_value v l).
Proof.
  intros.
  unfold Script_list.cons_value, "+i".
  rewrite Pervasives.normalize_identity.
  sauto lq: on.
  hfcrush.
Qed.