🏁 Init_storage.v

Proofs

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.

Lemma patch_script_is_valid param ctxt
  (H_ctxt : Raw_context.Valid.t ctxt) :
  letP ? ctxt := Init_storage.patch_script param ctxt in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.

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.

Lemma prepare_is_valid standalone level predecessor_timestamp timestamp
  (H_ctxt :
    ∃ sim_standalone,
      Raw_context.to_context sim_standalone = standalone ∧
      Raw_context.standalone.Valid.simulation sim_standalone
  )
  (H_level : Int32.Valid.t level)
  (H_predecessor_timestamp : Time.Valid.t predecessor_timestamp)
  (H_timestamp : Time.Valid.t timestamp) :
  letP ? '(ctxt , updates , migrations ) :=
    Init_storage.prepare standalone level predecessor_timestamp timestamp in
  Raw_context.Valid.t ctxt ∧
  Receipt_repr.balance_updates.Valid.t updates ∧
  List.Forall Migration_repr.origination_result.Valid.t migrations.
Proof.
Admitted.