Skip to main content

⛽ Gas_limit_repr.v

Proofs

See code, Gitlab , OCaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Proto_alpha.Environment.

Require TezosOfOCaml.Proto_alpha.Gas_limit_repr.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Compare.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Data_encoding.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Pervasives.
Require TezosOfOCaml.Proto_alpha.Proofs.Utils.
Require TezosOfOCaml.Proto_alpha.Proofs.Saturation_repr.

#[global] Hint Unfold
  Gas_limit_repr.Arith.add
  Gas_limit_repr.Arith.op_eq
  Gas_limit_repr.Arith.scaling_factor
  Gas_limit_repr.Arith.sub
  Gas_limit_repr.Arith.zero
  Gas_limit_repr.S.add
  Gas_limit_repr.S.erem
  Gas_limit_repr.S.sub
  Gas_limit_repr.S.mul
  Gas_limit_repr.scaling_factor
  : tezos_z.

Lemma scaling_factor_eq : Gas_limit_repr.scaling_factor = 1000.
  reflexivity.
Qed.
#[global] Hint Rewrite scaling_factor_eq : tezos_z.

Module Is_rounded.
  Definition t (x : int) := ((x / 1000) × 1000)%Z = x.
  #[global] Hint Unfold t : tezos_z.
End Is_rounded.

Module Is_roundable.
  Definition t x := 0 x (Saturation_repr.saturated - 1000).
  #[global] Hint Unfold t : tezos_z.

  Lemma implies_strictly_valid : x,
    t x Saturation_repr.Strictly_valid.t x.
    lia.
  Qed.
End Is_roundable.

