Skip to main content

🍬 Script_int.v

Proofs

See code, Gitlab , OCaml

Non-negativity predicate for [repr].
  Definition non_negative (repr : Script_int.repr) : Prop :=
    0 repr.
  #[global] Hint Unfold non_negative : tezos_z.

Positivity predicate for [repr]. @Proto_L: very useful for file [Ticket_amount.v], where natural numbers are assumed to be *strictly* positive (according to mli).
  Definition positive (repr : Script_int.repr) : Prop :=
    0 < repr.
  #[global] Hint Unfold positive: tezos_z.
  End Valid.

A positive number is non_negative.
  Lemma positive_implies_non_negative repr :
    Valid.positive repr Valid.non_negative repr.
  Proof.
    unfold Valid.positive, Valid.non_negative.
    intros H. lia.
  Qed.

Non-negative + non-null implies positive.
  Lemma non_negative_non_zero_implies_positive n : Valid.non_negative n
    (n 0) Valid.positive n.
  Proof.
    unfold Valid.non_negative, Valid.positive.
    intros H1 H2. lia.
  Qed.
End repr.

Proto_L: [num] uses a phantom type which can be (unbounded) [n] or [z]. We use the precidate [n_num.Valid.t] to specify the [n] case.
Module n_num.
Formerly [Module N.]
  Module Valid.
Non-negativity predicate for [num].
    Definition t num : Prop :=
      let 'Script_int.Num_tag n_value := num in repr.Valid.non_negative n_value.
    #[global] Hint Unfold t : tezos_z.

Positivity predicate for [num]. @Proto_L: very useful for file [Ticket_amount.v], where natural numbers are assumed to be *strictly* positive (according to mli).
    Definition positive num : Prop :=
      let 'Script_int.Num_tag n_value := num in repr.Valid.positive n_value.
    #[global] Hint Unfold positive: tezos_z.
  End Valid.

A positive number is non_negative.
  Lemma positive_implies_valid num :
    Valid.positive num Valid.t num.
  Proof.
    destruct num. simpl.
    apply repr.positive_implies_non_negative.
  Qed.

  Lemma valid_non_zero_implies_positive n :
    Valid.t n (n Script_int.Num_tag 0) Valid.positive n.
  Proof.
    destruct n. simpl in ×. intros H1 H2.
    apply repr.non_negative_non_zero_implies_positive ;
      [ assumption |].
   unfold "~". intro Hcon.
   apply H2. rewrite Hcon. reflexivity.
   Qed.
End n_num.

[compare] is valid. 2022/11/18: I didn't look at the meaning of this lemma.
Lemma compare_is_valid :
  Compare.Valid.t (fun _True) id Script_int.compare.
Proof.
  apply (Compare.equality (
    let proj '(Script_int.Num_tag z) := z in
    Compare.projection proj Z.compare
  )); [sauto lq: on|].
  eapply Compare.implies.
  { eapply Compare.projection_is_valid.
    apply Compare.z_is_valid.
  }
  all: sauto.
Qed.

The function [to_int64] is valid.
@TODO: simplify the proof.
  destruct Script_int.to_int64 as [z64|] eqn:eq_z64 ; [| constructor ].
  rewrite <- eq_z64.
  destruct z as [z0].
  unfold Script_int.to_int64 in ×.
  apply Option.catch_error_some in eq_z64 ; [| assumption ].
  destruct eq_z64 as [eq_z64 H_z64].
  unfold Z.to_int64 in ×.
  step.
  { destruct (Option.catch) as [ z |] eqn:eq_opt_catch.
    { apply Option.catch_error_some in eq_opt_catch ; [| assumption ].
      destruct eq_opt_catch. subst z0 z64.
      simpl. unfold Int64.Valid.t. lia.
    }
    constructor.
  }
  { exfalso.
    specialize (H_z64 (Build_extensible "Overflow" unit tt)).
    apply H_z64.
    reflexivity.
  }
Qed.

The function [to_int64] is the identity on inputs in [int64] bounds.
Lemma to_int64_eq (z : Z.t) :
  Int64.Valid.t z
  Script_int.to_int64 (Script_int.Num_tag z) = Some z.
Proof.
  intros.
  simpl.
  rewrite Z.to_int64_eq by lia.
  now rewrite Option.catch_no_errors.
Qed.

[to_zint] preserves non-negativity.
Lemma to_zint_non_negative x_value :
  n_num.Valid.t x_value
  repr.Valid.non_negative (Script_int.to_zint x_value).
Proof.
  unfold n_num.Valid.t.
  intros H.
  destruct x_value. assumption.
Qed.

[to_zint] preserves positivity.
Lemma to_zint_positive x_value :
  n_num.Valid.positive x_value
  0 < Script_int.to_zint x_value.
Proof.
  unfold n_num.Valid.t.
  intros H.
  destruct x_value. assumption.
Qed.

(* [to_zint] followed by [of_zint] is the identity. *)
Lemma of_zint_to_zint_inv num :
  Script_int.of_zint (Script_int.to_zint num) = num.
Proof.
  unfold Script_int.of_zint, Script_int.to_zint. destruct num. reflexivity.
Qed.

The addition of non_negative numbers gives a non-negative result.
Lemma add_n_num_is_valid a b :
  n_num.Valid.t a
  n_num.Valid.t b
  n_num.Valid.t (Script_int.add a b).
