Skip to main content

🍃 Timelock.v

Environment

Gitlab

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

Require TezosOfOCaml.Environment.Structs.V0.Bytes.
Require TezosOfOCaml.Environment.Structs.V0.Data_encoding.

Parameter chest : Set.

Parameter chest_encoding : Data_encoding.t chest.

Parameter chest_key : Set.

Parameter chest_key_encoding : Data_encoding.t chest_key.

Inductive opening_result : Set :=
| Correct : Bytes.t opening_result
| Bogus_cipher : opening_result
| Bogus_opening : opening_result.

Parameter open_chest : chest chest_key int opening_result.

Parameter get_plaintext_size : chest int.