Module Arith.
  Lemma compare_is_valid :
    Compare.Valid.t (fun _True) id Gas_limit_repr.Arith.compare.
  Proof. Compare.valid_auto. Qed.
  #[global] Hint Resolve compare_is_valid : Compare_db.

  Lemma integral_of_int_exn_eq : {i : int},
    Saturation_repr.Strictly_valid.t (i × 1000) %Z
    Gas_limit_repr.Arith.integral_of_int_exn i = (1000 × i)%Z.
    intros.
    unfold Gas_limit_repr.Arith.integral_of_int_exn, Gas_limit_repr.S.of_int_opt.
    rewrite Saturation_repr.Strictly_valid.true_eq; [|Utils.tezos_z_easy].
    autounfold with tezos_z; autorewrite with tezos_z; [|Utils.tezos_z_easy].
    unfold Compare.Int, Z, Compare.S.op_eq.
    rewrite Saturation_repr.scale_fast_eq; try Utils.tezos_z_easy.
    rewrite Saturation_repr.saturate_eq; [|Utils.tezos_z_easy].
    assert (H_if : 1000 × i =? 4611686018427387903 = false) by lia.
    now rewrite H_if.
  Qed.

  Lemma integral_exn_eq : {z : Z.t},
    Saturation_repr.Strictly_valid.t (1000 × z)%Z
    Gas_limit_repr.Arith.integral_exn z = (1000 × z)%Z.

    intros z H.
    unfold Gas_limit_repr.Arith.integral_exn,
           Gas_limit_repr.Arith.integral_of_int_exn, to_int,
           Gas_limit_repr.S.of_int_opt.
    autounfold with tezos_z in H.
    rewrite Pervasives.normalize_identity; [|
        Utils.tezos_z_auto].
    rewrite Saturation_repr.Strictly_valid.true_eq; [|Utils.tezos_z_easy].
    autounfold with tezos_z;
    autorewrite with tezos_z; [|Utils.tezos_z_easy].
    rewrite Saturation_repr.scale_fast_eq;
      try Utils.tezos_z_easy.
    unfold Compare.Int, Z, Compare.S.op_eq.
    rewrite Saturation_repr.saturate_eq; [|Utils.tezos_z_easy].
    assert (H_if : 1000 × z =? 4611686018427387903 = false) by lia.
    now rewrite H_if.
  Qed.

  Lemma integral_to_z_integral_exn : {x},
    Saturation_repr.Strictly_valid.t (1000 × x)%Z
    Gas_limit_repr.Arith.integral_to_z (Gas_limit_repr.Arith.integral_exn x) = x.
    intros x H.
    autounfold with tezos_z in H.
    unfold Gas_limit_repr.Arith.integral_exn, to_int,
      Gas_limit_repr.Arith.integral_of_int_exn.
    rewrite Pervasives.normalize_identity; [|
        Utils.tezos_z_easy].
    rewrite Saturation_repr.of_int_opt_eq; [|
        Utils.tezos_z_easy].
    rewrite Saturation_repr.scale_fast_eq;
      try Utils.tezos_z_easy.
    rewrite Saturation_repr.saturate_eq;
      try Utils.tezos_z_easy.

    unfold Gas_limit_repr.Arith.integral_exn, to_int,
      Gas_limit_repr.Arith.integral_to_z,
      Gas_limit_repr.S.to_z,
      of_int, Gas_limit_repr.S.ediv,
      Gas_limit_repr.Arith.scaling_factor,
      Gas_limit_repr.scaling_factor.
    change (Gas_limit_repr.S.mul_safe_of_int_exn 1000)%Z
      with 1000%Z.
    unfold Gas_limit_repr.S.op_eq,
      Compare.Int, Z, Compare.S.op_eq,
      Gas_limit_repr.S.saturated, Pervasives.max_int.
    assert (H_if : (1000 × x)%Z =? 4611686018427387903 = false) by lia.
    unfold "=i"; simpl (Compare.Int.(S.op_eq)).
    rewrite H_if.
    unfold "/i".
    rewrite Pervasives.normalize_identity; [lia|
        Utils.tezos_z_auto].
  Qed.

  Lemma integral_to_z_eq : {x},
    Gas_limit_repr.Arith.integral_to_z x = x /i 1000.
    intros.
    unfold Gas_limit_repr.Arith.integral_to_z,
      Gas_limit_repr.S.to_z, of_int, Gas_limit_repr.S.ediv,
      Gas_limit_repr.scaling_factor,
      Gas_limit_repr.scaling_factor.
    now change (Gas_limit_repr.S.mul_safe_of_int_exn 1000) with 1000.
  Qed.

  Lemma usafe_fp_eq : {x},
    Saturation_repr.Strictly_valid.t x
    Gas_limit_repr.Arith.unsafe_fp x = Z.to_int x.
    intros.
    unfold Gas_limit_repr.Arith.unsafe_fp, to_int, Gas_limit_repr.Arith.of_int_opt, Gas_limit_repr.S.of_int_opt.
    rewrite Pervasives.normalize_identity.
    { autounfold with tezos_z in H.
      now rewrite Saturation_repr.Strictly_valid.true_eq. }
    { revert H. Utils.tezos_z_auto. }
  Qed.

  Lemma z_integral_encoding_is_valid
    : Data_encoding.Valid.t
      (fun x
        Is_rounded.t x
        Saturation_repr.Valid.t x)
      Gas_limit_repr.Arith.z_integral_encoding.
    Data_encoding.Valid.data_encoding_auto.
    intros x H.
    destruct H.
    split; [constructor|].
    unfold Gas_limit_repr.Arith.integral_to_z,
      Gas_limit_repr.S.to_z, of_int, Gas_limit_repr.S.ediv,
      Gas_limit_repr.Arith.scaling_factor,
      Gas_limit_repr.scaling_factor,
      Gas_limit_repr.S.mul_safe_of_int_exn; simpl.
    unfold Gas_limit_repr.Arith.integral_exn,
      Gas_limit_repr.Arith.integral_of_int_exn, to_int,
      Gas_limit_repr.S.of_int_opt, "/i".
    replace (x / 1000 × 1000 / 1000) with (x / 1000) by lia.
    rewrite Saturation_repr.Strictly_valid.true_eq.
    rewrite Saturation_repr.scale_fast_eq.
    rewrite Saturation_repr.saturate_eq.
    change Gas_limit_repr.Arith.scaling_factor with 1000.
    repeat rewrite Pervasives.normalize_identity.
    rewrite Z.mul_comm. rewrite H.
    unfold Gas_limit_repr.S.op_eq, Compare.Int, Z, Compare.S.op_eq,
      Gas_limit_repr.S.saturated, Pervasives.max_int.
    autounfold with tezos_z in ×.
    simpl (Compare.Int.(S.op_eq)).
    now replace (x =? 4611686018427387903) with false by lia.

    all: Utils.tezos_z_easy.
  Qed.
  #[global] Hint Resolve z_integral_encoding_is_valid : Data_encoding_db.

  Lemma n_integral_encoding_is_valid :
    Data_encoding.Valid.t
      (fun x
        Is_rounded.t x
        Saturation_repr.Valid.t x)
      Gas_limit_repr.Arith.n_integral_encoding.

    Data_encoding.Valid.data_encoding_auto.
    intros x H. destruct H as [H0 H1].
    autounfold with tezos_z in H1.
    intros; split.
    { unfold Gas_limit_repr.Arith.integral_to_z,
        Gas_limit_repr.S.to_z, of_int,
        Gas_limit_repr.S.ediv, "/i",
        Gas_limit_repr.Arith.scaling_factor,
        Gas_limit_repr.scaling_factor.
      change (Gas_limit_repr.S.mul_safe_of_int_exn 1000) with 1000.
      rewrite Pervasives.normalize_identity;
        [lia|Utils.tezos_z_easy]. }
    { unfold Gas_limit_repr.Arith.integral_to_z,
        Gas_limit_repr.S.to_z, of_int,
        Gas_limit_repr.S.ediv,
        Gas_limit_repr.Arith.scaling_factor,
        Gas_limit_repr.scaling_factor, "/i".
      change (Gas_limit_repr.S.mul_safe_of_int_exn 1000) with 1000.
      rewrite Pervasives.normalize_identity;
        [|Utils.tezos_z_easy].
      unfold Gas_limit_repr.Arith.integral_exn,
        to_int, Gas_limit_repr.Arith.integral_of_int_exn,
        Gas_limit_repr.S.of_int_opt.
      rewrite Saturation_repr.Strictly_valid.true_eq.
      unfold Gas_limit_repr.S.op_eq, Compare.Int, Z, Compare.S.op_eq.
      rewrite Saturation_repr.scale_fast_eq.
      rewrite Saturation_repr.saturate_eq.
      rewrite Pervasives.normalize_identity.
      unfold Gas_limit_repr.Arith.scaling_factor,
        Gas_limit_repr.scaling_factor,
        Gas_limit_repr.S.saturated,
        Pervasives.max_int.
      change (Gas_limit_repr.S.mul_safe_of_int_exn 1000) with 1000.
      unfold "=i"; simpl (Compare.Int.(S.op_eq)).
      replace (1000 × (x / 1000) =? 4611686018427387903) with false by lia.
      now rewrite Z.mul_comm.

      all: Utils.tezos_z_easy.
    }
  Qed.
  #[global] Hint Resolve n_integral_encoding_is_valid : Data_encoding_db.

  Lemma ceil_is_valid : {x},
    Saturation_repr.Valid.t x
    Saturation_repr.Valid.t (Gas_limit_repr.Arith.ceil x).
    unfold Gas_limit_repr.Arith.ceil.
    intros.
    match goal with
    | [|- context [ if ?e then _ else _] ] ⇒ destruct e eqn:Eq_1
    end; try assumption.

    unfold Gas_limit_repr.Arith.add.
    apply Saturation_repr.add_is_valid.
  Qed.

  Lemma ceil_id : {x},
    Is_roundable.t x
    BinInt.Z.rem x 1000 = 0
    Gas_limit_repr.Arith.ceil x = x.
    intros;
    unfold Gas_limit_repr.Arith.ceil;
    autounfold with tezos_z in *;
    autorewrite with tezos_z; [|Utils.tezos_z_auto];
    rewrite H0;
    now change (normalize_int 0 =i 0) with true.
  Qed.

  Lemma ceil_non_mod_1000_eq : {x},
    Is_roundable.t x%Z
    BinInt.Z.rem x 1000 0
    Gas_limit_repr.Arith.ceil x = (x + (1000 - (BinInt.Z.rem x 1000)))%Z.
    intros.
    unfold Gas_limit_repr.Arith.ceil;
    autounfold with tezos_z in *;
    autorewrite with tezos_z; [|Utils.tezos_z_auto];
    unfold Compare.Int, Z,
      Compare.S.op_gteq,
      Compare.S.op_eq,
      Compare.S.max.
    assert (normalize_int (BinInt.Z.rem x 1000) =? 0 = false) by Utils.tezos_z_auto.
    rewrite H1.
    rewrite Utils.BinInt_Z_max_eq;
      [|Utils.tezos_z_auto].
    assert (normalize_int
    (x + normalize_int (1000 - normalize_int (BinInt.Z.rem x 1000))) >=? 0 = true) by Utils.tezos_z_auto.
    rewrite H2.
    Utils.tezos_z_auto.
  Qed.

  Lemma ceil_is_rounded : {x},
    Is_roundable.t x%Z
    Is_rounded.t (Gas_limit_repr.Arith.ceil x).
    intros x H.
    autounfold with tezos_z in H.
    assert (Hx : BinInt.Z.rem x 1000 = 0 BinInt.Z.rem x 1000 0) by lia.
    destruct Hx.
    { rewrite ceil_id; Utils.tezos_z_easy. }
    { rewrite ceil_non_mod_1000_eq; Utils.tezos_z_easy. }
  Qed.

  Lemma floor_is_valid : {x},
    Saturation_repr.Valid.t x
    Saturation_repr.Valid.t (Gas_limit_repr.Arith.floor x).

    unfold Gas_limit_repr.Arith.floor.
    intros.
    apply Saturation_repr.sub_valid; try assumption.
  Qed.

  Lemma n_fp_encoding_is_valid :
    Data_encoding.Valid.t
    Saturation_repr.Strictly_valid.t
    Gas_limit_repr.Arith.n_fp_encoding.
    unfold Gas_limit_repr.Arith.n_fp_encoding,
      Gas_limit_repr.S.n_encoding.
    Data_encoding.Valid.data_encoding_auto.
  Qed.
  #[global] Hint Resolve n_fp_encoding_is_valid : Data_encoding_db.
