🎰 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.

[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.

[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.

[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.

[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.

[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.

[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.

[Proto_alpha.Slot_repr.create] is valid

  Lemma create_is_valid (min max : int)
    : letP? r := Slot_repr.Range.create min max in
      Valid.t r.
  Proof. Admitted.
End Range.