🍬 Script_int.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Script_int.
Require TezosOfOCaml.Environment.V8.Proofs.Compare.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Proto_alpha.Proofs.Tez_repr.
#[global] Hint Unfold
Script_int.zero
Script_int.zero_n
Script_int.one_n
Script_int.of_int
Script_int.of_int32
Script_int.of_int64
Script_int.of_zint
Script_int.to_int
Script_int.to_int64
Script_int.to_zint
Script_int.add
Script_int.sub
Script_int.mul
Script_int.ediv
Script_int.add_n
Script_int.succ_n
Script_int.mul_n
Script_int.ediv_n
Script_int.abs
Script_int.neg
Script_int.int_value
: tezos_z.
Module repr.
Module Valid.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Script_int.
Require TezosOfOCaml.Environment.V8.Proofs.Compare.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Proto_alpha.Proofs.Tez_repr.
#[global] Hint Unfold
Script_int.zero
Script_int.zero_n
Script_int.one_n
Script_int.of_int
Script_int.of_int32
Script_int.of_int64
Script_int.of_zint
Script_int.to_int
Script_int.to_int64
Script_int.to_zint
Script_int.add
Script_int.sub
Script_int.mul
Script_int.ediv
Script_int.add_n
Script_int.succ_n
Script_int.mul_n
Script_int.ediv_n
Script_int.abs
Script_int.neg
Script_int.int_value
: tezos_z.
Module repr.
Module Valid.
Non-negativity predicate for [repr].
Definition non_negative (repr : Script_int.repr) : Prop :=
0 ≤ repr.
#[global] Hint Unfold non_negative : tezos_z.
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.
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.
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.
(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.]
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.
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.
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.
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.
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.
Lemma to_int64_is_valid (z : Script_int.num) :
Option.Forall Int64.Valid.t (Script_int.to_int64 z).
Proof.
Option.Forall Int64.Valid.t (Script_int.to_int64 z).
Proof.
@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.
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.
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.
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.
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.
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.
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.
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.
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.
Lemma ediv_tez_is_valid (a b : Z.t) :
Tez_repr.Repr.Valid.t a →
Tez_repr.Repr.Valid.t 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.
apply ediv_teznat_is_valid; lia.
Qed.
Tez_repr.Repr.Valid.t a →
Tez_repr.Repr.Valid.t 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.
apply ediv_teznat_is_valid; lia.
Qed.
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.
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.
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.
→ 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.
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.