🇿 Zk_rollup_parameters.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V7.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_parameters.

Require TezosOfOCaml.Proto_alpha.Proofs.Ticket_scanner.
Require TezosOfOCaml.Proto_alpha.Proofs.Zk_rollup_operation_repr.

Module deposit_parameters.
  Module Valid.

The validity predicate for the [Zk_rollup_parameters.deposit_parameters] type

    Record t (x : Zk_rollup_parameters.deposit_parameters) : Prop := {
      ex_ticket : Ticket_scanner.ex_ticket.Valid.t
        x.(Zk_rollup_parameters.deposit_parameters.ex_ticket);
      zkru_operation : Zk_rollup_operation_repr.Valid.t
        x.(Zk_rollup_parameters.deposit_parameters.zkru_operation)
      }.
  End Valid.
End deposit_parameters.

The function [get_deposit_parameters] is valid.

Lemma get_deposit_parameters_is_valid
  (ty : Script_typed_ir.ty)
  (md1 md2 : Script_typed_ir.ty_metadata)
  (db : Dependent_bool.dand)
  (ticket : Script_typed_ir.ticket
    (Script_family.Ty.to_Set
      (Script_typed_ir.ty.Valid.to_Ty_t ty)))
  (op : Zk_rollup_operation_repr.t)
  (b : bytes) :
  Script_typed_ir.ty.Valid.t ty →
  Script_typed_ir.ty.Comparable.t ty →
  Script_typed_ir.ticket.Valid.t (Script_typed_ir.ty.Valid.to_Ty_t ty) ticket →
  Zk_rollup_operation_repr.Valid.t op →
  Binary.to_bytes_opt
    None
    Zk_rollup_operation_repr.encoding
    op = Some b →
  letP? params :=
    Zk_rollup_parameters.get_deposit_parameters
      (Script_typed_ir.Pair_t
        (Script_typed_ir.Ticket_t ty md1)
        Script_typed_ir.Bytes_t
        md2 db)
      (ticket, b) in
  deposit_parameters.Valid.t params.
Proof.
  intros ticket_valid ty_valid ty_comp op_valid op_b.
  unfold Zk_rollup_parameters.get_deposit_parameters.
  pose proof (Data_encoding.Valid.of_bytes_opt_to_bytes_opt
    Zk_rollup_operation_repr.encoding_is_valid op op_valid) as pf.
  unfold Zk_rollup_operation_repr.t in ×.
  rewrite op_b in pf.
  rewrite pf; simpl.
  now constructor.
Qed.