1 import Base 2 import ./geom.bend as G 3 import ./protein.bend as P 4 import ./topology.bend as T 5 import ./force.bend as F 6 import ./rmsd.bend as R 7 import ./sasa.bend as S 8 import ./rng.bend as Rng 9 import ./pdb.bend as Pdb 10 import ./par.bend as Par 11 import ./bonded.bend as B 12 import ./pbc.bend as Pbc 13 import ./sim.bend as Sim 14 import ./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 19 def empty_atoms() -> List<&2, P.Atom>: 20 Nil{} 21 22 # Counting contacts in an empty set finds nothing, at any point and cutoff. 23 law 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. 29 law has_close_nil: 30 for qp: G.Vec3 31 for min2: F32 32 {T.has_close(empty_atoms(), qp, min2) == False{} : Bool} 33 34 def empty_cx() -> P.Complex: 35 P.Complex{Nil{}} 36 37 # Spread of nothing is zero. 38 law 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. 43 law 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. 49 law 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. 54 law complex_atoms_nil: 55 {P.Complex.num_atoms(empty_cx()) == 0n : Nat} 56 57 # LJ energy of nothing is zero, at any parameters. 58 law 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.) 67 law rmsd_nil: 68 {R.rmsd(empty_atoms(), empty_atoms()) == 0.0 : F32} 69 70 # Nothing has no surface. 71 law 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. 78 law 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. 91 law 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. 99 law 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. 107 law 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. 114 law 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. 122 law 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. 129 law 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. 136 law 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. 146 law 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. 156 law 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. 168 law 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. 180 law 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. 189 law 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. 197 law 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. 206 law 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. 213 law 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. 220 law 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. 232 law 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. 237 law 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). 246 law rng_next_0: 247 {Rng.rng_next(0) == 1684164658 : U32} 248 249 law rng_next_1: 250 {Rng.rng_next(1) == 1580013426 : U32} 251 252 # One atom with nothing near it exposes all six sample points. 253 law 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. 259 law 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. 265 law 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. 275 law 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. 284 law 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. 290 law 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. 297 law 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. 303 law 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. 310 law 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. 317 law 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). 323 law 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. 328 law 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. 334 law 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. 340 law 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. 346 law 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. 351 law 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. 358 law pow10_3: 359 {Pdb.pow10(3n) == 1000 : U32} 360 361 # Iron reads as 26. 362 law elem_iron: 363 {Pdb.elem_no("FE") == 26 : U32} 364 365 # Carbon reads as 6. 366 law elem_carbon: 367 {Pdb.elem_1('C') == 6 : U32} 368 369 # ATOM records (6-column tag) pass the filter. 370 law atom_line_yes: 371 {Pdb.is_atom_line("ATOM 1 N ALA A 1") == True{} : Bool} 372 373 # Anything else does not. 374 law atom_line_no: 375 {Pdb.is_atom_line("HETATM 9999 O HOH A 101") == False{} : Bool} 376 377 # No lines in, no lines out. 378 law 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. 382 law 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). 386 law 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. 390 law 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. 394 law parse_f32_bad: 395 {Pdb.parse_f32("abc") == None{} : Maybe<&2, F32>} 396 397 # The two-line ALA snippet parses to two atoms ... 398 law pdb_num_atoms: 399 {P.Complex.num_atoms(Pdb.complex_of(Pdb.parse_pdb(Pdb.demo_text()))) == 2n : Nat} 400 401 # ... in one residue ... 402 law pdb_num_residues: 403 {P.Complex.num_residues(Pdb.complex_of(Pdb.parse_pdb(Pdb.demo_text()))) == 1n : Nat} 404 405 # ... in one chain ... 406 law pdb_num_chains: 407 {P.Complex.num_chains(Pdb.complex_of(Pdb.parse_pdb(Pdb.demo_text()))) == 1n : Nat} 408 409 # ... with nothing skipped ... 410 law 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. 414 law pdb_skipped_1: 415 {Pdb.skipped_of(Pdb.parse_pdb(Pdb.demo_bad_text())) == 1n : Nat} 416 417 law 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. 421 law 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. 425 law 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. 433 law 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. 439 law 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. 450 law 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. 457 law 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. 465 law 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. 478 law 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. 489 law lj_eps_c: 490 {F.lj_eps(6) == 0.066 : F32} 491 492 law lj_eps_h: 493 {F.lj_eps(1) == 0.03 : F32} 494 495 law lj_sig_o: 496 {F.lj_sig(8) == 2.96 : F32} 497 498 # Unknown elements take the generic pair. 499 law lj_sig_default: 500 {F.lj_sig(99) == 3.0 : F32} 501 502 # An element row over a cons cell splits head from tail. 503 law 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. 512 law 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. 522 law 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. 527 law 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. 536 law 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. 542 law 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. 553 law 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. 558 law 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. 562 law 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. 568 law bonded12_hit: 569 {B.bonded12_flat([1, 2], 1, 2) == True{} : Bool} 570 571 # An unlisted pair is not. 572 law 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]. 576 law neighbors_one: 577 {B.bond_neighbors(1, [1, 2, 2, 3]) == [2] : List<&2, U32>} 578 579 # 1 and 3 share neighbor 2. 580 law 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). 584 law excluded_both: 585 {B.excluded(2, 3, [1, 2, 2, 3]) == True{} : Bool} 586 587 # Pair bonds flatten in order. 588 law flatten_bonds_one: 589 {B.flatten_bonds([(1, 2)]) == [1, 2] : List<&2, U32>} 590 591 # Excluded rows sum nothing over nothing. 592 law 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 601 law 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 609 law 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 618 law 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. 627 law 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 635 law 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). 643 law 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. 647 law 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. 653 law conect_lines_nil: 654 {Pdb.conect_lines(Nil{}) == Nil{} : List<&2, String>} 655 656 # CONECT lines survive, everything else drops. 657 law 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. 661 law parse_conect_one: 662 {Pdb.parse_conect_line("CONECT 20 282") == [(20, 282)] : List<&1, U32 & U32>} 663 664 # A partnerless record binds nothing. 665 law 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. 671 law mass_c: 672 {F.mass(6) == 12.011 : F32} 673 674 law mass_h: 675 {F.mass(1) == 1.008 : F32} 676 677 # A Coulomb row over a cons cell splits head from tail. 678 law 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. 690 law 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. 702 law 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 711 law 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 721 law 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 731 law 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 739 law 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 749 law 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 759 law 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. 770 law cov_rad_c: 771 {B.cov_rad(6) == 0.76 : F32} 772 773 # An inference row over nothing finds nothing. 774 law 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. 781 law 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. 790 law infer_total_nil: 791 {B.infer_total(empty_atoms()) == Nil{} : List<&1, U32 & U32>} 792 793 # Bond forces sum nothing over nothing. 794 law 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. 800 law 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 809 law dyn_of_atoms_nil: 810 {Sim.dyn_of_atoms(empty_atoms()) == Nil{} : List<&2, Sim.DynAtom>} 811 812 law 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 817 law dyn_atoms_nil: 818 {Sim.dyn_atoms(Nil{}) == Nil{} : List<&2, P.Atom>} 819 820 law vv_scale_nil: 821 for lam: F32 822 {Sim.vv_scale(Nil{}, lam) == Nil{} : List<&2, Sim.DynAtom>} 823 824 law 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 830 law vv_half_nil: 831 for dt: F32 832 {Sim.vv_half(Nil{}, dt) == Nil{} : List<&2, Sim.DynAtom>} 833 834 law 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 840 law vv_full_nil: 841 for dt: F32 842 {Sim.vv_full(Nil{}, dt) == Nil{} : List<&2, Sim.DynAtom>} 843 844 law 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 850 law ke_sim_nil: 851 {Sim.ke_sim_of(Nil{}) == 0.0 : F32} 852 853 law 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 864 law 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. 873 law zero_charges_nil: 874 {Sim.zero_charges(empty_atoms()) == Nil{} : List<&2, F32>} 875 876 # Zero charges split head from tail. 877 law 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. 883 law 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. 888 law maxforce2_nil: 889 {Sim.maxforce2_of(Nil{}) == 0.0 : F32} 890 891 # Setting forces over nothing is nothing. 892 law 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. 897 law add_forces_nil: 898 {Sim.add_forces(Nil{}, Nil{}) == Nil{} : List<&2, G.Vec3>} 899 900 # Force addition splits head pair from tail pairs. 901 law 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. 909 law 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. 913 law 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. 920 law pad_left_golden: 921 {Pdb.pad_left("AB", 5n) == " AB" : String} 922 923 law pad_right_golden: 924 {Pdb.pad_right("AB", 5n) == "AB " : String} 925 926 law fmt_u32_golden: 927 {Pdb.fmt_u32(5n, 42) == " 42" : String} 928 929 law 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. 935 law tpl_has_bond_ala: 936 {Tpl.tpl_has_bond("ALA", "N", "CA") == True{} : Bool} 937 938 # ... but not N-O. 939 law tpl_has_bond_miss: 940 {Tpl.tpl_has_bond("ALA", "N", "O") == False{} : Bool} 941 942 # Unknown residues link nothing. 943 law tpl_has_bond_unknown: 944 {Tpl.tpl_has_bond("ZZZ", "N", "CA") == False{} : Bool} 945 946 # HIS variants share heavy topology. 947 law tpl_has_bond_his: 948 {Tpl.tpl_has_bond("HID", "N", "CA") == True{} : Bool} 949 950 # Template rows split head from tail. 951 law tpl_row_nil: 952 for a: Tpl.TplAtom 953 {Tpl.tpl_row(a, Nil{}) == Nil{} : List<&1, U32 & U32>} 954 955 law 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 961 law tpl_total_nil: 962 {Tpl.tpl_total(Nil{}) == Nil{} : List<&1, U32 & U32>} 963 964 # The snippet's first atom parses with identity intact. 965 law 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]. 971 law 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. 975 law 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. 979 law angle_triples_auto_golden: 980 {B.angle_triples_auto([1, 2, 2, 3]) == [(1, 2, 3), (3, 2, 1)] : List<&1, U32 & U32 & U32>}