TrapForge

Author verifiable, adversarial data tasks for AI agents - and prove they have exactly one right answer.

Most "hard" data tasks for agents are hard for the wrong reason: the instructions are ambiguous, several answers are defensible, and the grader quietly rewards whichever one the author happened to pick. TrapForge is being built to take the opposite approach: every task ships with a machine-checked argument that its data admits exactly one interpretation. The target pipeline is a synthetic corpus with hidden integer structure, an exact constraint system built from what the corpus reveals, a uniqueness proof (or a concrete counterexample pair of hidden worlds), a reference solver, a naive baseline that fails on hidden deciding cases, and a byte-exact pytest grader.

What exists today is the exact math that pipeline stands on, the uniqueness prover built on it (a constraint model, an exact solver that returns a unique world or a concrete counterexample pair, JSON certificates with a standalone checker, a gate that extends a sample until the proof holds), a task-family plugin API with canonical byte-exact writers, the first task family (an affine-scrambled ledger with a reference solver and a naive baseline that it traps), and a CLI over all of it. Everything is pure Python 3.12 integers (no floats, no numpy), implemented from scratch and property-tested against brute force and sympy (a dev-only oracle). Any generated instance exports as a self-contained task bundle (digest-pinned Dockerfile, standalone reference solver and baseline, byte-exact SHA-256 grader, uniqueness certificate), and trapforge verify proves the reference passes and the baseline fails, locally and in Docker with the network disabled. The other two task families are on the Roadmap.

Why this exists

This project generalizes the kind of work I do building benchmark tasks for AI coding agents at an AI-data company: reproducible environments, reference solutions that really compute the answer, byte-exact graders, and synthetic datasets that are provably unambiguous. All task designs, examples and data here are original.

Features (implemented and tested)

Area	Module	What it gives you
Modular arithmetic	trapforge.modular	extended gcd, modular inverse with typed errors, CRT for non-coprime moduli, full solution sets of a*x = b (mod m) and of mixed-moduli systems, and re-checkable inconsistency proofs
Integer linear algebra	trapforge.linalg	immutable Matrix with Bareiss determinant and rank, Hermite and Smith normal forms with unimodular transforms, saturated integer kernels, solve_diophantine returning an AffineLattice or an UnsolvableSystem certificate, exact lexicographic enumeration of lattice points in a box
Prover constraint model	trapforge.prover	bounded integer unknowns, linear equations, linear congruences and a finite case split over discrete choices (for example an unknown counter period), with validation, case instantiation, violation reports and a JSON round trip
Uniqueness prover	trapforge.prover.prove	reduces every case to one Diophantine system (one slack per congruence), solves it with solve_diophantine, enumerates the lattice inside the box, and returns UniqueProof, Ambiguity (counterexample pair plus the exact size of the ambiguity space, or a capped lower bound) or Infeasible
Certificates	trapforge.prover.check_certificate	canonical JSON certificate per verdict; a standalone checker (standard library only) re-verifies it without the solver: lattice point, kernel basis, integer right inverse and a nonsingular rank minor per solvable case, integer Fredholm weights per unsolvable case
Uniqueness gate	trapforge.prover.gate	extends a generated sample with further observations, lazily, until exactly one world fits; stops at the shortest prefix, records the ambiguity size after each step, and raises on a planted world that breaks the sample
Canonical writers	trapforge.canonical	byte-exact CSV, JSON and text writers (\n endings, sorted keys, ASCII, no floats, no CSV quoting: cells that would need it are rejected), a strict CSV reader, and a SHA-256 digest over a whole file set
Task-family plugin API	trapforge.families	TaskFamily protocol (generate, solve, baseline), TaskInstance (corpus, hidden world, expected bytes, visible sample, constraint system), Difficulty, a validating Registry, and a string-seeded RNG so a (family, difficulty, seed) triple gives the same bytes in every process
Affine ledger family	trapforge.families.ledger	account numbers scrambled by x -> (a*x + b) mod m with composite m; every instance is gated to a unique map; a reference solver built on linear congruences; a naive baseline that treats m as prime and is right on the visible sample, wrong on every hidden deciding record
Bundle exporter	trapforge.bundle	instruction.md, data/, a Dockerfile pinned to a python:3.12-slim digest, solution/ and baseline/ solvers that vendor TrapForge's pure-Python modules (no installs), tests/test_outputs.py grading byte for byte against an embedded SHA-256 (the expected bytes are not shipped), proof/uniqueness.cert.json and task.json; refuses instances whose answer is not unique; golden files pin the layout
Bundle verifier	trapforge.verify	re-checks that the certificate proves a unique answer, runs both solvers and the bundle's grader in fresh copies with python -I -S (no site-packages), and repeats the runs in a container with --network none when Docker answers, then removes the image; the grader always runs on whatever the baseline wrote (a nonzero exit is not enough to count as trapped), a baseline that is missing or cannot start is a failed check, and a solver past 600 s is stopped (its container removed) and graded instead of crashing the run
CLI	trapforge	crt, solve, system, prove, check, families, generate, export and verify commands over the layers above, plus info
Container	Dockerfile	multi-stage uv build on python:3.12-slim pinned by digest, non-root user, LABEL project=trapforge
Demo	make demo	scripts/demo.sh runs the CLI over the bundled examples/ inputs and one generated task, then exports and verifies it (the image run skips the two bundle steps)