End Arith.

Module Cost.
  Module Valid.
    Definition t (x : Gas_limit_repr.cost) : Prop :=
      Saturation_repr.Valid.t x.
  End Valid.
End Cost.

Lemma S_z_encoding_is_valid :
  Data_encoding.Valid.t Saturation_repr.Strictly_valid.t
    Gas_limit_repr.S.z_encoding.
  apply Saturation_repr.z_encoding_is_valid.
Qed.
#[global] Hint Resolve S_z_encoding_is_valid : Data_encoding_db.

Lemma Arith_z_fp_encoding_is_valid :
  Data_encoding.Valid.t Saturation_repr.Strictly_valid.t
    Gas_limit_repr.Arith.z_fp_encoding.
  Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve Arith_z_fp_encoding_is_valid : Data_encoding_db.

Module Valid.
  Definition t (x : Gas_limit_repr.t) : Prop :=
    match x with
    | Gas_limit_repr.Limited {|
        Gas_limit_repr.t.Limited.remaining := remaining
      |} ⇒ Saturation_repr.Strictly_valid.t remaining
    | Gas_limit_repr.UnaccountedTrue
    end.
End Valid.

Lemma encoding_is_valid : Data_encoding.Valid.t Valid.t Gas_limit_repr.encoding.
  unfold Gas_limit_repr.encoding.
  Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.

