1	# lock/lock: the lock document. What a package is (its source and its files),
2	# where the ledger says each package comes from, the imports a package's
3	# sources name, and the text of ez.lock.toml, written and read back. Nix reads
4	# the lock and fetches each file as a fixed-output derivation, so `bend` never
5	# touches the network inside the sandbox.
6	#
7	# A package resolves from the hub, or, when it was vendored from a repo that
8	# never published, from the git rev recorded for it. Both end up as the same
9	# BEND_LIB tree. ez.toml is the only record of where a package comes from.
10	#
11	# Everything here is pure. Deciding the lock is lock/plan.bend's, over the
12	# World lock/world.bend describes, and reading and writing are
13	# lock/run.bend's. `ez fetch` reads a lock back in fetch/plan.bend.
14	import Base
15	import ../toml/toml.bend as T
16	import ../ledger/manifest.bend as M
17	import ../pkg/pkg.bend as K
18	
19	# where a package's bytes come from. A hub package needs nothing else; a git
20	# one pins a commit, the entry its hash was computed from, the directory inside
21	# the checkout its paths are written from, and the NAR hash nix rebuilds it by.
22	type Src is Data:
23	  Hub{}
24	  Git{url: String, rev: String, entry: String, root: String, nar: String, tag: String}
25	
26	# a package the lock records
27	type Pack is Data:
28	  Pack{hash: String, src: Src, files: List<&2, K.Item>}
29	
30	# a package's origin, as ez.toml records it
31	type Origin is Data:
32	  Origin{hash: String, src: Src}
33	
34	# a `<name>@<version>` and the `0x` name it names. The hub rules that a
35	# version never moves (EZ-TRUST-6), so once a name has named a hash the pair
36	# is a fact, and the lock records it under `[names]` beside the package it
37	# names, which is recorded under its hash like any hub package.
38	type Name is Data:
39	  Name{nv: String, hash: String}
40	
41	# the `0x` name an import carries, which is everything before its first `/`
42	def spec.hash(spec: String) -> String:
43	  K.word(String.split(spec, '/'), 0n)
44	
45	# an import's package, or nothing when it names a module of this project
46	def spec.put(+spec: String) -> List<&2, String>:
47	  Bool.pick(List<&2, String>, K.is_hub(spec), [spec.hash(spec)], [])
48	
49	# every package a list of imports names
50	def specs(ms: List<&2, String>) -> List<&2, String>:
51	  match ms:
52	    case []:
53	      []
54	    case h <> t:
55	      List.append(&2, String, spec.put(h), specs(t))
56	
57	# every package the sources of one package import
58	def kids(srcs: List<&2, String>) -> List<&2, String>:
59	  match srcs:
60	    case []:
61	      []
62	    case h <> t:
63	      List.append(&2, String, specs(K.scan.mods(K.scan(h))), kids(t))
64	
65	# an import's `<name>@<version>`, or nothing when it names no package by
66	# name. A named import is a dependency, never a module of this project
67	# (EZ-HUB-3), whether or not the hub rules its name in.
68	def named.put(+spec: String) -> List<&2, String>:
69	  +nv = K.named.of(spec)
70	  Bool.pick(List<&2, String>, String.is_empty(nv), [], [nv])
71	
72	# every name a list of imports names
73	def named(ms: List<&2, String>) -> List<&2, String>:
74	  match ms:
75	    case []:
76	      []
77	    case h <> t:
78	      List.append(&2, String, named.put(h), named(t))
79	
80	# every name the sources of one package import
81	def kids.named(srcs: List<&2, String>) -> List<&2, String>:
82	  match srcs:
83	    case []:
84	      []
85	    case h <> t:
86	      List.append(&2, String, named(K.scan.mods(K.scan(h))), kids.named(t))
87	
88	# the hash this name names when it is the one looked for, otherwise the
89	# rest's. The rest arrives as a thunk, so the first hit ends the scan.
90	def name.at(hit: Bool, hash: String, rest: Unit -> String) -> String:
91	  match hit:
92	    case True{}:
93	      hash
94	    case False{}:
95	      rest(Unit{})
96	
97	# the hash a table of names gives a name, the first it records for it, or ""
98	# when it records none
99	def name.find(ns: List<&2, Name>, +nv: String) -> String:
100	  match ns:
101	    case []:
102	      ""
103	    case Name{+n, h} <> t:
104	      name.at(String.eq(n, nv), h, _u => name.find(t, nv))
105	
106	# a name's hash, or nothing when the table does not resolve it
107	def name.put(+hash: String) -> List<&2, String>:
108	  Bool.pick(List<&2, String>, String.is_empty(hash), [], [hash])
109	
110	# the hashes a table gives a list of names, leaving out the ones it does not
111	# resolve
112	def name.hashes(+ns: List<&2, Name>, nvs: List<&2, String>) -> List<&2, String>:
113	  match nvs:
114	    case []:
115	      []
116	    case +h <> t:
117	      List.append(&2, String, name.put(name.find(ns, h)), name.hashes(ns, t))
118	
119	# every package the sources of one package import, by hash and by a name the
120	# table resolves
121	def kids.in(+ns: List<&2, Name>, +srcs: List<&2, String>) -> List<&2, String>:
122	  List.append(&2, String, kids(srcs), name.hashes(ns, kids.named(srcs)))
123	
124	# a name with the hash the table gives it, or nothing when it gives none
125	def name.one(+nv: String, +hash: String) -> List<&2, Name>:
126	  Bool.pick(List<&2, Name>, String.is_empty(hash), [], [Name{nv, hash}])
127	
128	# each name the table resolves, with its hash; one it does not is left out
129	def name.pairs(+ns: List<&2, Name>, nvs: List<&2, String>) -> List<&2, Name>:
130	  match nvs:
131	    case []:
132	      []
133	    case +h <> t:
134	      List.append(&2, Name, name.one(h, name.find(ns, h)), name.pairs(ns, t))
135	
136	# whether a hash is a package's `0x` name as bend reads one out of a names
137	# file: `0x` and 32 lowercase hex digits
138	def hex.char(+ch: Char) -> Bool:
139	  +x = Char.to_u32(ch)
140	  Bool.or(Char.is_digit(ch), Bool.and(U32.is_ge(x, 97), U32.is_le(x, 102)))
141	
142	def hex.all(text: String) -> Bool:
143	  match text:
144	    case SNil{}:
145	      True{}
146	    case SCon{+h, t}:
147	      +rest = hex.all(t)
148	      Bool.and(hex.char(h), rest)
149	
150	def hash.ok(+hash: String) -> Bool:
151	  Bool.and(Nat.is_eq(String.length(hash), 34n),
152	    Bool.and(String.starts_with(hash, "0x"), hex.all(String.drop(hash, 2n))))
153	
154	# the text of the file bend reads a name's hash from, `$BEND_LIB/names/<nv>`
155	def name.text(+hash: String) -> String:
156	  hash ++ "\n"
157	
158	# a name kept when the hub rules it in and it names a `0x` hash, since that
159	# is the only pair bend would read back
160	def name.valid(name: Name) -> Bool:
161	  Name{+nv, +hash} = name
162	  Bool.and(K.name.ok(nv), hash.ok(hash))
163	
164	def names.valid.pick(ok: Bool, +name: Name, rest: List<&2, Name>) -> List<&2, Name>:
165	  match ok:
166	    case True{}:
167	      name <> rest
168	    case False{}:
169	      rest
170	
171	# the names of a list that bend would read back
172	def names.valid(ns: List<&2, Name>) -> List<&2, Name>:
173	  match ns:
174	    case []:
175	      []
176	    case +h <> t:
177	      names.valid.pick(name.valid(h), h, names.valid(t))
178	
179	# a table's path, as segments
180	def segs(sect: T.Sect) -> List<&2, String>:
181	  T.Sect{n, _ps} = sect
182	  T.segments(n)
183	
184	# whether a table's path is these three segments
185	def is3(+ss: List<&2, String>, first: String, second: String, third: String) -> Bool:
186	  Bool.and(Nat.is_eq(List.length(&2, String, ss), 3n),
187	    Bool.and(String.eq(K.word(ss, 0n), first),
188	      Bool.and(String.eq(K.word(ss, 1n), second), String.eq(K.word(ss, 2n), third))))
189	
190	# whether a table's path is one segment, this one
191	def named1(+ss: List<&2, String>, first: String) -> Bool:
192	  Bool.and(Nat.is_eq(List.length(&2, String, ss), 1n), String.eq(K.word(ss, 0n), first))
193	
194	# whether a table's path is three segments, headed and tailed by these, whatever
195	# the hash between them is
196	def named3(+ss: List<&2, String>, first: String, third: String) -> Bool:
197	  Bool.and(Nat.is_eq(List.length(&2, String, ss), 3n),
198	    Bool.and(String.eq(K.word(ss, 0n), first), String.eq(K.word(ss, 2n), third)))
199	
200	# the pairs of a table when it is the one asked for, otherwise the rest's
201	def at.pick(hit: Bool, sect: T.Sect, rest: List<&2, T.Kv>) -> List<&2, T.Kv>:
202	  match hit:
203	    case True{}:
204	      T.Sect{_n, ps} = sect
205	      ps
206	    case False{}:
207	      rest
208	
209	# the pairs of the table at this three segment path, or none
210	def at3(ss: List<&2, T.Sect>, +first: String, +second: String, +third: String) -> List<&2, T.Kv>:
211	  match ss:
212	    case []:
213	      []
214	    case +h <> t:
215	      at.pick(is3(segs(h), first, second, third), h, at3(t, first, second, third))
216	
217	# a git origin keeps every key it was written with; anything else is the hub
218	def src.go(git: Bool, +ps: List<&2, T.Kv>) -> Src:
219	  match git:
220	    case True{}:
221	      Git{T.value(ps, "url"), T.value(ps, "rev"), T.value(ps, "entry"),
222	        T.value(ps, "root"), T.value(ps, "narHash"), T.value(ps, "tag")}
223	    case False{}:
224	      Hub{}
225	
226	# where a table says a package's bytes come from
227	def src_of(+ps: List<&2, T.Kv>) -> Src:
228	  src.go(String.eq(T.value(ps, "kind"), "git"), ps)
229	
230	# a ledger's dependency as an origin: the repo and rev it names, or the hub.
231	# A hub dependency is recorded too, so that a package the ledger names is told
232	# apart from one it does not, which also resolves from the hub but is not
233	# vouched for by anything a clone has.
234	def ledger.put(git: Bool, +dep: M.Dep) -> List<&2, Origin>:
235	  match git:
236	    case True{}:
237	      [Origin{M.dep.hash(dep), Git{M.source.url(M.source.dep(dep)),
238	        M.source.rev(M.source.dep(dep)), M.dep.entry(dep),
239	        M.source.root(M.source.dep(dep)), M.source.nar(M.source.dep(dep)),
240	        M.source.tag(M.source.dep(dep))}}]
241	    case False{}:
242	      [Origin{M.dep.hash(dep), Hub{}}]
243	
244	# every origin a ledger's dependencies record, in the order written
245	def ledger.origins(ds: List<&2, M.Dep>) -> List<&2, Origin>:
246	  match ds:
247	    case []:
248	      []
249	    case +h <> t:
250	      List.append(&2, Origin,
251	        ledger.put(M.source.is_git(M.source.dep(h)), h), ledger.origins(t))
252	
253	# every origin a ledger records. A ledger that would not parse records none,
254	# so a broken ez.toml leaves the lock exactly where it was without a guess.
255	def ledger.read(parsed: M.Read) -> List<&2, Origin>:
256	  match parsed:
257	    case M.Bad{_why}:
258	      []
259	    case M.Good{m}:
260	      M.Manifest{_n, _e, _b, _h, _pa, _pv, ds, _ts} = m
261	      ledger.origins(ds)
262	
263	# a dependency's name, when the ledger records it by one
264	def ledger.name(+dep: M.Dep) -> List<&2, Name>:
265	  +nv = M.source.nv(M.source.dep(dep))
266	  Bool.pick(List<&2, Name>, String.is_empty(nv), [], [Name{nv, M.dep.hash(dep)}])
267	
268	# every name a ledger's dependencies record, each with the hash it named when
269	# it was added
270	def ledger.names.of(ds: List<&2, M.Dep>) -> List<&2, Name>:
271	  match ds:
272	    case []:
273	      []
274	    case +h <> t:
275	      List.append(&2, Name, ledger.name(h), ledger.names.of(t))
276	
277	# every name a ledger records. One that would not parse records none.
278	def ledger.names(parsed: M.Read) -> List<&2, Name>:
279	  match parsed:
280	    case M.Bad{_why}:
281	      []
282	    case M.Good{m}:
283	      M.Manifest{_n, _e, _b, _h, _pa, _pv, ds, _ts} = m
284	      ledger.names.of(ds)
285	
286	# this origin's source when the hash matches, otherwise whatever the rest gave
287	def origin.at(known: Origin, rest: Src, wanted: String) -> Src:
288	  Origin{n, s} = known
289	  Bool.pick(Src, String.eq(n, wanted), s, rest)
290	
291	# where a package comes from, which is the hub unless an origin says otherwise
292	def origin(ds: List<&2, Origin>, +wanted: String) -> Src:
293	  match ds:
294	    case []:
295	      Hub{}
296	    case x <> t:
297	      origin.at(x, origin(t, wanted), wanted)
298	
299	# the hash an origin is recorded under
300	def origin.hash(known: Origin) -> String:
301	  Origin{n, _s} = known
302	  n
303	
304	# one `<sha256> <path>` line of a manifest
305	def line.put(+ws: List<&2, String>) -> List<&2, K.Item>:
306	  Bool.pick(List<&2, K.Item>, Nat.is_eq(List.length(&2, String, ws), 2n),
307	    [K.Item{K.word(ws, 1n), K.word(ws, 0n)}], [])
308	
309	# every file a manifest names
310	def manifest.files(ls: List<&2, String>) -> List<&2, K.Item>:
311	  match ls:
312	    case []:
313	      []
314	    case h <> t:
315	      List.append(&2, K.Item, line.put(K.words(h)), manifest.files(t))
316	
317	# a url under the hub
318	def url_of(+hub: String, +hash: String, at: String) -> String:
319	  hub ++ "/" ++ hash ++ "/" ++ at
320	
321	# bend accepts any prefix of the sha256, and a package's `0x` name is the first
322	# 32 characters of its manifest's digest
323	def want(+hash: String) -> String:
324	  String.drop(hash, 2n)
325	
326	# why a fetched checkout is not the one the ledger pins, or "" when it is.
327	# The NAR hash is over the whole checkout, so a rev that no longer holds what
328	# it held when it was pinned is caught here, before anything is laid out. A
329	# ledger with no NAR hash has nothing to check the checkout against, and an
330	# unchecked tree is not one a lock may record.
331	def nar.why.go(none: Bool, same: Bool, +want: String, +got: String, +url: String, +rev: String) -> String:
332	  match none:
333	    case True{}:
334	      "ez: ez.toml records no narHash for " ++ url ++ " at " ++ rev ++
335	        ", so its tree cannot be checked; run `ez lock --upgrade` to pin it"
336	    case False{}:
337	      match same:
338	        case True{}:
339	          ""
340	        case False{}:
341	          "ez: " ++ url ++ " at " ++ rev ++ " has narHash " ++ got ++
342	            ", and ez.toml records " ++ want
343	
344	def nar.why(+want: String, +got: String, +url: String, +rev: String) -> String:
345	  nar.why.go(String.is_empty(want), String.eq(want, got), want, got, url, rev)
346	
347	# the hash a package is recorded under
348	def pack.hash(package: Pack) -> String:
349	  Pack{h, _s, _f} = package
350	  h
351	
352	# one step of a scan that is looking for one hit. Every scan in this file
353	# wants it, so it is stated once here.
354	#
355	# `Bool.or` is an ordinary function and reduces both of its sides, so a scan
356	# written with it reads the whole list even when the head answers. The rest of
357	# the scan arrives as a thunk, which is a value, and only the arm that wants
358	# it applies it; handed in as an ordinary argument it would be reduced before
359	# this def could decline it.
360	def any.step(here: Bool, rest: Unit -> Bool) -> Bool:
361	  match here:
362	    case True{}:
363	      True{}
364	    case False{}:
365	      rest(Unit{})
366	
367	# whether the ledger names a package. One it does not name still resolves from
368	# the hub, since the hub serves bytes by the hash they digest to, but when the
369	# hub does not have it there is nothing else to ask: nothing a clone has says
370	# where it came from, so the lock says that and stops.
371	def known(ds: List<&2, Origin>, +wanted: String) -> Bool:
372	  match ds:
373	    case []:
374	      False{}
375	    case x <> t:
376	      any.step(String.eq(origin.hash(x), wanted), _u => known(t, wanted))
377	
378	# whether a package is already resolved. The wanted hash is compared first,
379	# the way pkg's `fresh` compares a path, so a walk that passes over a hash it
380	# has is a walk whose hashes are distinct without a symmetry lemma.
381	def has(ds: List<&2, Pack>, +wanted: String) -> Bool:
382	  match ds:
383	    case []:
384	      False{}
385	    case x <> t:
386	      any.step(String.eq(wanted, pack.hash(x)), _u => has(t, wanted))
387	
388	# whether a name is already among the ones a walk has seen. Base's
389	# `List.contains` applies an erased equality, which Bend's termination check
390	# cannot see through; this scan is structural. `any.step` is what lets it
391	# stop at the name it was looking for instead of reading past it.
392	def seen.holds(xs: List<&2, String>, +needle: String) -> Bool:
393	  match xs:
394	    case []:
395	      False{}
396	    case +h <> t:
397	      any.step(String.eq(h, needle), _u => seen.holds(t, needle))
398	
399	# a key worth writing, or nothing at all when its value is empty, so an absent
400	# tag leaves no trace
401	def kv(key: String, +val: String) -> List<&2, T.Kv>:
402	  Bool.pick(List<&2, T.Kv>, String.is_empty(val), [], [T.Kv{key, val}])
403	
404	# the keys a source contributes to the lock
405	def src.pairs(source: Src) -> List<&2, T.Kv>:
406	  match source:
407	    case Hub{}:
408	      [T.Kv{"kind", "hub"}]
409	    case Git{url, rev, entry, root, nar, tag}:
410	      List.concat(&2, T.Kv,
411	        [[T.Kv{"kind", "git"}], kv("url", url), kv("rev", rev), kv("entry", entry),
412	         kv("root", root), kv("narHash", nar), kv("tag", tag)])
413	
414	# a file of a package as a `"<path>" = "<sha256>"` pair
415	def file.pair(item: K.Item) -> T.Kv:
416	  K.Item{at, sum} = item
417	  T.Kv{at, sum}
418	
419	# every file of a package, in path order
420	def file.pairs(fs: List<&2, K.Item>) -> List<&2, T.Kv>:
421	  match fs:
422	    case []:
423	      []
424	    case h <> t:
425	      file.pair(h) <> file.pairs(t)
426	
427	# the two tables a package is written as, from its files already in path
428	# order and each one once
429	def pack.sects.of(hash: String, src: Src, fs: List<&2, K.Item>) -> List<&2, T.Sect>:
430	  +at = "packages." ++ T.quote(hash)
431	  [T.Sect{at ++ ".source", src.pairs(src)},
432	   T.Sect{at ++ ".files", file.pairs(fs)}]
433	
434	# the two tables a package is written as
435	def pack.sects(package: Pack) -> List<&2, T.Sect>:
436	  Pack{hash, src, files} = package
437	  pack.sects.of(hash, src, K.files_of(files))
438	
439	# every package, in hash order
440	def pack.all(ps: List<&2, Pack>) -> List<&2, T.Sect>:
441	  match ps:
442	    case []:
443	      []
444	    case h <> t:
445	      List.append(&2, T.Sect, pack.sects(h), pack.all(t))
446	
447	# packages are written in hash order, so a lock is the same text however it was
448	# resolved
449	def pack.le(left: Pack, right: Pack) -> Bool:
450	  String.is_le(pack.hash(left), pack.hash(right))
451	
452	# where a package goes among the packages already in order. The rest of the
453	# insertion is a parameter, because two defs that call each other are not
454	# allowed.
455	def pack.ins.put(le: Bool, item: Pack, head: Pack, tail: List<&2, Pack>, rest: List<&2, Pack>) -> List<&2, Pack>:
456	  match le:
457	    case True{}:
458	      item <> (head <> tail)
459	    case False{}:
460	      head <> rest
461	
462	# a package inserted into a list already in hash order
463	def pack.ins(ps: List<&2, Pack>, +item: Pack) -> List<&2, Pack>:
464	  match ps:
465	    case []:
466	      [item]
467	    case Con{+h, +t}:
468	      pack.ins.put(pack.le(item, h), item, h, t, pack.ins(t, item))
469	
470	# the packages in hash order. Insertion rather than Base's `List.sort`: that
471	# one is a fuelled bottom-up merge sort, whose recursion Bend cannot check, so
472	# it is reported as unsafe and every proof downstream of it inherits the
473	# report. An insertion sort shrinks its list at every step, so Bend checks it,
474	# and a lock names tens of packages, not thousands.
475	def pack.sort(ps: List<&2, Pack>) -> List<&2, Pack>:
476	  match ps:
477	    case []:
478	      []
479	    case Con{+h, t}:
480	      pack.ins(pack.sort(t), h)
481	
482	# the `[lock]` table: what resolved the lock. The bend that ran the lock is
483	# not recorded: it is not something a clone has, and the flake pins the bend
484	# a build uses. A lock written before this that records one still reads,
485	# since nothing reads the key.
486	def lock.sect(hub: String) -> T.Sect:
487	  T.Sect{"lock", [T.Kv{"version", "2"}, T.Kv{"hub", hub}]}
488	
489	# the lock as a document: what resolved it, then every package it resolved,
490	# in hash order. `render` writes its text a block at a time; that the two
491	# agree is lock/LAWS.bend's `render_is_doc`.
492	def doc(hub: String, ps: List<&2, Pack>) -> List<&2, T.Sect>:
493	  List.append(&2, T.Sect, [lock.sect(hub)], pack.all(pack.sort(ps)))
494	
495	# a package's two tables as one block of text, filed under its hash. The lock
496	# puts packages in hash order by sorting these blocks with `K.file.sort`,
497	# whose order-independence pkg proves; a second sort over packages would need
498	# that proof again, and Bend's function values are linear, so one sort by a
499	# key function applied at every comparison cannot be written. A block's path
500	# is its package's hash, so distinct hashes are distinct paths.
501	def pack.block(package: Pack) -> K.Item:
502	  Pack{+hash, src, files} = package
503	  K.Item{hash, T.render(pack.sects.of(hash, src, K.files_of(files)))}
504	
505	# every package, as its block
506	def pack.blocks(ps: List<&2, Pack>) -> List<&2, K.Item>:
507	  match ps:
508	    case []:
509	      []
510	    case h <> t:
511	      pack.block(h) <> pack.blocks(t)
512	
513	# the text of every block, in the order given
514	def block.texts(bs: List<&2, K.Item>) -> List<&2, String>:
515	  match bs:
516	    case []:
517	      []
518	    case K.Item{_hash, text} <> t:
519	      text <> block.texts(t)
520	
521	# the lock's text: the `[lock]` table, each block in the order given, then the
522	# rest, assembled as ez's document text (`T.render`) and written as eztoml
523	# writes it (`T.normal`). Every part of it is fixed by the blocks' order, so
524	# the order the walk found packages in does not reach the file (EZ-DOC-2).
525	def text.of(hub: String, bs: List<&2, K.Item>, rest: List<&2, String>) -> String:
526	  T.normal(String.join(T.render.sect(lock.sect(hub)) <>
527	    List.append(&2, String, block.texts(bs), rest), "\n"))
528	
529	# the lock as the text written to ez.lock.toml, its packages in hash order
530	def render(hub: String, ps: List<&2, Pack>) -> String:
531	  text.of(hub, K.file.sort(pack.blocks(ps)), [])
532	
533	# the keys a pinned CLI contributes. The same names a `[tools.*]` section
534	# uses in ez.toml, and not the `[packages.*]` source table.
535	def tool.pairs(+entry: String, +binary: String, source: M.Source) -> List<&2, T.Kv>:
536	  match source:
537	    case M.Hub{_named}:
538	      List.concat(&2, T.Kv, [kv("entry", entry), kv("bin", binary)])
539	    case M.Git{url, rev, tag, root, nar, _vend}:
540	      List.concat(&2, T.Kv,
541	        [kv("git", url), kv("rev", rev), kv("tag", tag), kv("root", root),
542	         kv("narHash", nar), kv("entry", entry), kv("bin", binary)])
543	
544	# one `[tools.<name>]` table
545	def tool.sect(pin: M.Tool) -> T.Sect:
546	  M.Tool{n, e, b, s} = pin
547	  T.Sect{"tools." ++ n, tool.pairs(e, b, s)}
548	
549	# every pinned CLI, in the order the ledger holds them
550	def tool.sects(ts: List<&2, M.Tool>) -> List<&2, T.Sect>:
551	  match ts:
552	    case []:
553	      []
554	    case h <> t:
555	      tool.sect(h) <> tool.sects(t)
556	
557	# the lock with its tools after the packages. An empty tool list adds no
558	# table, so a ledger with no tools writes the lock `render` writes.
559	def render.tools(ts: List<&2, M.Tool>, hub: String, ps: List<&2, Pack>) -> String:
560	  text.of(hub, K.file.sort(pack.blocks(ps)), T.render.all(tool.sects(ts)))
561	
562	# a name as the pair the `[names]` table writes it as, which is the shape a
563	# file of a package is written in: its `<name>@<version>` as a quoted key and
564	# its hash as the value
565	def name.file(name: Name) -> K.Item:
566	  Name{nv, hash} = name
567	  K.Item{nv, hash}
568	
569	# every name, so
570	def name.files(ns: List<&2, Name>) -> List<&2, K.Item>:
571	  match ns:
572	    case []:
573	      []
574	    case h <> t:
575	      name.file(h) <> name.files(t)
576	
577	# the `[names]` table: every name the lock resolved, in name order and each
578	# once, sorted and deduplicated the way a package's files are. A lock that
579	# resolved no name has no such table, so a project with no named import
580	# locks to the text it always did.
581	def names.sects(ns: List<&2, Name>) -> List<&2, T.Sect>:
582	  match ns:
583	    case []:
584	      []
585	    case +h <> +t:
586	      [T.Sect{"names", file.pairs(K.files_of(name.files(h <> t)))}]
587	
588	# the lock with its names and then its tools after the packages
589	def render.names(ns: List<&2, Name>, ts: List<&2, M.Tool>, hub: String, ps: List<&2, Pack>) -> String:
590	  text.of(hub, K.file.sort(pack.blocks(ps)),
591	    T.render.all(List.append(&2, T.Sect, names.sects(ns), tool.sects(ts))))
592	
593	# the same, told whether the tool list is empty
594	def render.pick(empty: Bool, hub: String, ps: List<&2, Pack>, ts: List<&2, M.Tool>) -> String:
595	  match empty:
596	    case True{}:
597	      render(hub, ps)
598	    case False{}:
599	      render.tools(ts, hub, ps)
600	
601	# the `[lock]` table of a lock that was read
602	def lock.pairs(ss: List<&2, T.Sect>) -> List<&2, T.Kv>:
603	  match ss:
604	    case []:
605	      []
606	    case +h <> t:
607	      at.pick(named1(segs(h), "lock"), h, lock.pairs(t))
608	
609	# the hub a lock was resolved against
610	def lock.hub(ss: List<&2, T.Sect>) -> String:
611	  T.value(lock.pairs(ss), "hub")
612	
613	# the `[names]` table of a lock that was read
614	def names.pairs(ss: List<&2, T.Sect>) -> List<&2, T.Kv>:
615	  match ss:
616	    case []:
617	      []
618	    case +h <> t:
619	      at.pick(named1(segs(h), "names"), h, names.pairs(t))
620	
621	# a pair of the `[names]` table as a name
622	def pair.name(kv: T.Kv) -> Name:
623	  T.Kv{k, v} = kv
624	  Name{k, v}
625	
626	# every pair of the `[names]` table, as names
627	def pair.names(ps: List<&2, T.Kv>) -> List<&2, Name>:
628	  match ps:
629	    case []:
630	      []
631	    case h <> t:
632	      pair.name(h) <> pair.names(t)
633	
634	# every name a lock records, in the order its table holds them
635	def names(+ss: List<&2, T.Sect>) -> List<&2, Name>:
636	  pair.names(names.pairs(ss))
637	
638	# every name a lock's text records that bend would read back. A lock that
639	# does not parse records none.
640	def names.read(text: String) -> List<&2, Name>:
641	  names.valid(names(T.sects(T.parse(text))))
642	
643	# every hash a lock records, one per `[packages."<hash>".files]` table
644	def hash.put(hit: Bool, sect: T.Sect, rest: List<&2, String>) -> List<&2, String>:
645	  match hit:
646	    case True{}:
647	      T.Sect{n, _ps} = sect
648	      K.word(T.segments(n), 1n) <> rest
649	    case False{}:
650	      rest
651	
652	# every hash a lock records
653	def hashes(ss: List<&2, T.Sect>) -> List<&2, String>:
654	  match ss:
655	    case []:
656	      []
657	    case +h <> t:
658	      hash.put(named3(segs(h), "packages", "files"), h, hashes(t))
659	
660	# a pair of a files table as a file
661	def pair.file(kv: T.Kv) -> K.Item:
662	  T.Kv{k, v} = kv
663	  K.Item{k, v}
664	
665	# every pair of a files table, as files
666	def pair.files(ps: List<&2, T.Kv>) -> List<&2, K.Item>:
667	  match ps:
668	    case []:
669	      []
670	    case h <> t:
671	      pair.file(h) <> pair.files(t)
672	
673	# the package a lock records under this hash
674	def pack_of(+ss: List<&2, T.Sect>, +key: String) -> Pack:
675	  Pack{key, src_of(at3(ss, "packages", key, "source")),
676	    pair.files(at3(ss, "packages", key, "files"))}
677	
678	# every package a lock records
679	def packs.at(+ss: List<&2, T.Sect>, hs: List<&2, String>) -> List<&2, Pack>:
680	  match hs:
681	    case []:
682	      []
683	    case h <> t:
684	      pack_of(ss, h) <> packs.at(ss, t)
685	
686	# every package a lock records
687	def packs(+ss: List<&2, T.Sect>) -> List<&2, Pack>:
688	  packs.at(ss, hashes(ss))
689	
690	# a package's source
691	def pack.src(package: Pack) -> Src:
692	  Pack{_h, s, _f} = package
693	  s
694	
695	# a package's files
696	def pack.files(package: Pack) -> List<&2, K.Item>:
697	  Pack{_h, _s, f} = package
698	  f
699	
700	# the manifest text a package is served with
701	def pack.manifest(package: Pack) -> String:
702	  K.manifest_of(pack.files(package))
703	
704	# where a package comes from, in a word
705	def src.kind(source: Src) -> String:
706	  match source:
707	    case Hub{}:
708	      "hub"
709	    case Git{_u, _r, _e, _ro, _n, _t}:
710	      "git"
711	
712	# the commit a package is pinned to, or "" when it comes from the hub
713	def src.rev(source: Src) -> String:
714	  match source:
715	    case Hub{}:
716	      ""
717	    case Git{_u, rev, _e, _ro, _n, _t}:
718	      rev
719	
720	# the repo a package was vendored from, or "" when it comes from the hub
721	def src.url(source: Src) -> String:
722	  match source:
723	    case Hub{}:
724	      ""
725	    case Git{url, _r, _e, _ro, _n, _t}:
726	      url
727	
728	# the directory inside a checkout a vendored package's paths are written from
729	def src.root(source: Src) -> String:
730	  match source:
731	    case Hub{}:
732	      ""
733	    case Git{_u, _r, _e, root, _n, _t}:
734	      root
735	
736	# the NAR hash nix rebuilds a vendored package's checkout by, or "" when it
737	# comes from the hub
738	def src.nar(source: Src) -> String:
739	  match source:
740	    case Hub{}:
741	      ""
742	    case Git{_u, _r, _e, _ro, nar, _t}:
743	      nar