Every "no solution" answer comes with a certificate that can be re-checked without trusting the solver: a conflicting pair of congruences and a witness modulus, or integer weights w and a modulus d such that d divides every entry of w A but not w . b.

Quickstart

Requires uv and make. No GPU, no API keys, no network at run time.

git clone https://github.com/vipul21435/trapforge.git
cd trapforge
uv sync        # locked runtime + dev dependencies
make check     # ruff, mypy --strict, pytest with the 85% branch-coverage gate
make demo      # the CLI end to end on examples/

These five commands were run in a fresh clone: make check reported 792 passed at 99.66% branch coverage, and the whole sequence (clone, sync, check, demo) took 57 s wall time on an Apple-silicon laptop, Docker test and demo steps included. With Docker, make docker-demo builds the image and runs the same demo inside it.

CLI usage

The command list from trapforge --help (Typer draws it in a box; the frame is dropped here):

Usage: trapforge [OPTIONS] COMMAND [ARGS]...
Commands:
  info      Print the package version and the Python it runs on.
  crt       Combine congruences with any moduli (coprime or not) into one residue class.
  solve     Solve an integer system A x = b exactly and list its solutions inside a box.
  system    Validate and print a constraint system; optionally test a candidate assignment.
  prove     Decide how many hidden worlds fit a constraint system, with a re-checked certificate.
  check     Re-check a uniqueness certificate from scratch, without running the solver.
  families  List the registered task families.
  generate  Generate one task instance, prove it unique and run its reference and baseline.
  export    Export one instance as a self-contained task bundle (see `trapforge verify`).
  verify    Prove that the reference passes and the baseline fails, locally and in Docker.

Exit code 0 means the input was valid (with or without a solution); 1 means a check failed (check on a certificate that does not hold, prove --require-unique on a sample that is not unique, generate on an instance that is not unique, not reproduced by its reference solver or not missed by its baseline, verify on a bundle whose reference fails or whose baseline passes); 2 means the input could not be read or parsed. The outputs below are copied from make demo.

crt combines congruences whose moduli share factors, or proves they conflict:

$ trapforge crt 5:12 5:18
#0: x = 5 (mod 12)
#1: x = 5 (mod 18)
combined: x = 5 (mod 36)

$ trapforge crt 1:4 2:6
#0: x = 1 (mod 4)
#1: x = 2 (mod 6)
no solution: congruences #0 and #1 are incompatible: #0 forces x = 1 (mod 2) but #1 forces x = 0 (mod 2)
certificate re-checked: True

solve reads {"matrix", "rhs", "lower", "upper"} from JSON, prints the whole integer solution lattice and the points inside the box, and says whether the box pins down one point:

$ trapforge solve examples/checksums.json
system: 2 equations, 3 unknowns
integer solutions: x = (4, 2, 7) + t0*(290, -699, 67), t in Z^1
  (4, 2, 7)
box (0, 0, 0)..(9, 9, 9): exactly one point in the box (unique)

$ trapforge solve examples/checksums-ambiguous.json --limit 3
system: 1 equation, 3 unknowns
integer solutions: x = (0, 0, 13) + t0*(1, 0, -1) + t1*(0, 1, -1), t in Z^2
  (0, 4, 9)
  (0, 5, 8)
  (0, 6, 7)
box (0, 0, 0)..(9, 9, 9): more than 3 points in the box (ambiguous)

$ trapforge solve examples/parity.json
system: 2 equations, 2 unknowns
no integer solution: weighting the equations by (0, 1) makes every coefficient a multiple of 2, but the right-hand side becomes 1, which is not
certificate re-checked: True

system loads a constraint system in the prover's JSON format and tests candidate hidden worlds against it. The bundled ledger example is the trap the affine-ledger family is built around: with a composite modulus, two different affine maps fit every anchor.

$ trapforge system examples/ledger-anchors.json --check a=5 --check b=7
unknowns: 1 <= a <= 11, 0 <= b <= 11
anchor x=1: a + b = 0 (mod 12)
anchor x=3: 3*a + b = 10 (mod 12)
2 unknowns, 2 constraints, 1 case
a=5, b=7 satisfies every constraint

$ trapforge system examples/ledger-anchors.json --check a=11 --check b=1
...
a=11, b=1 satisfies every constraint

$ trapforge system examples/wrapping-clock.json --check P=18 --check T=41 --check w=2
choices: P in {12, 18}
unknowns: 0 <= T <= 100, 0 <= w <= 8
beacon: T - P*w = 5
sync: T = 5 (mod 36)
2 unknowns, 2 constraints, 2 cases
P=18, T=41, w=2 satisfies every constraint

prove decides how many hidden worlds fit, prints a counterexample pair when there is more than one, and re-checks its own certificate with the standalone checker. --certificate FILE writes the certificate as canonical JSON; --require-unique turns "not unique" into exit code 1 for scripted gating.

$ trapforge prove examples/ledger-anchors.json
system: 2 unknowns, 2 constraints, 1 case
ambiguous: exactly 2 worlds fit, for example a=5, b=7 and a=11, b=1 (they differ in a, b)
certificate re-checked: True (verified: ambiguous, 2 solutions)

$ trapforge prove examples/ledger-anchors-unique.json
system: 2 unknowns, 3 constraints, 1 case
unique: a=5, b=7
certificate re-checked: True (verified: unique, 1 solution)

$ trapforge prove examples/wrapping-clock.json
system: 2 unknowns, 2 constraints, 2 cases
ambiguous: exactly 6 worlds fit, for example P=12, T=5, w=0 and P=12, T=41, w=3 (they differ in T, w)
certificate re-checked: True (verified: ambiguous, 6 solutions)

check re-verifies a certificate using only the checker (exit 1 if it does not hold). examples/ledger-anchors-unique.cert.json is the certificate prove --certificate writes for the unique ledger; a test regenerates it and compares the bytes.

$ trapforge check examples/ledger-anchors-unique.cert.json
verified: unique, 1 solution

The lattice evidence in that certificate (an excerpt, indentation trimmed):

"basis": [
  [12, 0, 1, 3, 2],
  [0, 12, 1, 1, 1]
],
"evidence": "lattice",
"minor": {
  "columns": [0, 1, 2],
  "rows": [0, 1, 2]
},
"point": [5, 7, 1, 1, 1],

The columns are (a, b, s1, s2, s3), one slack per congruence. The basis moves a and b only in steps of 12, so the box 1 <= a <= 11, 0 <= b <= 11 holds the single point a=5, b=7; the rank-3 minor shows there are no further kernel directions.

families and generate run the task-family registry. generate builds one instance, proves the constraint system its corpus implies, runs the reference solver and the naive baseline, and prints the instance's SHA-256; --out DIR writes its files.

