🦏 Sc_rollup_storage.v

Proofs

See code, Gitlab , OCaml

Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_storage.

Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Pervasives.

(* @TODO this seems to be a very non-interesting property *)
Axiom originate_is_valid : ∀ {ctxt} {kind} {boot_sector},
  match Sc_rollup_storage.originate ctxt kind boot_sector with
  | Pervasives.Ok (_, size, _) ⇒ Pervasives.Int.Valid.non_negative size
  | Pervasives.Error _ ⇒ True
  end.