💍 Commitment_storage.v
Proofs
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.
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.
Lemma committed_amount_is_valid ctxt bpkh :
Raw_context.Valid.t ctxt →
letP? amount := Commitment_storage.committed_amount ctxt bpkh in
Tez_repr.Valid.t amount.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
letP? amount := Commitment_storage.committed_amount ctxt bpkh in
Tez_repr.Valid.t amount.
Proof.
Admitted.
The function [increase_commitment_only_call_from_token] is valid.
Lemma increase_commitment_only_call_from_token_is_valid ctxt bpkh amount :
Raw_context.Valid.t ctxt →
Tez_repr.Valid.t amount →
letP? ctxt :=
Commitment_storage.increase_commitment_only_call_from_token
ctxt bpkh amount in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
Tez_repr.Valid.t amount →
letP? ctxt :=
Commitment_storage.increase_commitment_only_call_from_token
ctxt bpkh amount in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
The function [decrease_commitment_only_call_from_token] is valid.
Lemma decrease_commitment_only_call_from_token_is_valid ctxt bpkh amount :
Raw_context.Valid.t ctxt →
Tez_repr.Valid.t amount →
letP? ctxt :=
Commitment_storage.decrease_commitment_only_call_from_token
ctxt bpkh amount in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
Tez_repr.Valid.t amount →
letP? ctxt :=
Commitment_storage.decrease_commitment_only_call_from_token
ctxt bpkh amount in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
Assume that all the committed values are valid
Axiom stored_values_are_valid : ∀ ctxt bpkh x,
Commitment_storage.committed_amount ctxt bpkh = Pervasives.Ok x →
Tez_repr.Valid.t x.
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 bpkh,
Storage.Commitments.(Storage_sigs.Indexed_data_storage.find)
ctxt bpkh ≠
Pervasives.Ok (Some Tez_repr.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.
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.
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.
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
Lemma increase_by_zero_id ctxt bpkh :
Commitment_storage.increase_commitment_only_call_from_token
ctxt bpkh Tez_repr.zero = Pervasives.Ok ctxt.
Proof.
easy.
Qed.
Commitment_storage.increase_commitment_only_call_from_token
ctxt bpkh Tez_repr.zero = Pervasives.Ok ctxt.
Proof.
easy.
Qed.