Skip to main content

👥 Delegate_sampler.v

Proofs

See code, Gitlab , OCaml

[Delegate_sampler.Delegate_sampler_state.Cache.(find)] is valid
    Axiom find_is_valid
      : (ctxt : Proto_alpha.Raw_context.t)
          (identifier : string),
        letP? _ := Delegate_sampler.Delegate_sampler_state.Cache
                     .(Cache_repr.INTERFACE.find)
                        ctxt identifier in True.
  End Cache.

[Delegate_sampler.Delegate_sampler_state.get] is valid
  Lemma get_is_valid
    (ctxt : Proto_alpha.Raw_context.t)
    (cycle : Cycle_repr.t)
    : letP? _ := Delegate_sampler.Delegate_sampler_state.get ctxt cycle in
      True.
  Proof. Admitted.
End Delegate_sampler_state.

Module Random.
[Delegate_sampler.Range.sampler_for_cycle] is_valid
[Delegate_sampler.Range.owner] is valid
  Lemma owner_is_valid
    (ctxt : Proto_alpha.Raw_context.t)
    (level : Level_repr.t)
    (slot : Slot_repr.t)
    : Raw_context.Valid.t ctxt
      Level_repr.Valid.t level
      Slot_repr.Valid.t slot
      letP? '(ctxt, _) := Delegate_sampler.Random.owner ctxt level slot in
      Raw_context.Valid.t ctxt.
  Proof.
    intros Hv_ctxt Hv_lvl Hv_slot.
    unfold Delegate_sampler.Random.owner.
    eapply split_letP; [
      apply Random.sampler_for_cycle_is_valid; trivial; apply Hv_lvl
    |].
    intros [[] ?] [].
    apply split_letP_triv; [apply Sampler.sample_is_valid|];
      trivial.
  Qed.
End Random.

[Delegate_sampler.slot_owner] has no internal errors
[Delegate_sampler.baking_rights_owner] is valid