🔫 Bond_id_repr.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Bond_id_repr.

Require TezosOfOCaml.Environment.V8.Proofs.Compare.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.RPC_arg.
Require TezosOfOCaml.Proto_alpha.Proofs.Storage_description.
Require TezosOfOCaml.Environment.V8.Proofs.Blake2B.
Require TezosOfOCaml.Proto_alpha.Proofs.Sc_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Tx_rollup_repr.

The [compare] function is valid.

Lemma compare_is_valid :
  Compare.Valid.t (fun _ ⇒ True) id Bond_id_repr.compare.
Proof.
  simpl.
  apply (Compare.equality (
    let proj_sc_rollup_bond_id x :=
      match x with
      | Bond_id_repr.Sc_rollup_bond_id x ⇒ Some x
      | _ ⇒ None
      end in
    let proj_tx_rollup_bond_id x :=
      match x with
      | Bond_id_repr.Tx_rollup_bond_id x ⇒ Some x
      | _ ⇒ None
      end in
    let proj x :=
      (proj_sc_rollup_bond_id x, proj_tx_rollup_bond_id x) in
    Compare.projection proj (
      Compare.lexicographic
        (Compare.Option.compare Sc_rollup_repr.Address.compare)
        (Compare.Option.compare Tx_rollup_repr.compare)
      )
  )); [intros [] []; cbn; hauto lq: on |].
  Compare.valid_auto.
  sauto q: on.
Qed.
#[global] Hint Resolve compare_is_valid : Compare_db.

The [encoding] is valid.

Lemma encoding_is_valid :
  Data_encoding.Valid.t (fun _ ⇒ True) Bond_id_repr.encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.

Module Helper.
  Import Bond_id_repr.
  #[bypass_check(guard)]
  Definition starts_with (prefix : string) (s_value : string) : bool :=
    let len_s : int :=
      String.length s_value
    in let len_pre : int :=
      String.length prefix in
    let fix aux (i_value : int) {struct i_value} : bool :=
      if i_value =i len_pre then
        true
      else
        if
          Compare.Char.(Compare.S.op_ltgt) (String.get s_value i_value)
            (String.get prefix i_value)
        then
          false
        else
          aux (i_value +i 1) in
    (len_s ≥i len_pre) && (aux 0).

  Definition rpc_arg' : RPC_arg.arg t :=
    let construct (function_parameter : t) : string :=
      match function_parameter with
      | Tx_rollup_bond_id id ⇒ Tx_rollup_repr.to_b58check id
      | Sc_rollup_bond_id id ⇒ Sc_rollup_repr.Address.to_b58check id
      end in
    let destruct (id : string) : Pervasives.result t string :=
      if starts_with
           Tx_rollup_prefixes.rollup_address.(Tx_rollup_prefixes.t.prefix) id
      then
        match Tx_rollup_repr.of_b58check_opt id with
        | Some id ⇒ Result.ok (Tx_rollup_bond_id id)
        | None ⇒ Result.error_value "Cannot parse transaction rollup id"
        end
      else
        if starts_with Sc_rollup_repr.Address.prefix id then
          match Sc_rollup_repr.Address.of_b58check_opt id with
          | Some id ⇒ Result.ok (Sc_rollup_bond_id id)
          | None ⇒ Result.error_value "Cannot parse smart contract rollup id"
          end
        else
          Result.error_value "Cannot parse rollup id" in
    RPC_arg.make (Some "A bond identifier.") "bond_id" destruct construct tt.

  Fact rpc_arg_equal : rpc_arg = rpc_arg'.
  Proof.
    trivial.
  Qed.

  Module Tx_rollup_repr.
    (* TODO: prove if possible *)
    Axiom starts_with : ∀ v,
      starts_with
        Tx_rollup_prefixes.rollup_address.(Tx_rollup_prefixes.t.prefix)
        (Tx_rollup_repr.to_b58check v) = true.
  End Tx_rollup_repr.

  Module Sc_rollup_repr.
    Module Address.
      (* TODO: prove if possible *)
      Axiom starts_with_tx : ∀ v,
        starts_with
          Tx_rollup_prefixes.rollup_address.(Tx_rollup_prefixes.t.prefix)
          (Sc_rollup_repr.Address.to_b58check v) = false.

      (* TODO: prove if possible *)
      Axiom starts_with : ∀ v,
        starts_with Sc_rollup_repr.Address.prefix
          (Sc_rollup_repr.Address.to_b58check v) = true.
    End Address.
  End Sc_rollup_repr.
