Skip to main content

🍬 Script_map.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Script_map.

Require TezosOfOCaml.Environment.V8.Proofs.Map.
Require TezosOfOCaml.Proto_alpha.Proofs.Gas_comparable_input_size.
(* Require TezosOfOCaml.Proto_alpha.Proofs.Script_comparable. *)
Require TezosOfOCaml.Proto_alpha.Proofs.Script_family.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_typed_ir.
Require Import TezosOfOCaml.Proto_alpha.Simulations.Script_family.

The function [empty_from] is valid
The function [empty] is valid
The function [update] is valid