➰ Cycle_repr.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Cycle_repr.
Require TezosOfOCaml.Environment.V8.Proofs.Int32.
Require TezosOfOCaml.Proto_alpha.Proofs.Storage_description.
#[global] Hint Unfold
Cycle_repr.op_eq
Cycle_repr.op_ltgt
Cycle_repr.op_lt
Cycle_repr.op_lteq
Cycle_repr.op_gteq
Cycle_repr.op_gt
Cycle_repr.compare
Cycle_repr.equal
Cycle_repr.max
Cycle_repr.min
Cycle_repr.to_int32
Cycle_repr.of_int32_exn
: tezos_z.
Module Valid.
Definition t (cycle : Cycle_repr.t) : Prop :=
0 ≤ cycle ≤ Int32.max_int.
#[global] Hint Unfold t : tezos_z.
End Valid.
Lemma encoding_is_valid
: Data_encoding.Valid.t Int32.Valid.t Cycle_repr.encoding.
Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
Lemma rpc_arg_is_valid : RPC_arg.Valid.t Valid.t Cycle_repr.rpc_arg.
apply RPC_arg.Valid.like.
eapply RPC_arg.Valid.implies; [apply RPC_arg.Valid.uint31|].
autounfold with tezos_z; simpl.
lia.
Qed.
Lemma compare_is_valid : Compare.Valid.t (fun _ ⇒ True) id Cycle_repr.compare.
Proof.
apply Compare.int32_is_valid.
Qed.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Cycle_repr.
Require TezosOfOCaml.Environment.V8.Proofs.Int32.
Require TezosOfOCaml.Proto_alpha.Proofs.Storage_description.
#[global] Hint Unfold
Cycle_repr.op_eq
Cycle_repr.op_ltgt
Cycle_repr.op_lt
Cycle_repr.op_lteq
Cycle_repr.op_gteq
Cycle_repr.op_gt
Cycle_repr.compare
Cycle_repr.equal
Cycle_repr.max
Cycle_repr.min
Cycle_repr.to_int32
Cycle_repr.of_int32_exn
: tezos_z.
Module Valid.
Definition t (cycle : Cycle_repr.t) : Prop :=
0 ≤ cycle ≤ Int32.max_int.
#[global] Hint Unfold t : tezos_z.
End Valid.
Lemma encoding_is_valid
: Data_encoding.Valid.t Int32.Valid.t Cycle_repr.encoding.
Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
Lemma rpc_arg_is_valid : RPC_arg.Valid.t Valid.t Cycle_repr.rpc_arg.
apply RPC_arg.Valid.like.
eapply RPC_arg.Valid.implies; [apply RPC_arg.Valid.uint31|].
autounfold with tezos_z; simpl.
lia.
Qed.
Lemma compare_is_valid : Compare.Valid.t (fun _ ⇒ True) id Cycle_repr.compare.
Proof.
apply Compare.int32_is_valid.
Qed.
The function [add] is valid.
Lemma add_is_valid a b :
Valid.t b →
letP? x := Cycle_repr.add a b in
True.
Proof.
intros.
unfold Cycle_repr.add.
step; simpl; [trivial|lia].
Qed.
Valid.t b →
letP? x := Cycle_repr.add a b in
True.
Proof.
intros.
unfold Cycle_repr.add.
step; simpl; [trivial|lia].
Qed.
[add a b] is closed under [Cycle_repr.t] when [a + b] does not overflow
Lemma add_is_valid' a b :
Int32.Valid.t (a + b)%Z →
Cycle_repr.Valid.t a →
Cycle_repr.Valid.t b →
letP? r := Cycle_repr.add a b in
Cycle_repr.Valid.t r.
Proof.
intros H_valid_sum H_Valid_a H_Valid_b.
unfold Cycle_repr.add; cbn.
step; cbn; [|lia].
red. unfold Int32.of_int.
rewrite Int32.normalize_identity; [|lia].
unfold "+i32".
rewrite Int32.normalize_identity by lia.
lia.
Qed.
Int32.Valid.t (a + b)%Z →
Cycle_repr.Valid.t a →
Cycle_repr.Valid.t b →
letP? r := Cycle_repr.add a b in
Cycle_repr.Valid.t r.
Proof.
intros H_valid_sum H_Valid_a H_Valid_b.
unfold Cycle_repr.add; cbn.
step; cbn; [|lia].
red. unfold Int32.of_int.
rewrite Int32.normalize_identity; [|lia].
unfold "+i32".
rewrite Int32.normalize_identity by lia.
lia.
Qed.
The function [sub] is valid.
Lemma sub_is_valid a b :
Valid.t b →
letP? r := Cycle_repr.sub a b in
Option.Forall Valid.t r.
Proof.
intros.
unfold Cycle_repr.sub.
step; simpl; [|lia].
step; simpl; lia.
Qed.
Valid.t b →
letP? r := Cycle_repr.sub a b in
Option.Forall Valid.t r.
Proof.
intros.
unfold Cycle_repr.sub.
step; simpl; [|lia].
step; simpl; lia.
Qed.
[add a b] may overflow yielding a negative cycle. The cycle
increases very slowly so this is not a problem in pratice. It was
reported on the devteam channel anyway.
Lemma add_may_overflow :
∃ a b,
Cycle_repr.Valid.t a →
Cycle_repr.Valid.t b →
letP? r := Cycle_repr.add a b in
¬ Cycle_repr.Valid.t r.
Proof.
∃ Int32.max_int, 1.
intros ? ?. cbn in ×. lia.
Qed.
∃ a b,
Cycle_repr.Valid.t a →
Cycle_repr.Valid.t b →
letP? r := Cycle_repr.add a b in
¬ Cycle_repr.Valid.t r.
Proof.
∃ Int32.max_int, 1.
intros ? ?. cbn in ×. lia.
Qed.
[add a b = Error _] implies that [b] is negative
Lemma add_err_impl a b e :
Cycle_repr.add a b = Pervasives.Error e →
b < 0.
Proof.
unfold Cycle_repr.add. cbn. step; [easy|].
intros _. lia.
Qed.
Cycle_repr.add a b = Pervasives.Error e →
b < 0.
Proof.
unfold Cycle_repr.add. cbn. step; [easy|].
intros _. lia.
Qed.
[sub a b = Error _] implies that [b] is negative
Lemma sub_err_impl a b e :
Cycle_repr.sub a b = Pervasives.Error e →
b < 0.
Proof.
unfold Cycle_repr.sub. cbn. step; [step|]; try easy.
lia.
Qed.
Cycle_repr.sub a b = Pervasives.Error e →
b < 0.
Proof.
unfold Cycle_repr.sub. cbn. step; [step|]; try easy.
lia.
Qed.
The function [succ] is valid
Lemma succ_is_valid x :
Cycle_repr.Valid.t (x +Z 1) →
let x' := Cycle_repr.succ x in
Cycle_repr.Valid.t x' ∧ x' = x +Z 1.
Proof.
unfold Cycle_repr.succ.
unfold Int32.succ.
lia.
Qed.
Cycle_repr.Valid.t (x +Z 1) →
let x' := Cycle_repr.succ x in
Cycle_repr.Valid.t x' ∧ x' = x +Z 1.
Proof.
unfold Cycle_repr.succ.
unfold Int32.succ.
lia.
Qed.
[pred] is valid
Lemma pred_is_valid cycle cycle' :
Cycle_repr.Valid.t cycle →
Cycle_repr.pred cycle = Some cycle' →
Cycle_repr.Valid.t cycle'.
Proof.
intros H_valid.
destruct cycle.
{ easy. }
{ unfold Cycle_repr.pred, Int32.pred.
inj. rewrite <- Hinj. lia.
}
{ lia. }
Qed.
Lemma Index_is_valid
: Storage_description.INDEX.Valid.t Valid.t Cycle_repr.Index.
Proof.
constructor.
{ constructor; try reflexivity.
{ cbv.
intros;
rewrite Int32.of_string_opt_to_string;
reflexivity.
}
{ cbv - [length].
intro path.
destruct path as [|s[]]; trivial.
assert (H_s := Int32.to_string_of_string_opt s).
destruct (Int32.of_string_opt s); congruence.
}
}
{ apply rpc_arg_is_valid. }
{ Data_encoding.Valid.data_encoding_auto.
autounfold with tezos_z; lia.
}
{ apply compare_is_valid. }
Qed.
Module Index.
Cycle_repr.Valid.t cycle →
Cycle_repr.pred cycle = Some cycle' →
Cycle_repr.Valid.t cycle'.
Proof.
intros H_valid.
destruct cycle.
{ easy. }
{ unfold Cycle_repr.pred, Int32.pred.
inj. rewrite <- Hinj. lia.
}
{ lia. }
Qed.
Lemma Index_is_valid
: Storage_description.INDEX.Valid.t Valid.t Cycle_repr.Index.
Proof.
constructor.
{ constructor; try reflexivity.
{ cbv.
intros;
rewrite Int32.of_string_opt_to_string;
reflexivity.
}
{ cbv - [length].
intro path.
destruct path as [|s[]]; trivial.
assert (H_s := Int32.to_string_of_string_opt s).
destruct (Int32.of_string_opt s); congruence.
}
}
{ apply rpc_arg_is_valid. }
{ Data_encoding.Valid.data_encoding_auto.
autounfold with tezos_z; lia.
}
{ apply compare_is_valid. }
Qed.
Module Index.
[compare] function is valid
Lemma compare_is_valid : Compare.Valid.t (fun _ ⇒ True) id Cycle_repr.compare.
Proof.
apply Index_is_valid.
Qed.
#[global] Hint Resolve compare_is_valid : Compare_db.
End Index.
Proof.
apply Index_is_valid.
Qed.
#[global] Hint Resolve compare_is_valid : Compare_db.
End Index.