$ trapforge families
affine-ledger: account numbers scrambled by x -> (a*x + b) mod m with composite m

$ trapforge generate affine-ledger --seed 7
affine-ledger / easy / seed 7
  anchors: 4
  deciding_records: 4
  decoy_anchors: 0
  modulus: 36
  sample_records: 2
  shared_factor: 4
  transactions: 40
  worlds_from_first_two_anchors: 4
proof: unique: a=17, b=7 (certificate re-checked: True)
reference: matches the expected output
baseline: 4 of 7 output lines differ; matches the visible sample
sha256: c91f178cc5830e227c04c9b436b7b79a1c0007286c33ef79aadb55a569471e4d

The same command inside the Linux image (make docker-demo) printed the same SHA-256.

export and verify turn that instance into a task bundle and check it. The output directory must not exist or be empty; verify runs Docker when a daemon answers (--docker requires it, --no-docker skips it) and exits 1 when any check fails:

$ trapforge export affine-ledger --seed 7 --out bundle
affine-ledger / easy / seed 7
  data/: 4 files
  solution/: 20 files
  baseline/: 20 files
  tests/: 1 file
  proof/: 1 file
wrote 49 files under bundle

$ find bundle -path '*/vendor' -prune -o -type f -print | sort
bundle/Dockerfile
bundle/baseline/solve.py
bundle/data/anchors.csv
bundle/data/ledger.csv
bundle/data/params.json
bundle/data/queries.csv
bundle/instruction.md
bundle/proof/uniqueness.cert.json
bundle/solution/solve.py
bundle/task.json
bundle/tests/test_outputs.py

$ trapforge verify bundle
ok   certificate proves a unique answer: verified: unique, 1 solution
ok   local solution passes the grader: PASS test_output_matches_byte_for_byte
ok   local baseline fails the grader: FAIL test_output_matches_byte_for_byte: expected 72 bytes, got 69
ok   docker image builds: built trapforge-task:trapforge-verify-s3cw5t3d from the pinned base image
ok   docker solution passes the grader: PASS test_output_matches_byte_for_byte
ok   docker baseline fails the grader: FAIL test_output_matches_byte_for_byte: expected 72 bytes, got 69
verified

The bundle's Dockerfile bakes in only the instruction and the corpus:

FROM python:3.12-slim@sha256:f77ac9e44ae96ef2c90b8053ea08c31f8be030f824196b0ae4db6d462c84e51f
LABEL project=trapforge \
      trapforge.family="affine-ledger" \
      trapforge.difficulty="easy" \
      trapforge.seed="7"
RUN useradd --create-home --uid 10001 solver \
    && mkdir -p /task/output \
    && chown solver /task/output
WORKDIR /task
COPY instruction.md ./
COPY data/ data/
USER solver

verify mounts solution/ (or baseline/) and tests/ read-only plus an empty output/, and runs python -I -S solution/solve.py /task and then python -I -S tests/test_outputs.py in containers started with --network none. The grader also runs under pytest (pytest tests/test_outputs.py, 2 tests).

Library usage

from trapforge.modular import Congruence, LinearCongruence, crt, solve_linear_system

# Two counters that wrap at 12 and 18 both read 5: when can that happen?
print(crt([Congruence(5, 12), Congruence(5, 18)]))

# An affine scramble 6*x + 4 (mod 10) produced 0. Which x mod 10 are possible?
scramble = LinearCongruence(6, -4, 10)
print(list(scramble.solve().residues_mod(10)))

# One more fact (x is odd) pins x down; a contradicting fact yields a checkable proof.
print(solve_linear_system([scramble, Congruence(1, 2)]))
system = [scramble, Congruence(2, 10)]
proof = solve_linear_system(system)
print(proof)
print(proof.verify(system))

x = 5 (mod 36)
[1, 6]
x = 1 (mod 10)
congruences #0 and #1 are incompatible: #0 forces x = 1 (mod 5) but #1 forces x = 2 (mod 5)
True

from trapforge.linalg import Matrix, smith_normal_form, solve_diophantine

