bend-prot

Releases (1):
  0.1.0.0  0xdf198d67659100c90a58ecd6b01d034d  indexed  https://jend.leeeet.dev/files.txt?path=bend-prot@0.1.0.0

Definitions (623, 1 to 100 shown):
  LAWS.empty_atoms (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=empty_atoms)
   def empty_atoms() -> List<&2, P.Atom>:
  LAWS.count_below_nil (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=count_below_nil)
   # Counting contacts in an empty set finds nothing, at any point and cutoff.
   law count_below_nil:
     for qp: G.Vec3
     for c2: F32
     {T.count_below(empty_atoms(), qp, c2) == 0n : Nat}
  LAWS.has_close_nil (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=has_close_nil)
   # An empty set has no clash, at any point and threshold.
   law has_close_nil:
     for qp: G.Vec3
     for min2: F32
     {T.has_close(empty_atoms(), qp, min2) == False{} : Bool}
  LAWS.empty_cx (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=empty_cx)
   def empty_cx() -> P.Complex:
  LAWS.sum_dist2_nil (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=sum_dist2_nil)
   # Spread of nothing is zero.
   law sum_dist2_nil:
     for qp: G.Vec3
     {T.sum_dist2(empty_atoms(), qp) == 0.0 : F32}
  LAWS.contacts_between_nil (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=contacts_between_nil)
   # An empty set links nothing to anything.
   law contacts_between_nil:
     for ys: List<&2, P.Atom>
     for c2: F32
     {T.contacts_between(empty_atoms(), ys, c2) == 0n : Nat}
  LAWS.min_dist2_nil (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=min_dist2_nil)
   # No closest approach exists from an empty set.
   law min_dist2_nil:
     for qp: G.Vec3
     {T.min_dist2_to(empty_atoms(), qp) == None{} : Maybe<&2, F32>}
  LAWS.complex_atoms_nil (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=complex_atoms_nil)
   # An empty complex holds no atoms.
   law complex_atoms_nil:
     {P.Complex.num_atoms(empty_cx()) == 0n : Nat}
  LAWS.lj_nil (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=lj_nil)
   # LJ energy of nothing is zero, at any parameters.
   law lj_nil:
     for eps: F32
     for sig2: F32
     for c2: F32
     {F.lj_total(empty_atoms(), empty_atoms(), eps, sig2, c2) == 0.0 : F32}
  LAWS.rmsd_nil (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=rmsd_nil)
   # The empty set is at zero RMSD from itself (empty case, by computation).
   # (This says nothing about nonempty sets; see rmsd_single. Unequal lengths
   # silently answer 0 by zip semantics; see rmsd_checked_some/none.)
   law rmsd_nil:
     {R.rmsd(empty_atoms(), empty_atoms()) == 0.0 : F32}
  LAWS.sasa_nil (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=sasa_nil)
   # Nothing has no surface.
   law sasa_nil:
     for rad: F32
     for rc2: F32
     for area_pt: F32
     {S.sasa_all(empty_atoms(), S.sasa_offsets(), rad, empty_atoms(), rc2, area_pt) == Nil{} : List<&2, F32>}
  LAWS.sd_fuel0 (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=sd_fuel0)
   # Zero minimization steps change nothing, on any input, not just nothing.
   law sd_fuel0:
     for xs: List<&2, P.Atom>
     for eps: F32
     for sig2: F32
     for c2: F32
     for dt: F32
     {F.minimize(0n, xs, eps, sig2, c2, dt) == xs : List<&2, P.Atom>}
  LAWS.count_cons (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=count_cons)
   # Counting a cons cell is the head hit plus the count of the tail.
   law count_cons:
     for h: P.Atom
     for t: List<&2, P.Atom>
     for qp: G.Vec3
     for c2: F32
     {T.count_below(h <> t, qp, c2) == Nat.add(T.count_below(t, qp, c2), T.head_hit_nat(h, qp, c2)) : Nat}
  LAWS.contacts_cons (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=contacts_cons)
   # Interface counting peels one head the same way.
   law contacts_cons:
     for x: P.Atom
     for xt: List<&2, P.Atom>
     for ys: List<&2, P.Atom>
     for c2: F32
     {T.contacts_between(x <> xt, ys, c2) == Nat.add(T.contacts_between(xt, ys, c2), T.contacts_of_head(x, ys, c2)) : Nat}
  LAWS.sumd2_count_cons (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=sumd2_count_cons)
   # The fused spread/count pass extends by one head distance.
   law sumd2_count_cons:
     for h: P.Atom
     for t: List<&2, P.Atom>
     for qp: G.Vec3
     {T.sumd2_count(h <> t, qp) == T.sumd2_extend(T.head_dist2(h, qp), T.sumd2_count(t, qp)) : F32 & Nat}
  LAWS.coord_cons (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=coord_cons)
   # Coordination counts peel one head.
   law coord_cons:
     for x: P.Atom
     for xt: List<&2, P.Atom>
     for ys: List<&2, P.Atom>
     for c2: F32
     {T.coord_counts(x <> xt, ys, c2) == T.contacts_of_head(x, ys, c2) <> T.coord_counts(xt, ys, c2) : List<&2, Nat>}
  LAWS.min_dist2_cons (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=min_dist2_cons)
   # Closest-approach folds one head into the running best.
   law min_dist2_cons:
     for h: P.Atom
     for t: List<&2, P.Atom>
     for qp: G.Vec3
     {T.min_dist2_to(h <> t, qp) == T.min_cons(h, T.min_dist2_to(t, qp), qp) : Maybe<&2, F32>}
  LAWS.min_link2_cons (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=min_link2_cons)
   # Set linkage folds one head linkage into the running best.
   law min_link2_cons:
     for h: P.Atom
     for t: List<&2, P.Atom>
     for ys: List<&2, P.Atom>
     {T.min_link2(h <> t, ys) == T.min_maybe(T.min_link2(t, ys), T.head_link(h, ys)) : Maybe<&2, F32>}
  LAWS.lj_row_cons (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=lj_row_cons)
   # An LJ row over a cons cell splits head from tail.
   law lj_row_cons:
     for pi: G.Vec3
     for eps: F32
     for sig2: F32
     for c2: F32
     for h: P.Atom
     for t: List<&2, P.Atom>
     {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}
  LAWS.lj_total_cons (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=lj_total_cons)
   # An LJ total over a cons cell splits head from tail.
   law lj_total_cons:
     for h: P.Atom
     for t: List<&2, P.Atom>
     for ys: List<&2, P.Atom>
     for eps: F32
     for sig2: F32
     for c2: F32
     {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}
  LAWS.coul_row_cons (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=coul_row_cons)
   # A Coulomb row splits head charge from tail charges.
   law coul_row_cons:
     for pi: G.Vec3
     for qi: F32
     for ke: F32
     for c2: F32
     for h: P.Atom
     for t: List<&2, P.Atom>
     for qh: F32
     for qt: List<&2, F32>
     {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}
  LAWS.coul_total_cons (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=coul_total_cons)
   # A Coulomb total splits head charge from tail charges.
   law coul_total_cons:
     for h: P.Atom
     for t: List<&2, P.Atom>
     for qh: F32
     for qt: List<&2, F32>
     for ys: List<&2, P.Atom>
     for qs_e: List<&2, F32>
     for ke: F32
     for c2: F32
     {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}
  LAWS.sd_sweep_cons (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=sd_sweep_cons)
   # A sweep over cons cells moves the head and sweeps the tail.
   law sd_sweep_cons:
     for h: P.Atom
     for t: List<&2, P.Atom>
     for f: G.Vec3
     for ft: List<&2, G.Vec3>
     for dt: F32
     {F.sd_sweep(h <> t, f <> ft, dt) == F.sd_move(h, f, dt) <> F.sd_sweep(t, ft, dt) : List<&2, P.Atom>}
  LAWS.pair_sumd2_cons (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=pair_sumd2_cons)
   # A pair-distance fold splits the head pair from the tail pairs.
   law pair_sumd2_cons:
     for x: P.Atom
     for xt: List<&2, P.Atom>
     for y: P.Atom
     for yt: List<&2, P.Atom>
     {R.pair_sumd2(x <> xt, y <> yt) == R.pair_head(x, y, R.pair_sumd2(xt, yt)) : F32 & Nat}
  LAWS.rmsd_to_all_cons (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=rmsd_to_all_cons)
   # Scoring against a cons ensemble scores the head and the tail.
   law rmsd_to_all_cons:
     for q: List<&2, P.Atom>
     for h: List<&2, P.Atom>
     for t: List<&2, List<&2, P.Atom>>
     {R.rmsd_to_all(q, h <> t) == R.rmsd_against(q, h) <> R.rmsd_to_all(q, t) : List<&2, F32>}
  LAWS.count_single (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=count_single)
   # Counting one atom is that atom's hit.
   law count_single:
     for h: P.Atom
     for qp: G.Vec3
     for c2: F32
     {T.count_below([h], qp, c2) == T.head_hit_nat(h, qp, c2) : Nat}
  LAWS.has_close_single (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=has_close_single)
   # One atom is close exactly when its head test says so.
   law has_close_single:
     for h: P.Atom
     for qp: G.Vec3
     for min2: F32
     {T.has_close([h], qp, min2) == T.head_is_close(h, qp, min2) : Bool}
  LAWS.min_single (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=min_single)
   # The closest approach to a singleton is its one distance.
   law min_single:
     for s: U32
     for e: U32
     for x: F32
     for y: F32
     for z: F32
     for qx: F32
     for qy: F32
     for qz: F32
     {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>}
  LAWS.rg_about_nil (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=rg_about_nil)
   # Spread about a point of nothing is zero through rg_of.
   law rg_about_nil:
     for qp: G.Vec3
     {T.rg_about(empty_atoms(), qp) == 0.0 : F32}
  LAWS.rmsd_single (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=rmsd_single)
   # A singleton is at the RMSD its one pair distance dictates.
   law rmsd_single:
     for s: U32
     for e: U32
     for x: F32
     for y: F32
     for z: F32
     {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}
  LAWS.rng_next_0 (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=rng_next_0)
   # splitmix32 golden values (catches mistyped mixer constants).
   law rng_next_0:
     {Rng.rng_next(0) == 1684164658 : U32}
  LAWS.rng_next_1 (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=rng_next_1)
   law rng_next_1:
     {Rng.rng_next(1) == 1580013426 : U32}
  LAWS.sasa_single (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=sasa_single)
   # One atom with nothing near it exposes all six sample points.
   law sasa_single:
     {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>}
  LAWS.pair_trunc_right (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=pair_trunc_right)
   # Pair folds against an empty list answer the identity.
   law pair_trunc_right:
     for x: P.Atom
     for xt: List<&2, P.Atom>
     {R.pair_sumd2(x <> xt, empty_atoms()) == (0.0, 0n) : F32 & Nat}
  LAWS.coul_trunc_charges (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=coul_trunc_charges)
   # Coulomb with no charges answers zero, however many atoms remain.
   law coul_trunc_charges:
     for h: P.Atom
     for t: List<&2, P.Atom>
     for ys: List<&2, P.Atom>
     for qs: List<&2, F32>
     for ke: F32
     for c2: F32
     {F.coul_total(h <> t, Nil{}, ys, qs, ke, c2) == 0.0 : F32}
  LAWS.sd_trunc_forces (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=sd_trunc_forces)
   # A sweep with no forces leaves the atoms in place.
   law sd_trunc_forces:
     for h: P.Atom
     for t: List<&2, P.Atom>
     for dt: F32
     {F.sd_sweep(h <> t, Nil{}, dt) == h <> t : List<&2, P.Atom>}
  LAWS.contacts_nil_right (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=contacts_nil_right)
   # Nothing links to anything, however many heads are peeled.
   law contacts_nil_right:
     for xs: List<&2, P.Atom>
     for c2: F32
     {T.contacts_between(xs, empty_atoms(), c2) == 0n : Nat}
  LAWS.min_link2_nil_right (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=min_link2_nil_right)
   # No closest approach exists from any set held against nothing.
   law min_link2_nil_right:
     for xs: List<&2, P.Atom>
     {T.min_link2(xs, empty_atoms()) == None{} : Maybe<&2, F32>}
  LAWS.rmsd_checked_some (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=rmsd_checked_some)
   # Equal-length singletons check cleanly.
   law rmsd_checked_some:
     for x: P.Atom
     for y: P.Atom
     {R.rmsd_checked([x], [y]) == Some{R.rmsd([x], [y])} : Maybe<&2, F32>}
  LAWS.rmsd_checked_none (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=rmsd_checked_none)
   # Unequal lengths answer None{} instead of a silent zero.
   law rmsd_checked_none:
     for x: P.Atom
     {R.rmsd_checked([x], empty_atoms()) == None{} : Maybe<&2, F32>}
  LAWS.append_atoms_assoc (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=append_atoms_assoc)
   # Appending atom lists associates.
   law append_atoms_assoc:
     for xs: List<&2, P.Atom>
     for ys: List<&2, P.Atom>
     for zs: List<&2, P.Atom>
     {P.append_atoms(P.append_atoms(xs, ys), zs) == P.append_atoms(xs, P.append_atoms(ys, zs)) : List<&2, P.Atom>}
  LAWS.flatten_residues_append (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=flatten_residues_append)
   # Flattening distributes over appending residue lists.
   law flatten_residues_append:
     for xs: List<&2, P.Residue>
     for ys: List<&2, P.Residue>
     {P.flatten_residues(P.append_residues(xs, ys)) == P.append_atoms(P.flatten_residues(xs), P.flatten_residues(ys)) : List<&2, P.Atom>}
  LAWS.add_zero_right (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=add_zero_right)
   # Adding zero on the right changes nothing (induction seed for comm).
   law add_zero_right:
     for b: Nat
     {Nat.add(b, 0n) == b : Nat}
  LAWS.add_succ_right (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=add_succ_right)
   # Adding a successor on the right pulls out front.
   law add_succ_right:
     for b: Nat
     for a: Nat
     {Nat.add(b, 1n+a) == 1n+Nat.add(b, a) : Nat}
  LAWS.add_comm (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=add_comm)
   # Nat addition commutes.
   law add_comm:
     for a: Nat
     for b: Nat
     {Nat.add(a, b) == Nat.add(b, a) : Nat}
  LAWS.count_atoms_append (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=count_atoms_append)
   # Counting an append splits into the counts.
   law count_atoms_append:
     for xs: List<&2, P.Atom>
     for ys: List<&2, P.Atom>
     {P.count_atoms(P.append_atoms(xs, ys)) == Nat.add(P.count_atoms(xs), P.count_atoms(ys)) : Nat}
  LAWS.count_flatten_eq (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=count_flatten_eq)
   # Counting a flattening agrees with counting residues in place.
   law count_flatten_eq:
     for rs: List<&2, P.Residue>
     {P.count_atoms(P.flatten_residues(rs)) == P.count_atoms_in(rs) : Nat}
  LAWS.complex_flatten_eq (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=complex_flatten_eq)
   # A complex holds as many atoms as its flattening lists.
   law complex_flatten_eq:
     for chains: List<&2, P.Chain>
     {P.Complex.num_atoms(P.Complex{chains}) == P.count_atoms(P.Complex.flatten(P.Complex{chains})) : Nat}
  LAWS.pow10_3 (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=pow10_3)
   # 10^3 is 1000.
   law pow10_3:
     {Pdb.pow10(3n) == 1000 : U32}
  LAWS.elem_iron (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=elem_iron)
   # Iron reads as 26.
   law elem_iron:
     {Pdb.elem_no("FE") == 26 : U32}
  LAWS.elem_carbon (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=elem_carbon)
   # Carbon reads as 6.
   law elem_carbon:
     {Pdb.elem_1('C') == 6 : U32}
  LAWS.atom_line_yes (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=atom_line_yes)
   # ATOM records (6-column tag) pass the filter.
   law atom_line_yes:
     {Pdb.is_atom_line("ATOM      1  N   ALA A   1") == True{} : Bool}
  LAWS.atom_line_no (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=atom_line_no)
   # Anything else does not.
   law atom_line_no:
     {Pdb.is_atom_line("HETATM 9999  O   HOH A 101") == False{} : Bool}
  LAWS.atom_lines_nil (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=atom_lines_nil)
   # No lines in, no lines out.
   law atom_lines_nil:
     {Pdb.atom_lines(Nil{}) == Nil{} : List<&2, String>}
  LAWS.atom_lines_keep (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=atom_lines_keep)
   # Non-ATOM lines drop, ENDMDL stops the file, the tail never parses.
   law atom_lines_keep:
     {Pdb.atom_lines(["ATOM      1  N", "TER", "ENDMDL", "ATOM      2  CA"]) == ["ATOM      1  N"] : List<&2, String>}
  LAWS.parse_f32_one (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=parse_f32_one)
   # 12.5 parses to 12 + 5/10 (stuck F32, identical both sides).
   law parse_f32_one:
     {Pdb.parse_f32("12.5") == Some{(U32.to_f32(12) + (U32.to_f32(5) / U32.to_f32(10) : F32) : F32)} : Maybe<&2, F32>}
  LAWS.parse_f32_neg (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=parse_f32_neg)
   # Signs apply outside the magnitude.
   law parse_f32_neg:
     {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>}
  LAWS.parse_f32_bad (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=parse_f32_bad)
   # Non-numeric fields fail instead of answering zero.
   law parse_f32_bad:
     {Pdb.parse_f32("abc") == None{} : Maybe<&2, F32>}
  LAWS.pdb_num_atoms (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=pdb_num_atoms)
   # The two-line ALA snippet parses to two atoms ...
   law pdb_num_atoms:
     {P.Complex.num_atoms(Pdb.complex_of(Pdb.parse_pdb(Pdb.demo_text()))) == 2n : Nat}
  LAWS.pdb_num_residues (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=pdb_num_residues)
   # ... in one residue ...
   law pdb_num_residues:
     {P.Complex.num_residues(Pdb.complex_of(Pdb.parse_pdb(Pdb.demo_text()))) == 1n : Nat}
  LAWS.pdb_num_chains (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=pdb_num_chains)
   # ... in one chain ...
   law pdb_num_chains:
     {P.Complex.num_chains(Pdb.complex_of(Pdb.parse_pdb(Pdb.demo_text()))) == 1n : Nat}
  LAWS.pdb_skipped_0 (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=pdb_skipped_0)
   # ... with nothing skipped ...
   law pdb_skipped_0:
     {Pdb.skipped_of(Pdb.parse_pdb(Pdb.demo_text())) == 0n : Nat}
  LAWS.pdb_skipped_1 (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=pdb_skipped_1)
   # ... while a bad serial skips exactly its line.
   law pdb_skipped_1:
     {Pdb.skipped_of(Pdb.parse_pdb(Pdb.demo_bad_text())) == 1n : Nat}
  LAWS.pdb_bad_atoms (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=pdb_bad_atoms)
   law pdb_bad_atoms:
     {P.Complex.num_atoms(Pdb.complex_of(Pdb.parse_pdb(Pdb.demo_bad_text()))) == 1n : Nat}
  LAWS.pdb_first_elem (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=pdb_first_elem)
   # ... and the first atom is nitrogen.
   law pdb_first_elem:
     {Pdb.first_elem(Pdb.complex_of(Pdb.parse_pdb(Pdb.demo_text()))) == Some{7} : Maybe<&2, U32>}
  LAWS.sasa_total_cons (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=sasa_total_cons)
   # Total area splits head from tail.
   law sasa_total_cons:
     for h: F32
     for t: List<&2, F32>
     {S.sasa_total(h <> t) == (h + S.sasa_total(t) : F32) : F32}
  LAWS.count_par4_nil (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=count_par4_nil)
   # Empty input counts nothing, through the fallback arm.
   law count_par4_nil:
     for qp: G.Vec3
     for c2: F32
     {Par.count_par4(empty_atoms(), qp, c2) == 0n : Nat}
  LAWS.count_par4_step (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=count_par4_step)
   # A full unrolled step splits four parallel hits plus the tail.
   law count_par4_step:
     for h1: P.Atom
     for h2: P.Atom
     for h3: P.Atom
     for h4: P.Atom
     for t: List<&2, P.Atom>
     for qp: G.Vec3
     for c2: F32
     {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}
  LAWS.count_par4_small (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=count_par4_small)
   # Short inputs take the sequential fallback exactly.
   law count_par4_small:
     for h: P.Atom
     for qp: G.Vec3
     for c2: F32
     {Par.count_par4([h], qp, c2) == T.count_below([h], qp, c2) : Nat}
  LAWS.lj_row_par4_nil (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=lj_row_par4_nil)
   # Empty rows sum nothing, through the fallback arm.
   law lj_row_par4_nil:
     for pi: G.Vec3
     for eps: F32
     for sig2: F32
     for c2: F32
     {Par.lj_row_par4(pi, eps, sig2, c2, empty_atoms()) == 0.0 : F32}
  LAWS.lj_row_par4_step (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=lj_row_par4_step)
   # A full unrolled row splits four parallel heads plus the tail.
   law lj_row_par4_step:
     for pi: G.Vec3
     for eps: F32
     for sig2: F32
     for c2: F32
     for h1: P.Atom
     for h2: P.Atom
     for h3: P.Atom
     for h4: P.Atom
     for t: List<&2, P.Atom>
     {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}
  LAWS.lj_row_par4_small (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=lj_row_par4_small)
   # Short rows take the sequential fallback exactly.
   law lj_row_par4_small:
     for pi: G.Vec3
     for eps: F32
     for sig2: F32
     for c2: F32
     for h: P.Atom
     {Par.lj_row_par4(pi, eps, sig2, c2, [h]) == F.lj_row(pi, eps, sig2, c2, [h]) : F32}
  LAWS.lj_eps_c (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=lj_eps_c)
   # Carbon takes illustrative OPLS-style parameters.
   law lj_eps_c:
     {F.lj_eps(6) == 0.066 : F32}
  LAWS.lj_eps_h (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=lj_eps_h)
   law lj_eps_h:
     {F.lj_eps(1) == 0.03 : F32}
  LAWS.lj_sig_o (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=lj_sig_o)
   law lj_sig_o:
     {F.lj_sig(8) == 2.96 : F32}
  LAWS.lj_sig_default (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=lj_sig_default)
   # Unknown elements take the generic pair.
   law lj_sig_default:
     {F.lj_sig(99) == 3.0 : F32}
  LAWS.lj_row_elem_cons (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=lj_row_elem_cons)
   # An element row over a cons cell splits head from tail.
   law lj_row_elem_cons:
     for si: U32
     for pi: G.Vec3
     for c2: F32
     for h: P.Atom
     for t: List<&2, P.Atom>
     {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}
  LAWS.lj_total_elem_cons (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=lj_total_elem_cons)
   # An element total over a cons cell splits head from tail.
   law lj_total_elem_cons:
     for h: P.Atom
     for t: List<&2, P.Atom>
     for ys: List<&2, P.Atom>
     for c2: F32
     {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}
  LAWS.bond_total_nil (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=bond_total_nil)
   # No bonds bind nothing.
   law bond_total_nil:
     for k: F32
     {B.bond_total(empty_atoms(), Nil{}, k) == 0.0 : F32}
  LAWS.bond_total_cons (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=bond_total_cons)
   # A bond total splits head bond from tail bonds.
   law bond_total_cons:
     for xs: List<&2, P.Atom>
     for s1: U32
     for s2: U32
     for t: List<&1, U32 & U32>
     for k: F32
     {B.bond_total(xs, (s1, s2) <> t, k) == (B.bond_cov_pair(xs, s1, s2, k) + B.bond_total(xs, t, k) : F32) : F32}
  LAWS.angle_total_nil (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=angle_total_nil)
   # No angles bend nothing.
   law angle_total_nil:
     for k: F32
     for eq: F32
     {B.angle_total(empty_atoms(), Nil{}, k, eq) == 0.0 : F32}
  LAWS.angle_total_cons (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=angle_total_cons)
   # An angle total splits head triple from tail triples.
   law angle_total_cons:
     for xs: List<&2, P.Atom>
     for sa: U32
     for sb: U32
     for sc: U32
     for t: List<&1, U32 & U32 & U32>
     for k: F32
     for eq: F32
     {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}
  LAWS.pos_of_serial_none (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=pos_of_serial_none)
   # Nobody is found in nothing.
   law pos_of_serial_none:
     for s: U32
     {B.pos_of_serial(empty_atoms(), s) == None{} : Maybe<&2, G.Vec3>}
  LAWS.pos_of_serial_some (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=pos_of_serial_some)
   # A singleton finds its atom's position.
   law pos_of_serial_some:
     {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>}
  LAWS.bonded12_nil (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=bonded12_nil)
   # No bonds exclude nothing.
   law bonded12_nil:
     for a: U32
     for b: U32
     {B.bonded12_flat(Nil{}, a, b) == False{} : Bool}
  LAWS.bonded12_hit (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=bonded12_hit)
   # A listed pair (either order) is 1-2 excluded.
   law bonded12_hit:
     {B.bonded12_flat([1, 2], 1, 2) == True{} : Bool}
  LAWS.bonded12_miss (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=bonded12_miss)
   # An unlisted pair is not.
   law bonded12_miss:
     {B.bonded12_flat([1, 2], 1, 3) == False{} : Bool}
  LAWS.neighbors_one (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=neighbors_one)
   # Neighbors of 1 in [(1,2),(2,3)] are just [2].
   law neighbors_one:
     {B.bond_neighbors(1, [1, 2, 2, 3]) == [2] : List<&2, U32>}
  LAWS.excluded13_one (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=excluded13_one)
   # 1 and 3 share neighbor 2.
   law excluded13_one:
     {B.excluded13(1, 3, [1, 2, 2, 3]) == True{} : Bool}
  LAWS.excluded_both (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=excluded_both)
   # 2 and 3 are directly bonded (1-2 wins over 1-3 either way).
   law excluded_both:
     {B.excluded(2, 3, [1, 2, 2, 3]) == True{} : Bool}
  LAWS.flatten_bonds_one (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=flatten_bonds_one)
   # Pair bonds flatten in order.
   law flatten_bonds_one:
     {B.flatten_bonds([(1, 2)]) == [1, 2] : List<&2, U32>}
  LAWS.lj_row_excl_nil (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=lj_row_excl_nil)
   # Excluded rows sum nothing over nothing.
   law lj_row_excl_nil:
     for si: U32
     for pi: G.Vec3
     for eps: F32
     for sig2: F32
     for c2: F32
     for bonds: List<&2, U32>
     {B.lj_row_excl(si, pi, eps, sig2, c2, empty_atoms(), bonds) == 0.0 : F32}
  LAWS.lj_total_excl_nil (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=lj_total_excl_nil)
   law lj_total_excl_nil:
     for ys: List<&2, P.Atom>
     for eps: F32
     for sig2: F32
     for c2: F32
     for bonds: List<&2, U32>
     {B.lj_total_excl(empty_atoms(), ys, eps, sig2, c2, bonds) == 0.0 : F32}
  LAWS.coul_row_excl_nil (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=coul_row_excl_nil)
   law coul_row_excl_nil:
     for si: U32
     for pi: G.Vec3
     for qi: F32
     for ke: F32
     for c2: F32
     for bonds: List<&2, U32>
     {B.coul_row_excl(si, pi, qi, ke, c2, empty_atoms(), Nil{}, bonds) == 0.0 : F32}
  LAWS.coul_total_excl_nil (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=coul_total_excl_nil)
   law coul_total_excl_nil:
     for ys: List<&2, P.Atom>
     for qs_e: List<&2, F32>
     for ke: F32
     for c2: F32
     for bonds: List<&2, U32>
     {B.coul_total_excl(empty_atoms(), Nil{}, ys, qs_e, ke, c2, bonds) == 0.0 : F32}
  LAWS.lj_row_elem_excl_nil (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=lj_row_elem_excl_nil)
   # Element-excluded rows/totals sum nothing over nothing.
   law lj_row_elem_excl_nil:
     for si: U32
     for se: U32
     for pi: G.Vec3
     for c2: F32
     for bonds: List<&2, U32>
     {B.lj_row_elem_excl(si, se, pi, empty_atoms(), c2, bonds) == 0.0 : F32}
  LAWS.lj_total_elem_excl_nil (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=lj_total_elem_excl_nil)
   law lj_total_elem_excl_nil:
     for ys: List<&2, P.Atom>
     for c2: F32
     for bonds: List<&2, U32>
     {B.lj_total_elem_excl(empty_atoms(), ys, c2, bonds) == 0.0 : F32}
  LAWS.lj_row_elem_excl_hit (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=lj_row_elem_excl_hit)
   # A directly bonded pair contributes exactly 0.0 (wiring pin: the row must
   # test serials, not elements; the sum is (0.0 + 0.0) since F32.add is stuck).
   law lj_row_elem_excl_hit:
     {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}
  LAWS.lj_row_elem_excl_link (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=lj_row_elem_excl_link)
   # Same through a 1-3 link.
   law lj_row_elem_excl_link:
     {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}
  LAWS.conect_lines_nil (https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/LAWS.bend&name=conect_lines_nil)
   # No lines in, no bonds out.
   law conect_lines_nil:
     {Pdb.conect_lines(Nil{}) == Nil{} : List<&2, String>}
More: https://jend.leeeet.dev/packages/bend-prot.txt?definitions_offset=100