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
60(** {1 Producing and Verifying Proofs}
61
62 These operations are parameterized by a codec for hashing. *)
63
64module Make (C : Codec.S) : sig
65 type hash = C.hash
66 type contents = string
67
68 module Tree : sig
69 type t
70 (** Proof-aware tree that records accesses during [produce]. *)
71
72 val find : t -> string list -> contents option
73 val find_tree : t -> string list -> t option
74 val mem : t -> string list -> bool
75 val list : t -> string list -> (string * [ `Node | `Contents ]) list
76 val add : t -> string list -> contents -> t
77 val add_tree : t -> string list -> t -> t
78 val remove : t -> string list -> t
79 val hash : t -> hash
80 end
81
82 val produce :
83 hash Backend.t -> hash -> (Tree.t -> Tree.t * 'a) -> (hash, contents) t * 'a
84 (** [produce backend root_hash f] runs [f] on the tree at [root_hash],
85 recording all accesses. Returns a proof containing only accessed paths. *)
86
87 val verify :
88 (hash, contents) t ->
89 (Tree.t -> Tree.t * 'a) ->
90 (Tree.t * 'a, [ `Proof_mismatch of string ]) result
91 (** [verify proof f] replays [f] on the proof tree. Returns [Ok] if the result
92 tree's hash matches [after proof], [Error] otherwise. *)
93
94 val to_tree : (hash, contents) t -> Tree.t
95 (** [to_tree proof] converts a proof to a tree for inspection. *)
96
97 val hash_of_tree : (hash, contents) tree -> hash kinded_hash
98 (** [hash_of_tree t] computes the root hash of a proof tree. *)
99end
100
101module Git : module type of Make (Codec.Git)
102module Mst : module type of Make (Codec.Mst)