# Three hidden digits, observed only through two weighted checksums.
A = Matrix.of([[1, 10, 100], [7, 3, 1]])
solutions = solve_diophantine(A, [724, 41])
print(solutions)
print(list(solutions.points_in_box((0, 0, 0), (9, 9, 9))))

# Smith normal form with both transforms: U @ C @ V == S.
C = Matrix.of([[2, 4, 4], [-6, 6, 12], [10, -4, -16]])
form = smith_normal_form(C)
print(form.invariant_factors, form.U @ C @ form.V == form.S)

x = (4, 2, 7) + t0*(290, -699, 67), t in Z^1
[(4, 2, 7)]
(2, 6, 12) True

from trapforge.prover import ConstraintSystem, Congruent, gate, prove


def anchor(x: int, y: int) -> Congruent:
    """The ledger shows that record x was scrambled to y under x -> (a*x + b) mod 12."""
    return Congruent.of({"a": x, "b": 1}, y, 12, f"anchor x={x}")


sample = ConstraintSystem.build({"a": (1, 11), "b": (0, 11)}, [anchor(1, 0), anchor(3, 10)])
proof = prove(sample)
print(proof)
print(proof.check().reason)

# Reveal more records only until the planted map (a, b) = (5, 7) is the only one left.
result = gate(sample, [anchor(7, 6), anchor(2, 5), anchor(4, 3)], hidden={"a": 5, "b": 7})
print(result)
print([constraint.label for constraint in result.added])

ambiguous: exactly 2 worlds fit, for example a=5, b=7 and a=11, b=1 (they differ in a, b)
verified: ambiguous, 2 solutions
passed after 2 more constraints (sizes 2, 2, 1): unique: a=5, b=7
['anchor x=7', 'anchor x=2']

The anchor at x=7 reads 6 under both maps, so it does not help; the gate keeps it (the sample is a prefix of the stream) and stops after x=2, which separates them.

from trapforge.families import REGISTRY, Difficulty
from trapforge.families.ledger import naive_map, recover_map
from trapforge.prover import ConstraintSystem, prove

family = REGISTRY.get("affine-ledger")
instance = family.generate(7, Difficulty.EASY)
print(instance.files["anchors.csv"].decode(), end="")

# The first two anchors alone admit several maps; every anchor together admits one.
first_two = ConstraintSystem(instance.system.unknowns, instance.system.constraints[:2])
print(prove(first_two))
print(prove(instance.system))

# The reference solver uses every anchor; the naive one treats m = 36 as if it were prime.
print(recover_map(instance.files), naive_map(instance.files))
print(family.solve(instance.files) == instance.expected)
print(family.baseline(instance.files) == instance.expected)

account,scrambled
18,25
10,33
0,7
1,24
ambiguous: exactly 4 worlds fit, for example a=8, b=25 and a=17, b=7 (they differ in a, b)
unique: a=17, b=7
(17, 7) (8, 25)
True
False

All outputs above come from running the snippets with uv run python; the module docstrings carry more examples, and tests/test_doctests.py runs all of them so they cannot drift.

Task families

A family implements the TaskFamily protocol: generate(seed, difficulty) returns a TaskInstance holding the corpus files, the planted hidden world, the byte-exact expected output, the visible sample of that output, and the ConstraintSystem the corpus implies about the hidden world (the planted world must satisfy it, or construction fails). solve(files) is the reference solver and baseline(files) the naive one; both see only the corpus. All randomness comes from family_rng, a random.Random seeded from a string (hashed with SHA-512, so PYTHONHASHSEED does not matter), and every file goes through trapforge.canonical. TaskInstance.bundle() lays the instance out as data/, expected/, sample/ and meta/ (instruction, planted world, constraint system), and digest() is SHA-256 over that bundle.

Affine-scrambled ledger (affine-ledger)

A ledger export replaced every account number x by (a*x + b) mod m. m is published and composite; a (coprime to m) and b are hidden. The corpus has params.json, anchors.csv (accounts matched by hand, in the order they were confirmed), ledger.csv (transactions by scrambled account) and queries.csv; the answer is balances.csv.

The trap is built in four steps:

