vblt.org
forked from
gazagnaire.org/irmin
Persistent store with Git semantics: lazy reads, delayed writes, content-addressing
1(** Merkle proofs for content-addressed trees.
2
3 Proofs are sparse trees where unvisited paths are replaced by their hash
4 ("blinded"). They allow verification of computations without full tree
5 access.
6
7 {[
8 (* Producer has full tree access *)
9 let proof, result = Proof.produce store tree (fun t ->
10 let v = Tree.find t ["foo"; "bar"] in
11 (t, v))
12
13 (* Verifier only needs the proof *)
14 match Proof.verify proof (fun t ->
15 let v = Tree.find t ["foo"; "bar"] in
16 (t, v)) with
17 | Ok (_, v) -> (* v is trusted *)
18 | Error `Proof_mismatch -> (* invalid proof *)
19 ]}
20
21 Compatible with ATProto's MST proof format when using the MST codec. *)
22
23(** {1 Proof Trees} *)
24
25type 'hash kinded_hash = [ `Contents of 'hash | `Node of 'hash ]
26(** Hash tagged with its kind. *)
27
28(** Sparse tree with blinded (hash-only) subtrees. *)
29type ('hash, 'contents) tree =
30 | Contents of 'contents
31 | Blinded_contents of 'hash
32 | Node of ('hash, 'contents) node
33 | Blinded_node of 'hash
34
35and ('hash, 'contents) node = (string * ('hash, 'contents) tree) list
36(** Node entries, sorted by key. *)
37
38(** {1 Proofs} *)
39
40type ('hash, 'contents) t
41(** A Merkle proof with before/after state hashes. *)
42
43val v :
44 before:'hash kinded_hash ->
45 after:'hash kinded_hash ->
46 ('hash, 'contents) tree ->
47 ('hash, 'contents) t
48(** [v ~before ~after tree] creates a proof that state changed from [before] to
49 [after], with [tree] containing the minimal data needed to verify. *)
50
51val before : ('hash, _) t -> 'hash kinded_hash
52(** [before p] is the root hash before the computation. *)
53
54val after : ('hash, _) t -> 'hash kinded_hash
55(** [after p] is the root hash after the computation. *)
56
57val state : ('hash, 'contents) t -> ('hash, 'contents) tree
58(** [state p] is the sparse tree proving the computation. *)
59
60val pp :
61 (Format.formatter -> 'hash -> unit) ->
62 (Format.formatter -> 'contents -> unit) ->
63 Format.formatter ->
64 ('hash, 'contents) t ->
65 unit
66(** [pp pp_hash pp_contents fmt p] pretty-prints a proof. *)
67
68(** {1 Producing and Verifying Proofs}
69
70 These operations are parameterized by a codec for hashing. *)
71
72module Make (C : Codec.S) : sig
73 type hash = C.hash
74 type contents = string
75
76 module Tree : sig
77 type t
78 (** Proof-aware tree that records accesses during [produce]. *)
79
80 val find : t -> string list -> contents option
81 (** [find t path] returns the contents at [path], or [None] if not found. *)
82
83 val find_tree : t -> string list -> t option
84 (** [find_tree t path] returns the subtree at [path], or [None] if not
85 found. *)
86
87 val mem : t -> string list -> bool
88 (** [mem t path] checks whether a value exists at [path]. *)
89
90 val list : t -> string list -> (string * [ `Node | `Contents ]) list
91 (** [list t path] returns the children of [path], each tagged as either a
92 node or contents. *)
93
94 val add : t -> string list -> contents -> t
95 (** [add t path contents] returns a new tree with contents added or updated
96 at [path]. *)
97
98 val add_tree : t -> string list -> t -> t
99 (** [add_tree t path subtree] returns a new tree with [subtree] grafted at
100 [path]. *)
101
102 val remove : t -> string list -> t
103 (** [remove t path] returns a new tree with the value at [path] removed. *)
104
105 val hash : t -> hash
106 (** [hash t] computes the root hash of the tree. *)
107 end
108
109 val produce :
110 hash Backend.t -> hash -> (Tree.t -> Tree.t * 'a) -> (hash, contents) t * 'a
111 (** [produce backend root_hash f] runs [f] on the tree at [root_hash],
112 recording all accesses. Returns a proof containing only accessed paths. *)
113
114 val verify :
115 (hash, contents) t ->
116 (Tree.t -> Tree.t * 'a) ->
117 (Tree.t * 'a, [ `Proof_mismatch of string ]) result
118 (** [verify proof f] replays [f] on the proof tree. Returns [Ok] if the result
119 tree's hash matches [after proof], [Error] otherwise. *)
120
121 val to_tree : (hash, contents) t -> Tree.t
122 (** [to_tree proof] converts a proof to a tree for inspection. *)
123
124 val hash_of_tree : (hash, contents) tree -> hash kinded_hash
125 (** [hash_of_tree t] computes the root hash of a proof tree. *)
126end
127
128module Git : module type of Make (Codec.Git)
129module Mst : module type of Make (Codec.Mst)