⚗️ Liquidity_baking_storage.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Liquidity_baking_storage.

Require TezosOfOCaml.Proto_alpha.Proofs.Liquidity_baking_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.

The function [get_cpmm_address] is valid.

Lemma get_cpmm_address_is_valid ctxt
  (H_ctxt : Raw_context.Valid.t ctxt) :
  letP? _ := Liquidity_baking_storage.get_cpmm_address ctxt in
  True.
Proof.
Admitted.

The function [get_toggle_ema ] is valid.

Lemma get_toggle_ema_is_valid ctxt
  (H_ctxt : Raw_context.Valid.t ctxt) :
  letP? ema := Liquidity_baking_storage.get_toggle_ema ctxt in
  Liquidity_baking_repr.Toggle_EMA.Valid.t ema.
Proof.
Admitted.

The function [on_cpmm_exists] is valid.

Lemma on_cpmm_exists_is_valid {A : Set} (P : A → Prop) ctxt f
  (H_ctxt : Raw_context.Valid.t ctxt)
  (H_f : ∀ ctxt contract,
    Raw_context.Valid.t ctxt →
    letP? '(ctxt, items) := f ctxt contract in
    Raw_context.Valid.t ctxt ∧
    List.Forall P items
  ) :
  letP? '(ctxt, items) := Liquidity_baking_storage.on_cpmm_exists ctxt f in
  Raw_context.Valid.t ctxt ∧
  List.Forall P items.
Proof.
Admitted.

The function [update_toggle_ema] is valid.

Lemma update_toggle_ema_is_valid ctxt toggle_vote
  (H_ctxt : Raw_context.Valid.t ctxt) :
  letP? '(ctxt, ema) :=
    Liquidity_baking_storage.update_toggle_ema ctxt toggle_vote in
  Raw_context.Valid.t ctxt ∧
  Liquidity_baking_repr.Toggle_EMA.Valid.t ema.
Proof.
Admitted.

The function [on_subsidy_allowed] is valid.

Lemma on_subsidy_allowed_is_valid {A : Set} (P : A → Prop) ctxt toggle_vote f
  (H_ctxt : Raw_context.Valid.t ctxt)
  (H_f : ∀ ctxt contract,
    Raw_context.Valid.t ctxt →
    letP? '(ctxt, items) := f ctxt contract in
    Raw_context.Valid.t ctxt ∧
    List.Forall P items
  ) :
  letP? '(ctxt, items, ema) :=
    Liquidity_baking_storage.on_subsidy_allowed ctxt toggle_vote f in
  Raw_context.Valid.t ctxt ∧
  List.Forall P items ∧
  Liquidity_baking_repr.Toggle_EMA.Valid.t ema.
Proof.
Admitted.