1. The first two anchors differ by a multiple of a factor d of m, so (x2 - x1)*a = y2 - y1 (mod m) has d solutions for a. The planted a is drawn at or above m / d, so the smallest solution, which is what a solver that treats m as prime keeps, is always wrong.
2. Decoy anchors (medium: 2, hard: 4) sit in the class of x1 modulo d, where every candidate map agrees, so they look informative and cut nothing.
3. The uniqueness gate then reveals further anchors, one at a time, only until exactly one map fits; the instance's constraint system is that gated sample.
4. The visible sample of the answer shows accounts on which the naive map agrees with the true one; the hidden deciding records are accounts on which it does not, and the ledger is extended until every deciding record has a different balance under the two maps.

For trapforge generate affine-ledger --seed 7 (m = 36, d = 4), the expected output and the naive baseline's output:

expected/balances.csv     naive baseline
account,balance           account,balance
7,-27586                  7,35624
11,50565                  11,-87848
12,75043                  12,-87600
14,-12223                 14,-12223      <- visible sample
26,-61484                 26,-61484      <- visible sample
28,16902                  28,0

Difficulty	Moduli	Shared factor d	Decoys	Active accounts / transactions (at least)	Sample / deciding records
easy	24, 36, 40, 60	2 to 6	0	10 / 40	2 / 4
medium	360, 420, 504, 720, 840	4 to 30	2	30 / 160	3 / 9
hard	27720, 30030, 55440, 65520	12 to 120	4	80 / 640	4 / 20

The prover's box 1 <= a <= m - 1, 0 <= b <= m - 1 does not encode "a is coprime to m" (that is not a linear constraint), so uniqueness is proved over a superset of the maps the instruction allows; the reference solver additionally keeps only units.

Architecture

flowchart LR
    subgraph today["implemented"]
        MOD["modular<br/>gcd, inverse, CRT,<br/>linear congruences"]
        LIN["linalg<br/>Matrix, HNF, SNF,<br/>kernel, Diophantine,<br/>box enumeration"]
        MODEL["prover.model<br/>unknowns, equations,<br/>congruences, case split"]
        SOLVER["prover.solver + gating<br/>UniqueProof / Ambiguity<br/>gate"]
        CERT["prover.certificate<br/>standalone checker<br/>(stdlib only)"]
        CAN["canonical<br/>byte-exact writers,<br/>SHA-256 digests"]
        FAM["families<br/>plugin API, registry,<br/>affine ledger"]
        BUNDLE["bundle + verify<br/>digest-pinned task dirs,<br/>SHA-256 graders, Docker check"]
        CLI["cli (Typer)<br/>crt, solve, system, prove,<br/>check, families, generate,<br/>export, verify"]
        EX[("examples/*.json")]
    end
    subgraph planned["roadmap"]
        MORE["task families<br/>clocks, warehouse"]
    end
    MOD --> CLI
    LIN --> CLI
    MODEL --> CLI
    LIN --> SOLVER
    MODEL --> SOLVER
    SOLVER --> CERT
    SOLVER --> CLI
    CERT --> CLI
    EX --> CLI
    SOLVER --> FAM
    MOD --> FAM
    CAN --> FAM
    FAM --> CLI
    FAM --> BUNDLE
    CERT --> BUNDLE
    BUNDLE --> CLI
    FAM -.-> MORE

Loading

src/trapforge/
  modular.py            number theory over Python int
  linalg/               matrix.py, hermite.py, smith.py, lattice.py, diophantine.py
  prover/model.py       the constraint model the uniqueness prover reasons about
  prover/solver.py      exact per-case solver, verdicts and certificate writer
  prover/certificate.py standalone certificate checker (standard library only)
  prover/gating.py      the uniqueness gate
  canonical.py          canonical byte-exact writers and SHA-256 digests
  families/base.py      Difficulty, TaskInstance, the TaskFamily protocol, family_rng
  families/registry.py  the family registry
  families/ledger.py    the affine-scrambled ledger family
  bundle.py             task bundle exporter (Dockerfile, solvers, grader templates)
  verify.py             reference-passes / baseline-fails check, locally and in Docker
  cli.py                Typer CLI
