Skip to main content

🥷 Sapling_services.v


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

The encoding [Args.encoding] is valid.
    Lemma encoding_is_valid :
      Data_encoding.Valid.t (fun _True) Sapling_services.S.Args.encoding.
    #[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)).
End S.