Skip to main content

💍 Commitment_storage.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Commitment_storage.

Require TezosOfOCaml.Environment.V8.Proofs.Int64.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
Require TezosOfOCaml.Proto_alpha.Proofs.Tez_repr.

The function [committed_amount] is valid.
The function [increase_commitment_only_call_from_token] is valid.
The function [decrease_commitment_only_call_from_token] is valid.
Assume that all the committed values are valid
[Tez_repr.zero] is never stored in the context This is true by the defintion of [increase_*] and decrease_*] functions and prooved by [decrease_does_not_store_zero] and [increase_does_not_store_zero]
Axiom stored_values_are_never_zero :
   ctxt bpkh,
    Storage.Commitments.(Storage_sigs.Indexed_data_storage.find)
                          ctxt bpkh
      Pervasives.Ok (Some Tez_repr.zero).

Helper lemma to derive [Stoorage.Commitments.find ... = None] from [commited_amount ... = Ok Tez_repr.zero]
Lemma committed_zero_to_find_neq ctxt bpkh :
      Commitment_storage.committed_amount ctxt bpkh
      = Pervasives.Ok Tez_repr.zero
      Storage.Commitments.(Storage_sigs.Indexed_data_storage.find)
        ctxt bpkh = Pervasives.Ok None.
Proof.
  unfold Commitment_storage.committed_amount.
  unfold Option.value_value.
  destruct Storage.Commitments.(
    Storage_sigs.Indexed_data_storage.find) eqn:?; [|easy];
    destruct o eqn:?; [|easy]. simpl.
  intros Hinj. injection Hinj as Hinj. rewrite Hinj in Heqt.
  now apply stored_values_are_never_zero in Heqt.
Qed.

Decreasing by the same amount committed removes the committed value. In other words, [Tez_repr.zero] is not stored
Lemma decrease_does_not_store_zero ctxt bpkh amount :
    Commitment_storage.committed_amount ctxt bpkh =
      Pervasives.Ok amount
    Commitment_storage.decrease_commitment_only_call_from_token
      ctxt bpkh amount =
      Pervasives.Ok
        (Storage.Commitments.(Storage_sigs.Indexed_data_storage.remove)
                               ctxt bpkh).
Proof.
  intros.
  unfold Commitment_storage.decrease_commitment_only_call_from_token.
  rewrite H. simpl.
  assert (Hminus_eq_zero : Tez_repr.op_minusquestion amount amount =
                             Pervasives.Ok Tez_repr.zero).
  { unfold Tez_repr.op_minusquestion. destruct amount.
    simpl. rewrite Z.leb_refl.
    replace (r -i64 r) with 0 by lia.
    easy. }
  rewrite Hminus_eq_zero. simpl. easy.
Qed.

Assumming that there is no committed value ([committed_amount] returns [Tez_repr.zero]), increase by [Tez_repr.zero] followed by feching returns [None]
Lemma increase_does_not_store_zero ctxt bpkh :
    Commitment_storage.committed_amount ctxt bpkh =
      Pervasives.Ok Tez_repr.zero
    letP? ctxt' :=
      Commitment_storage.increase_commitment_only_call_from_token
        ctxt bpkh Tez_repr.zero in
    Storage.Commitments.(Storage_sigs.Indexed_data_storage.find)
                          ctxt bpkh = Pervasives.Ok None.
Proof.
  unfold Commitment_storage.committed_amount.
  unfold Option.value_value.
  destruct _.(Storage_sigs.Indexed_data_storage.find) eqn:?;
    [destruct o eqn:?; [|easy]; simpl|easy].
  simpl. intros. injection H as H. rewrite H in Heqt.
    now apply stored_values_are_never_zero in Heqt.
Qed.

[increase_commitment_only_call_from_token] of [Tez_repr.zero] is an identity