End Helper.

The [rpc_arg] is valid.

Lemma rpc_arg_is_valid : RPC_arg.Valid.t (fun _ ⇒ True) Bond_id_repr.rpc_arg.
Proof.
  rewrite Helper.rpc_arg_equal.
  constructor.
  { intros [] [].
    { unfold Helper.rpc_arg'.
      simpl.
      rewrite Helper.Tx_rollup_repr.starts_with.
      rewrite Tx_rollup_repr.of_b58_opt_to_b58_eq.
      reflexivity.
    }
    { unfold Helper.rpc_arg'.
      simpl.
      rewrite Helper.Sc_rollup_repr.Address.starts_with_tx.
      rewrite Helper.Sc_rollup_repr.Address.starts_with.
      rewrite Sc_rollup_repr.Address.of_b58_opt_to_b58_eq.
      reflexivity.
    }
  }
  { simpl.
    intros s.
    pose proof (Tx_rollup_repr.to_b58_opt_of_b58_eq s).
    pose proof (Sc_rollup_repr.Address.to_b58_opt_of_b58_eq s).
    destruct Tx_rollup_repr.of_b58check_opt;
    destruct Sc_rollup_repr.Address.of_b58check_opt;
    destruct Helper.starts_with; simpl; trivial;
    destruct Helper.starts_with; simpl; trivial.
  }
Qed.

The path encoding part of the [Index] is valid.

Lemma index_path_encoding_is_valid :
  Path_encoding.S.Valid.t
    (Storage_description.INDEX.to_Path Bond_id_repr.Index).
Proof.
  constructor; simpl;
    unfold Bond_id_repr.Index.to_path, Bond_id_repr.Index.of_path;
    intros.
  { now step. }
  { unfold Binary.to_bytes_exn; simpl.
    pose proof (Data_encoding.Valid.of_bytes_opt_to_bytes_opt
      encoding_is_valid v) as H_of_to_bytes.
    destruct Binary.to_bytes_opt eqn:H_binary_to_bytes_eq; [|tauto].
    destruct Hex.of_bytes eqn:H_hex_of_bytes_eq.
    rewrite <- H_hex_of_bytes_eq.
    rewrite Hex.to_bytes_of_bytes.
    rewrite <- H_binary_to_bytes_eq.
    destruct Binary.to_bytes_opt; simpl; hauto lq: on.
  }
  { repeat (destruct path; simpl; trivial).
    pose proof (Hex.of_bytes_to_bytes (Hex.Hex s)) as H_hex.
    destruct Hex.to_bytes; simpl; [|exact I].
    pose proof (Data_encoding.Valid.to_bytes_opt_of_bytes_opt
      encoding_is_valid b) as H_encoding.
    destruct Binary.of_bytes_opt; [|exact I].
    unfold Binary.to_bytes_exn.
    hauto lq: on.
  }
  { now step. }
Qed.

The [Index] is valid.

Lemma Index_is_valid :
  Storage_description.INDEX.Valid.t (fun _ ⇒ True) Bond_id_repr.Index.
Proof.
  constructor.
  { apply index_path_encoding_is_valid. }
  { apply rpc_arg_is_valid. }
  { apply encoding_is_valid. }
  { apply compare_is_valid. }
Qed.

Module Index.

The [compare] function is valid.

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