Proof.
  intros H_a H_b.
  destruct_all Script_int.num.
  lia.
Qed.

When there are no divisions by zero, [ediv] has a simpler expression.
Lemma ediv_not_zero (a b : Z.t) :
  b 0
  Script_int.ediv (Script_int.Num_tag a) (Script_int.Num_tag b) =
  Some (
    Script_int.Num_tag (Zeuclid.ZEuclid.div a b),
    Script_int.Num_tag (Zeuclid.ZEuclid.modulo a b)
  ).
Proof.
  intros.
  unfold Script_int.ediv, Z.ediv_rem.
  destruct (_ =? _) eqn:?.
  { lia. }
  { now rewrite Option.catch_no_errors. }
Qed.

The division by zero returns [None].
Lemma ediv_zero (a : Z.t) :
  Script_int.ediv (Script_int.Num_tag a) (Script_int.Num_tag 0) =
  None.
Proof.
  unfold Script_int.ediv, Z.ediv_rem; simpl.
  set (f := fun '(quo, rem)
    (Script_int.Num_tag quo, Script_int.Num_tag rem)
  ).
  epose proof (Pervasives.raise_let _ f) as H_raise.
  unfold f in H_raise.
  rewrite H_raise.
  now rewrite Option.catch_raise.
Qed.

Bounds of the [ediv] operator when used for the [IEdiv_teznat] instruction.
Lemma ediv_teznat_is_valid (a b : Z.t) :
  Tez_repr.Repr.Valid.t a
  0 b
  Option.Forall
    (fun '(Script_int.Num_tag quo, Script_int.Num_tag rem)
      Tez_repr.Repr.Valid.t quo Tez_repr.Repr.Valid.t rem)
    (Script_int.ediv (Script_int.Num_tag a) (Script_int.Num_tag b)).
Proof.
  intros H_a H_b.
  destruct (b =? 0) eqn:?.
  { replace b with 0 by lia.
    now rewrite ediv_zero.
  }
  { rewrite ediv_not_zero by lia; simpl.
    unfold Tez_repr.Repr.Valid.t in *; split.
    { unfold Zeuclid.ZEuclid.div.
      nia.
    }
    { unfold Zeuclid.ZEuclid.modulo.
      replace (BinInt.Z.abs b) with b by lia.
      assert (a mod b a) by (apply Z.mod_le; lia).
      lia.
    }
  }
Qed.

Bounds of the [ediv] operator when used for the [IEdiv_tez] instruction.
Bounds of the [ediv] operator when used for the [IEdiv_int] instruction.
Lemma ediv_int_is_valid (a b : Z.t) :
  Option.Forall
    (fun '(_, rem)n_num.Valid.t rem)
    (Script_int.ediv (Script_int.Num_tag a) (Script_int.Num_tag b)).
Proof.
  destruct (b =? 0) eqn:?.
  { replace b with 0 by lia.
    now rewrite ediv_zero.
  }
  { rewrite ediv_not_zero by lia; simpl.
    unfold n_num.Valid.t.
    unfold Zeuclid.ZEuclid.modulo.
    nia.
  }
Qed.

Bounds of the [ediv] operator when used for the [IEdiv_nat] instruction. Not sure if the name of this lemma is right.
Lemma ediv_n_num_is_valid (a b : Z.t) :
  0 a
  0 b
  Option.Forall
    (fun '(quo, rem)n_num.Valid.t quo
      n_num.Valid.t rem)
    (Script_int.ediv (Script_int.Num_tag a) (Script_int.Num_tag b)).
Proof.
  intros.
  destruct (b =? 0) eqn:?.
  { replace b with 0 by lia.
    now rewrite ediv_zero.
  }
  { rewrite ediv_not_zero by lia; simpl.
    unfold n_num.Valid.t.
    unfold Zeuclid.ZEuclid.div, Zeuclid.ZEuclid.modulo.
    nia.
  }
Qed.

If [x_value] is non-negative, then [is_nat] returns [Some x_value].
Lemma is_nat_non_negative x_value : repr.Valid.non_negative x_value
   Script_int.is_nat (Script_int.Num_tag x_value) =
    Some (Script_int.Num_tag x_value).
Proof.
  intros H. unfold repr.Valid.non_negative in H.
  unfold Script_int.is_nat.
  destruct (_ <Z _) eqn:eq_b ; [lia | reflexivity].
Qed.

[is_nat_inversion] allows backward reasoning on the output of [is_nat].
Lemma is_nat_inversion x_value :
  match (Script_int.is_nat (Script_int.Num_tag x_value)) with
  | None¬repr.Valid.non_negative x_value
  | Some (Script_int.Num_tag x_value0) ⇒
      x_value0 = x_value repr.Valid.non_negative x_value
  end.
Proof.
  unfold Script_int.is_nat.
  destruct (x_value <Z Z.zero) eqn:eq_b.
  { intro H. unfold repr.Valid.non_negative in H. lia. }
  { repeat split. lia. }
Qed.

Lemma z_encoding_is_valid :
  Data_encoding.Valid.t (fun _True) Script_int.z_encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve z_encoding_is_valid : Data_encoding_db.

Lemma n_encoding_is_valid :
  Data_encoding.Valid.t n_num.Valid.t Script_int.n_encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve n_encoding_is_valid : Data_encoding_db.