👥 Delegate_slashed_deposits_storage.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Delegate_slashed_deposits_storage.

Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
Require TezosOfOCaml.Proto_alpha.Proofs.Receipt_repr.

The function [already_slashed_for_double_endorsing] is valid.

Lemma already_slashed_for_double_endorsing_is_valid ctxt delegate level
  (H_ctxt : Raw_context.Valid.t ctxt)
  (H_level : Level_repr.Valid.t level) :
  letP? _ :=
    Delegate_slashed_deposits_storage.already_slashed_for_double_endorsing
      ctxt delegate level in
  True.
Proof.
Admitted.

The function [already_slashed_for_double_baking] is valid.

Lemma already_slashed_for_double_baking_is_valid ctxt delegate level
  (H_ctxt : Raw_context.Valid.t ctxt)
  (H_level : Level_repr.Valid.t level) :
  letP? _ :=
    Delegate_slashed_deposits_storage.already_slashed_for_double_baking
      ctxt delegate level in
  True.
Proof.
Admitted.

The function [punish_double_endorsing] is valid.

Lemma punish_double_endorsing_is_valid ctxt delegate level
  (H_ctxt : Raw_context.Valid.t ctxt)
  (H_level : Level_repr.Valid.t level) :
  letP? '(ctxt, amount, updates) :=
    Delegate_slashed_deposits_storage.punish_double_endorsing
      ctxt delegate level in
  Raw_context.Valid.t ctxt ∧
  Tez_repr.Valid.t amount ∧
  Receipt_repr.balance_updates.Valid.t updates.
Proof.
Admitted.

The function [punish_double_baking] is valid.

Lemma punish_double_baking_is_valid ctxt delegate level
  (H_ctxt : Raw_context.Valid.t ctxt)
  (H_level : Level_repr.Valid.t level) :
  letP? '(ctxt, amount, updates) :=
    Delegate_slashed_deposits_storage.punish_double_baking
      ctxt delegate level in
  Raw_context.Valid.t ctxt ∧
  Tez_repr.Valid.t amount ∧
  Receipt_repr.balance_updates.Valid.t updates.
Proof.
Admitted.

The function [clear_outdated_slashed_deposits] is valid.

Lemma clear_outdated_slashed_deposits_is_valid ctxt new_cycle
  (H_ctxt : Raw_context.Valid.t ctxt)
  (H_new_cycle : Cycle_repr.Valid.t new_cycle) :
  letP? ctxt :=
    Delegate_slashed_deposits_storage.clear_outdated_slashed_deposits
      ctxt new_cycle in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.