💎 Nonce_storage.v
Translated OCaml
File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Constants_storage.
Require TezosOfOCaml.Proto_alpha.Cycle_repr.
Require TezosOfOCaml.Proto_alpha.Level_repr.
Require TezosOfOCaml.Proto_alpha.Level_storage.
Require TezosOfOCaml.Proto_alpha.Nonce_hash.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Seed_repr.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
Definition t : Set := Seed_repr.nonce.
Definition nonce : Set := t.
Definition encoding : Data_encoding.t Seed_repr.nonce :=
Seed_repr.nonce_encoding.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Constants_storage.
Require TezosOfOCaml.Proto_alpha.Cycle_repr.
Require TezosOfOCaml.Proto_alpha.Level_repr.
Require TezosOfOCaml.Proto_alpha.Level_storage.
Require TezosOfOCaml.Proto_alpha.Nonce_hash.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Seed_repr.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
Definition t : Set := Seed_repr.nonce.
Definition nonce : Set := t.
Definition encoding : Data_encoding.t Seed_repr.nonce :=
Seed_repr.nonce_encoding.
Init function; without side-effects in Coq
Definition init_module : unit :=
let '_ :=
Error_monad.register_error_kind Error_monad.Branch
"nonce.too_late_revelation" "Too late nonce revelation"
"Nonce revelation happens too late"
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"This nonce cannot be revealed anymore."
CamlinternalFormatBasics.End_of_format)
"This nonce cannot be revealed anymore.")))
Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Too_late_revelation" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Too_late_revelation" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"nonce.too_early_revelation" "Too early nonce revelation"
"Nonce revelation happens before cycle end"
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"This nonce should not yet be revealed"
CamlinternalFormatBasics.End_of_format)
"This nonce should not yet be revealed")))
Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Too_early_revelation" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Too_early_revelation" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Branch "nonce.already_revealed"
"Already revealed nonce" "Duplicated revelation for a nonce."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"This nonce was already revealed"
CamlinternalFormatBasics.End_of_format)
"This nonce was already revealed"))) Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Already_revealed_nonce" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Already_revealed_nonce" unit tt) in
Error_monad.register_error_kind Error_monad.Branch "nonce.inconsistent"
"Inconsistent nonce"
"The provided nonce is inconsistent with the committed nonce hash."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"This nonce revelation is invalid (inconsistent with the committed hash)"
CamlinternalFormatBasics.End_of_format)
"This nonce revelation is invalid (inconsistent with the committed hash)")))
Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Inconsistent_nonce" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Inconsistent_nonce" unit tt).
Definition get_unrevealed (ctxt : Raw_context.t) (level : Level_repr.t)
: M? Storage.Seed.unrevealed_nonce :=
let current_level := Level_storage.current ctxt in
match Cycle_repr.pred current_level.(Level_repr.t.cycle) with
| None ⇒ Error_monad.tzfail (Build_extensible "Too_early_revelation" unit tt)
| Some revealed_cycle ⇒
if Cycle_repr.op_lt revealed_cycle level.(Level_repr.t.cycle) then
Error_monad.tzfail (Build_extensible "Too_early_revelation" unit tt)
else
if
(Cycle_repr.op_lt level.(Level_repr.t.cycle) revealed_cycle) ||
(current_level.(Level_repr.t.cycle_position) ≥i32
(Constants_storage.nonce_revelation_threshold ctxt))
then
Error_monad.tzfail (Build_extensible "Too_late_revelation" unit tt)
else
let? function_parameter :=
Storage.Seed.Nonce.(Storage_sigs.Non_iterable_indexed_data_storage.get)
ctxt level in
match function_parameter with
| Storage.Cycle.Revealed _ ⇒
Error_monad.tzfail (Build_extensible "Already_revealed_nonce" unit tt)
| Storage.Cycle.Unrevealed status ⇒ return? status
end
end.
Definition record_hash
(ctxt : Raw_context.t) (unrevealed : Storage.Seed.unrevealed_nonce)
: M? Raw_context.t :=
let level := Level_storage.current ctxt in
Storage.Seed.Nonce.(Storage_sigs.Non_iterable_indexed_data_storage.init_value)
ctxt level (Storage.Cycle.Unrevealed unrevealed).
Definition check_unrevealed
(ctxt : Raw_context.t) (level : Level_repr.t) (nonce_value : Seed_repr.nonce)
: M? unit :=
let? unrevealed := get_unrevealed ctxt level in
Error_monad.fail_unless
(Seed_repr.check_hash nonce_value
unrevealed.(Storage.Cycle.unrevealed_nonce.nonce_hash))
(Build_extensible "Inconsistent_nonce" unit tt).
Definition reveal
(ctxt : Raw_context.t) (level : Level_repr.t) (nonce_value : Seed_repr.nonce)
: M? Raw_context.t :=
Storage.Seed.Nonce.(Storage_sigs.Non_iterable_indexed_data_storage.update)
ctxt level (Storage.Cycle.Revealed nonce_value).
Definition unrevealed : Set := Storage.Seed.unrevealed_nonce.
Definition status : Set := Storage.Seed.nonce_status.
Definition get
: Raw_context.t → Level_repr.t → M? Storage.Seed.nonce_status :=
Storage.Seed.Nonce.(Storage_sigs.Non_iterable_indexed_data_storage.get).
Inductive nonce_presence : Set :=
| No_nonce_expected : nonce_presence
| Nonce_expected : status → nonce_presence.
Definition check (ctxt : Raw_context.t) (level : Level_repr.t)
: M? nonce_presence :=
let? function_parameter :=
Storage.Seed.Nonce.(Storage_sigs.Non_iterable_indexed_data_storage.find)
ctxt level in
match function_parameter with
| None ⇒ return? No_nonce_expected
| Some status ⇒ return? (Nonce_expected status)
end.
Definition of_bytes : bytes → M? Seed_repr.nonce := Seed_repr.make_nonce.
Definition hash_value : Seed_repr.nonce → Nonce_hash.t := Seed_repr.hash_value.
Definition check_hash : Seed_repr.nonce → Nonce_hash.t → bool :=
Seed_repr.check_hash.
let '_ :=
Error_monad.register_error_kind Error_monad.Branch
"nonce.too_late_revelation" "Too late nonce revelation"
"Nonce revelation happens too late"
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"This nonce cannot be revealed anymore."
CamlinternalFormatBasics.End_of_format)
"This nonce cannot be revealed anymore.")))
Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Too_late_revelation" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Too_late_revelation" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"nonce.too_early_revelation" "Too early nonce revelation"
"Nonce revelation happens before cycle end"
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"This nonce should not yet be revealed"
CamlinternalFormatBasics.End_of_format)
"This nonce should not yet be revealed")))
Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Too_early_revelation" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Too_early_revelation" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Branch "nonce.already_revealed"
"Already revealed nonce" "Duplicated revelation for a nonce."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"This nonce was already revealed"
CamlinternalFormatBasics.End_of_format)
"This nonce was already revealed"))) Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Already_revealed_nonce" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Already_revealed_nonce" unit tt) in
Error_monad.register_error_kind Error_monad.Branch "nonce.inconsistent"
"Inconsistent nonce"
"The provided nonce is inconsistent with the committed nonce hash."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"This nonce revelation is invalid (inconsistent with the committed hash)"
CamlinternalFormatBasics.End_of_format)
"This nonce revelation is invalid (inconsistent with the committed hash)")))
Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Inconsistent_nonce" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Inconsistent_nonce" unit tt).
Definition get_unrevealed (ctxt : Raw_context.t) (level : Level_repr.t)
: M? Storage.Seed.unrevealed_nonce :=
let current_level := Level_storage.current ctxt in
match Cycle_repr.pred current_level.(Level_repr.t.cycle) with
| None ⇒ Error_monad.tzfail (Build_extensible "Too_early_revelation" unit tt)
| Some revealed_cycle ⇒
if Cycle_repr.op_lt revealed_cycle level.(Level_repr.t.cycle) then
Error_monad.tzfail (Build_extensible "Too_early_revelation" unit tt)
else
if
(Cycle_repr.op_lt level.(Level_repr.t.cycle) revealed_cycle) ||
(current_level.(Level_repr.t.cycle_position) ≥i32
(Constants_storage.nonce_revelation_threshold ctxt))
then
Error_monad.tzfail (Build_extensible "Too_late_revelation" unit tt)
else
let? function_parameter :=
Storage.Seed.Nonce.(Storage_sigs.Non_iterable_indexed_data_storage.get)
ctxt level in
match function_parameter with
| Storage.Cycle.Revealed _ ⇒
Error_monad.tzfail (Build_extensible "Already_revealed_nonce" unit tt)
| Storage.Cycle.Unrevealed status ⇒ return? status
end
end.
Definition record_hash
(ctxt : Raw_context.t) (unrevealed : Storage.Seed.unrevealed_nonce)
: M? Raw_context.t :=
let level := Level_storage.current ctxt in
Storage.Seed.Nonce.(Storage_sigs.Non_iterable_indexed_data_storage.init_value)
ctxt level (Storage.Cycle.Unrevealed unrevealed).
Definition check_unrevealed
(ctxt : Raw_context.t) (level : Level_repr.t) (nonce_value : Seed_repr.nonce)
: M? unit :=
let? unrevealed := get_unrevealed ctxt level in
Error_monad.fail_unless
(Seed_repr.check_hash nonce_value
unrevealed.(Storage.Cycle.unrevealed_nonce.nonce_hash))
(Build_extensible "Inconsistent_nonce" unit tt).
Definition reveal
(ctxt : Raw_context.t) (level : Level_repr.t) (nonce_value : Seed_repr.nonce)
: M? Raw_context.t :=
Storage.Seed.Nonce.(Storage_sigs.Non_iterable_indexed_data_storage.update)
ctxt level (Storage.Cycle.Revealed nonce_value).
Definition unrevealed : Set := Storage.Seed.unrevealed_nonce.
Definition status : Set := Storage.Seed.nonce_status.
Definition get
: Raw_context.t → Level_repr.t → M? Storage.Seed.nonce_status :=
Storage.Seed.Nonce.(Storage_sigs.Non_iterable_indexed_data_storage.get).
Inductive nonce_presence : Set :=
| No_nonce_expected : nonce_presence
| Nonce_expected : status → nonce_presence.
Definition check (ctxt : Raw_context.t) (level : Level_repr.t)
: M? nonce_presence :=
let? function_parameter :=
Storage.Seed.Nonce.(Storage_sigs.Non_iterable_indexed_data_storage.find)
ctxt level in
match function_parameter with
| None ⇒ return? No_nonce_expected
| Some status ⇒ return? (Nonce_expected status)
end.
Definition of_bytes : bytes → M? Seed_repr.nonce := Seed_repr.make_nonce.
Definition hash_value : Seed_repr.nonce → Nonce_hash.t := Seed_repr.hash_value.
Definition check_hash : Seed_repr.nonce → Nonce_hash.t → bool :=
Seed_repr.check_hash.