Skip to main content

⛽ Gas_limit_repr.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V7.

Require TezosOfOCaml.Environment.V7.Proofs.Compare.
Require TezosOfOCaml.Environment.V7.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V7.Proofs.Pervasives.
Require TezosOfOCaml.Environment.V7.Proofs.Utils.

Require TezosOfOCaml.Proto_alpha.Gas_limit_repr.
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.mul_scaling_factor
  Gas_limit_repr.scaling_factor
  Gas_limit_repr.mul_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.
  Module Integral.
Validity predicate for [integral].
    Module Valid.
      Definition t (x : Gas_limit_repr.Arith.integral) : Prop :=
        Is_rounded.t x Saturation_repr.Strictly_valid.t x.
    End Valid.
  End Integral.

  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.
  Proof.
    intros.
    unfold Gas_limit_repr.Arith.integral_exn.
    rewrite Z.to_int_eq by lia.
    rewrite integral_of_int_exn_eq by lia.
    reflexivity.
  Qed.

  Lemma mul_scaling_factor_eq : Gas_limit_repr.Arith.mul_scaling_factor = 1000.
  Proof.
    reflexivity.
  Qed.
  #[global] Hint Rewrite mul_scaling_factor_eq : tezos_z.

  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.
  Proof.
    intros.
    unfold Gas_limit_repr.Arith.integral_to_z.
    rewrite integral_exn_eq by assumption.
    unfold Gas_limit_repr.S.to_z, Z.of_int.
    rewrite mul_scaling_factor_eq.
    lia.
  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.
  Proof.
    intros.
    unfold Gas_limit_repr.Arith.unsafe_fp.
    rewrite Z.to_int_eq by lia.
    rewrite Saturation_repr.of_int_opt_eq; lia.
  Qed.

  Lemma z_integral_encoding_is_valid :
    Data_encoding.Valid.t Integral.Valid.t
      Gas_limit_repr.Arith.z_integral_encoding.
  Proof.
    Data_encoding.Valid.data_encoding_auto.
    intros x H.
    destruct H.
    split; [constructor|].
    rewrite integral_to_z_eq.
    rewrite integral_exn_eq; lia.
  Qed.
  #[global] Hint Resolve z_integral_encoding_is_valid : Data_encoding_db.

  Lemma n_integral_encoding_is_valid :
    Data_encoding.Valid.t Integral.Valid.t
      Gas_limit_repr.Arith.n_integral_encoding.
  Proof.
    Data_encoding.Valid.data_encoding_auto.
    intros x H. destruct H as [H0 H1].
    intros; split.
    { rewrite integral_to_z_eq.
      lia.
    }
    { rewrite integral_to_z_eq.
      rewrite integral_exn_eq; lia.
    }
  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).
  Proof.
    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_is_valid : Saturation_repr.Valid.t Gas_limit_repr.read_base_weight.
  gas_limit_repr_auto.
Qed.

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

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

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

Lemma cost_to_milligas_is_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.Strictly_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
        Saturation_repr.Strictly_valid.t gas_counter'
        ).
  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; [|constructor].
  split; [lia|].
  lia.
Qed.

The function [raw_consume] is valid and equivalent to subtraction
Lemma raw_consume_is_valid' gas gas' cost :
  Saturation_repr.Strictly_valid.t gas
  Saturation_repr.Strictly_valid.t cost
  Gas_limit_repr.raw_consume gas cost = Some gas'
  gas' = gas - cost cost gas.
Proof.
  intros H_gas H_cost.
  unfold Gas_limit_repr.raw_consume,
    Gas_limit_repr.Arith.sub_opt,
    Gas_limit_repr.cost_to_milligas,
    Gas_limit_repr.S.sub_opt.
  step; cbn; [|easy].
  inj. lia.
Qed.

Lemma alloc_cost_is_valid : {x},
    Saturation_repr.Valid.t x
    Saturation_repr.Valid.t (Gas_limit_repr.alloc_cost x).
Proof.
  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;
    [| apply Saturation_repr.add_is_valid].
  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; fcrush.
Qed.

Lemma alloc_bytes_is_valid : {x},
    Saturation_repr.Valid.t x
    Saturation_repr.Valid.t (Gas_limit_repr.alloc_bytes_cost x).
Proof.
  intros.
  unfold Gas_limit_repr.alloc_bytes_cost.
  apply alloc_cost_is_valid.
  apply Saturation_repr.safe_int_is_valid.
Qed.

Lemma atomic_step_cost_is_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_is_valid : {x},
  Saturation_repr.Valid.t x
  Saturation_repr.Valid.t (Gas_limit_repr.step_cost x).
Proof.
  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).
  hfcrush.
Qed.

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

Lemma read_bytes_cost_is_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_is_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_is_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_is_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_is_valid.
  { apply alloc_cost_is_valid.
    autorewrite with tezos_z; try reflexivity; try Utils.tezos_z_auto.
  }
  { unfold Gas_limit_repr.alloc_bytes_cost.
    apply alloc_cost_is_valid.
    apply Saturation_repr.safe_int_is_valid.
  }
Qed.

The function [check_gas_limit_is_valid] is valid
[raw_consume counter cost = Some v] implies [cost <= counter]
Lemma raw_consume_succ_impl counter cost v :
  Saturation_repr.Strictly_valid.t counter
  Saturation_repr.Valid.t cost
  Gas_limit_repr.raw_consume counter cost = Some v
  Saturation_repr.Strictly_valid.t v cost counter.
Proof.
  intros ? ?.
  unfold Gas_limit_repr.raw_consume,
    Gas_limit_repr.Arith.sub_opt,
    Gas_limit_repr.cost_to_milligas,
    Gas_limit_repr.S.sub_opt.
  cbn. step; cbn; [|easy].
  inj. rewrite <- Hinj.
  split; lia.
Qed.