Skip to main content

💎 Nonce_storage.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml
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
  | NoneError_monad.fail (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.fail (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.fail (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.fail (Build_extensible "Already_revealed_nonce" unit tt)
        | Storage.Cycle.Unrevealed statusreturn? 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
  | Nonereturn? No_nonce_expected
  | Some statusreturn? (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.