⛽ Gas_limit_repr.v
Proofs
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.
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.Unaccounted ⇒ True
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.
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.Unaccounted ⇒ True
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.
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
Lemma check_gas_limit_is_valid i1 i2 :
Gas_limit_repr.Arith.Integral.Valid.t i1 →
Gas_limit_repr.Arith.Integral.Valid.t i2 →
letP? x := Gas_limit_repr.check_gas_limit i1 i2 in
True.
Proof.
Admitted.
Gas_limit_repr.Arith.Integral.Valid.t i1 →
Gas_limit_repr.Arith.Integral.Valid.t i2 →
letP? x := Gas_limit_repr.check_gas_limit i1 i2 in
True.
Proof.
Admitted.
[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.
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.