examples/               bundled JSON inputs for the CLI and the demo
scripts/demo.sh         the end-to-end demo, runnable locally or in the image

Measured numbers

Every number here comes from a command in this repo, run on the current tree.

Number	Value	Command
Tests	792 passed, Docker test included (62 CLI, 1 demo script, 13 doctest modules, 78 linalg, 89 modular, 122 prover, 33 canonical writers, 367 families: 34 plugin API, 333 affine ledger; 27 bundle and verify)	make cov and uv run pytest -q --co
Ledger instances checked by the test suite	73 (seeds 0-39 easy, 0-24 medium, 0-7 hard): each proved unique with a re-checked certificate, reproduced by the reference solver, missed by the baseline on every deciding record	uv run pytest -q tests/test_family_ledger.py
Ledger instances through the CLI gate	300 of 300 exit 0 (seeds 0-99 at each difficulty)	for d in easy medium hard; do for s in $(seq 0 99); do uv run trapforge generate affine-ledger --seed $s --difficulty $d > /dev/null || echo "FAIL $d $s"; done; done
Ledger generation time (gate proofs included)	median 0.7 ms easy, 2.2 ms medium, 16.1 ms hard; slowest 30.6 ms (seeds 0-99 each; varies a few ms between runs)	the timing snippet below
Tampered certificates rejected	40 hand-written tamperings, each with its expected reason	uv run pytest -q tests/test_prover_certificate.py -k tampered
Branch coverage of src/	99.66% (2250 statements, 696 branches); CI fails under 85%	make cov
Demo wall time	3.9 s for all 17 steps, Docker verification included	time make demo
Bundle verification	6 of 6 checks pass for affine-ledger seed 7 (certificate; reference passes and baseline fails, locally and in Docker with --network none)	trapforge export affine-ledger --seed 7 --out bundle && trapforge verify bundle
Wide-box proof	x + y = 10 with both unknowns in 0..10**9: exactly 11 worlds, 0.14 s wall for the whole prove command (it took minutes before the projected walk)	time uv run trapforge prove examples/wide-sum.json
Image size	47.7 MB content size (223 MB unpacked on disk)	make docker-build && docker images trapforge
Source and test size	4798 lines in src/, 4446 lines in tests/	git ls-files src | xargs wc -l, same for tests

The timing snippet (Apple-silicon laptop, one process, uv run python -):

import time
from trapforge.families import REGISTRY, Difficulty

family = REGISTRY.get("affine-ledger")
for difficulty in Difficulty:
    times = []
    for seed in range(100):
        start = time.perf_counter()
        family.generate(seed, difficulty)
        times.append(time.perf_counter() - start)
    times.sort()
    print(difficulty.value, f"median {times[50] * 1000:.1f} ms, max {times[-1] * 1000:.1f} ms")

The property tests use Hypothesis against brute force on small inputs and against sympy on large ones (moduli up to 10^30, 30-digit planted solutions, dense 10x10 matrices), and tampered certificates must always be rejected. The prover is checked against brute force on random small systems (exact and capped counts, witnesses, certificates), and a soundness property perturbs one integer of a certificate at random: whenever the checker still accepts, its verdict and count must be the truth. CI runs a derandomized profile (HYPOTHESIS_PROFILE=ci) so any failure reproduces.

Design decisions

