Skip to main content

🏁 Init_storage.v


See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Init_storage.

Require TezosOfOCaml.Proto_alpha.Proofs.Migration_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
Require TezosOfOCaml.Proto_alpha.Proofs.Receipt_repr.

The function [patch_script] is valid.
The function [prepare_first_block] is valid. Lemma prepare_first_block_is_valid {A : Set} (chain_id : A) standalone typecheck level timestamp (H_standalone : Raw_context.standalone.Valid.simulation standalone) (H_typecheck : forall ctxt script, Raw_context.Valid.t ctxt -> letP? '(_, ctxt) := typecheck ctxt script in Raw_context.Valid.t ctxt ) (H_level : Int32.Valid.t level) (H_timestamp : Time.Valid.t timestamp) : letP? ctxt := Init_storage.prepare_first_block chain_id (Raw_context.to_context standalone) typecheck level timestamp in Raw_context.Valid.t ctxt. Proof. Admitted.
The function [prepare] is valid.