Skip to main content

🥷 Sapling_services.v

Proofs

See code, Gitlab , OCaml

The definition of a valid [diff_query].
  Module Valid.
    Import Sapling_services.diff_query.

    Record t (q : Sapling_services.diff_query) : Prop := {
      offset_commitment :
        Option.Forall Int64.Valid.non_negative q.(offset_commitment);
      offset_nullifier :
        Option.Forall Int64.Valid.non_negative q.(offset_nullifier);
    }.
  End Valid.
End Diff_query.

Module S.
  Module Args.
The query [get_diff_query] is valid.
    Lemma get_diff_query_is_valid :
      RPC_query.Valid.t Diff_query.Valid.t
        Sapling_services.S.Args.get_diff_query.
    Proof.
      RPC_query.valid_auto.
    Qed.

The encoding [Args.encoding] is valid.
    Lemma encoding_is_valid :
      Data_encoding.Valid.t (fun _True) Sapling_services.S.Args.encoding.
    Proof.
      Data_encoding.Valid.data_encoding_auto.
    Qed.
    #[global] Hint Resolve encoding_is_valid : Data_encoding_db.
  End Args.

The [get_diff] service is valid.
  Lemma get_diff_is_valid :
    RPC_service.Valid.t Diff_query.Valid.t (fun _True) (fun _True)
      (fst (Sapling_services.S.get_diff)).
  Proof.
    RPC_service.rpc_auto.
  Qed.
End S.