🔫 Bond_id_repr.v

Proofs

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 x :=
      let 'Bond_id_repr.Tx_rollup_bond_id x := x in
    x in
    Compare.projection proj Tx_rollup_repr.compare
  )); [sauto lq: on rew: off|].
  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.

The [rpc_arg] is valid.

Lemma rpc_arg_is_valid : RPC_arg.Valid.t (fun _ ⇒ True) Bond_id_repr.rpc_arg.
Proof.
  constructor.
  { intros [] [].
    unfold Bond_id_repr.rpc_arg.
    simpl.
    rewrite Tx_rollup_repr.of_b58_to_b58_eq.
    reflexivity.
  }
  { simpl.
    intros s.
    pose proof (Tx_rollup_repr.to_b58_of_b58_eq s).
    destruct Tx_rollup_repr.of_b58check; 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; trivial).
    pose proof (Hex.of_bytes_to_bytes (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.
    rewrite H_encoding.
    now rewrite H_hex.
  }
  { 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.