https://gitlab.com/nomadic-labs/mi-cho-coq
Tip revision: 416793b544257750fdc08474933a5c139fe3e056 authored by Yann Regis-Gianas on 08 March 2021, 10:11:49 UTC
Dexter2/Spec: Take care of division by zero
Dexter2/Spec: Take care of division by zero
Tip revision: 416793b
dexter_spec_util.v
(* Open Source License *)
(* Copyright (c) 2021 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. *)
(* Coq *)
Require Import NArith.
Require Import ZArith.
Require Import Coq.micromega.Lia.
(* Mi-Cho-Coq *)
Require Import semantics.
Import syntax.
Import comparable.
Require Import util.
Import error.
(* Contracts *)
Require Import contract_semantics.
(* Dexter *)
Require Import dexter_spec.
Require Import dexter_util.
Module Tactics.
Ltac auto_fuel :=
repeat match goal with
| [ |- context G[eval_precond] ]
=> more_fuel; simpl
end.
Tactic Notation "step" integer(k) reference(contract) :=
do k (more_fuel ;
cbn beta delta [
eval_precond_opcode
eval_seq_precond_body eval_seq_precond_body_aux
eval_precond eval_precond_body contract ] iota zeta);
simpl stack_split;
simpl stack_app;
cbn iota beta.
(* TODO: Arvid: This tactic, and its usage could be omitted if the
appropriate mutez definitions and operations are rendered
Opaque *)
Ltac fold_mutez_goal :=
match goal with
| [ |- context[(exist (A := Vector.t _ _) ?P ?bv ?Hpbv)] ] =>
match bv with
(Vector.cons ?T ?f ?len ?l) =>
let z := eval cbn in (int64bv.to_Z bv) in
replace (exist P bv Hpbv)
with (exist P (int64bv.of_Z_safe z eq_refl) Hpbv)
by reflexivity
end
end.
Ltac N_add_comm y :=
match goal with
[ |- context[(?x + y)%N]] =>
replace (x + y)%N with (y + x)%N
by apply N.add_comm
end.
Ltac ex_and_comm_intro x :=
repeat rewrite ex_and_comm;
apply forall_ex; intro x.
(** Dexter specification-specific tactics *)
Hint Unfold
dexter_spec.nat_to_mutez
dexter_spec.mutez_to_nat
dexter_spec.mutez_sub
dexter_spec.env_sender : spec.
Ltac unfold_spec :=
autounfold with spec.
End Tactics.
(*! Lemmas on specification !*)
Lemma comparison_to_int_spec_cmp_eqb :
forall a x y,
dexter_spec.cmp_eqb x y =
(comparison_to_int (compare a x y) =? 0)%Z.
Proof.
intros a x y. unfold dexter_spec.cmp_eqb. now destruct (compare _ _ _).
Qed.
Lemma comparison_to_int_compare_spec_cmp_leb_tez x y :
@dexter_spec.cmp_leb mutez x y <->
(comparison_to_int (tez.compare y x) >=? 0)%Z = true.
Proof.
change tez.compare with (compare mutez).
unfold dexter_spec.cmp_leb.
destruct (compare mutez x y) eqn:eq.
1: rewrite compare_eq_comm in eq.
2: rewrite compare_gt_lt in eq.
3: rewrite <- compare_gt_lt in eq.
all: rewrite eq; unfold Z.geb; simpl; intuition; auto.
Qed.
Lemma comparison_to_int_compare_spec_cmp_geb_nat :
forall a b,
(@dexter_spec.cmp_geb nat a b) =
(comparison_to_int (compare int (Z.of_N a - Z.of_N b) 0) >=? 0)%Z.
Proof.
intros a b.
unfold dexter_spec.cmp_geb.
rewrite comparison_to_int_compare_int_geb.
rewrite Z.geb_leb.
destruct (compare_nat_compare_spec a b); symmetry;
destruct (Z.leb_spec0 0%Z (Z.of_N a - Z.of_N b)); try congruence; try lia.
Qed.
Lemma mutez_add_correct:
forall (x y z : tez.mutez),
tez.of_Z (tez.to_Z y + tez.to_Z x) = Return z <->
dexter_spec.mutez_add x y z.
Proof. intros x y. now rewrite Z.add_comm. Qed.
Lemma check_deadline_correct :
forall env deadline,
(comparison_to_int (now env ?= deadline) <? 0)%Z = true <->
dexter_spec.check_deadline env deadline.
Proof.
intros env deadline.
unfold dexter_spec.check_deadline, dexter_spec.cmp_ltb. simpl.
destruct (_ ?= _)%Z; cbv; intuition.
Qed.
(*! Spec_NCeiling !*)
Lemma Spec_Nceiling_mod :
forall (x y : N),
(Z.of_N (x mod y) =? 0)%Z = true ->
dexter_spec.Nceiling x y = (x / y)%N.
Proof.
intros x y H.
apply Z_mod_to_N_mod in H.
unfold dexter_spec.Nceiling.
rewrite surjective_pairing with (p := N.div_eucl _ _).
unfold N.modulo in H.
now rewrite H.
Qed.
Lemma Spec_Nceiling_rem :
forall (x y : N),
(Z.of_N (x mod y) =? 0)%Z = false ->
dexter_spec.Nceiling x y = (x / y + 1)%N.
Proof.
intros x y H.
generalize (Z_mod_to_N_mod x y); intro Hconv.
apply not_iff_compat in Hconv.
unfold dexter_spec.Nceiling.
rewrite surjective_pairing with (p := N.div_eucl _ _).
unfold N.modulo in H.
destruct (snd _) eqn:Heqn; intuition.
Qed.