➰ Cycle_repr.v

Proofs

See code, Gitlab , OCaml

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.

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.

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

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.

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

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

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

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.

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

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