Lemma cost_encoding_is_valid :
  Data_encoding.Valid.t Saturation_repr.Strictly_valid.t Gas_limit_repr.cost_encoding.
  Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve cost_encoding_is_valid : Data_encoding_db.

Ltac gas_limit_repr_auto :=
  repeat (match goal with
    |[|- Saturation_repr.Valid.t ?x ] ⇒ unfold x
    |[|- Saturation_repr.Valid.t (?f _) ] ⇒ unfold f
  end);
  Utils.tezos_z_autounfold; simpl;
    autounfold with tezos_z; autorewrite with tezos_z;
    first [reflexivity | Utils.tezos_z_auto].

Lemma allocation_weight_is_valid : Saturation_repr.Valid.t Gas_limit_repr.allocation_weight.
  gas_limit_repr_auto.
Qed.

Lemma step_weight_is_valid : Saturation_repr.Valid.t Gas_limit_repr.step_weight.
  gas_limit_repr_auto.
Qed.

Lemma read_base_weight_valid : Saturation_repr.Valid.t Gas_limit_repr.read_base_weight.
  gas_limit_repr_auto.
Qed.

Lemma write_base_weight_valid : Saturation_repr.Valid.t Gas_limit_repr.write_base_weight.
  gas_limit_repr_auto.
Qed.

Lemma byte_read_weight_valid : Saturation_repr.Valid.t Gas_limit_repr.byte_read_weight.
  gas_limit_repr_auto.
Qed.

Lemma byte_written_weight_valid : Saturation_repr.Valid.t Gas_limit_repr.byte_written_weight.
  gas_limit_repr_auto.
Qed.

Lemma cost_to_milligas_valid : {x}, Saturation_repr.Valid.t x Saturation_repr.Valid.t (Gas_limit_repr.cost_to_milligas x).
  unfold Gas_limit_repr.cost_to_milligas; intros;assumption.
Qed.

