Skip to main content

🎫 Ticket_amount.v


See code, Gitlab , OCaml

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.
Positivity (aka validity, as per the .mli file, predicate for the type [t].
  Definition t := Script_int.n_num.Valid.positive.
  #[global] Hint Unfold t : tezos_z.

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.

Being valid implies being non_negative.
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.
  intros H.
  unfold Ticket_amount.of_n.
  destruct eqn:eq_b ; simpl ; try constructor ; assumption.

[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 [] could be in order, would factorize proofs and avoid calling [lia] several times...
  intros H. destruct n_value as [n0]. simpl in H.
  unfold Ticket_amount.of_n.
  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. *)
  assert (Hcomp : n0 =1 ).
  { unfold
    destruct (_ <? _) eqn:? ; [lia |].
    destruct (_ =? _) eqn:? ; [lia | reflexivity].
  rewrite Hcomp in Heqb. inversion Heqb.

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.
  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 ( z_res Script_int.zero_n >i 0) eqn:eq_b ; [|
  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.

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.
  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.

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).
  intros H_a H_b.
  destruct_all Script_int.num.
  unfold Ticket_amount.add.

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
  intros [num] Hnum.
  { 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.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.