🍃 Timelock.v
Environment
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.
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.