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