• Exact integers only. Every value is a Python int; Matrix.of rejects floats and Fractions. A silently truncated 2.5 would break a uniqueness proof.
• Proofs instead of "no". Inconsistent systems return certificate objects with a verify method that re-checks them with a gcd or one vector-matrix product, never by re-solving. The CLI prints the re-check next to every certificate.
• Certificates that are cheaper to check than to find. A uniqueness certificate never asks the checker to run Smith or Hermite forms: it re-checks M p = r, M K^T = 0, K W = I for a supplied right inverse W, one nonzero determinant for the rank, and then walks the box. The checker imports only the standard library so it can be vendored or audited on its own.
• Counterexamples, not just "not unique". An ambiguous sample returns the first two worlds that fit (in case order, then lexicographic order) and the size of the ambiguity space (exact up to a cap), which is what a task author needs to decide which record to reveal next.
• Canonical solution sets. An AffineLattice keeps its kernel basis in Hermite normal form and its point reduced modulo it, so equal sets compare equal and box enumeration is exact, lazy and lexicographic.
• One byte spelling per task. Every emitted file goes through trapforge.canonical, all randomness comes from a string-seeded random.Random, and tests pin SHA-256 digests of generated instances across processes and platforms.
• Traps that are proved, not hoped for. A family states what its corpus implies as a constraint system; the uniqueness gate decides how much of the corpus to reveal, and the tests re-prove every generated instance and check that the naive baseline matches the visible sample yet misses every hidden deciding record.
• SNF on top of HNF. smith_normal_form diagonalizes the Hermite form of A rather than A; on one seeded dense 10x10 matrix this cut the largest entry of V from 539 digits to 31, and a regression test bounds transform size.
• sympy is a test oracle, not a dependency. The runtime depends only on Typer, so an exported reference solver vendors the math modules and runs in a bare python:3.12-slim image; verify runs it with python -I -S to prove nothing else is needed.
• Graders that do not embed the answer. The grader holds only the SHA-256 and the byte count of the expected output, and a bundle ships only instances with a proved unique answer. The certificate in proof/ does contain the hidden map, so an agent should get the image built from the bundle's Dockerfile (which copies only instruction.md and data/), not the bundle directory; see Known issues.
• Box walks that usually cost what the answer costs. Before enumerating lattice points, every box bound is projected onto the leading parameters (Fourier-Motzkin), so a system with 11 solutions in a box of width 109 takes 11 steps, not 109. The projection is of the real relaxation, so integer-hollow lattices are still walked in time linear in the width; see Known issues.
• Reproducible builds. uv.lock is enforced with uv sync --locked in CI and in the Dockerfile, and both base images are pinned by digest.

The full decision log lives in PLAN.md.

Known issues

Found in review and not fixed yet.

• verify does not bind the certificate or the grader to the bundle. It requires a valid unique certificate but does not compare its system with data/ or task.json, and it uses the bundle's own tests/test_outputs.py as the oracle without checking its embedded digest against task.json. A swapped certificate or a weakened grader still verifies.
• proof/uniqueness.cert.json reveals the answer. Its witness is the hidden map, and the expected output follows from it and data/. Hand agents the built image, not the bundle directory. The generated grader's docstring still says the bundle does not reveal the answer.
• Hollow lattices make box walks slow. On a system such as x - N*y - z = 0 with z fixed, the walk visits every value of x in the box, not only the few that extend, so a small certificate with very wide bounds can stall check_certificate, trapforge check and trapforge verify.
• Ledger overflow errors. A balance whose decimal form passes Python's 4300-digit conversion limit raises a plain ValueError from the writers instead of LedgerError, and canonical.csv_bytes / json_bytes raise ValueError instead of CanonicalError for such integers.
• Ledger input leniency. A ledger.csv account outside 0..m-1 is dropped silently instead of rejected, and -0 or leading zeros in queries.csv are accepted, which can produce duplicate output rows.
• TaskInstance validation gaps. family is not type-checked, a non-mapping files raises AttributeError, an unhashable output raises TypeError, and integers past the digit limit in seed or extras raise ValueError, all instead of FamilyError.

Roadmap

Built in the slices listed in PLAN.md. Slices 1-4 and 7 are done; slice 8 is partly done (the CLI image and a make demo that exports and verifies a bundle).

• Slice 5: multi-clock log merge family (wrapping counters with unknown periods, CRT with non-coprime moduli).
• Slice 6: warehouse conservation family (a hidden transfer matrix behind aggregates).
• Slice 8: compose pipeline that forges and verifies one bundle per family, and bundle verification inside make docker-demo.
• Slice 9: difficulty report and benchmarks (baseline failure rates, ambiguity-space size, generation and proof latency) and authoring docs.

License

MIT - see LICENSE.