Skip to main content

🍃 Operation.v

Proofs

See code, Gitlab

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

Require Import TezosOfOCaml.Environment.V8.

Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.

Axiom shell_header_encoding_is_valid
  : Data_encoding.Valid.t (fun _True) Operation.shell_header_encoding.
#[global] Hint Resolve shell_header_encoding_is_valid : Data_encoding_db.

Axiom Included_HASHABLE_encoding_is_valid :
  Data_encoding.Valid.t (fun _ : Operation.tTrue)
  Operation.Included_HASHABLE.(S.HASHABLE.encoding).
#[global] Hint Resolve Included_HASHABLE_encoding_is_valid : Data_encoding_db.