Lemma raw_consume_is_valid gas_counter cost
    : cost gas_counter
    Saturation_repr.Valid.t cost
    Saturation_repr.Valid.t gas_counter
    Option.post_when_success (Gas_limit_repr.raw_consume gas_counter cost)
      (fun gas_counter'
        Gas_limit_repr.Arith.op_lteq gas_counter' gas_counter = true).
  unfold Option.post_when_success.
  unfold Gas_limit_repr.raw_consume.
  unfold Gas_limit_repr.Arith.sub_opt.
  unfold Gas_limit_repr.cost_to_milligas.
  unfold Gas_limit_repr.S.sub_opt.
  unfold Cost.Valid.t.
  unfold Saturation_repr.Valid.t.
  unfold Saturation_repr.saturated, Pervasives.max_int.
  cbn; autounfold with tezos_z.
  unfold Pervasives.normalize_int, two_pow_62, two_pow_63, two_pow_62.
  repeat rewrite Zminus_0_r.
  simpl. unfold Z.compare, Z.sub.
  intros.
  match goal with
  | [|- context[if ?e then _ else _]] ⇒ destruct e eqn:H_eq
  end; try constructor.
  lia.
Qed.

Lemma alloc_cost_valid : {x},
    Saturation_repr.Valid.t x
    Saturation_repr.Valid.t (Gas_limit_repr.alloc_cost x).

  intros.
  unfold Gas_limit_repr.alloc_cost,
    Gas_limit_repr.allocation_weight,
    Gas_limit_repr.scaling_factor.

  apply Saturation_repr.scale_fast_valid; try Utils.tezos_z_auto.
  Utils.tezos_z_autounfold.
  autorewrite with tezos_z; try Utils.tezos_z_auto; try reflexivity;
  try autorewrite with tezos_z; try reflexivity;
  try Utils.tezos_z_auto.
  apply Saturation_repr.add_is_valid.
Qed.

Lemma alloc_bytes_valid : {x},
    Saturation_repr.Valid.t x
    Saturation_repr.Valid.t (Gas_limit_repr.alloc_bytes_cost x).
  intros.
  unfold Gas_limit_repr.alloc_bytes_cost.
  apply alloc_cost_valid.
  apply Saturation_repr.safe_int_is_valid.
Qed.

Lemma atomic_step_cost_valid : {x},
  Saturation_repr.Valid.t x
  Saturation_repr.Valid.t (Gas_limit_repr.atomic_step_cost x).
  intro x.
  unfold Gas_limit_repr.atomic_step_cost, Gas_limit_repr.S.may_saturate_value.
  autounfold with tezos_z; trivial.
Qed.

Lemma step_cost_valid : {x},
  Saturation_repr.Valid.t x
  Saturation_repr.Valid.t (Gas_limit_repr.step_cost x).
  unfold Gas_limit_repr.step_cost, Gas_limit_repr.step_cost,
    Gas_limit_repr.step_weight, Gas_limit_repr.scaling_factor.
  autounfold with tezos_z.
  intros.
  apply Saturation_repr.scale_fast_valid; try (autounfold with tezos_z; lia).
  autorewrite with tezos_z; try (autounfold with tezos_z; lia);
  reflexivity.
Qed.

Lemma free_valid : Saturation_repr.Valid.t Gas_limit_repr.free.
  unfold Gas_limit_repr.free.
  Utils.tezos_z_auto.
Qed.

Lemma read_bytes_cost_valid : {x},
    Saturation_repr.Valid.t x
    Saturation_repr.Valid.t (Gas_limit_repr.read_bytes_cost x).
  unfold Gas_limit_repr.read_bytes_cost.
  intros; apply Saturation_repr.add_is_valid.
Qed.

Lemma write_bytes_cost_valid : {x : int},
    Saturation_repr.Valid.t x
    Saturation_repr.Valid.t (Gas_limit_repr.write_bytes_cost x).

  unfold Gas_limit_repr.write_bytes_cost.
  intros.
  apply Saturation_repr.add_is_valid.
Qed.

Lemma op_plusat_valid : {x y},
  Saturation_repr.Valid.t x
  Saturation_repr.Valid.t y
  Saturation_repr.Valid.t (Gas_limit_repr.op_plusat x y).
  intros.
  apply Saturation_repr.add_is_valid.
Qed.

Lemma op_starat_valid : {x y},
  Saturation_repr.Valid.t x
  Saturation_repr.Valid.t y
  Saturation_repr.Valid.t (Gas_limit_repr.op_starat x y).

  intros x y. unfold Gas_limit_repr.op_starat.
  apply Saturation_repr.mul_is_valid.
Qed.

Lemma alloc_mbytes_cost_is_valid : {x},
  Saturation_repr.Valid.t x
  Saturation_repr.Valid.t (Gas_limit_repr.alloc_mbytes_cost x).
  intros.
  unfold Gas_limit_repr.alloc_mbytes_cost.
  apply op_plusat_valid.
  { apply alloc_cost_valid. autorewrite with tezos_z; try reflexivity; try Utils.tezos_z_auto. }
  { unfold Gas_limit_repr.alloc_bytes_cost.
    apply alloc_cost_valid.
    apply Saturation_repr.safe_int_is_valid.
  }
Qed.