https://gitlab.com/nomadic-labs/mi-cho-coq
Tip revision: 94c4e4dc7061a23ce6a19c07b1012960ef0ea4a7 authored by Guillaume Claret on 08 March 2021, 20:16:48 UTC
Dexter2/Proof: prove tokenToToken
Dexter2/Proof: prove tokenToToken
Tip revision: 94c4e4d
int64bv.v
(* Open Source License *)
(* Copyright (c) 2019 Nomadic Labs. <contact@nomadic-labs.com> *)
(* Permission is hereby granted, free of charge, to any person obtaining a *)
(* copy of this software and associated documentation files (the "Software"), *)
(* to deal in the Software without restriction, including without limitation *)
(* the rights to use, copy, modify, merge, publish, distribute, sublicense, *)
(* and/or sell copies of the Software, and to permit persons to whom the *)
(* Software is furnished to do so, subject to the following conditions: *)
(* The above copyright notice and this permission notice shall be included *)
(* in all copies or substantial portions of the Software. *)
(* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR *)
(* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, *)
(* FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL *)
(* THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER *)
(* LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING *)
(* FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER *)
(* DEALINGS IN THE SOFTWARE. *)
(* Signed 64-bits integers: these are used to represent Tez amounts *)
Require Import Bvector.
Require Import ZArith.
Require Import Zdigits.
Require Import Lia.
Require error.
Definition int64 := Bvector 64.
Definition sign : int64 -> bool := Bsign 63.
Definition to_Z : int64 -> Z := two_compl_value 63.
Lemma to_Z_lower_bound : forall b : int64, (- two_power_nat 63 <= to_Z b)%Z.
Proof.
unfold int64, to_Z.
generalize 63.
intros n b.
refine (@VectorDef.caseS
_
(fun n b => - two_power_nat n <= two_compl_value n b)%Z
_ n b).
clear n b.
intros b n t.
simpl.
generalize b; clear b.
induction t.
+ simpl.
unfold eq_rec_r.
simpl.
intro b; destruct b; simpl; omega.
+ simpl two_compl_value.
unfold eq_rec_r.
simpl.
specialize (IHt h).
generalize IHt; clear IHt.
destruct (two_compl_value n (h :: t)).
* destruct b; simpl; nia.
* destruct b; simpl; nia.
* generalize (shift_nat n 1); intro p0; simpl.
destruct b; simpl; try nia.
apply Pos2Z.neg_le_neg.
unfold "<="%Z in IHt.
unfold "?="%Z in IHt.
rewrite <- Pos.compare_antisym in IHt.
change (p <= p0)%positive in IHt.
transitivity (p~0)%positive.
-- rewrite <- Pos.succ_pred_double.
lia.
-- nia.
Qed.
Lemma unsigned_to_Z_lower_bound : forall b : int64, sign b = false -> (0 <= to_Z b)%Z.
Proof.
unfold int64, to_Z.
unfold sign.
generalize 63.
intros n b.
refine (@VectorDef.caseS
_
(fun n b => Bsign n b = false-> 0 <= two_compl_value n b)%Z
_ n b).
clear n b.
intros b n t.
generalize b; clear b.
induction t.
+ simpl.
unfold eq_rec_r.
simpl.
intros []; simpl; intuition discriminate.
+ assert (forall n b t, Bsign (S n) (b :: t) = Bsign n t)
as HsignS
by reflexivity.
intro b. rewrite HsignS. clear HsignS. intro Hsign.
simpl two_compl_value.
unfold eq_rec_r.
simpl.
specialize (IHt h Hsign).
destruct (two_compl_value n (h :: t)).
* destruct b; simpl; lia.
* destruct b; simpl; lia.
* lia.
Qed.
Lemma to_Z_upper_bound : forall b : int64, (to_Z b < two_power_nat 63)%Z.
unfold int64, to_Z.
generalize 63.
intros n b.
refine (@VectorDef.caseS
_
(fun n b => two_compl_value n b < two_power_nat n)%Z
_ n b).
clear n b.
intros b n t.
generalize b; clear b.
induction t.
+ unfold two_power_nat.
simpl.
unfold eq_rec_r.
simpl.
intro b; destruct b; simpl; omega.
+ simpl two_compl_value.
unfold eq_rec_r.
simpl.
specialize (IHt h).
generalize IHt; clear IHt.
unfold two_power_nat.
destruct (two_compl_value n (h :: t)).
* destruct b; simpl; nia.
* destruct b; simpl; nia.
* generalize (shift_nat n 1); intro p0; simpl.
destruct b; simpl; nia.
Qed.
Definition of_Z_unsafe : Z -> int64 := Z_to_two_compl 63.
Definition of_Z_safe (z : Z) :
((z >=? - two_power_nat 63) && (z <? two_power_nat 63))%Z = true -> int64 :=
fun _ => of_Z_unsafe z.
Definition of_Z (z : Z) : error.M int64 :=
if ((z >=? - two_power_nat 63) && (z <? two_power_nat 63))%bool%Z
then
error.Return (of_Z_unsafe z)
else
error.Failed _ error.Overflow.
Lemma of_Z_safe_is_of_Z z H : of_Z z = error.Return (of_Z_safe z H).
Proof.
unfold of_Z, of_Z_safe.
rewrite H.
reflexivity.
Qed.
Definition int0_inversion (b : Bvector 0) : Bnil = b :=
match b in Vector.t _ 0 return Bnil = b with
| Vector.nil _ => eq_refl
end.
Definition intn_inversion n (b : Bvector (S n)) : exists a v, b = Bcons a n v :=
match b in Vector.t _ (S _) return exists a v, b = Bcons a _ v with
| Vector.cons _ a _ v => ex_intro _ a (ex_intro _ v eq_refl)
end.
Definition int64_inversion (b : int64) : exists a v, b = Bcons a 63 v :=
intn_inversion 63 b.
Lemma of_Z_to_Z_eqv z b : to_Z b = z <-> of_Z z = error.Return b.
Proof.
unfold of_Z, to_Z.
split.
- intro; subst z.
destruct (int64_inversion b) as (a, (v, H)).
rewrite H.
unfold of_Z_unsafe.
rewrite two_compl_to_Z_to_two_compl.
rewrite <- H; clear H.
assert ((two_compl_value 63 b >=? - two_power_nat 63)%Z = true) as Hlow.
+ rewrite Z.geb_le.
apply to_Z_lower_bound.
+ rewrite Hlow; clear Hlow.
assert ((two_compl_value 63 b <? two_power_nat 63)%Z = true) as Hhigh.
* rewrite Z.ltb_lt.
apply to_Z_upper_bound.
* rewrite Hhigh; clear Hhigh.
reflexivity.
- intro H.
case_eq ((z >=? - two_power_nat 63) && (z <? two_power_nat 63))%Z.
+ intro Hcond.
rewrite Hcond in H.
apply (f_equal (fun o => match o with error.Return x => x | _ => b end)) in H.
subst b.
apply andb_prop in Hcond.
destruct Hcond as (H1, H2).
apply Z_to_two_compl_to_Z.
* apply Z.le_ge.
apply Z.geb_le.
assumption.
* apply Z.ltb_lt.
assumption.
+ intro Hcond.
rewrite Hcond in H.
discriminate.
Qed.
Lemma of_Z_to_Z b : of_Z (to_Z b) = error.Return b.
Proof.
rewrite <- of_Z_to_Z_eqv.
reflexivity.
Qed.
Lemma of_Z_of_N
(n : N)
(H : (n < 2 ^ 63)%N) :
of_Z (Z.of_N n) = error.Return (of_Z_unsafe (Z.of_N n)).
Proof.
unfold of_Z.
pose (lower_bound := (Z.of_N n >=? - two_power_nat 63)%Z).
assert (lower_bound_eq : (Z.of_N n >=? - two_power_nat 63)%Z = lower_bound) by reflexivity.
rewrite lower_bound_eq.
pose (upper_bound := (Z.of_N n <? two_power_nat 63)%Z).
assert (upper_bound_eq : (Z.of_N n <? two_power_nat 63)%Z = upper_bound) by reflexivity.
rewrite upper_bound_eq.
rewrite two_power_nat_equiv in *.
Ltac lower_bound_false lower_bound_eq :=
(
rewrite Z.geb_leb in lower_bound_eq;
apply (proj1 (Z.leb_nle _ _)) in lower_bound_eq;
refine (False_ind _ (lower_bound_eq _));
refine (Z.le_trans _ _ _
(proj2 (Z.opp_nonpos_nonneg _) (Z.pow_nonneg _ _ _))
(N2Z.is_nonneg _)
);
intuition
).
destruct lower_bound, upper_bound;
(reflexivity || lower_bound_false lower_bound_eq || idtac).
apply (proj1 (Z.ltb_nlt _ _)) in upper_bound_eq.
refine (False_ind _ (upper_bound_eq _)).
apply (proj1 (N2Z.inj_lt _ _)) in H.
assert (Z_pow_eq : Z.of_N (2 ^ 63) = (2 ^ Z.of_nat 63)%Z).
+ rewrite N2Z.inj_pow.
f_equal.
+ rewrite Z_pow_eq in H.
exact H.
Qed.
(* Returns x / (2 ^ n) where / is integer division:
see iter_Zdigits_Zmod2_div_pow2. *)
Definition iter_Zdigits_Zmod2 (n : Datatypes.nat) (x : Z) :=
nat_rec _
(fun y => y)
(fun _ f y => f (Zdigits.Zmod2 y))
n x.
(* The sign bit of the two's complement representation of x in n+1 bits
(i.e. the (n+1)th or final bit) is set iff (x / (2 ^ n)) is odd *)
Fixpoint iter_Zdigits_Zmod2_correct (n : Datatypes.nat) (x : Z) :
Bvector.Bsign _ (Zdigits.Z_to_two_compl n x) = Z.odd (iter_Zdigits_Zmod2 n x).
Proof.
destruct n.
- reflexivity.
- simpl.
rewrite (iter_Zdigits_Zmod2_correct n _).
reflexivity.
Qed.
Fixpoint iter_Zdigits_Zmod2_upper_bound (n m : Datatypes.nat) (z : Z)
(H : (z < two_power_nat (n + m))%Z) :
(iter_Zdigits_Zmod2 n z < two_power_nat m)%Z.
Proof.
destruct n.
- assumption.
- exact (iter_Zdigits_Zmod2_upper_bound n m
(Zdigits.Zmod2 z)
(Zdigits.Zlt_two_power_nat_S _ _ H)
).
Qed.
Lemma Zdigits_bit_value_bounds (b : Datatypes.bool) :
(0 <= Zdigits.bit_value b <= 1)%Z.
Proof.
destruct b; simpl; split; lia.
Qed.
Lemma Zmod2_nonneg (z : Z) :
(0 <= z)%Z <-> (0 <= Zdigits.Zmod2 z)%Z.
Proof.
pose (Zdigits_bit_value_bounds (Z.odd z)).
split; intro H.
- rewrite (Zdigits.Zmod2_twice z) in H; lia.
- rewrite (Zdigits.Zmod2_twice z); lia.
Qed.
Fixpoint iter_Zdigits_Zmod2_nonneg (n : Datatypes.nat) (z : Z) :
forall (H : (0 <= z)%Z),
(0 <= iter_Zdigits_Zmod2 n z)%Z.
Proof.
intro H.
destruct n.
- assumption.
- simpl in H |- *.
exact (iter_Zdigits_Zmod2_nonneg n
(Zdigits.Zmod2 z)
(proj1 (Zmod2_nonneg _) H)
).
Qed.
Lemma odd_iter_Zdigits_Zmod2
(n : Datatypes.nat) (z : Z)
(lb : (0 <= z)%Z)
(ub : (z < two_power_nat n)%Z) :
Z.odd (iter_Zdigits_Zmod2 n z) = false.
Proof.
pose (H_nonneg := iter_Zdigits_Zmod2_nonneg n _ lb).
rewrite <- (Nat.add_0_r n) in ub.
pose (H_nonpos := iter_Zdigits_Zmod2_upper_bound n 0%nat z ub).
pose (z' := iter_Zdigits_Zmod2 n z).
assert (z_eq' : z' = iter_Zdigits_Zmod2 n z) by reflexivity.
rewrite <- z_eq' in *.
destruct z'.
- auto.
- destruct (Zlt_not_le _ _ (Pos2Z.pos_is_pos _) (Zlt_succ_le _ 0%Z H_nonpos)).
- destruct (Zlt_not_le _ _ (Pos2Z.neg_is_neg _) H_nonneg).
Qed.
Lemma sign_of_Z_of_N (n : N) (H : (n < 2 ^ 63)%N) :
Bool.Is_true (negb (sign (of_Z_unsafe (Z.of_N n)))).
Proof.
unfold sign.
unfold of_Z_unsafe.
rewrite iter_Zdigits_Zmod2_correct.
refine (error.IT_eq_rev _ _).
refine (proj2 (Bool.negb_true_iff _) _).
refine (odd_iter_Zdigits_Zmod2 _ (Z.of_N n) _ _).
- exact (N2Z.is_nonneg _).
- assert (H_pow_2_63 : two_power_nat 63 = Z.of_N (2 ^ 63)%N).
+ rewrite two_power_nat_equiv.
rewrite N2Z.inj_pow.
f_equal.
+ rewrite H_pow_2_63.
refine (proj1 (N2Z.inj_lt _ _) _).
assumption.
Qed.
Definition compare (a b : int64) : comparison :=
Z.compare (to_Z a) (to_Z b).
(* To avoid a name clash in OCaml extracted code. *)
Definition int64_compare (a b : int64) : comparison := compare a b.
Lemma compare_eq_iff (a b : int64) : compare a b = Eq <-> a = b.
Proof.
unfold compare.
rewrite Z.compare_eq_iff.
split.
- intro H.
apply (f_equal of_Z) in H.
rewrite of_Z_to_Z in H.
rewrite of_Z_to_Z in H.
injection H.
auto.
- apply f_equal.
Qed.
Lemma Pos_pred_double_spec :
forall p,
Pos.pred_double p = (Pos.sub (Pos.mul 2 p) 1).
Proof. destruct p; simpl; reflexivity. Qed.
Lemma Pos_pred_double_inj :
forall p p',
Pos.pred_double p = Pos.pred_double p' ->
p = p'.
Proof.
intros p p' H.
repeat rewrite Pos_pred_double_spec in H.
lia.
Qed.
Lemma digits_neg_inj :
forall a b p p',
(bit_value b + Z.neg p~0)%Z = (bit_value a + Z.neg p'~0)%Z ->
a = b /\ p = p'.
Proof.
intros a b p p' H.
destruct a, b; simpl in H; inversion H.
- apply Pos_pred_double_inj in H1. intuition.
- destruct p'; inversion H1.
- destruct p; inversion H1.
- intuition.
Qed.
Lemma digits_pos_inj :
forall a b p p',
(bit_value b + Z.pos p~0)%Z = (bit_value a + Z.pos p'~0)%Z ->
a = b /\ p = p'.
Proof.
intros a b p p' H.
destruct a, b; simpl in H; inversion H; intuition congruence.
Qed.
Lemma bit_value_inj : forall b b', bit_value b = bit_value b' -> b = b'.
Proof. intros b b'. destruct b, b'; simpl; intuition; discriminate. Qed.
Lemma to_Z_inj :
forall b b',
int64bv.to_Z b = int64bv.to_Z b' ->
b = b'.
Proof.
unfold int64, to_Z.
generalize 63.
intros n b.
refine (@VectorDef.caseS
_
(fun n b =>
forall b',
two_compl_value n b = two_compl_value n b' -> b = b')%Z
_ n b).
clear n b.
intros b n t.
generalize b; clear b.
induction t.
+ intros b b' H.
destruct (intn_inversion 0 b') as (a, (v, H')).
subst b'.
generalize H.
simpl.
unfold eq_rec_r. simpl.
intros H'.
apply Z.opp_inj in H'.
apply bit_value_inj in H'.
subst b.
now replace v with Bnil by apply int0_inversion.
+ simpl two_compl_value.
unfold eq_rec_r.
intros b b'.
destruct (intn_inversion (S n) b') as (a, (t', H')).
rewrite H'. simpl.
intro Heq. unfold Bcons.
specialize (IHt h t').
destruct (two_compl_value n (h :: t)) eqn:H2c1;
destruct (two_compl_value n t') eqn:H2c2;
(try (destruct a, b; simpl in Heq; lia)).
* repeat rewrite Z.add_0_r in Heq.
apply bit_value_inj in Heq. subst a.
f_equal.
now apply IHt.
* apply digits_pos_inj in Heq as [Hab Hpp0]. subst.
f_equal.
now apply IHt.
* apply digits_neg_inj in Heq as [Hab Hpp0]. subst.
f_equal.
now apply IHt.
Qed.