🍃 Timelock.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 chest_encoding_is_valid : Data_encoding.Valid.t (fun _ ⇒ True) Timelock.chest_encoding.
#[global] Hint Resolve chest_encoding_is_valid : Data_encoding_db.

Axiom chest_key_encoding_is_valid : Data_encoding.Valid.t (fun _ ⇒ True) Timelock.chest_key_encoding.
#[global] Hint Resolve chest_key_encoding_is_valid : Data_encoding_db.