🎫 Ticket_amount.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Ticket_amount.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_int.
Module Valid.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Ticket_amount.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_int.
Module Valid.
Positivity (aka validity, as per the .mli file, predicate for the type
[t].
Non-negativity predicate for [t].
@Proto_L: Allows using the lemmas of [Script_int].
Definition non_negative := Script_int.n_num.Valid.t.
(* : Prop := *)
(* let 'Script_int.Num_tag n0 := n in n0 >= 0. *)
#[global] Hint Unfold non_negative : tezos_z.
End Valid.
(* : Prop := *)
(* let 'Script_int.Num_tag n0 := n in n0 >= 0. *)
#[global] Hint Unfold non_negative : tezos_z.
End Valid.
Being valid implies being non_negative.
Lemma valid_implies_non_negative n : Valid.t n → Valid.non_negative n.
Proof.
unfold Valid.t, Valid.non_negative.
apply Script_int.n_num.positive_implies_valid.
Qed.
Proof.
unfold Valid.t, Valid.non_negative.
apply Script_int.n_num.positive_implies_valid.
Qed.
The function [of_n] is valid.
Lemma of_n_is_valid n_value :
Valid.t n_value →
let of_n_opt := Ticket_amount.of_n n_value in
Option.Forall Valid.t of_n_opt.
Proof.
intros H.
unfold Ticket_amount.of_n.
destruct Script_int.compare eqn:eq_b ; simpl ; try constructor ; assumption.
Qed.
Valid.t n_value →
let of_n_opt := Ticket_amount.of_n n_value in
Option.Forall Valid.t of_n_opt.
Proof.
intros H.
unfold Ticket_amount.of_n.
destruct Script_int.compare eqn:eq_b ; simpl ; try constructor ; assumption.
Qed.
[of_n n_value] ouputs [Some n_value] when (in pseudo-code [n_value > 0]).
Note that [of_n 0] (in pseudo-code) is [None]
@TODO: 2022/11/21 Some lemmas about [Z.compare] could be in order, would factorize
proofs and avoid calling [lia] several times...
Proof.
intros H. destruct n_value as [n0]. simpl in H.
unfold Ticket_amount.of_n.
unfold Script_int.compare.
destruct Script_int.zero_n as [repr0] eqn:eq_repr0.
inversion eq_repr0 as [eq_0]. subst repr0.
clear eq_repr0.
step ; [ reflexivity |]. (* [step] produces [Heqb] in the context. *)
exfalso.
assert (Hcomp : Z.compare n0 Z.zero =1 ).
{ unfold Z.compare.
destruct (_ <? _) eqn:? ; [lia |].
destruct (_ =? _) eqn:? ; [lia | reflexivity].
}
rewrite Hcomp in Heqb. inversion Heqb.
Qed.
intros H. destruct n_value as [n0]. simpl in H.
unfold Ticket_amount.of_n.
unfold Script_int.compare.
destruct Script_int.zero_n as [repr0] eqn:eq_repr0.
inversion eq_repr0 as [eq_0]. subst repr0.
clear eq_repr0.
step ; [ reflexivity |]. (* [step] produces [Heqb] in the context. *)
exfalso.
assert (Hcomp : Z.compare n0 Z.zero =1 ).
{ unfold Z.compare.
destruct (_ <? _) eqn:? ; [lia |].
destruct (_ =? _) eqn:? ; [lia | reflexivity].
}
rewrite Hcomp in Heqb. inversion Heqb.
Qed.
The function [of_z] is valid.
Lemma of_z_is_valid z_value :
Valid.t z_value →
let of_z_opt := Ticket_amount.of_z z_value in
Option.Forall Valid.t of_z_opt.
Proof.
intros H.
unfold Ticket_amount.of_z.
destruct Script_int.is_nat as [z_res|] eqn:eq_is_nat ; [| constructor ].
simpl. unfold Ticket_amount.of_n. unfold Option.Forall.
destruct z_value as [z0] eqn:eq_z.
(* hfcrush. *)
destruct (Script_int.compare z_res Script_int.zero_n >i 0) eqn:eq_b ; [|
constructor].
specialize (Script_int.is_nat_inversion z0) as H0.
rewrite eq_is_nat in H0.
destruct z_res as [z_res0].
destruct H0 as [H1 H2]. rewrite H1. assumption.
Qed.
Valid.t z_value →
let of_z_opt := Ticket_amount.of_z z_value in
Option.Forall Valid.t of_z_opt.
Proof.
intros H.
unfold Ticket_amount.of_z.
destruct Script_int.is_nat as [z_res|] eqn:eq_is_nat ; [| constructor ].
simpl. unfold Ticket_amount.of_n. unfold Option.Forall.
destruct z_value as [z0] eqn:eq_z.
(* hfcrush. *)
destruct (Script_int.compare z_res Script_int.zero_n >i 0) eqn:eq_b ; [|
constructor].
specialize (Script_int.is_nat_inversion z0) as H0.
rewrite eq_is_nat in H0.
destruct z_res as [z_res0].
destruct H0 as [H1 H2]. rewrite H1. assumption.
Qed.
The function [of_z] is (almost) the identity for positive inputs.
(it outputs [None] for [0]).
Lemma of_z_id_eq z_value:
Valid.t z_value → Ticket_amount.of_z z_value = Some z_value.
Proof.
intros H.
destruct z_value as [z0].
unfold Ticket_amount.of_z.
remember H as H0. clear HeqH0.
unfold Script_int.n_num.Valid.t in H.
specialize (of_n_id_eq (Script_int.Num_tag z0)) as H1.
apply H1 in H0. clear H1.
apply valid_implies_non_negative in H.
specialize (Script_int.is_nat_non_negative z0 H) as H2.
rewrite H2. simpl. rewrite H0. reflexivity.
Qed.
Valid.t z_value → Ticket_amount.of_z z_value = Some z_value.
Proof.
intros H.
destruct z_value as [z0].
unfold Ticket_amount.of_z.
remember H as H0. clear HeqH0.
unfold Script_int.n_num.Valid.t in H.
specialize (of_n_id_eq (Script_int.Num_tag z0)) as H1.
apply H1 in H0. clear H1.
apply valid_implies_non_negative in H.
specialize (Script_int.is_nat_non_negative z0 H) as H2.
rewrite H2. simpl. rewrite H0. reflexivity.
Qed.
When given two valid (i.e. non-negative) numbers, [add] (which is an alias
of [Script_int.add]@Proto_L) has a valid output.
Alias of Lemma [Script_int.add_n_num_is_valid].
Lemma add_is_valid a b :
Valid.t a → Valid.t b → Valid.t (Ticket_amount.add a b).
Proof.
intros H_a H_b.
destruct_all Script_int.num.
unfold Ticket_amount.add.
lia.
Qed.
Valid.t a → Valid.t b → Valid.t (Ticket_amount.add a b).
Proof.
intros H_a H_b.
destruct_all Script_int.num.
unfold Ticket_amount.add.
lia.
Qed.
The encoding [encoding] is valid w.r.t. [Valid.positive]
Note: [Valid.t] is not enough because of the function [of_n],
which succeeds only for *strictly* positive numbers.
Lemma encoding_is_valid : Data_encoding.Valid.t Valid.t
Ticket_amount.encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
intros [num] Hnum.
split.
{ remember Hnum as Hnonneg. clear HeqHnonneg.
apply Script_int.to_zint_non_negative.
Ticket_amount.encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
intros [num] Hnum.
split.
{ remember Hnum as Hnonneg. clear HeqHnonneg.
apply Script_int.to_zint_non_negative.
Adding hints could help automatize this proof.
apply Script_int.n_num.positive_implies_valid in Hnonneg.
assumption. }
{ unfold Ticket_amount.of_zint. rewrite Script_int.of_zint_to_zint_inv.
apply of_z_id_eq in Hnum.
rewrite Hnum. reflexivity.
}
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
assumption. }
{ unfold Ticket_amount.of_zint. rewrite Script_int.of_zint_to_zint_inv.
apply of_z_id_eq in Hnum.
rewrite Hnum. reflexivity.
}
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.