🥖 Baking.v

Simulations

See code, See proofs, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.

Require TezosOfOCaml.Proto_alpha.Delegate_sampler.

Simulation for [Baking.baking_rights].

Definition baking_rights
  (c_value : Raw_context.t) (level : Level_repr.t)
  : M? (Misc.lazy_list_t Delegate_consensus_key.t) :=
  let fix f_value
    (c_value : Raw_context.t) (fuel : nat)
    {struct fuel} : M? (Misc.lazy_list_t Delegate_consensus_key.t) :=
    match fuel with
    | Datatypes.O ⇒
        Error_monad.error_value
          (Build_extensible "Round_overflow" int (Int32.max_int + 1)%Z)
    | Datatypes.S fuel ⇒
        let? '(c_value, _slot, consensus_pk) :=
          Delegate_sampler.baking_rights_owner
            c_value level (Int32.max_int - Z.of_nat fuel)
        in
        return?
          (Misc.LCons (Delegate_consensus_key.pkh consensus_pk)
             (fun (function_parameter : unit) ⇒
                let '_ := function_parameter in
                f_value c_value fuel))
    end
  in f_value c_value (Z.to_nat (Int32.max_int + 1)).