LAWS.bend

bend-prot@0.1.0.0 · 980 lines · 156 definitions

1import Base
2import bend-prot@0.1.0.0/geom.bend as G
3import bend-prot@0.1.0.0/protein.bend as P
4import bend-prot@0.1.0.0/topology.bend as T
5import bend-prot@0.1.0.0/force.bend as F
6import bend-prot@0.1.0.0/rmsd.bend as R
7import bend-prot@0.1.0.0/sasa.bend as S
8import bend-prot@0.1.0.0/rng.bend as Rng
9import bend-prot@0.1.0.0/pdb.bend as Pdb
10import bend-prot@0.1.0.0/par.bend as Par
11import bend-prot@0.1.0.0/bonded.bend as B
12import bend-prot@0.1.0.0/pbc.bend as Pbc
13import bend-prot@0.1.0.0/sim.bend as Sim
14import bend-prot@0.1.0.0/tpl.bend as Tpl
15
16# Laws: precise specs an AI must prove before merging. Humans write claims here
17# and never touch them; PROOF.bend fills each one with a def of the same name.
18
19def empty_atoms() -> List<&2, P.Atom>:
20  Nil{}
21
22# Counting contacts in an empty set finds nothing, at any point and cutoff.
23law count_below_nil:
24  for qp: G.Vec3
25  for c2: F32
26  {T.count_below(empty_atoms(), qp, c2) == 0n : Nat}
27
28# An empty set has no clash, at any point and threshold.
29law has_close_nil:
30  for qp: G.Vec3
31  for min2: F32
32  {T.has_close(empty_atoms(), qp, min2) == False{} : Bool}
33
34def empty_cx() -> P.Complex:
35  P.Complex{Nil{}}
36
37# Spread of nothing is zero.
38law sum_dist2_nil:
39  for qp: G.Vec3
40  {T.sum_dist2(empty_atoms(), qp) == 0.0 : F32}
41
42# An empty set links nothing to anything.
43law contacts_between_nil:
44  for ys: List<&2, P.Atom>
45  for c2: F32
46  {T.contacts_between(empty_atoms(), ys, c2) == 0n : Nat}
47
48# No closest approach exists from an empty set.
49law min_dist2_nil:
50  for qp: G.Vec3
51  {T.min_dist2_to(empty_atoms(), qp) == None{} : Maybe<&2, F32>}
52
53# An empty complex holds no atoms.
54law complex_atoms_nil:
55  {P.Complex.num_atoms(empty_cx()) == 0n : Nat}
56
57# LJ energy of nothing is zero, at any parameters.
58law lj_nil:
59  for eps: F32
60  for sig2: F32
61  for c2: F32
62  {F.lj_total(empty_atoms(), empty_atoms(), eps, sig2, c2) == 0.0 : F32}
63
64# The empty set is at zero RMSD from itself (empty case, by computation).
65# (This says nothing about nonempty sets; see rmsd_single. Unequal lengths
66# silently answer 0 by zip semantics; see rmsd_checked_some/none.)
67law rmsd_nil:
68  {R.rmsd(empty_atoms(), empty_atoms()) == 0.0 : F32}
69
70# Nothing has no surface.
71law sasa_nil:
72  for rad: F32
73  for rc2: F32
74  for area_pt: F32
75  {S.sasa_all(empty_atoms(), S.sasa_offsets(), rad, empty_atoms(), rc2, area_pt) == Nil{} : List<&2, F32>}
76
77# Zero minimization steps change nothing, on any input, not just nothing.
78law sd_fuel0:
79  for xs: List<&2, P.Atom>
80  for eps: F32
81  for sig2: F32
82  for c2: F32
83  for dt: F32
84  {F.minimize(0n, xs, eps, sig2, c2, dt) == xs : List<&2, P.Atom>}
85
86# --- Step equations: each fold's cons case, by computation. ---
87# Together with the Nil laws above, these pin every recursion's skeleton:
88# each function is characterized on all inputs up to its head terms.
89
90# Counting a cons cell is the head hit plus the count of the tail.
91law count_cons:
92  for h: P.Atom
93  for t: List<&2, P.Atom>
94  for qp: G.Vec3
95  for c2: F32
96  {T.count_below(h <> t, qp, c2) == Nat.add(T.count_below(t, qp, c2), T.head_hit_nat(h, qp, c2)) : Nat}
97
98# Interface counting peels one head the same way.
99law contacts_cons:
100  for x: P.Atom
101  for xt: List<&2, P.Atom>
102  for ys: List<&2, P.Atom>
103  for c2: F32
104  {T.contacts_between(x <> xt, ys, c2) == Nat.add(T.contacts_between(xt, ys, c2), T.contacts_of_head(x, ys, c2)) : Nat}
105
106# The fused spread/count pass extends by one head distance.
107law sumd2_count_cons:
108  for h: P.Atom
109  for t: List<&2, P.Atom>
110  for qp: G.Vec3
111  {T.sumd2_count(h <> t, qp) == T.sumd2_extend(T.head_dist2(h, qp), T.sumd2_count(t, qp)) : F32 & Nat}
112
113# Coordination counts peel one head.
114law coord_cons:
115  for x: P.Atom
116  for xt: List<&2, P.Atom>
117  for ys: List<&2, P.Atom>
118  for c2: F32
119  {T.coord_counts(x <> xt, ys, c2) == T.contacts_of_head(x, ys, c2) <> T.coord_counts(xt, ys, c2) : List<&2, Nat>}
120
121# Closest-approach folds one head into the running best.
122law min_dist2_cons:
123  for h: P.Atom
124  for t: List<&2, P.Atom>
125  for qp: G.Vec3
126  {T.min_dist2_to(h <> t, qp) == T.min_cons(h, T.min_dist2_to(t, qp), qp) : Maybe<&2, F32>}
127
128# Set linkage folds one head linkage into the running best.
129law min_link2_cons:
130  for h: P.Atom
131  for t: List<&2, P.Atom>
132  for ys: List<&2, P.Atom>
133  {T.min_link2(h <> t, ys) == T.min_maybe(T.min_link2(t, ys), T.head_link(h, ys)) : Maybe<&2, F32>}
134
135# An LJ row over a cons cell splits head from tail.
136law lj_row_cons:
137  for pi: G.Vec3
138  for eps: F32
139  for sig2: F32
140  for c2: F32
141  for h: P.Atom
142  for t: List<&2, P.Atom>
143  {F.lj_row(pi, eps, sig2, c2, h <> t) == (F.lj_row(pi, eps, sig2, c2, t) + F.lj_head(pi, eps, sig2, c2, h) : F32) : F32}
144
145# An LJ total over a cons cell splits head from tail.
146law lj_total_cons:
147  for h: P.Atom
148  for t: List<&2, P.Atom>
149  for ys: List<&2, P.Atom>
150  for eps: F32
151  for sig2: F32
152  for c2: F32
153  {F.lj_total(h <> t, ys, eps, sig2, c2) == (F.lj_total(t, ys, eps, sig2, c2) + F.lj_self_atom(h, ys, eps, sig2, c2) : F32) : F32}
154
155# A Coulomb row splits head charge from tail charges.
156law coul_row_cons:
157  for pi: G.Vec3
158  for qi: F32
159  for ke: F32
160  for c2: F32
161  for h: P.Atom
162  for t: List<&2, P.Atom>
163  for qh: F32
164  for qt: List<&2, F32>
165  {F.coul_row(pi, qi, ke, c2, h <> t, qh <> qt) == (F.coul_row(pi, qi, ke, c2, t, qt) + F.coul_head(pi, qi, ke, c2, h, qh) : F32) : F32}
166
167# A Coulomb total splits head charge from tail charges.
168law coul_total_cons:
169  for h: P.Atom
170  for t: List<&2, P.Atom>
171  for qh: F32
172  for qt: List<&2, F32>
173  for ys: List<&2, P.Atom>
174  for qs_e: List<&2, F32>
175  for ke: F32
176  for c2: F32
177  {F.coul_total(h <> t, qh <> qt, ys, qs_e, ke, c2) == (F.coul_total(t, qt, ys, qs_e, ke, c2) + F.coul_self(h, qh, ys, qs_e, ke, c2) : F32) : F32}
178
179# A sweep over cons cells moves the head and sweeps the tail.
180law sd_sweep_cons:
181  for h: P.Atom
182  for t: List<&2, P.Atom>
183  for f: G.Vec3
184  for ft: List<&2, G.Vec3>
185  for dt: F32
186  {F.sd_sweep(h <> t, f <> ft, dt) == F.sd_move(h, f, dt) <> F.sd_sweep(t, ft, dt) : List<&2, P.Atom>}
187
188# A pair-distance fold splits the head pair from the tail pairs.
189law pair_sumd2_cons:
190  for x: P.Atom
191  for xt: List<&2, P.Atom>
192  for y: P.Atom
193  for yt: List<&2, P.Atom>
194  {R.pair_sumd2(x <> xt, y <> yt) == R.pair_head(x, y, R.pair_sumd2(xt, yt)) : F32 & Nat}
195
196# Scoring against a cons ensemble scores the head and the tail.
197law rmsd_to_all_cons:
198  for q: List<&2, P.Atom>
199  for h: List<&2, P.Atom>
200  for t: List<&2, List<&2, P.Atom>>
201  {R.rmsd_to_all(q, h <> t) == R.rmsd_against(q, h) <> R.rmsd_to_all(q, t) : List<&2, F32>}
202
203# --- Singletons and golden values: the heads compute. ---
204
205# Counting one atom is that atom's hit.
206law count_single:
207  for h: P.Atom
208  for qp: G.Vec3
209  for c2: F32
210  {T.count_below([h], qp, c2) == T.head_hit_nat(h, qp, c2) : Nat}
211
212# One atom is close exactly when its head test says so.
213law has_close_single:
214  for h: P.Atom
215  for qp: G.Vec3
216  for min2: F32
217  {T.has_close([h], qp, min2) == T.head_is_close(h, qp, min2) : Bool}
218
219# The closest approach to a singleton is its one distance.
220law min_single:
221  for s: U32
222  for e: U32
223  for x: F32
224  for y: F32
225  for z: F32
226  for qx: F32
227  for qy: F32
228  for qz: F32
229  {T.min_dist2_to([P.Atom{s, e, G.V3{x, y, z}}], G.V3{qx, qy, qz}) == Some{G.Vec3.dist2(G.V3{x, y, z}, G.V3{qx, qy, qz})} : Maybe<&2, F32>}
230
231# Spread about a point of nothing is zero through rg_of.
232law rg_about_nil:
233  for qp: G.Vec3
234  {T.rg_about(empty_atoms(), qp) == 0.0 : F32}
235
236# A singleton is at the RMSD its one pair distance dictates.
237law rmsd_single:
238  for s: U32
239  for e: U32
240  for x: F32
241  for y: F32
242  for z: F32
243  {R.rmsd([P.Atom{s, e, G.V3{x, y, z}}], [P.Atom{s, e, G.V3{x, y, z}}]) == F32.sqrt(((G.Vec3.dist2(G.V3{x, y, z}, G.V3{x, y, z}) + 0.0 : F32) / F32.from_nat(1n) : F32)) : F32}
244
245# splitmix32 golden values (catches mistyped mixer constants).
246law rng_next_0:
247  {Rng.rng_next(0) == 1684164658 : U32}
248
249law rng_next_1:
250  {Rng.rng_next(1) == 1580013426 : U32}
251
252# One atom with nothing near it exposes all six sample points.
253law sasa_single:
254  {S.sasa_of([P.Atom{1, 6, G.V3{0.0, 0.0, 0.0}}], 2.0, 16.0, 1.0) == [(1.0 * F32.from_nat(6n) : F32)] : List<&2, F32>}
255
256# --- Truncation pins: mismatched lockstep inputs drop the rest. ---
257
258# Pair folds against an empty list answer the identity.
259law pair_trunc_right:
260  for x: P.Atom
261  for xt: List<&2, P.Atom>
262  {R.pair_sumd2(x <> xt, empty_atoms()) == (0.0, 0n) : F32 & Nat}
263
264# Coulomb with no charges answers zero, however many atoms remain.
265law coul_trunc_charges:
266  for h: P.Atom
267  for t: List<&2, P.Atom>
268  for ys: List<&2, P.Atom>
269  for qs: List<&2, F32>
270  for ke: F32
271  for c2: F32
272  {F.coul_total(h <> t, Nil{}, ys, qs, ke, c2) == 0.0 : F32}
273
274# A sweep with no forces leaves the atoms in place.
275law sd_trunc_forces:
276  for h: P.Atom
277  for t: List<&2, P.Atom>
278  for dt: F32
279  {F.sd_sweep(h <> t, Nil{}, dt) == h <> t : List<&2, P.Atom>}
280
281# --- Induction: empty arguments annihilate, by induction on atoms. ---
282
283# Nothing links to anything, however many heads are peeled.
284law contacts_nil_right:
285  for xs: List<&2, P.Atom>
286  for c2: F32
287  {T.contacts_between(xs, empty_atoms(), c2) == 0n : Nat}
288
289# No closest approach exists from any set held against nothing.
290law min_link2_nil_right:
291  for xs: List<&2, P.Atom>
292  {T.min_link2(xs, empty_atoms()) == None{} : Maybe<&2, F32>}
293
294# --- Checked entry points: mismatches are values, not silence. ---
295
296# Equal-length singletons check cleanly.
297law rmsd_checked_some:
298  for x: P.Atom
299  for y: P.Atom
300  {R.rmsd_checked([x], [y]) == Some{R.rmsd([x], [y])} : Maybe<&2, F32>}
301
302# Unequal lengths answer None{} instead of a silent zero.
303law rmsd_checked_none:
304  for x: P.Atom
305  {R.rmsd_checked([x], empty_atoms()) == None{} : Maybe<&2, F32>}
306
307# --- Structural algebra: the hierarchy agrees with the flat lists. ---
308
309# Appending atom lists associates.
310law append_atoms_assoc:
311  for xs: List<&2, P.Atom>
312  for ys: List<&2, P.Atom>
313  for zs: List<&2, P.Atom>
314  {P.append_atoms(P.append_atoms(xs, ys), zs) == P.append_atoms(xs, P.append_atoms(ys, zs)) : List<&2, P.Atom>}
315
316# Flattening distributes over appending residue lists.
317law flatten_residues_append:
318  for xs: List<&2, P.Residue>
319  for ys: List<&2, P.Residue>
320  {P.flatten_residues(P.append_residues(xs, ys)) == P.append_atoms(P.flatten_residues(xs), P.flatten_residues(ys)) : List<&2, P.Atom>}
321
322# Adding zero on the right changes nothing (induction seed for comm).
323law add_zero_right:
324  for b: Nat
325  {Nat.add(b, 0n) == b : Nat}
326
327# Adding a successor on the right pulls out front.
328law add_succ_right:
329  for b: Nat
330  for a: Nat
331  {Nat.add(b, 1n+a) == 1n+Nat.add(b, a) : Nat}
332
333# Nat addition commutes.
334law add_comm:
335  for a: Nat
336  for b: Nat
337  {Nat.add(a, b) == Nat.add(b, a) : Nat}
338
339# Counting an append splits into the counts.
340law count_atoms_append:
341  for xs: List<&2, P.Atom>
342  for ys: List<&2, P.Atom>
343  {P.count_atoms(P.append_atoms(xs, ys)) == Nat.add(P.count_atoms(xs), P.count_atoms(ys)) : Nat}
344
345# Counting a flattening agrees with counting residues in place.
346law count_flatten_eq:
347  for rs: List<&2, P.Residue>
348  {P.count_atoms(P.flatten_residues(rs)) == P.count_atoms_in(rs) : Nat}
349
350# A complex holds as many atoms as its flattening lists.
351law complex_flatten_eq:
352  for chains: List<&2, P.Chain>
353  {P.Complex.num_atoms(P.Complex{chains}) == P.count_atoms(P.Complex.flatten(P.Complex{chains})) : Nat}
354
355# --- PDB reader: slices, filters, parser goldens, end-to-end counts. ---
356
357# 10^3 is 1000.
358law pow10_3:
359  {Pdb.pow10(3n) == 1000 : U32}
360
361# Iron reads as 26.
362law elem_iron:
363  {Pdb.elem_no("FE") == 26 : U32}
364
365# Carbon reads as 6.
366law elem_carbon:
367  {Pdb.elem_1('C') == 6 : U32}
368
369# ATOM records (6-column tag) pass the filter.
370law atom_line_yes:
371  {Pdb.is_atom_line("ATOM      1  N   ALA A   1") == True{} : Bool}
372
373# Anything else does not.
374law atom_line_no:
375  {Pdb.is_atom_line("HETATM 9999  O   HOH A 101") == False{} : Bool}
376
377# No lines in, no lines out.
378law atom_lines_nil:
379  {Pdb.atom_lines(Nil{}) == Nil{} : List<&2, String>}
380
381# Non-ATOM lines drop, ENDMDL stops the file, the tail never parses.
382law atom_lines_keep:
383  {Pdb.atom_lines(["ATOM      1  N", "TER", "ENDMDL", "ATOM      2  CA"]) == ["ATOM      1  N"] : List<&2, String>}
384
385# 12.5 parses to 12 + 5/10 (stuck F32, identical both sides).
386law parse_f32_one:
387  {Pdb.parse_f32("12.5") == Some{(U32.to_f32(12) + (U32.to_f32(5) / U32.to_f32(10) : F32) : F32)} : Maybe<&2, F32>}
388
389# Signs apply outside the magnitude.
390law parse_f32_neg:
391  {Pdb.parse_f32("-3.25") == Some{(0.0 - (U32.to_f32(3) + (U32.to_f32(25) / U32.to_f32(100) : F32) : F32) : F32)} : Maybe<&2, F32>}
392
393# Non-numeric fields fail instead of answering zero.
394law parse_f32_bad:
395  {Pdb.parse_f32("abc") == None{} : Maybe<&2, F32>}
396
397# The two-line ALA snippet parses to two atoms ...
398law pdb_num_atoms:
399  {P.Complex.num_atoms(Pdb.complex_of(Pdb.parse_pdb(Pdb.demo_text()))) == 2n : Nat}
400
401# ... in one residue ...
402law pdb_num_residues:
403  {P.Complex.num_residues(Pdb.complex_of(Pdb.parse_pdb(Pdb.demo_text()))) == 1n : Nat}
404
405# ... in one chain ...
406law pdb_num_chains:
407  {P.Complex.num_chains(Pdb.complex_of(Pdb.parse_pdb(Pdb.demo_text()))) == 1n : Nat}
408
409# ... with nothing skipped ...
410law pdb_skipped_0:
411  {Pdb.skipped_of(Pdb.parse_pdb(Pdb.demo_text())) == 0n : Nat}
412
413# ... while a bad serial skips exactly its line.
414law pdb_skipped_1:
415  {Pdb.skipped_of(Pdb.parse_pdb(Pdb.demo_bad_text())) == 1n : Nat}
416
417law pdb_bad_atoms:
418  {P.Complex.num_atoms(Pdb.complex_of(Pdb.parse_pdb(Pdb.demo_bad_text()))) == 1n : Nat}
419
420# ... and the first atom is nitrogen.
421law pdb_first_elem:
422  {Pdb.first_elem(Pdb.complex_of(Pdb.parse_pdb(Pdb.demo_text()))) == Some{7} : Maybe<&2, U32>}
423
424# Total area splits head from tail.
425law sasa_total_cons:
426  for h: F32
427  for t: List<&2, F32>
428  {S.sasa_total(h <> t) == (h + S.sasa_total(t) : F32) : F32}
429
430# --- Parallel kernels: unrolled steps match, remainders fall back. ---
431
432# Empty input counts nothing, through the fallback arm.
433law count_par4_nil:
434  for qp: G.Vec3
435  for c2: F32
436  {Par.count_par4(empty_atoms(), qp, c2) == 0n : Nat}
437
438# A full unrolled step splits four parallel hits plus the tail.
439law count_par4_step:
440  for h1: P.Atom
441  for h2: P.Atom
442  for h3: P.Atom
443  for h4: P.Atom
444  for t: List<&2, P.Atom>
445  for qp: G.Vec3
446  for c2: F32
447  {Par.count_par4(h1 <> h2 <> h3 <> h4 <> t, qp, c2) == Nat.add(Nat.add(T.head_hit_nat(h1, qp, c2), T.head_hit_nat(h2, qp, c2)), Nat.add(T.head_hit_nat(h3, qp, c2), Nat.add(T.head_hit_nat(h4, qp, c2), Par.count_par4(t, qp, c2)))) : Nat}
448
449# Short inputs take the sequential fallback exactly.
450law count_par4_small:
451  for h: P.Atom
452  for qp: G.Vec3
453  for c2: F32
454  {Par.count_par4([h], qp, c2) == T.count_below([h], qp, c2) : Nat}
455
456# Empty rows sum nothing, through the fallback arm.
457law lj_row_par4_nil:
458  for pi: G.Vec3
459  for eps: F32
460  for sig2: F32
461  for c2: F32
462  {Par.lj_row_par4(pi, eps, sig2, c2, empty_atoms()) == 0.0 : F32}
463
464# A full unrolled row splits four parallel heads plus the tail.
465law lj_row_par4_step:
466  for pi: G.Vec3
467  for eps: F32
468  for sig2: F32
469  for c2: F32
470  for h1: P.Atom
471  for h2: P.Atom
472  for h3: P.Atom
473  for h4: P.Atom
474  for t: List<&2, P.Atom>
475  {Par.lj_row_par4(pi, eps, sig2, c2, h1 <> h2 <> h3 <> h4 <> t) == ((F.lj_head(pi, eps, sig2, c2, h1) + F.lj_head(pi, eps, sig2, c2, h2) : F32) + ((F.lj_head(pi, eps, sig2, c2, h3) + F.lj_head(pi, eps, sig2, c2, h4) : F32) + Par.lj_row_par4(pi, eps, sig2, c2, t) : F32) : F32) : F32}
476
477# Short rows take the sequential fallback exactly.
478law lj_row_par4_small:
479  for pi: G.Vec3
480  for eps: F32
481  for sig2: F32
482  for c2: F32
483  for h: P.Atom
484  {Par.lj_row_par4(pi, eps, sig2, c2, [h]) == F.lj_row(pi, eps, sig2, c2, [h]) : F32}
485
486# --- Per-element LJ: table goldens and step equations. ---
487
488# Carbon takes illustrative OPLS-style parameters.
489law lj_eps_c:
490  {F.lj_eps(6) == 0.066 : F32}
491
492law lj_eps_h:
493  {F.lj_eps(1) == 0.03 : F32}
494
495law lj_sig_o:
496  {F.lj_sig(8) == 2.96 : F32}
497
498# Unknown elements take the generic pair.
499law lj_sig_default:
500  {F.lj_sig(99) == 3.0 : F32}
501
502# An element row over a cons cell splits head from tail.
503law lj_row_elem_cons:
504  for si: U32
505  for pi: G.Vec3
506  for c2: F32
507  for h: P.Atom
508  for t: List<&2, P.Atom>
509  {F.lj_row_elem(si, pi, h <> t, c2) == (F.lj_row_elem(si, pi, t, c2) + F.lj_head_elem(si, pi, c2, h) : F32) : F32}
510
511# An element total over a cons cell splits head from tail.
512law lj_total_elem_cons:
513  for h: P.Atom
514  for t: List<&2, P.Atom>
515  for ys: List<&2, P.Atom>
516  for c2: F32
517  {F.lj_total_elem(h <> t, ys, c2) == (F.lj_total_elem(t, ys, c2) + F.lj_row_elem(P.Atom.elem(h), P.Atom.pos(h), ys, c2) : F32) : F32}
518
519# --- Bonded terms: empties, steps, lookups, exclusion goldens. ---
520
521# No bonds bind nothing.
522law bond_total_nil:
523  for k: F32
524  {B.bond_total(empty_atoms(), Nil{}, k) == 0.0 : F32}
525
526# A bond total splits head bond from tail bonds.
527law bond_total_cons:
528  for xs: List<&2, P.Atom>
529  for s1: U32
530  for s2: U32
531  for t: List<&1, U32 & U32>
532  for k: F32
533  {B.bond_total(xs, (s1, s2) <> t, k) == (B.bond_cov_pair(xs, s1, s2, k) + B.bond_total(xs, t, k) : F32) : F32}
534
535# No angles bend nothing.
536law angle_total_nil:
537  for k: F32
538  for eq: F32
539  {B.angle_total(empty_atoms(), Nil{}, k, eq) == 0.0 : F32}
540
541# An angle total splits head triple from tail triples.
542law angle_total_cons:
543  for xs: List<&2, P.Atom>
544  for sa: U32
545  for sb: U32
546  for sc: U32
547  for t: List<&1, U32 & U32 & U32>
548  for k: F32
549  for eq: F32
550  {B.angle_total(xs, (sa, sb, sc) <> t, k, eq) == (B.angle_triple(xs, sa, sb, sc, k, eq) + B.angle_total(xs, t, k, eq) : F32) : F32}
551
552# Nobody is found in nothing.
553law pos_of_serial_none:
554  for s: U32
555  {B.pos_of_serial(empty_atoms(), s) == None{} : Maybe<&2, G.Vec3>}
556
557# A singleton finds its atom's position.
558law pos_of_serial_some:
559  {B.pos_of_serial([P.Atom{1, 6, G.V3{1.0, 2.0, 3.0}}], 1) == Some{G.V3{1.0, 2.0, 3.0}} : Maybe<&2, G.Vec3>}
560
561# No bonds exclude nothing.
562law bonded12_nil:
563  for a: U32
564  for b: U32
565  {B.bonded12_flat(Nil{}, a, b) == False{} : Bool}
566
567# A listed pair (either order) is 1-2 excluded.
568law bonded12_hit:
569  {B.bonded12_flat([1, 2], 1, 2) == True{} : Bool}
570
571# An unlisted pair is not.
572law bonded12_miss:
573  {B.bonded12_flat([1, 2], 1, 3) == False{} : Bool}
574
575# Neighbors of 1 in [(1,2),(2,3)] are just [2].
576law neighbors_one:
577  {B.bond_neighbors(1, [1, 2, 2, 3]) == [2] : List<&2, U32>}
578
579# 1 and 3 share neighbor 2.
580law excluded13_one:
581  {B.excluded13(1, 3, [1, 2, 2, 3]) == True{} : Bool}
582
583# 2 and 3 are directly bonded (1-2 wins over 1-3 either way).
584law excluded_both:
585  {B.excluded(2, 3, [1, 2, 2, 3]) == True{} : Bool}
586
587# Pair bonds flatten in order.
588law flatten_bonds_one:
589  {B.flatten_bonds([(1, 2)]) == [1, 2] : List<&2, U32>}
590
591# Excluded rows sum nothing over nothing.
592law lj_row_excl_nil:
593  for si: U32
594  for pi: G.Vec3
595  for eps: F32
596  for sig2: F32
597  for c2: F32
598  for bonds: List<&2, U32>
599  {B.lj_row_excl(si, pi, eps, sig2, c2, empty_atoms(), bonds) == 0.0 : F32}
600
601law lj_total_excl_nil:
602  for ys: List<&2, P.Atom>
603  for eps: F32
604  for sig2: F32
605  for c2: F32
606  for bonds: List<&2, U32>
607  {B.lj_total_excl(empty_atoms(), ys, eps, sig2, c2, bonds) == 0.0 : F32}
608
609law coul_row_excl_nil:
610  for si: U32
611  for pi: G.Vec3
612  for qi: F32
613  for ke: F32
614  for c2: F32
615  for bonds: List<&2, U32>
616  {B.coul_row_excl(si, pi, qi, ke, c2, empty_atoms(), Nil{}, bonds) == 0.0 : F32}
617
618law coul_total_excl_nil:
619  for ys: List<&2, P.Atom>
620  for qs_e: List<&2, F32>
621  for ke: F32
622  for c2: F32
623  for bonds: List<&2, U32>
624  {B.coul_total_excl(empty_atoms(), Nil{}, ys, qs_e, ke, c2, bonds) == 0.0 : F32}
625
626# Element-excluded rows/totals sum nothing over nothing.
627law lj_row_elem_excl_nil:
628  for si: U32
629  for se: U32
630  for pi: G.Vec3
631  for c2: F32
632  for bonds: List<&2, U32>
633  {B.lj_row_elem_excl(si, se, pi, empty_atoms(), c2, bonds) == 0.0 : F32}
634
635law lj_total_elem_excl_nil:
636  for ys: List<&2, P.Atom>
637  for c2: F32
638  for bonds: List<&2, U32>
639  {B.lj_total_elem_excl(empty_atoms(), ys, c2, bonds) == 0.0 : F32}
640
641# A directly bonded pair contributes exactly 0.0 (wiring pin: the row must
642# test serials, not elements; the sum is (0.0 + 0.0) since F32.add is stuck).
643law lj_row_elem_excl_hit:
644  {B.lj_row_elem_excl(1, 7, G.V3{0.0, 0.0, 0.0}, [P.Atom{2, 6, G.V3{1.0, 0.0, 0.0}}], 144.0, [1, 2]) == (0.0 + 0.0 : F32) : F32}
645
646# Same through a 1-3 link.
647law lj_row_elem_excl_link:
648  {B.lj_row_elem_excl(1, 7, G.V3{0.0, 0.0, 0.0}, [P.Atom{3, 6, G.V3{2.0, 0.0, 0.0}}], 144.0, [1, 2, 2, 3]) == (0.0 + 0.0 : F32) : F32}
649
650# --- CONECT: filter and parse goldens. ---
651
652# No lines in, no bonds out.
653law conect_lines_nil:
654  {Pdb.conect_lines(Nil{}) == Nil{} : List<&2, String>}
655
656# CONECT lines survive, everything else drops.
657law conect_keep:
658  {Pdb.conect_lines(["ATOM      1  N", "CONECT   20  282"]) == ["CONECT   20  282"] : List<&2, String>}
659
660# One record with one partner is one bond.
661law parse_conect_one:
662  {Pdb.parse_conect_line("CONECT   20  282") == [(20, 282)] : List<&1, U32 & U32>}
663
664# A partnerless record binds nothing.
665law parse_conect_none:
666  {Pdb.parse_conect_line("CONECT") == Nil{} : List<&1, U32 & U32>}
667
668# --- Masses and Coulomb forces. ---
669
670# Carbon weighs 12.011 amu.
671law mass_c:
672  {F.mass(6) == 12.011 : F32}
673
674law mass_h:
675  {F.mass(1) == 1.008 : F32}
676
677# A Coulomb row over a cons cell splits head from tail.
678law coul_frow_cons:
679  for pi: G.Vec3
680  for qi: F32
681  for ke: F32
682  for c2: F32
683  for h: P.Atom
684  for t: List<&2, P.Atom>
685  for qh: F32
686  for qt: List<&2, F32>
687  {F.coul_frow(pi, qi, ke, c2, h <> t, qh <> qt) == G.Vec3.add(F.coul_frow(pi, qi, ke, c2, t, qt), F.coul_fhead(pi, qi, ke, c2, h, qh)) : G.Vec3}
688
689# Coulomb forces over cons cells split head from tail.
690law coul_forces_cons:
691  for h: P.Atom
692  for t: List<&2, P.Atom>
693  for qh: F32
694  for qt: List<&2, F32>
695  for ys: List<&2, P.Atom>
696  for qs_e: List<&2, F32>
697  for ke: F32
698  for c2: F32
699  {F.coul_forces(h <> t, qh <> qt, ys, qs_e, ke, c2) == F.coul_fself_atom(h, qh, ys, qs_e, ke, c2) <> F.coul_forces(t, qt, ys, qs_e, ke, c2) : List<&2, G.Vec3>}
700
701# No charges feel nothing.
702law coul_frow_nil:
703  for pi: G.Vec3
704  for qi: F32
705  for ke: F32
706  for c2: F32
707  {F.coul_frow(pi, qi, ke, c2, empty_atoms(), Nil{}) == G.V3{0.0, 0.0, 0.0} : G.Vec3}
708
709# --- PBC: mirror equations and empties. ---
710
711law lj_row_pbc_cons:
712  for pi: G.Vec3
713  for eps: F32
714  for sig2: F32
715  for c2: F32
716  for box: G.Vec3
717  for h: P.Atom
718  for t: List<&2, P.Atom>
719  {Pbc.lj_row_pbc(pi, eps, sig2, c2, box, h <> t) == (Pbc.lj_row_pbc(pi, eps, sig2, c2, box, t) + Pbc.lj_head_pbc(pi, eps, sig2, c2, box, h) : F32) : F32}
720
721law lj_total_pbc_cons:
722  for h: P.Atom
723  for t: List<&2, P.Atom>
724  for ys: List<&2, P.Atom>
725  for eps: F32
726  for sig2: F32
727  for c2: F32
728  for box: G.Vec3
729  {Pbc.lj_total_pbc(h <> t, ys, eps, sig2, c2, box) == (Pbc.lj_total_pbc(t, ys, eps, sig2, c2, box) + Pbc.lj_self_atom_pbc(h, ys, eps, sig2, c2, box) : F32) : F32}
730
731law lj_row_pbc_nil:
732  for pi: G.Vec3
733  for eps: F32
734  for sig2: F32
735  for c2: F32
736  for box: G.Vec3
737  {Pbc.lj_row_pbc(pi, eps, sig2, c2, box, empty_atoms()) == 0.0 : F32}
738
739law lj_frow_pbc_cons:
740  for pi: G.Vec3
741  for eps: F32
742  for sig2: F32
743  for c2: F32
744  for box: G.Vec3
745  for h: P.Atom
746  for t: List<&2, P.Atom>
747  {Pbc.lj_frow_pbc(pi, eps, sig2, c2, box, h <> t) == G.Vec3.add(Pbc.lj_frow_pbc(pi, eps, sig2, c2, box, t), Pbc.lj_fhead_pbc(pi, eps, sig2, c2, box, h)) : G.Vec3}
748
749law lj_forces_pbc_cons:
750  for h: P.Atom
751  for t: List<&2, P.Atom>
752  for ys: List<&2, P.Atom>
753  for eps: F32
754  for sig2: F32
755  for c2: F32
756  for box: G.Vec3
757  {Pbc.lj_forces_pbc(h <> t, ys, eps, sig2, c2, box) == Pbc.lj_fself_atom_pbc(h, ys, eps, sig2, c2, box) <> Pbc.lj_forces_pbc(t, ys, eps, sig2, c2, box) : List<&2, G.Vec3>}
758
759law lj_forces_pbc_nil:
760  for ys: List<&2, P.Atom>
761  for eps: F32
762  for sig2: F32
763  for c2: F32
764  for box: G.Vec3
765  {Pbc.lj_forces_pbc(empty_atoms(), ys, eps, sig2, c2, box) == Nil{} : List<&2, G.Vec3>}
766
767# --- Bonded additions: radii, inference, forces. ---
768
769# Carbon's covalent radius is 0.76 A.
770law cov_rad_c:
771  {B.cov_rad(6) == 0.76 : F32}
772
773# An inference row over nothing finds nothing.
774law infer_row_nil:
775  for si: U32
776  for pi: G.Vec3
777  for ei: U32
778  {B.infer_row(si, pi, ei, empty_atoms()) == Nil{} : List<&1, U32 & U32>}
779
780# An inference row splits head from tail.
781law infer_row_cons:
782  for si: U32
783  for pi: G.Vec3
784  for ei: U32
785  for h: P.Atom
786  for t: List<&2, P.Atom>
787  {B.infer_row(si, pi, ei, h <> t) == B.append_infer(B.infer_one(si, pi, ei, P.Atom.serial(h), P.Atom.elem(h), P.Atom.pos(h)), B.infer_row(si, pi, ei, t)) : List<&1, U32 & U32>}
788
789# Nothing infers from nothing.
790law infer_total_nil:
791  {B.infer_total(empty_atoms()) == Nil{} : List<&1, U32 & U32>}
792
793# Bond forces sum nothing over nothing.
794law bond_forces_nil:
795  for bonds: List<&2, U32>
796  for k: F32
797  {B.bond_forces(empty_atoms(), bonds, k) == Nil{} : List<&2, G.Vec3>}
798
799# Bond forces split head atom from tail atoms.
800law bond_forces_cons:
801  for h: P.Atom
802  for t: List<&2, P.Atom>
803  for bonds: List<&2, U32>
804  for k: F32
805  {B.bond_forces(h <> t, bonds, k) == B.bond_force_list(P.Atom.serial(h), bonds, h <> t, k) <> B.bond_forces(t, bonds, k) : List<&2, G.Vec3>}
806
807# --- Engine: maps split head from tail; drivers stop on empty fuel. ---
808
809law dyn_of_atoms_nil:
810  {Sim.dyn_of_atoms(empty_atoms()) == Nil{} : List<&2, Sim.DynAtom>}
811
812law dyn_of_atoms_cons:
813  for h: P.Atom
814  for t: List<&2, P.Atom>
815  {Sim.dyn_of_atoms(h <> t) == Sim.dyn_of_atom(h) <> Sim.dyn_of_atoms(t) : List<&2, Sim.DynAtom>}
816
817law dyn_atoms_nil:
818  {Sim.dyn_atoms(Nil{}) == Nil{} : List<&2, P.Atom>}
819
820law vv_scale_nil:
821  for lam: F32
822  {Sim.vv_scale(Nil{}, lam) == Nil{} : List<&2, Sim.DynAtom>}
823
824law vv_scale_cons:
825  for h: Sim.DynAtom
826  for t: List<&2, Sim.DynAtom>
827  for lam: F32
828  {Sim.vv_scale(h <> t, lam) == Sim.vv_scale_head(h, lam) <> Sim.vv_scale(t, lam) : List<&2, Sim.DynAtom>}
829
830law vv_half_nil:
831  for dt: F32
832  {Sim.vv_half(Nil{}, dt) == Nil{} : List<&2, Sim.DynAtom>}
833
834law vv_half_cons:
835  for h: Sim.DynAtom
836  for t: List<&2, Sim.DynAtom>
837  for dt: F32
838  {Sim.vv_half(h <> t, dt) == Sim.vv_half_head(h, dt) <> Sim.vv_half(t, dt) : List<&2, Sim.DynAtom>}
839
840law vv_full_nil:
841  for dt: F32
842  {Sim.vv_full(Nil{}, dt) == Nil{} : List<&2, Sim.DynAtom>}
843
844law vv_full_cons:
845  for h: Sim.DynAtom
846  for t: List<&2, Sim.DynAtom>
847  for dt: F32
848  {Sim.vv_full(h <> t, dt) == Sim.vv_full_head(h, dt) <> Sim.vv_full(t, dt) : List<&2, Sim.DynAtom>}
849
850law ke_sim_nil:
851  {Sim.ke_sim_of(Nil{}) == 0.0 : F32}
852
853law md_run_zero:
854  for ds: List<&2, Sim.DynAtom>
855  for qs: List<&2, F32>
856  for bonds: List<&2, U32>
857  for p: Sim.SimParams
858  for dt: F32
859  for tau: F32
860  for temp0: F32
861  for n: Nat
862  {Sim.md_run(0n, ds, qs, bonds, p, dt, tau, temp0, n) == ds : List<&2, Sim.DynAtom>}
863
864law min_run_zero:
865  for ds: List<&2, Sim.DynAtom>
866  for qs: List<&2, F32>
867  for bonds: List<&2, U32>
868  for p: Sim.SimParams
869  for dt: F32
870  {Sim.min_run(0n, ds, qs, bonds, p, dt) == ds : List<&2, Sim.DynAtom>}
871
872# Zero charges over nothing is nothing.
873law zero_charges_nil:
874  {Sim.zero_charges(empty_atoms()) == Nil{} : List<&2, F32>}
875
876# Zero charges split head from tail.
877law zero_charges_cons:
878  for h: P.Atom
879  for t: List<&2, P.Atom>
880  {Sim.zero_charges(h <> t) == 0.0 <> Sim.zero_charges(t) : List<&2, F32>}
881
882# Normalized sweeps move nothing over nothing.
883law sd_norm_sweep_nil:
884  for dt: F32
885  {Sim.sd_norm_sweep(Nil{}, dt) == Nil{} : List<&2, Sim.DynAtom>}
886
887# No atoms carry no max force.
888law maxforce2_nil:
889  {Sim.maxforce2_of(Nil{}) == 0.0 : F32}
890
891# Setting forces over nothing is nothing.
892law dyn_set_force_nil:
893  for fs: List<&2, G.Vec3>
894  {Sim.dyn_set_force(Nil{}, fs) == Nil{} : List<&2, Sim.DynAtom>}
895
896# Adding empties is empty.
897law add_forces_nil:
898  {Sim.add_forces(Nil{}, Nil{}) == Nil{} : List<&2, G.Vec3>}
899
900# Force addition splits head pair from tail pairs.
901law add_forces_cons:
902  for x: G.Vec3
903  for xt: List<&2, G.Vec3>
904  for y: G.Vec3
905  for yt: List<&2, G.Vec3>
906  {Sim.add_forces(x <> xt, y <> yt) == G.Vec3.add(x, y) <> Sim.add_forces(xt, yt) : List<&2, G.Vec3>}
907
908# No flats pair to nothing.
909law pairs_of_flat_nil:
910  {Sim.pairs_of_flat(Nil{}) == Nil{} : List<&1, U32 & U32>}
911
912# Flat pairs split head pair from tail pairs.
913law pairs_of_flat_cons:
914  for x: U32
915  for y: U32
916  for t: List<&2, U32>
917  {Sim.pairs_of_flat(x <> y <> t) == (x, y) <> Sim.pairs_of_flat(t) : List<&1, U32 & U32>}
918
919# Padding and symbols print as written.
920law pad_left_golden:
921  {Pdb.pad_left("AB", 5n) == "   AB" : String}
922
923law pad_right_golden:
924  {Pdb.pad_right("AB", 5n) == "AB   " : String}
925
926law fmt_u32_golden:
927  {Pdb.fmt_u32(5n, 42) == "   42" : String}
928
929law elem_sym_golden:
930  {Pdb.elem_sym(26) == "FE" : String}
931
932# --- Templates: dispatch goldens, name matching, parse goldens. ---
933
934# ALA links N-CA in the template.
935law tpl_has_bond_ala:
936  {Tpl.tpl_has_bond("ALA", "N", "CA") == True{} : Bool}
937
938# ... but not N-O.
939law tpl_has_bond_miss:
940  {Tpl.tpl_has_bond("ALA", "N", "O") == False{} : Bool}
941
942# Unknown residues link nothing.
943law tpl_has_bond_unknown:
944  {Tpl.tpl_has_bond("ZZZ", "N", "CA") == False{} : Bool}
945
946# HIS variants share heavy topology.
947law tpl_has_bond_his:
948  {Tpl.tpl_has_bond("HID", "N", "CA") == True{} : Bool}
949
950# Template rows split head from tail.
951law tpl_row_nil:
952  for a: Tpl.TplAtom
953  {Tpl.tpl_row(a, Nil{}) == Nil{} : List<&1, U32 & U32>}
954
955law tpl_row_cons:
956  for a: Tpl.TplAtom
957  for h: Tpl.TplAtom
958  for t: List<&2, Tpl.TplAtom>
959  {Tpl.tpl_row(a, h <> t) == Tpl.append_tpl(Tpl.tpl_one(a, h), Tpl.tpl_row(a, t)) : List<&1, U32 & U32>}
960
961law tpl_total_nil:
962  {Tpl.tpl_total(Nil{}) == Nil{} : List<&1, U32 & U32>}
963
964# The snippet's first atom parses with identity intact.
965law parse_tpl_golden:
966  {Tpl.parse_tpl_line("ATOM      1  N   ALA A   1      11.104  13.207   2.100  1.00 13.79           N  ") == Some{Tpl.TA{1, 65, 1n, "ALA", "N"}} : Maybe<&2, Tpl.TplAtom>}
967
968# --- Angle auto-derivation goldens. ---
969
970# Neighbors of 2 excluding 1 in [(1,2),(2,3)] are just [3].
971law neighbors_except_golden:
972  {B.bond_neighbors_except(2, 1, [1, 2, 2, 3]) == [3] : List<&2, U32>}
973
974# A fan over [3, 4] from (1, 2) lists both triples.
975law fan_triples_golden:
976  {B.fan_triples(1, 2, [3, 4]) == [(1, 2, 3), (1, 2, 4)] : List<&1, U32 & U32 & U32>}
977
978# A two-bond chain auto-derives both directed angles.
979law angle_triples_auto_golden:
980  {B.angle_triples_auto([1, 2, 2, 3]) == [(1, 2, 3), (3, 2, 1)] : List<&1, U32 & U32 & U32>}