🌌 Alpha_context.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Alpha_context.

Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Error_monad.
Require TezosOfOCaml.Proto_alpha.Proofs.Contract_hash.
Require TezosOfOCaml.Proto_alpha.Proofs.Lazy_storage_diff.
Require TezosOfOCaml.Proto_alpha.Proofs.Operation_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.

Module Script.
  Lemma force_decode_in_context_gas_consume ctxt lexpr
    : Error_monad.post_when_success
        (Alpha_context.Script.force_decode_in_context
          Alpha_context.Script.When_needed ctxt lexpr)
        (fun '(_, ctxt') ⇒
          Raw_context.Consume_gas.Valid.t ctxt ctxt'
            [Script_repr.force_decode_cost lexpr]
        ).
    unfold Alpha_context.Script.force_decode_in_context.
    eapply Error_monad.post_when_success_bind;
      [apply Raw_context.Consume_gas.Valid.consume_gas|]; simpl.
    intros ctxt' H.
    now destruct (Script_repr.force_decode _).
  Qed.
End Script.

(* encoding_is_valid can be found at Proofs.Tez_repr. Alpha_context.Tez is a
 * symnonym Tez_repr, so all properties of Tez_repr applies to this one too. 
 *)

Module Operation.

The encoding [Alpha_context.Operation.unsigned_encoding] is valid.

  Lemma unsigned_encoding_is_valid :
    Data_encoding.Valid.t
    (fun '(_, x) ⇒ Operation_repr.Packed_contents_list.Valid.t x)
    Alpha_context.Operation.unsigned_encoding.
  Proof.
    Data_encoding.Valid.data_encoding_auto.
  Qed.
  #[global] Hint Resolve unsigned_encoding_is_valid : Data_encoding_db.
End Operation.

Module Round.

The encoding [Alpha_context.Round.round_durations_encoding] is valid.

  Lemma round_durations_encoding_is_valid :
    Data_encoding.Valid.t
    Round_repr.Durations.Valid.t
    Alpha_context.Round.round_durations_encoding.
  Proof.
    Data_encoding.Valid.data_encoding_auto.
  Qed.
  #[global] Hint Resolve round_durations_encoding_is_valid : Data_encoding_db.
End Round.

Module Big_map.
  Module Id.

The encoding [Alpha_context.Big_map.Id.encoding] is valid.

    Lemma encoding_is_valid :
      Data_encoding.Valid.t (fun _ ⇒ True) Alpha_context.Big_map.Id.encoding.
    Proof.
      Data_encoding.Valid.data_encoding_auto.
    Qed.
    #[global] Hint Resolve encoding_is_valid : Data_encoding_db.
  End Id.
End Big_map.

Module Sapling.
  Module Id.

The encoding [Alpha_context.Sapling.Id.encoding] is valid.

    Lemma encoding_is_valid :
      Data_encoding.Valid.t (fun _ ⇒ True) Alpha_context.Sapling.Id.encoding.
    Proof.
      Data_encoding.Valid.data_encoding_auto.
    Qed.
    #[global] Hint Resolve encoding_is_valid : Data_encoding_db.
  End Id.
End Sapling.