Skip to main content

🥷 Sapling_repr.v

Proofs

See code, Gitlab , OCaml

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

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

Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Data_encoding.
Require TezosOfOCaml.Proto_alpha.Environment.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.
    unfold normalize_int, two_pow_62, two_pow_63.
    match goal with
    | |- context[if ?e then _ else _] ⇒ destruct e eqn:?
    end;
      hauto lq: on use: Bool.andb_false_iff solve: lia.
  Qed.

  Lemma unparse_parse (z : Z.t) :
    Valid.t z
    match Sapling_repr.Memo_size.parse_z z with
    | Pervasives.Ok iSapling_repr.Memo_size.unparse_to_z i = z
    | Pervasives.Error _True
    end.
  Proof.
    intro H; destruct z eqn:DZ.
    { simpl; lia. }
    { unfold Sapling_repr.Memo_size.parse_z; simpl.
      destruct (_ <=? _) eqn:R; lia. }
    { destruct H; lia. }
  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.