🥷 Sapling_repr.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Sapling_repr.

Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.Sapling.
Require TezosOfOCaml.Proto_alpha.Proofs.Commitment_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Saturation_repr.

Lemma transaction_encoding_is_valid :
  Data_encoding.Valid.t (fun _ ⇒ True) Sapling_repr.transaction_encoding.
  Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve transaction_encoding_is_valid : Data_encoding_db.

Lemma diff_encoding_is_valid :
  Data_encoding.Valid.t (fun _ ⇒ True) Sapling_repr.diff_encoding.
  Data_encoding.Valid.data_encoding_auto.
  intuition;
  hauto l: on use: List.Forall_True.
Qed.
#[global] Hint Resolve diff_encoding_is_valid : Data_encoding_db.

Module Memo_size.
  Module Valid.
    Definition t (size : Sapling_repr.Memo_size.t) : Prop :=
      0 ≤ size ≤ Sapling_repr.Memo_size.max_uint16_z.
  End Valid.

  #[global] Hint Unfold
    Sapling_repr.Memo_size.max_uint16
    Sapling_repr.Memo_size.max_uint16_z
    Sapling_repr.Memo_size.unparse_to_z
    Valid.t
    : tezos_z.

  Lemma encoding_is_valid :
    Data_encoding.Valid.t Valid.t Sapling_repr.Memo_size.encoding.
    Data_encoding.Valid.data_encoding_auto.
  Qed.
  #[global] Hint Resolve encoding_is_valid : Data_encoding_db.

  Lemma parse_unparse (size : Sapling_repr.Memo_size.t) :
    Valid.t size →
    Sapling_repr.Memo_size.parse_z
      (Sapling_repr.Memo_size.unparse_to_z size) =
    Pervasives.Ok size.
    unfold Sapling_repr.Memo_size.parse_z.
    autounfold with tezos_z; simpl.
    intros.
    rewrite Z.to_int_eq by lia.
    repeat (destruct (_ <=? _) eqn:? in |- *); simpl; lia.
  Qed.

  Lemma unparse_parse (z : Z.t) :
    Valid.t z →
    match Sapling_repr.Memo_size.parse_z z with
    | Pervasives.Ok i ⇒ Sapling_repr.Memo_size.unparse_to_z i = z
    | Pervasives.Error _ ⇒ True
    end.
  Proof.
    intro H.
    unfold Sapling_repr.Memo_size.parse_z.
    repeat (destruct (_ ≤Z _) eqn:? in |- *); simpl; trivial.
    rewrite Z.to_int_eq by lia.
    reflexivity.
  Qed.
End Memo_size.

#[local] Ltac _auto :=
  intros;
  match goal with
  | [|- Saturation_repr.Valid.t (?f _)] ⇒ unfold f
  end;
  unfold Cache_memory_helpers.op_plusexclamation;
  apply Saturation_repr.add_is_valid.

Lemma ciphertext_size_is_valid : ∀ size,
  Saturation_repr.Valid.t size →
  Saturation_repr.Valid.t (Sapling_repr.ciphertext_size size).
  _auto.
Qed.

Lemma output_in_memory_size_is_valid : ∀ size,
  Saturation_repr.Valid.t (Sapling_repr.output_in_memory_size size).
  _auto.
Qed.

Lemma transaction_in_memory_size_is_valid : ∀ transaction,
  Saturation_repr.Valid.t (Sapling_repr.transaction_in_memory_size transaction).
  _auto.
Qed.

Lemma diff_in_memory_size_is_valid : ∀ diff,
  Saturation_repr.Valid.t (Sapling_repr.diff_in_memory_size diff).
  _auto.
Qed.

Lemma input_in_memory_size_is_valid :
  Saturation_repr.Valid.t Sapling_repr.input_in_memory_size.
  unfold Sapling_repr.input_in_memory_size.
  cbv - ["<="]; lia.
Qed.