package irmin

  1. Overview
  2. Docs
package irmin
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file proof_intf.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
(*
 * Copyright (c) 2013-2022 Thomas Gazagnaire <thomas@gazagnaire.org>
 *
 * Permission to use, copy, modify, and distribute this software for any
 * purpose with or without fee is hereby granted, provided that the above
 * copyright notice and this permission notice appear in all copies.
 *
 * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
 * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
 * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
 * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
 * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
 * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
 * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 *)

module type S = sig
  (** Proofs are compact representations of trees which can be shared between
      peers.

      This is expected to be used as follows:

      - A first peer runs a function [f] over a tree [t]. While performing this
        computation, it records: the hash of [t] (called [before] below), the
        hash of [f t] (called [after] below) and a subset of [t] which is needed
        to replay [f] without any access to the first peer's storage. Once done,
        all these informations are packed into a proof of type [t] that is sent
        to the second peer.

      - The second peer generates an initial tree [t'] from [p] and computes
        [f t']. Once done, it compares [t']'s hash and [f t']'s hash to [before]
        and [after]. If they match, they know that the result state [f t'] is a
        valid context state, without having to have access to the full storage
        of the first peer. *)

  type contents
  type hash
  type step
  type metadata

  type kinded_hash = [ `Contents of hash * metadata | `Node of hash ]
  [@@deriving irmin]

  type 'a inode = { length : int; proofs : (int * 'a) list } [@@deriving irmin]
  (** The type for (internal) inode proofs.

      These proofs encode large directories into a tree-like structure.

      Invariants are dependent on the backend.

      [length] is the total number of entries in the children of the inode. It's
      the size of the "flattened" version of that inode. [length] can be used to
      prove the correctness of operations such as [Tree.length] and
      [Tree.list ~offset ~length] in an efficient way.

      [proofs] contains the children proofs. It is a sparse list of ['a] values.
      These values are associated to their index in the list, and the list is
      kept sorted in increasing order of indices. ['a] can be a concrete proof
      or a hash of that proof.

      {e For [irmin-pack]}: [proofs] have a length of at most [Conf.entries]
      entries. For binary trees, this boolean index is a step of the left-right
      sequence / decision proof corresponding to the path in that binary tree. *)

  type 'a inode_extender = { length : int; segments : int list; proof : 'a }
  [@@deriving irmin]
  (** The type for inode extenders.

      An extender is a compact representation of a sequence of [inode] which
      contain only one child. As for inodes, the ['a] parameter can be a
      concrete proof or a hash of that proof.

      If an inode proof contains singleton children [i_0, ..., i_n] such as:
      [{length=l; proofs = [ (i_0, {proofs = ... { proofs = [ (i_n, p) ] }})]}],
      then it is compressed into the inode extender
      [{length=l; segment = [i_0;..;i_n]; proof=p}] sharing the same length [l]
      and final proof [p]. *)

  (** The type for compressed and partial Merkle tree proofs.

      Tree proofs do not provide any guarantee with the ordering of
      computations. For instance, if two effects commute, they won't be
      distinguishable by this kind of proof.

      [Value v] proves that a value [v] exists in the store.

      [Blinded_value h] proves a value with hash [h] exists in the store.

      [Node ls] proves that a a "flat" node containing the list of files [ls]
      exists in the store. {e For [irmin-pack]}: the length of [ls] is at most
      [Conf.stable_hash];

      [Blinded_node h] proves that a node with hash [h] exists in the store.

      [Inode i] proves that an inode [i] exists in the store.

      [Extender e] proves that an inode extender [e] exist in the store. *)
  type tree =
    | Contents of contents * metadata
    | Blinded_contents of hash * metadata
    | Node of (step * tree) list
    | Blinded_node of hash
    | Inode of inode_tree inode
    | Extender of inode_tree inode_extender
  [@@deriving irmin]

  (** The type for inode trees. It is a subset of [tree], limited to nodes.

      [Blinded_inode h] proves that an inode with hash [h] exists in the store.

      [Inode_values ls] is simliar to trees' [Node].

      [Inode_tree i] is similar to tree's [Inode].

      [Inode_extender e] is similar to trees' [Extender]. *)
  and inode_tree =
    | Blinded_inode of hash
    | Inode_values of (step * tree) list
    | Inode_tree of inode_tree inode
    | Inode_extender of inode_tree inode_extender
  [@@deriving irmin]

  type t [@@deriving irmin]
  (** The type for Merkle proofs.

      A proof [p] proves that the state advanced from [before p] to [after p].
      [state p]'s hash is [before p], and [state p] contains the minimal
      information for the computation to reach [after p]. *)

  val v : before:kinded_hash -> after:kinded_hash -> tree -> t
  (** [v ~before ~after p] proves that the state advanced from [before] to
      [after]. [p]'s hash is [before], and [p] contains the minimal information
      for the computation to reach [after]. *)

  val before : t -> kinded_hash
  (** [before t] it the state's hash at the beginning of the computation. *)

  val after : t -> kinded_hash
  (** [after t] is the state's hash at the end of the computation. *)

  val state : t -> tree
  (** [state t] is a subset of the initial state needed to prove that the proven
      computation could run without performing any I/O. *)
end

(** Environment that tracks side effects during the production/consumption of
    proofs.

    {1 The Merkle Proof Construction Algorithm}

    This description stands for [Set] proofs and assumes that the large nodes
    are represented by the backend as a tree structure (i.e. inodes).

    There are 4 distinct phases when working with Irmin's merkle proofs:
    [Produce | Serialise | Deserialise | Consume].

    {2 [Produce]}

    This phase runs the [f] function provided by the Irmin user. It builds an
    [after] tree from a [before] tree that has been setup with an [Env] that
    records every backend reads into two hash tables.

    During the next phase (i.e. [Serialise]) the cleared [before] tree will be
    traversed from root to stems only following the paths that are referenced in
    [Env].

    In practice [Env] doesn't exactly record the reads, it keeps track of all
    the [hash -> backend node] and [hash -> backend contents] mappings that are
    directly output of the backend stores through [P.Node.find] and
    [P.Contents.find]. This is obviously enough to remember the contents, the
    nodes and the inodes tips, but the inner inodes are not directly referenced
    in the hash tables.

    The inner inodes are in fact referenced in their inode tip which is itself
    referenced in [Env]'s hash tables. Since an inode shares its lazy pointers
    with the inodes derived from it, even the inner inodes that are loaded from
    the derived tips will be available from the original inode tip.

    {2 [Serialise]}

    In this phase, the [Env] contains everything necessary for the computation
    of a Merkle proof from a cleared [before]. The [Env] now affects
    [Node.cached_value] and [Contents.cached_value] allowing for the discovery
    of the cached closure.

    {2 [Deserialise]}

    In this phase the [Env] is filled by recursively destructing the proof and
    filling it before the [Consume] phase.

    {2 [Consume]}

    In this last phase the [Env] is again made accessible through
    [Node.cached_pvalue] and [Contents.cached_pvalue], making it possible for
    the user to reference by [hash] everything that was contained in the proof.

    {1 Nodes and Portable Nodes}

    While the [Produce] phase must be connected to the backend to records reads,
    the [Consume] phase must be disconnected from the backend.

    [Produce] manipulates backend nodes of type [Backend.Node.Val.t] (the ones
    enriched with backend keys)

    [Consume] is restricted to manipulating nodes of type
    [Backend.Node_portable.t]. *)
module type Env = sig
  type mode = Produce | Serialise | Deserialise | Consume
  type t [@@deriving irmin]
  type hash
  type node
  type pnode
  type contents

  val is_empty : t -> bool
  val empty : unit -> t
  val copy : into:t -> t -> unit

  (** {2 Modes} *)

  val set_mode : t -> mode -> unit

  val with_produce :
    (t -> start_serialise:(unit -> unit) -> 'a Lwt.t) -> 'a Lwt.t

  val with_consume :
    (t -> stop_deserialise:(unit -> unit) -> 'a Lwt.t) -> 'a Lwt.t

  (** {2 Interactions With [Tree]} *)

  val add_contents_from_store : t -> hash -> contents -> unit

  val add_node_from_store : t -> hash -> node -> node
  (** [add_node_from_store] returns a [node] and not [unit] because [Env] may
      take the opportunity to wrap the input node in [Node.Val.with_handler]. *)

  val add_contents_from_proof : t -> hash -> contents -> unit
  val add_pnode_from_proof : t -> hash -> pnode -> unit
  val find_contents : t -> hash -> contents option
  val find_node : t -> hash -> node option
  val find_pnode : t -> hash -> pnode option
end

module type Proof = sig
  module type S = S
  module type Env = Env

  exception Bad_proof of { context : string }

  val bad_proof_exn : string -> 'a

  module Make
      (C : Type.S)
      (H : Hash.S)
      (P : sig
        type step [@@deriving irmin]
      end)
      (M : Type.S) : sig
    include
      S
        with type contents := C.t
         and type hash := H.t
         and type step := P.step
         and type metadata := M.t
  end

  module Env
      (B : Backend.S)
      (P : S
             with type contents := B.Contents.Val.t
              and type hash := B.Hash.t
              and type step := B.Node.Val.step
              and type metadata := B.Node.Val.metadata) :
    Env
      with type hash := B.Hash.t
       and type contents := B.Contents.Val.t
       and type node := B.Node.Val.t
       and type pnode := B.Node_portable.t
end
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct