💍 Commitment_storage.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Commitment_storage.

Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Int64.
Require TezosOfOCaml.Proto_alpha.Environment.Pervasives.
Require TezosOfOCaml.Proto_alpha.Proofs.Tez_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Storage_sigs.
Require TezosOfOCaml.Proto_alpha.Proofs.Storage.

Assume that all the committed values are valid

Axiom stored_values_are_valid : ∀
    (ctxt : Raw_context.t) (bpkh : Blinded_public_key_hash.t)
    (x : Tez_repr.t),
    Commitment_storage.committed_amount ctxt bpkh = Pervasives.Ok x →
      Tez_repr.Valid.t x.

[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 : Raw_context.t)
    (bpkh : Blinded_public_key_hash.t),
    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 : Raw_context.t)
      (bpkh : Blinded_public_key_hash.t) :
      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 : Raw_context.t) (bpkh : Blinded_public_key_hash.t)
      (amount : Tez_repr.t) :
    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 : Raw_context.t)
      (bpkh : Blinded_public_key_hash.t) :
    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.

Lemma with_commitments_id : ∀ (state : Storage.Simulation.State),
    Storage.Simulation.with_commitments
      state.(Storage.Simulation.commitments)
              state = state.
Proof.
  sauto lq:on.
Qed.

[decrease_commitment_only_call_from_token] with [Tez_repr.zero] is an identity

Lemma decrease_by_zero_id ctxt bpkh :
  letP? ctxt' :=
    Commitment_storage.decrease_commitment_only_call_from_token
      ctxt bpkh Tez_repr.zero in
  Storage.parse ctxt = Storage.parse ctxt'.
Proof.
  intros.
  unfold Commitment_storage.decrease_commitment_only_call_from_token.
  simpl.
  destruct Commitment_storage.committed_amount eqn:?; [|easy].
  simpl. rewrite Tez_repr.op_minusquestion_zero_id;
    [|now apply (stored_values_are_valid ctxt bpkh t)].
  simpl.
  destruct (Tez_repr.op_eq _ _) eqn:Eq_zero.
  { assert (Hfind_eq_none :
             Storage.Commitments.(
                Storage_sigs.Indexed_data_storage.find) ctxt bpkh =
             Pervasives.Ok None).
    { revert Heqt.
      assert (Eq_zero' : t = Tez_repr.zero).
      { revert Eq_zero. unfold Tez_repr.zero. destruct t.
        simpl. rewrite Z.eqb_eq. intros Eq_zero. now rewrite Eq_zero. }
      rewrite Eq_zero'.
      unfold Commitment_storage.committed_amount.
      unfold Option.value_value.
      destruct _.(Storage_sigs.Indexed_data_storage.find) eqn:?;
        [|easy].
      simpl. destruct o eqn:?; [|easy].
      intros. injection Heqt as Heqt. rewrite Heqt in Heqt0.
      now apply stored_values_are_never_zero in Heqt0. }
    revert Hfind_eq_none. simpl.
    rewrite Storage.Eq.Commitments.eq.(
      Storage_sigs.Indexed_data_storage.Eq.remove).
    rewrite Storage.Eq.Commitments.eq.(
      Storage_sigs.Indexed_data_storage.Eq.find).
    simpl.
    unfold Storage_sigs.Indexed_data_storage.Op.find,
      Storage_sigs.Indexed_data_storage.Op.remove,
      Storage_sigs.Indexed_data_storage.State.Map.
    intros.
    assert (Hmap_find_eq_none': (Map.Make (
              Storage_sigs.Indexed_data_storage.State.Ord
              Storage.generic_Path_encoding)).(S.find)
    bpkh (Storage.Eq.Commitments.parse ctxt) = None).
    { revert Hfind_eq_none.
      destruct (Map.Make _).(S.find); [|easy].
      destruct o; [|easy].
      intros. injection Hfind_eq_none as Hfind_eq_none.
      discriminate Hfind_eq_none. }
    clear Hfind_eq_none.
    unfold Storage.Eq.Commitments.apply.
    rewrite Storage.parse_apply; simpl.
    unfold Storage_sigs.Indexed_data_storage.State.Map.
    rewrite Map.remove_find_none; trivial.
    now destruct Storage.parse. }
  { simpl.
    assert (Hfind_eq_some :
        Storage.Commitments.(
           Storage_sigs.Indexed_data_storage.find) ctxt bpkh =
           Pervasives.Ok (Some t)).
    { revert Heqt.
      unfold Commitment_storage.committed_amount.
      unfold Option.value_value.
      destruct _.(Storage_sigs.Indexed_data_storage.find) eqn:?;
                                                          [|easy].
      simpl. destruct o eqn:?.
      { intros. injection Heqt as Heqt. now rewrite Heqt. }
      { intros. injection Heqt as Heqt. rewrite Heqt in Eq_zero.
        scongruence. }
    }
    revert Heqt.
    unfold Commitment_storage.committed_amount.
    rewrite Hfind_eq_some. simpl.
    intros _.
    revert Hfind_eq_some.
    rewrite Storage.Eq.Commitments.eq.(
      Storage_sigs.Indexed_data_storage.Eq.find).
    rewrite Storage.Eq.Commitments.eq.(
      Storage_sigs.Indexed_data_storage.Eq.add).
    simpl.
    unfold Storage_sigs.Indexed_data_storage.Op.find,
      Storage_sigs.Indexed_data_storage.Op.add,
      Storage_sigs.Indexed_data_storage.State.Map.
    destruct (Map.Make _).(S.find) eqn:?;
                                   [destruct o; [|easy]|easy].
    intros. injection Hfind_eq_some as Hfind_eq_some.
    rewrite Hfind_eq_some in Heqo. clear Hfind_eq_some.
    unfold Storage.Eq.Commitments.parse,
      Storage.Eq.Commitments.apply.
    rewrite Storage.parse_apply. simpl.
    unfold Storage_sigs.Indexed_data_storage.State.Map.
    rewrite Map.add_found_eq; auto.
    { now rewrite with_commitments_id. }
    { apply Storage.generic_Path_encoding_Valid. }
  }
