🎰 Slot_repr.v
Proofs
See code, See simulations, Gitlab , OCaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Proto_alpha.Proofs.Error.
Require TezosOfOCaml.Proto_alpha.Slot_repr.
Require TezosOfOCaml.Proto_alpha.Simulations.Slot_repr.
Module Valid.
Definition t (s : Slot_repr.t) : Prop :=
0 ≤ s ≤ Pervasives.UInt16.max.
#[global] Hint Unfold t : tezos_z.
End Valid.
Lemma encoding_is_valid : Data_encoding.Valid.t Valid.t Slot_repr.encoding.
Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
Lemma zero_is_valid : Valid.t Slot_repr.zero.
easy.
Qed.
Lemma max_value_is_valid : Valid.t Slot_repr.max_value.
easy.
Qed.
Lemma max_value_eq : Slot_repr.max_value = Pervasives.UInt16.max.
reflexivity.
Qed.
Lemma of_int_eq : ∀ i,
Valid.t i →
Slot_repr.of_int i = return? i.
unfold Slot_repr.of_int.
rewrite max_value_eq.
autounfold with tezos_z.
intros.
destruct (_ || _) eqn:?; [| reflexivity ].
rewrite Bool.orb_true_iff in ×.
hauto q: on solve: lia.
Qed.
Lemma succ_is_valid : ∀ s,
Valid.t s →
s ≠ Pervasives.UInt16.max →
match Slot_repr.succ s with
| Pervasives.Ok s ⇒ Valid.t s
| Pervasives.Error _ ⇒ True
end.
intros; unfold Slot_repr.succ.
assert (Valid.t (s +i 1)) by
(repeat (autounfold with tezos_z in *; unfold normalize_int);
lia).
now rewrite of_int_eq.
Qed.
Module Range.
Module Interval.
Import Slot_repr.Range.t.Interval.
Record t (v : Slot_repr.Range.t.Interval) : Prop := {
lo : Slot_repr.Valid.t v.(lo);
hi : Slot_repr.Valid.t v.(hi);
}.
End Interval.
Module Valid.
Definition t (v : Slot_repr.Range.t) : Prop :=
match v with
| Slot_repr.Range.Interval i ⇒ Interval.t i
end.
End Valid.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Proto_alpha.Proofs.Error.
Require TezosOfOCaml.Proto_alpha.Slot_repr.
Require TezosOfOCaml.Proto_alpha.Simulations.Slot_repr.
Module Valid.
Definition t (s : Slot_repr.t) : Prop :=
0 ≤ s ≤ Pervasives.UInt16.max.
#[global] Hint Unfold t : tezos_z.
End Valid.
Lemma encoding_is_valid : Data_encoding.Valid.t Valid.t Slot_repr.encoding.
Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
Lemma zero_is_valid : Valid.t Slot_repr.zero.
easy.
Qed.
Lemma max_value_is_valid : Valid.t Slot_repr.max_value.
easy.
Qed.
Lemma max_value_eq : Slot_repr.max_value = Pervasives.UInt16.max.
reflexivity.
Qed.
Lemma of_int_eq : ∀ i,
Valid.t i →
Slot_repr.of_int i = return? i.
unfold Slot_repr.of_int.
rewrite max_value_eq.
autounfold with tezos_z.
intros.
destruct (_ || _) eqn:?; [| reflexivity ].
rewrite Bool.orb_true_iff in ×.
hauto q: on solve: lia.
Qed.
Lemma succ_is_valid : ∀ s,
Valid.t s →
s ≠ Pervasives.UInt16.max →
match Slot_repr.succ s with
| Pervasives.Ok s ⇒ Valid.t s
| Pervasives.Error _ ⇒ True
end.
intros; unfold Slot_repr.succ.
assert (Valid.t (s +i 1)) by
(repeat (autounfold with tezos_z in *; unfold normalize_int);
lia).
now rewrite of_int_eq.
Qed.
Module Range.
Module Interval.
Import Slot_repr.Range.t.Interval.
Record t (v : Slot_repr.Range.t.Interval) : Prop := {
lo : Slot_repr.Valid.t v.(lo);
hi : Slot_repr.Valid.t v.(hi);
}.
End Interval.
Module Valid.
Definition t (v : Slot_repr.Range.t) : Prop :=
match v with
| Slot_repr.Range.Interval i ⇒ Interval.t i
end.
End Valid.
[Proto_alpha.Slot_repr.Simulations.Range.fold_es] has the same behaviour
as [Proto_alpha.Slot_repr.Range.fold_es].
We need bypass_check(guard) here because Coq Guard does not accept a way
in which the original function is defined. But to go by induction we need
apply original function to it's arguments.
#[bypass_check(guard)]
Lemma fold_es_eq {A B : Set} f (acc : A) (fuel : nat) (hi lo : int) :
(fuel = Z.to_nat (hi - lo))%nat →
let range := Slot_repr.Range.Interval {|
Slot_repr.Range.t.Interval.lo := lo;
Slot_repr.Range.t.Interval.hi := hi
|} in
Valid.t range →
Proto_alpha.Slot_repr.Range.fold_es (B := B) f acc range
=
Simulations.Slot_repr.Range.fold_es
f acc (Z.to_nat hi) (Z.to_nat lo) fuel.
Proof.
intros Hfuel range Hv;
unfold
Proto_alpha.Slot_repr.Range.fold_es,
Slot_repr.Range.fold_es.
subst range; simpl.
rewrite ZifyInst.of_nat_to_nat_eq.
destruct Hv as [Hvlo Hvhi]; simpl in ×.
rewrite Z.max_r by lia.
step; [|reflexivity]; simpl.
unfold ">i", "+i"; simpl.
rewrite Pervasives.normalize_identity by lia.
remember (lo + 1)%Z as step_init eqn:Heqstep_init.
(* First, we need remove case hi = lo *)
match goal with
| |- ?f1 _ _ = ?f2 _ _ ⇒
remember f1 as loop_orig eqn:Elpo;
remember f2 as loop_sim eqn:Elps
end.
destruct fuel eqn:Efuel.
{ (* Efuel : fuel = 0%nat *)
destruct (Z.le_ge_cases hi lo) as [Hle | Hle].
{ (* hi <= lo *)
destruct step_init; [lia| |lia].
rewrite Elpo, Elps.
assert(H : Z.pos p >? hi = true) by lia.
rewrite H; reflexivity.
}
(* lo <= hi *)
assert(H_step_init : step_init = (hi + 1)%Z) by lia.
rewrite H_step_init.
assert (H : hi = lo) by lia.
rewrite Elpo, Elps.
destruct lo eqn:Elo; [..|exfalso; lia];
simpl BinInt.Z.add; cbv fix beta.
{ rewrite H; reflexivity. }
rewrite H.
assert (H0 : Z.pos (p + 1) > Z.pos p) by lia.
assert (H1 : ((Z.pos p + 1) = Z.pos (p + 1))%Z) by lia.
rewrite H1.
apply Zgt_is_gt_bool in H0; rewrite H0; reflexivity.
}
(* Efuel : fuel = Datatypes.S n *)
destruct hi; [..|destruct Hvhi; exfalso; lia].
{ (* Ehi : hi = 0 *)
destruct lo eqn:Elo; [..|destruct Hvlo; exfalso; lia];
simpl in Hfuel; discriminate.
}
assert(Hlt : lo < Z.pos p) by lia.
assert(H_step_init
: step_init = (Z.pos p - Z.of_nat (Datatypes.S n) + 1)%Z)
by lia.
rewrite H_step_init.
clear Efuel Hfuel fuel Heqr acc.
assert(Hn : (n ≤ Z.to_nat (Z.pos p - lo - 1))%nat) by lia.
remember (Datatypes.S n) as fuel eqn:Heqfuel.
rewrite Elpo, Elps.
assert(Hfuel : (fuel ≤ Z.to_nat (Z.pos p - lo))%nat) by lia.
clear
Heqstep_init H_step_init step_init Heqfuel
Hn n loop_orig Elpo loop_sim Elps.
(* Recursion, finally! *)
revert a; generalize dependent fuel.
fix IHloop 1.
intros fuel Hn a.
destruct fuel as [|n].
{ (* fuel = Datatypes.O *)
simpl.
assert(H0 : (Z.pos (p + 1) > Z.pos p)%Z) by lia.
apply Zgt_is_gt_bool in H0; rewrite H0; reflexivity.
}
(* fuel = Datatypes.S n *)
assert(Hzpos
: (Z.of_nat (Pos.to_nat p - Datatypes.S n) + 1)%Z ≤ Z.pos p)
by lia.
apply Z.ltb_ge in Hzpos.
remember (Z.pos p - Z.of_nat (Datatypes.S n) + 1)%Z
as acc1 eqn:Heqacc1.
assert(Hacc1 : acc1 > 0) by lia.
destruct acc1 as [|acc1|]; [exfalso; lia| |exfalso; lia].
assert(H_acc1_p : Z.pos acc1 >? Z.pos p = false) by lia.
assert (H_acc1_pn : Z.pos acc1 = Z.of_nat (Z.to_nat (Z.pos p) - n))
by lia.
rewrite <- H_acc1_pn, H_acc1_p.
clear H_acc1_p H_acc1_pn Hacc1.
destruct (f a) eqn:Efa; [|reflexivity]; simpl.
assert(Hacceq
: (Z.pos (acc1 + 1)) = (Z.pos p - Z.of_nat n + 1)%Z) by lia.
rewrite Hacceq, Pervasives.normalize_identity by lia.
apply IHloop; lia.
Qed.
Lemma fold_es_eq {A B : Set} f (acc : A) (fuel : nat) (hi lo : int) :
(fuel = Z.to_nat (hi - lo))%nat →
let range := Slot_repr.Range.Interval {|
Slot_repr.Range.t.Interval.lo := lo;
Slot_repr.Range.t.Interval.hi := hi
|} in
Valid.t range →
Proto_alpha.Slot_repr.Range.fold_es (B := B) f acc range
=
Simulations.Slot_repr.Range.fold_es
f acc (Z.to_nat hi) (Z.to_nat lo) fuel.
Proof.
intros Hfuel range Hv;
unfold
Proto_alpha.Slot_repr.Range.fold_es,
Slot_repr.Range.fold_es.
subst range; simpl.
rewrite ZifyInst.of_nat_to_nat_eq.
destruct Hv as [Hvlo Hvhi]; simpl in ×.
rewrite Z.max_r by lia.
step; [|reflexivity]; simpl.
unfold ">i", "+i"; simpl.
rewrite Pervasives.normalize_identity by lia.
remember (lo + 1)%Z as step_init eqn:Heqstep_init.
(* First, we need remove case hi = lo *)
match goal with
| |- ?f1 _ _ = ?f2 _ _ ⇒
remember f1 as loop_orig eqn:Elpo;
remember f2 as loop_sim eqn:Elps
end.
destruct fuel eqn:Efuel.
{ (* Efuel : fuel = 0%nat *)
destruct (Z.le_ge_cases hi lo) as [Hle | Hle].
{ (* hi <= lo *)
destruct step_init; [lia| |lia].
rewrite Elpo, Elps.
assert(H : Z.pos p >? hi = true) by lia.
rewrite H; reflexivity.
}
(* lo <= hi *)
assert(H_step_init : step_init = (hi + 1)%Z) by lia.
rewrite H_step_init.
assert (H : hi = lo) by lia.
rewrite Elpo, Elps.
destruct lo eqn:Elo; [..|exfalso; lia];
simpl BinInt.Z.add; cbv fix beta.
{ rewrite H; reflexivity. }
rewrite H.
assert (H0 : Z.pos (p + 1) > Z.pos p) by lia.
assert (H1 : ((Z.pos p + 1) = Z.pos (p + 1))%Z) by lia.
rewrite H1.
apply Zgt_is_gt_bool in H0; rewrite H0; reflexivity.
}
(* Efuel : fuel = Datatypes.S n *)
destruct hi; [..|destruct Hvhi; exfalso; lia].
{ (* Ehi : hi = 0 *)
destruct lo eqn:Elo; [..|destruct Hvlo; exfalso; lia];
simpl in Hfuel; discriminate.
}
assert(Hlt : lo < Z.pos p) by lia.
assert(H_step_init
: step_init = (Z.pos p - Z.of_nat (Datatypes.S n) + 1)%Z)
by lia.
rewrite H_step_init.
clear Efuel Hfuel fuel Heqr acc.
assert(Hn : (n ≤ Z.to_nat (Z.pos p - lo - 1))%nat) by lia.
remember (Datatypes.S n) as fuel eqn:Heqfuel.
rewrite Elpo, Elps.
assert(Hfuel : (fuel ≤ Z.to_nat (Z.pos p - lo))%nat) by lia.
clear
Heqstep_init H_step_init step_init Heqfuel
Hn n loop_orig Elpo loop_sim Elps.
(* Recursion, finally! *)
revert a; generalize dependent fuel.
fix IHloop 1.
intros fuel Hn a.
destruct fuel as [|n].
{ (* fuel = Datatypes.O *)
simpl.
assert(H0 : (Z.pos (p + 1) > Z.pos p)%Z) by lia.
apply Zgt_is_gt_bool in H0; rewrite H0; reflexivity.
}
(* fuel = Datatypes.S n *)
assert(Hzpos
: (Z.of_nat (Pos.to_nat p - Datatypes.S n) + 1)%Z ≤ Z.pos p)
by lia.
apply Z.ltb_ge in Hzpos.
remember (Z.pos p - Z.of_nat (Datatypes.S n) + 1)%Z
as acc1 eqn:Heqacc1.
assert(Hacc1 : acc1 > 0) by lia.
destruct acc1 as [|acc1|]; [exfalso; lia| |exfalso; lia].
assert(H_acc1_p : Z.pos acc1 >? Z.pos p = false) by lia.
assert (H_acc1_pn : Z.pos acc1 = Z.of_nat (Z.to_nat (Z.pos p) - n))
by lia.
rewrite <- H_acc1_pn, H_acc1_p.
clear H_acc1_p H_acc1_pn Hacc1.
destruct (f a) eqn:Efa; [|reflexivity]; simpl.
assert(Hacceq
: (Z.pos (acc1 + 1)) = (Z.pos p - Z.of_nat n + 1)%Z) by lia.
rewrite Hacceq, Pervasives.normalize_identity by lia.
apply IHloop; lia.
Qed.
[Proto_alpha.Simulation.Slot_repr.fold_es] is valid.
Lemma simulation_fold_es_is_valid
{A : Set} f (acc : A) (fuel hi lo : nat) (P : A → Prop)
: P acc →
(let range := Slot_repr.Range.Interval {|
Slot_repr.Range.t.Interval.lo := Z.of_nat lo;
Slot_repr.Range.t.Interval.hi := Z.of_nat hi
|} in
Valid.t range) →
(∀ acc num,
P acc → Slot_repr.Valid.t num → letP? a := f acc num in P a) →
(fuel = hi - lo)%nat →
letP? a := Simulations.Slot_repr.Range.fold_es f acc hi lo fuel in
P a.
Proof.
intros Pacc Hv Hf Hfuel.
unfold Slot_repr.Range.fold_es.
eapply Error.split_letP; [apply Hf; trivial; apply Hv|].
assert(Hfuel' : (fuel ≤ (hi - lo))%nat) by lia.
clear Hfuel Pacc acc.
generalize dependent fuel.
induction fuel as [|fuel]; [easy|].
intros Hfuel acc Pacc.
eapply Error.split_letP;
[apply Hf; trivial; destruct Hv as [[] []]; cbn in *; lia|].
intros acc' Pacc'.
apply IHfuel; lia.
Qed.
{A : Set} f (acc : A) (fuel hi lo : nat) (P : A → Prop)
: P acc →
(let range := Slot_repr.Range.Interval {|
Slot_repr.Range.t.Interval.lo := Z.of_nat lo;
Slot_repr.Range.t.Interval.hi := Z.of_nat hi
|} in
Valid.t range) →
(∀ acc num,
P acc → Slot_repr.Valid.t num → letP? a := f acc num in P a) →
(fuel = hi - lo)%nat →
letP? a := Simulations.Slot_repr.Range.fold_es f acc hi lo fuel in
P a.
Proof.
intros Pacc Hv Hf Hfuel.
unfold Slot_repr.Range.fold_es.
eapply Error.split_letP; [apply Hf; trivial; apply Hv|].
assert(Hfuel' : (fuel ≤ (hi - lo))%nat) by lia.
clear Hfuel Pacc acc.
generalize dependent fuel.
induction fuel as [|fuel]; [easy|].
intros Hfuel acc Pacc.
eapply Error.split_letP;
[apply Hf; trivial; destruct Hv as [[] []]; cbn in *; lia|].
intros acc' Pacc'.
apply IHfuel; lia.
Qed.
[Proto_alpha.Slot_repr.fold_es] is valid.
Lemma fold_es_is_valid
{A : Set} f (acc : A) (range : Slot_repr.Range.t) (P : A → Prop)
: Range.Valid.t range →
P acc →
(∀ acc num,
P acc → Slot_repr.Valid.t num → letP? a := f acc num in P a) →
letP? a := Proto_alpha.Slot_repr.Range.fold_es f acc range in P a.
Proof.
intros Hv Pacc Hf.
destruct range as [[lo hi]].
remember (Z.to_nat (hi - lo)) as fuel.
rewrite (fold_es_eq _ _ fuel); trivial.
apply simulation_fold_es_is_valid; trivial;
[rewrite !Z2Nat.id by apply Hv; trivial|].
rewrite Z2Nat.inj_sub in Heqfuel; destruct Hv; simpl in *; lia.
Qed.
{A : Set} f (acc : A) (range : Slot_repr.Range.t) (P : A → Prop)
: Range.Valid.t range →
P acc →
(∀ acc num,
P acc → Slot_repr.Valid.t num → letP? a := f acc num in P a) →
letP? a := Proto_alpha.Slot_repr.Range.fold_es f acc range in P a.
Proof.
intros Hv Pacc Hf.
destruct range as [[lo hi]].
remember (Z.to_nat (hi - lo)) as fuel.
rewrite (fold_es_eq _ _ fuel); trivial.
apply simulation_fold_es_is_valid; trivial;
[rewrite !Z2Nat.id by apply Hv; trivial|].
rewrite Z2Nat.inj_sub in Heqfuel; destruct Hv; simpl in *; lia.
Qed.
[Proto_alpha.Slot_repr.Simulations.Range.rev_fold_es] has the same
behaviour as [Proto_alpha.Slot_repr.Range.rev_fold_es].
We need bypass_check(guard) here because Coq Guard does not accept a way
in which the original function is defined. But to go by induction we need
apply original function to it's arguments.
#[bypass_check(guard)]
Lemma rev_fold_es_eq {A B : Set} f (acc : A) (fuel : nat) (hi lo : int) :
(fuel = Z.to_nat (hi - lo))%nat →
let range := Slot_repr.Range.Interval {|
Slot_repr.Range.t.Interval.lo := lo;
Slot_repr.Range.t.Interval.hi := hi
|} in
Valid.t range →
Proto_alpha.Slot_repr.Range.rev_fold_es (B := B) f acc range
=
Simulations.Slot_repr.Range.rev_fold_es
f acc (Z.to_nat hi) (Z.to_nat lo) fuel.
Proof.
intros Hfuel range Hv;
unfold
Proto_alpha.Slot_repr.Range.rev_fold_es,
Slot_repr.Range.rev_fold_es.
subst range; simpl.
rewrite ZifyInst.of_nat_to_nat_eq.
destruct Hv as [Hvlo Hvhi]; simpl in ×.
rewrite Z.max_r by lia.
step; [|reflexivity]; simpl.
unfold "<i", "-i"; simpl.
rewrite Pervasives.normalize_identity by lia.
remember (hi - 1)%Z as step_init.
(* First, we need remove case hi <= lo *)
match goal with
| |- ?f1 _ _ = ?f2 _ _ ⇒
remember f1 as loop_orig eqn:Elpo;
remember f2 as loop_sim eqn:Elps
end.
destruct fuel eqn:Efuel.
{ (* Efuel : fuel = 0%nat *)
destruct (Z.le_ge_cases hi lo) as [Hle | Hle].
{ (* hi <= lo *)
rewrite Elpo, Elps.
destruct step_init.
{ assert(H : 0 <? lo = true ) by lia.
rewrite H; reflexivity.
}
{ assert(H : Z.pos p <? lo = true ) by lia.
rewrite H; reflexivity.
}
assert(H : BinInt.Z.neg p ≥ -1 ) by lia.
assert(BinInt.Z.neg p < lo) by lia.
apply Z.ltb_lt in H0; rewrite H0; reflexivity.
}
(* lo <= hi *)
assert(H_step_init : step_init = (hi - 1)%Z) by lia.
rewrite H_step_init.
assert (H : hi = lo) by lia.
rewrite Elpo, Elps.
destruct lo eqn:Elo; [..|exfalso; lia];
simpl BinInt.Z.add; cbv fix beta.
{ rewrite H; reflexivity. }
assert(H1 : step_init ≥ 0) by lia.
rewrite <- H_step_init.
destruct step_init eqn:Esti; [..|exfalso; lia].
{ assert (H2 : 0 <? Z.pos p = true) by lia.
rewrite H2; reflexivity.
}
assert(H2 : Z.pos p0 <? Z.pos p = true) by lia.
rewrite H2; reflexivity.
}
(* Efuel : fuel = Datatypes.S n *)
destruct hi; [exfalso; lia| |destruct Hvhi; exfalso; lia].
(* hi = Z.pos *)
assert(Hlt : lo < Z.pos p) by lia.
assert(H_step_init
: step_init = (lo + Z.of_nat (Datatypes.S n) - 1)%Z)
by lia.
rewrite H_step_init.
clear Efuel Hfuel fuel Heqr acc.
assert(Hn : (n ≤ Z.to_nat (Z.pos p - lo - 1))%nat) by lia.
remember (Datatypes.S n) as fuel eqn:Heqfuel.
rewrite Elpo, Elps.
assert(Hfuel : (fuel ≤ Z.to_nat (Z.pos p - lo))%nat) by lia.
clear
Heqstep_init H_step_init step_init Heqfuel
Hn n loop_orig Elpo loop_sim Elps.
(* Recursion, finally! *)
revert a; generalize dependent fuel.
fix IHloop 1.
intros fuel Hn a.
destruct fuel as [|n].
{ (* fuel = Datatypes.O *)
simpl; rewrite Z.add_0_r.
remember (lo - 1) as step.
destruct step eqn:Estep.
{ assert(H : 0 <? lo = true) by lia.
rewrite H; reflexivity. }
{ assert(H : Z.pos p0 <? lo = true) by lia.
rewrite H; reflexivity. }
assert(H : BinInt.Z.neg p0 < lo) by lia.
apply Zlt_is_lt_bool in H; rewrite H; reflexivity.
}
(* fuel = Datatypes.S n *)
assert(H : (lo + Z.of_nat (Datatypes.S n) - 1) = (lo + Z.of_nat n)%Z)
by lia.
rewrite H; clear H.
remember (lo + Z.of_nat n)%Z as step eqn:Heqstep.
destruct step eqn:Estep; [..|exfalso; lia].
{ assert(H : 0 <? lo = false) by lia.
rewrite H; clear H.
assert(Hlo0 : lo = 0) by lia.
assert(Hn0 : n = 0%nat) by lia.
rewrite Hlo0, Hn0; reflexivity.
}
assert(H : Z.of_nat (Z.to_nat lo + n)%nat = (lo + Z.of_nat n)%Z) by lia.
rewrite H; clear H.
assert(H : Z.pos p0 <? lo = false) by lia.
rewrite H; clear H.
rewrite Heqstep; clear Heqstep.
rewrite Pervasives.normalize_identity by lia.
step; [|reflexivity].
apply IHloop; lia.
Qed.
Lemma rev_fold_es_eq {A B : Set} f (acc : A) (fuel : nat) (hi lo : int) :
(fuel = Z.to_nat (hi - lo))%nat →
let range := Slot_repr.Range.Interval {|
Slot_repr.Range.t.Interval.lo := lo;
Slot_repr.Range.t.Interval.hi := hi
|} in
Valid.t range →
Proto_alpha.Slot_repr.Range.rev_fold_es (B := B) f acc range
=
Simulations.Slot_repr.Range.rev_fold_es
f acc (Z.to_nat hi) (Z.to_nat lo) fuel.
Proof.
intros Hfuel range Hv;
unfold
Proto_alpha.Slot_repr.Range.rev_fold_es,
Slot_repr.Range.rev_fold_es.
subst range; simpl.
rewrite ZifyInst.of_nat_to_nat_eq.
destruct Hv as [Hvlo Hvhi]; simpl in ×.
rewrite Z.max_r by lia.
step; [|reflexivity]; simpl.
unfold "<i", "-i"; simpl.
rewrite Pervasives.normalize_identity by lia.
remember (hi - 1)%Z as step_init.
(* First, we need remove case hi <= lo *)
match goal with
| |- ?f1 _ _ = ?f2 _ _ ⇒
remember f1 as loop_orig eqn:Elpo;
remember f2 as loop_sim eqn:Elps
end.
destruct fuel eqn:Efuel.
{ (* Efuel : fuel = 0%nat *)
destruct (Z.le_ge_cases hi lo) as [Hle | Hle].
{ (* hi <= lo *)
rewrite Elpo, Elps.
destruct step_init.
{ assert(H : 0 <? lo = true ) by lia.
rewrite H; reflexivity.
}
{ assert(H : Z.pos p <? lo = true ) by lia.
rewrite H; reflexivity.
}
assert(H : BinInt.Z.neg p ≥ -1 ) by lia.
assert(BinInt.Z.neg p < lo) by lia.
apply Z.ltb_lt in H0; rewrite H0; reflexivity.
}
(* lo <= hi *)
assert(H_step_init : step_init = (hi - 1)%Z) by lia.
rewrite H_step_init.
assert (H : hi = lo) by lia.
rewrite Elpo, Elps.
destruct lo eqn:Elo; [..|exfalso; lia];
simpl BinInt.Z.add; cbv fix beta.
{ rewrite H; reflexivity. }
assert(H1 : step_init ≥ 0) by lia.
rewrite <- H_step_init.
destruct step_init eqn:Esti; [..|exfalso; lia].
{ assert (H2 : 0 <? Z.pos p = true) by lia.
rewrite H2; reflexivity.
}
assert(H2 : Z.pos p0 <? Z.pos p = true) by lia.
rewrite H2; reflexivity.
}
(* Efuel : fuel = Datatypes.S n *)
destruct hi; [exfalso; lia| |destruct Hvhi; exfalso; lia].
(* hi = Z.pos *)
assert(Hlt : lo < Z.pos p) by lia.
assert(H_step_init
: step_init = (lo + Z.of_nat (Datatypes.S n) - 1)%Z)
by lia.
rewrite H_step_init.
clear Efuel Hfuel fuel Heqr acc.
assert(Hn : (n ≤ Z.to_nat (Z.pos p - lo - 1))%nat) by lia.
remember (Datatypes.S n) as fuel eqn:Heqfuel.
rewrite Elpo, Elps.
assert(Hfuel : (fuel ≤ Z.to_nat (Z.pos p - lo))%nat) by lia.
clear
Heqstep_init H_step_init step_init Heqfuel
Hn n loop_orig Elpo loop_sim Elps.
(* Recursion, finally! *)
revert a; generalize dependent fuel.
fix IHloop 1.
intros fuel Hn a.
destruct fuel as [|n].
{ (* fuel = Datatypes.O *)
simpl; rewrite Z.add_0_r.
remember (lo - 1) as step.
destruct step eqn:Estep.
{ assert(H : 0 <? lo = true) by lia.
rewrite H; reflexivity. }
{ assert(H : Z.pos p0 <? lo = true) by lia.
rewrite H; reflexivity. }
assert(H : BinInt.Z.neg p0 < lo) by lia.
apply Zlt_is_lt_bool in H; rewrite H; reflexivity.
}
(* fuel = Datatypes.S n *)
assert(H : (lo + Z.of_nat (Datatypes.S n) - 1) = (lo + Z.of_nat n)%Z)
by lia.
rewrite H; clear H.
remember (lo + Z.of_nat n)%Z as step eqn:Heqstep.
destruct step eqn:Estep; [..|exfalso; lia].
{ assert(H : 0 <? lo = false) by lia.
rewrite H; clear H.
assert(Hlo0 : lo = 0) by lia.
assert(Hn0 : n = 0%nat) by lia.
rewrite Hlo0, Hn0; reflexivity.
}
assert(H : Z.of_nat (Z.to_nat lo + n)%nat = (lo + Z.of_nat n)%Z) by lia.
rewrite H; clear H.
assert(H : Z.pos p0 <? lo = false) by lia.
rewrite H; clear H.
rewrite Heqstep; clear Heqstep.
rewrite Pervasives.normalize_identity by lia.
step; [|reflexivity].
apply IHloop; lia.
Qed.
[Proto_alpha.Simulation.Slot_repr.rev_fold_es] is valid.
Lemma simulation_rev_fold_es_is_valid
{A : Set} f (acc : A) (fuel hi lo : nat) (P : A → Prop)
: P acc →
(let range := Slot_repr.Range.Interval {|
Slot_repr.Range.t.Interval.lo := Z.of_nat lo;
Slot_repr.Range.t.Interval.hi := Z.of_nat hi
|} in
Valid.t range) →
(∀ acc num,
P acc → Slot_repr.Valid.t num → letP? a := f acc num in P a) →
(fuel = hi - lo)%nat →
letP? a := Simulations.Slot_repr.Range.rev_fold_es f acc hi lo fuel in
P a.
Proof.
intros Pacc Hv Hf Hfuel.
unfold Slot_repr.Range.rev_fold_es.
eapply Error.split_letP; [apply Hf; trivial; apply Hv|].
assert(Hfuel' : (fuel ≤ (hi - lo))%nat) by lia.
clear Hfuel Pacc acc.
generalize dependent fuel.
induction fuel as [|fuel]; [easy|].
intros Hfuel acc Pacc.
eapply Error.split_letP; [
apply Hf; trivial; destruct Hv as [[] []]; cbn in *; lia
|].
intros acc' Pacc'.
apply IHfuel; lia.
Qed.
{A : Set} f (acc : A) (fuel hi lo : nat) (P : A → Prop)
: P acc →
(let range := Slot_repr.Range.Interval {|
Slot_repr.Range.t.Interval.lo := Z.of_nat lo;
Slot_repr.Range.t.Interval.hi := Z.of_nat hi
|} in
Valid.t range) →
(∀ acc num,
P acc → Slot_repr.Valid.t num → letP? a := f acc num in P a) →
(fuel = hi - lo)%nat →
letP? a := Simulations.Slot_repr.Range.rev_fold_es f acc hi lo fuel in
P a.
Proof.
intros Pacc Hv Hf Hfuel.
unfold Slot_repr.Range.rev_fold_es.
eapply Error.split_letP; [apply Hf; trivial; apply Hv|].
assert(Hfuel' : (fuel ≤ (hi - lo))%nat) by lia.
clear Hfuel Pacc acc.
generalize dependent fuel.
induction fuel as [|fuel]; [easy|].
intros Hfuel acc Pacc.
eapply Error.split_letP; [
apply Hf; trivial; destruct Hv as [[] []]; cbn in *; lia
|].
intros acc' Pacc'.
apply IHfuel; lia.
Qed.
[Proto_alpha.Slot_repr.rev_fold_es] is valid.
Lemma rev_fold_es_is_valid
{A : Set} f (acc : A) (range : Slot_repr.Range.t) (P : A → Prop)
: Range.Valid.t range →
P acc →
(∀ acc num,
P acc → Slot_repr.Valid.t num → letP? a := f acc num in P a) →
letP? a := Proto_alpha.Slot_repr.Range.rev_fold_es f acc range in P a.
Proof.
intros Hv Pacc Hf.
destruct range as [[lo hi]].
remember (Z.to_nat (hi - lo)) as fuel.
rewrite (rev_fold_es_eq _ _ fuel); trivial.
apply simulation_rev_fold_es_is_valid; trivial;
[rewrite !Z2Nat.id by apply Hv; trivial|].
rewrite Z2Nat.inj_sub in Heqfuel; destruct Hv; simpl in *; lia.
Qed.
{A : Set} f (acc : A) (range : Slot_repr.Range.t) (P : A → Prop)
: Range.Valid.t range →
P acc →
(∀ acc num,
P acc → Slot_repr.Valid.t num → letP? a := f acc num in P a) →
letP? a := Proto_alpha.Slot_repr.Range.rev_fold_es f acc range in P a.
Proof.
intros Hv Pacc Hf.
destruct range as [[lo hi]].
remember (Z.to_nat (hi - lo)) as fuel.
rewrite (rev_fold_es_eq _ _ fuel); trivial.
apply simulation_rev_fold_es_is_valid; trivial;
[rewrite !Z2Nat.id by apply Hv; trivial|].
rewrite Z2Nat.inj_sub in Heqfuel; destruct Hv; simpl in *; lia.
Qed.
[Proto_alpha.Slot_repr.create] is valid