🪜 Raw_level_repr.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.

Require TezosOfOCaml.Environment.V8.Proofs.Int32.
Require TezosOfOCaml.Environment.V8.Proofs.RPC_arg.
Require TezosOfOCaml.Proto_alpha.Proofs.Storage_description.

#[global] Hint Unfold
  Raw_level_repr.to_int32
  Raw_level_repr.op_eq
  Raw_level_repr.op_ltgt
  Raw_level_repr.op_lt
  Raw_level_repr.op_lteq
  Raw_level_repr.op_gteq
  Raw_level_repr.op_gt
  Raw_level_repr.compare
  Raw_level_repr.equal
  Raw_level_repr.max
  Raw_level_repr.min
  : tezos_z.

Module Valid.
  Definition t (i : Raw_level_repr.t) : Prop :=
    0 ≤ i ≤ Int32.max_int.
  #[global] Hint Unfold t : tezos_z.
End Valid.

[compare] function is valid

Lemma compare_is_valid :
  Compare.Valid.t (fun _ ⇒ True) id Raw_level_repr.compare.
Proof. Compare.valid_auto. Qed.
#[global] Hint Resolve compare_is_valid : Compare_db.

Propositional equality and [equal] are equivalent on [Raw_level_repr.t].

Lemma equal_is_valid :
  Compare.Equal.Valid.t (fun _ ⇒ True) Raw_level_repr.equal.
Proof.
  unfold Compare.Equal.Valid.t.
  intros level1 level2 _ _.
  split ; unfold Raw_level_repr.equal ; unfold Compare.Int32 ;
  unfold Z ; simpl ; intro H ; lia.
Qed.

Lemma rpc_arg_is_valid : RPC_arg.Valid.t Valid.t Raw_level_repr.rpc_arg.
  constructor; intros; simpl.
  { now rewrite Int32.of_string_opt_to_string. }
  { assert (H := Int32.to_string_of_string_opt s).
    now destruct (Int32.of_string_opt _).
  }
Qed.

Lemma root_value_is_valid : Valid.t Raw_level_repr.root_value.
Proof.
  easy.
Qed.

Axiom succ_is_valid : ∀ {l : Raw_level_repr.t},
  Valid.t l → Valid.t (Raw_level_repr.succ l).

Axiom pred_is_valid : ∀ {l : Raw_level_repr.t},
  Valid.t l →
  match Raw_level_repr.pred l with
  | Some l' ⇒ Valid.t l' ∧ l' = (l -Z 1)
  | None ⇒ True
  end.

Lemma of_int32_is_valid (i : int32) :
  Int32.Valid.t i →
  letP? l := Raw_level_repr.of_int32 i in
  Valid.t l.
Proof.
  unfold Raw_level_repr.of_int32; simpl.
  destruct (_ >=? _) eqn:?; simpl; [|easy].
  autounfold with tezos_z; lia.
Qed.

The function [of_int32] is the identity on valid levels.

Lemma of_int32_eq (i : int32) :
  Valid.t i →
  Raw_level_repr.of_int32 i = return? i.
Proof.
  intros.
  unfold Raw_level_repr.of_int32.
  destruct (_ ≥i32 _) eqn:?; lia.
Qed.

Lemma of_int32_to_int32 {l : Raw_level_repr.t}
  : Valid.t l →
    Raw_level_repr.of_int32 (Raw_level_repr.to_int32 l) = Pervasives.Ok l.
  unfold Raw_level_repr.of_int32, Raw_level_repr.to_int32.
  autounfold with tezos_z; simpl.
  destruct (_ >=? _) eqn:?; [reflexivity | lia].
Qed.

Lemma encoding_is_valid
  : Data_encoding.Valid.t Valid.t Raw_level_repr.encoding.
  Data_encoding.Valid.data_encoding_auto.
  intros.
  rewrite of_int32_to_int32; autounfold with tezos_z in *; intuition lia.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.

Module Index.

[compare] function is valid

  Lemma compare_is_valid
    : Compare.Valid.t (fun _ ⇒ True) id Raw_level_repr.Index.compare.
  Proof. Compare.valid_auto. Qed.
  #[global] Hint Resolve compare_is_valid : Compare_db.
End Index.

Lemma Index_Path_is_valid
  : Path_encoding.S.Valid.t
      (Storage_description.INDEX.to_Path Raw_level_repr.Index).
  constructor; intros; try reflexivity; cbv;
    try rewrite Int32.of_string_opt_to_string; trivial.
  destruct path as [|s[]]; trivial.
  assert (H_eq := Int32.to_string_of_string_opt s).
  destruct (Int32.of_string_opt s); congruence.
Qed.

Lemma Index_is_valid
  : Storage_description.INDEX.Valid.t Valid.t Raw_level_repr.Index.
  constructor; [
    exact Index_Path_is_valid |
    exact rpc_arg_is_valid |
    exact encoding_is_valid |
    exact Compare.int32_is_valid
  ].
Qed.

The expression [diff_value a b] is valid if [a <= b] and a and b are valid.

Lemma diff_value_is_valid level first_level :
  first_level ≤ level →
  Raw_level_repr.Valid.t level →
  Raw_level_repr.Valid.t first_level →
  let x := Raw_level_repr.diff_value level first_level in
  Raw_level_repr.Valid.t x ∧ x = level - first_level.
Proof.
  intros ? ? ?.
  unfold Raw_level_repr.diff_value.
  cbn in ×. unfold "-i32" in ×.
  split.
  { rewrite Int32.normalize_identity; lia. }
  { rewrite Int32.normalize_identity; [|lia].
    reflexivity.
  }
Qed.

The expression [diff a b] is positive if [a] and [b] are valid and [b <= a]. Helper lemma

Lemma diff_value_is_non_negative a b :
  Raw_level_repr.Valid.t a →
  Raw_level_repr.Valid.t b →
  b ≤ a →
  Raw_level_repr.diff_value a b ≥i32 0 = true.
Proof.
  intros ? ? H.
  unfold Raw_level_repr.diff_value.
  unfold "-i32".
  rewrite Int32.normalize_identity; [|lia].
  cbn. lia.
Qed.

The function [add] is valid

Lemma add_is_valid level n :
  Raw_level_repr.Valid.t level →
  Pervasives.Int.Valid.t n →
  letP? ' x := Raw_level_repr.add level n in
  Raw_level_repr.Valid.t x.
Proof.
Admitted.

The function [add] is equivalent to [+Z]

Lemma add_eq l i :
  Raw_level_repr.Valid.t l →
  Pervasives.Int.Valid.t i →
  letP? l' := Raw_level_repr.add l i in
    l' = l +Z i.
Proof.
Admitted.

The function [sub] is valid

Lemma sub_is_valid l i :
  Raw_level_repr.Valid.t l →
  Pervasives.Int.Valid.t i →
  letP? l' := Raw_level_repr.sub l i in
  Option.Forall Raw_level_repr.Valid.t l'.
Proof.
Admitted.

The function [sub] is equivalent to [-Z]

Lemma sub_eq l i :
  Raw_level_repr.Valid.t l →
  Pervasives.Int.Valid.t i →
  letP? l' := Raw_level_repr.sub l i in
   l' = Some (l -Z i).
Proof.
Admitted.

The function [pred_eq] is equivalent to [_ -Z 1]

Lemma pred_eq l :
  Raw_level_repr.Valid.t l →
  Option.Forall (fun x ⇒ x = l -Z 1) (Raw_level_repr.pred l).
Proof.
Admitted.