Qed.

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

Lemma increase_by_zero_id (ctxt : Raw_context.t)
      (bpkh : _) :
  Commitment_storage.increase_commitment_only_call_from_token
    ctxt bpkh Tez_repr.zero = Pervasives.Ok ctxt.
Proof.
  easy.
Qed.

increase and decrease functions are inversion of each other

Lemma increase_decrease_inverse
      (absolute_key : Context.key)
      (ctxt0 : Raw_context.t) (bpkh : _) (amount : Tez_repr.t) :
  (∀ x, Commitment_storage.committed_amount ctxt0 bpkh =
               Pervasives.Ok x →
             Tez_repr.Valid.t x) →
  Tez_repr.Valid.t amount →
  letP? ctxt1 :=
  Commitment_storage.increase_commitment_only_call_from_token
                   ctxt0 bpkh amount in
  letP? ctxt2 :=
    Commitment_storage.decrease_commitment_only_call_from_token
                     ctxt1 bpkh amount in
      Storage.parse ctxt0 = Storage.parse ctxt2.
Proof.
  intros.
  unfold Commitment_storage.increase_commitment_only_call_from_token.
  destruct Tez_repr.op_eq eqn:Htez_repr_eq.
  { assert (Hzero : amount = Tez_repr.zero).
    { revert Htez_repr_eq.
      destruct amount, Tez_repr.zero. simpl.
      intros. f_equal. lia. }
    simpl.
    rewrite Hzero.
    apply decrease_by_zero_id. }
  { destruct Commitment_storage.committed_amount
      as [committed|committed] eqn:Hcommitted; [|easy].
    simpl.
    unfold Tez_repr.op_plusquestion.
    destruct committed as [committed'].
    destruct amount as [amount'].
    destruct (_ +i64 _ <i64 _) eqn:?; [easy|].
    simpl.
    unfold Commitment_storage.decrease_commitment_only_call_from_token.
    unfold Commitment_storage.committed_amount.
    rewrite Storage.Eq.Commitments.eq.(
      Storage_sigs.Indexed_data_storage.Eq.find).
    rewrite Storage.Eq.Commitments.eq.(
      Storage_sigs.Indexed_data_storage.Eq.add).
    simpl.
    unfold Storage.Eq.Commitments.apply.
    unfold Storage.Eq.Commitments.parse.
    rewrite Storage.parse_apply.
    unfold Storage_sigs.Indexed_data_storage.Op.add.
    unfold Storage_sigs.Indexed_data_storage.Op.find.
    unfold Storage.Simulation.reduce.
    unfold Storage_sigs.Indexed_data_storage.reduce.
    unfold Storage.Simulation.with_commitments.
    simpl.
    unfold Storage_sigs.Indexed_data_storage.State.Map.
    set (Ord := Storage_sigs.Indexed_data_storage.State.Ord _).
    rewrite Map.find_add_eq_some.
    { simpl.
      destruct (_ <=? _ +i64 _) eqn:?; [|easy].
      simpl.
      assert (Hcommitted_is_valid : Tez_repr.Valid.t
               (Tez_repr.Tez_tag committed')) by
                now apply stored_values_are_valid in Hcommitted.
      rewrite Int64.add_sub_identity; [|lia|lia].
      destruct (_ =? 0) eqn:?H_committed_eq_0.
      { rewrite Storage.Eq.Commitments.eq.(
          Storage_sigs.Indexed_data_storage.Eq.remove).
        simpl.
        unfold Storage.Eq.Commitments.apply.
        repeat rewrite Storage.parse_apply; simpl.
        unfold Storage_sigs.Indexed_data_storage.State.Map.
        rewrite Map.remove_add_id.
        { apply Z.eqb_eq in H_committed_eq_0.
          rewrite H_committed_eq_0.
          replace (amount' +i64 0) with amount' by lia.
          assert (H_with_commiments_idemp :
                   ∀ (state : Storage.Simulation.State) x,
            Storage.Simulation.with_commitments
              state.(Storage.Simulation.commitments)
              (Storage.Simulation.with_commitments
                x state) = state) by sauto lq: on rew: off; easy.
        }
        { apply Storage.generic_Path_encoding_Valid. }
        assert (Hcommitted_eq_0 : committed' = 0) by lia.
        rewrite Hcommitted_eq_0 in Hcommitted.
        change (Tez_repr.Tez_tag 0) with Tez_repr.zero in Hcommitted.
        apply committed_zero_to_find_neq in Hcommitted.
        unfold Logic.not in Hcommitted.
        revert Hcommitted.
        rewrite Storage.Eq.Commitments.eq.(
          Storage_sigs.Indexed_data_storage.Eq.find); simpl.
        unfold Storage_sigs.Indexed_data_storage.Op.find.
        destruct (_.(S.find) _ _) eqn:?; [destruct o eqn:?|]; try easy.
        intros _. revert Heqo.
        unfold Storage_sigs.Indexed_data_storage.State.Map.
        apply Map.find_eq_none_implies_mem_eq_false.
      }
      { rewrite Storage.Eq.Commitments.eq.(
          Storage_sigs.Indexed_data_storage.Eq.add).
        simpl.
        unfold Storage.Eq.Commitments.apply.
        unfold Storage_sigs.Indexed_data_storage.Op.add.
        repeat (rewrite Storage.parse_apply; simpl).
        unfold Storage_sigs.Indexed_data_storage.State.Map.
        rewrite Map.add_add_eq.
        revert Hcommitted.
        unfold Commitment_storage.committed_amount.
        unfold Option.value_value.
        rewrite Storage.Eq.Commitments.eq.(
          Storage_sigs.Indexed_data_storage.Eq.find); simpl.
        unfold Storage_sigs.Indexed_data_storage.Op.find.
        unfold Storage_sigs.Indexed_data_storage.State.Map.
        set (Ord' := Storage_sigs.Indexed_data_storage.State.Ord _).
        destruct (_.(S.find) _ _) eqn:?; [|sauto q:on];
          destruct o; [|easy]. simpl.
        intros. injection Hcommitted as Hcommitted.
        rewrite Hcommitted in Heqo.
        rewrite Map.add_found_eq; auto.
        { assert (H_with_commitments_idemp :
                   ∀ (state : Storage.Simulation.State) x,
            Storage.Simulation.with_commitments
              state.(Storage.Simulation.commitments)
              (Storage.Simulation.with_commitments
                x state) = state) by sauto lq: on rew: off.
          easy.
        }
        { apply Storage.generic_Path_encoding_Valid. }
        { apply Storage.generic_Path_encoding_Valid. }
      }
    }
    { apply Storage.generic_Path_encoding_Valid. }
  }
Qed.