Skip to main content

🍃 Timelock.v

Environment

See proofs, Gitlab , OCaml

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

Require Proto_alpha.Environment.Bytes.
Require Proto_alpha.Environment.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.