Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@ All notable project changes are recorded here. Dates use ISO 8601 (`YYYY-MM-DD`)
## [Unreleased]

### Added
- `verify` and `gate` stay on the host unless `--isolated` is passed. That mode runs command, red-green and metric checks with no network, a fresh HOME, and the repository read-only except paths the check declares. The image digest is `env.image` on the contract under test. Without it, `--isolated` refuses and names `env.image`. The receipt records `isolated`, `env_digest` and `heuristic`. grep, wiring and the forbidden scan are one layer, not a boundary.
- Every subcommand refuses a flag it does not accept, exits 2, and names the unknown flag and the accepted ones. Nothing runs after that refusal (#33).
- The pre-push hook leaves out a commit already on the server default branch. It reads that head with `git ls-remote` of the push URL at send time, for an existing branch and for a new branch. A local remote-tracking ref does not count. If the server cannot be read, every commit in the range is gated (#31, #35).
- The pre-push hook gates the commit being pushed, at that sha, in a temporary worktree. It reads the local sha from stdin and does not gate the checked-out HEAD. The base is the most recent `proofline next` pin for the task, or the parent of that commit, and a refusal prints the base it used. `proofline next --base <rev>` records a newer pin. A worktree with no evidence still gates, and stale evidence in the pushing worktree cannot block a commit that passes at its own sha (#21, #22, #23).
Expand Down
2 changes: 2 additions & 0 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,8 @@

A coding agent reports that a task is finished. Proofline does not take the report: it holds the definition of done as a contract a machine can check, hands the agent one task at a time, re-runs every check itself when the agent reports, and lets a commit through only when the evidence says PASS. The agent gets a corrective prompt that names the file and the line to fix next, never a verdict it can argue with. Zero dependencies, Node 22+, Apache-2.0.

`proofline verify --isolated` and `proofline gate --isolated` run command, red-green and metric checks in a container. Local use stays off unless that flag is passed. The image digest is `env.image` on the contract under test. Without it, `--isolated` refuses and names `env.image`.

```mermaid
flowchart LR
C["proofline.json<br/>tasks, criteria, scope,<br/>forbidden actions"] --> N["proofline next<br/>one task, its brief,<br/>the base revision pinned"]
Expand Down
2 changes: 2 additions & 0 deletions docs/receipt.md
Original file line number Diff line number Diff line change
Expand Up @@ -21,3 +21,5 @@ The MCP tools `receipt` and `verify_receipt` return that same JSON. `tools/list`
When `GET /v1/state/digest` answers within 2 seconds, an L1 receipt gains `memory.vault_digest` and `memory.frontier`. An L2 receipt in ci mode gains only `memory_commitment`, the sha256 of the vault id, the digest and the frontier JSON, so a replica id is not in the receipt. No answer leaves the receipt unchanged. `--vault` writes `work/receipts/<date>-<role>-<sha7>.md` with origin `proofline`.

The weakening check is a warning beside the owner signature. It names a loosened threshold, a removed criterion, or a changed command. Once `guard/owner.pub` is pinned, a missing, altered or wrongly-signed contract is refused with `contract not owner-signed`.

grep, wiring and the forbidden scan are marked `heuristic` in the receipt. They are one layer, not a boundary. An isolated run records `isolated` and `env_digest`. A local run records `isolated` false.
1 change: 1 addition & 0 deletions fixtures/evasions/benchmark-code-edited/note.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
benchmark-code-edited is named in coverage_limits. The static checks do not catch it.
1 change: 1 addition & 0 deletions fixtures/evasions/check-reads-contract/note.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
check-reads-contract is named in coverage_limits. The static checks do not catch it.
1 change: 1 addition & 0 deletions fixtures/evasions/computed-dynamic-import/note.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
computed-dynamic-import is named in coverage_limits. The static checks do not catch it.
1 change: 1 addition & 0 deletions fixtures/evasions/env-dependent-test/note.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
env-dependent-test is named in coverage_limits. The static checks do not catch it.
1 change: 1 addition & 0 deletions fixtures/evasions/network-dependent-pass/note.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
network-dependent-pass is named in coverage_limits. The static checks do not catch it.
1 change: 1 addition & 0 deletions fixtures/evasions/pre-generated-cache/note.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
pre-generated-cache is named in coverage_limits. The static checks do not catch it.
1 change: 1 addition & 0 deletions fixtures/evasions/suite-command-wrapper/note.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
suite-command-wrapper is named in coverage_limits. The static checks do not catch it.
1 change: 1 addition & 0 deletions fixtures/evasions/test-removed-by-rename/note.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
test-removed-by-rename is named in coverage_limits. The static checks do not catch it.
1 change: 1 addition & 0 deletions fixtures/evasions/test-weakened-by-snapshot/note.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
test-weakened-by-snapshot is named in coverage_limits. The static checks do not catch it.
1 change: 1 addition & 0 deletions fixtures/evasions/timeout-raised-through-config/note.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
timeout-raised-through-config is named in coverage_limits. The static checks do not catch it.
6 changes: 6 additions & 0 deletions fixtures/tb06/contract.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
{
"image_name": "node:22.11.0",
"env": {
"image": "node:22.11.0@sha256:ec878c763e9fad09d22aae86e2edcb7a05b397dfe8411c16e2b90158d595e2ce"
}
}
18 changes: 18 additions & 0 deletions schema/receipt-v1.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
{
"$schema": "https://json-schema.org/draft/2020-12/schema",
"$id": "https://proofline.dev/receipt/v1",
"type": "object",
"properties": {
"isolated": { "type": "boolean" },
"env_digest": { "type": ["string", "null"] },
"heuristic": {
"type": "boolean",
"description": "grep, wiring and the forbidden scan are one layer, not a boundary"
},
"coverage_limits": {
"type": "array",
"items": { "type": "string" }
}
},
"required": ["isolated", "heuristic"]
}
19 changes: 12 additions & 7 deletions src/checks.mjs
Original file line number Diff line number Diff line change
Expand Up @@ -58,8 +58,10 @@ export function diffHunks(root, base) {
return files;
}

function runCounted(cmd, root, v) {
const r = run(cmd, { cwd: root, timeoutS: v.timeout_s || 900, env: v.env });
function runCounted(cmd, root, v, ctx) {
const r = ctx?.sandbox
? ctx.sandbox(cmd, { cwd: root, timeoutS: v.timeout_s || 900, env: v.env, writable: v.writable })
: run(cmd, { cwd: root, timeoutS: v.timeout_s || 900, env: v.env });
const txt = r.stdout + '\n' + r.stderr;
const num = (k) => { const m = txt.match(new RegExp(`^[#ℹ]\\s*${k}\\s+(\\d+)`, 'm')); return m ? +m[1] : undefined; };
r.counts = { tests: num('tests'), pass: num('pass'), fail: num('fail'), skipped: num('skipped'), todo: num('todo'), cancelled: num('cancelled') };
Expand Down Expand Up @@ -103,7 +105,7 @@ const named = (e) => {
export const verifiers = {
command(v, ctx) {
const expect = v.expect_exit ?? 0;
let r = runCounted(v.cmd, ctx.root, v);
let r = runCounted(v.cmd, ctx.root, v, ctx);
const first = ev(r), firstExit = r.exit;
if (r.exit === 127) return { status: 'error', detail: `command not found: ${v.cmd}`, evidence: first };
const tooMany = (r2) => {
Expand All @@ -117,7 +119,7 @@ export const verifiers = {
if (r.exit === expect) return { status: 'fail', detail: [...tooMany(r), named(first)].filter(Boolean).join('; '), evidence: first };
// Both runs keep their failing names: on a flaky result the first run's list is the tests that flapped.
for (let i = 0; i < (ctx.flakyReruns ?? 1); i++) {
r = runCounted(v.cmd, ctx.root, v);
r = runCounted(v.cmd, ctx.root, v, ctx);
if (r.exit === expect && !tooMany(r).length) return { status: 'flaky', detail: `failed (exit ${firstExit}${named(first) ? `; ${named(first)}` : ''}) then passed on re-run ${i + 1}: flaky, not a pass. Root-cause the non-determinism.`, evidence: { first, rerun: ev(r) } };
}
const rerun = ev(r), n = named(rerun.failing.length ? rerun : first);
Expand Down Expand Up @@ -150,8 +152,8 @@ export const verifiers = {
}
if (v.setup) run(v.setup, { cwd: wt, timeoutS: 900 });
const cmd = sub(v.cmd, { test: v.test_file, name: v.test_name || '' });
const red = runCounted(cmd, wt, v);
const green = runCounted(cmd, ctx.root, v);
const red = runCounted(cmd, wt, v, ctx);
const green = runCounted(cmd, ctx.root, v, ctx);
const evd = { base: ctx.base, red: ev(red), green: ev(green) };
if (red.exit === 127 || green.exit === 127) return { status: 'error', detail: 'test command not found', evidence: evd };
if (red.exit === 0) return { status: 'fail', detail: `test PASSES on base ${ctx.base.slice(0, 8)} without the change: it does not prove the change (tests how, not what?)`, evidence: evd };
Expand All @@ -174,7 +176,10 @@ export const verifiers = {
const m = (ctx.machine || readMachine)();
const machine = { load1: m.load1, cpus: m.cpus, load_per_cpu: +(m.load1 / Math.max(1, m.cpus)).toFixed(2), node: nodeVersion(ctx.root, v.env) };
if (typeof max === 'number' && m.load1 / Math.max(1, m.cpus) > max) return { r: null, machine };
return { r: run(v.cmd, { cwd: ctx.root, timeoutS: v.timeout_s || 1800, env: v.env }), machine };
const exec = ctx.sandbox
? (cmd, o) => ctx.sandbox(cmd, { ...o, writable: v.writable })
: (cmd, o) => run(cmd, o);
return { r: exec(v.cmd, { cwd: ctx.root, timeoutS: v.timeout_s || 1800, env: v.env }), machine };
})();
const on = `load ${machine.load1.toFixed(2)} / ${machine.cpus} CPUs, node ${machine.node || 'not found'}`;
if (!r) return { status: 'blocked', detail: `machine busy: load ${machine.load1.toFixed(2)} over ${machine.cpus} CPUs = ${machine.load_per_cpu.toFixed(2)} per CPU > max_load_per_cpu ${max}; the bench was not run. Re-run when the machine is idle.`, evidence: { cmd: v.cmd, machine } };
Expand Down
35 changes: 22 additions & 13 deletions src/engine.mjs
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ import { scanForbidden } from './forbidden.mjs';
import { parseClaims, checkClaim } from './claims.mjs';
import { record, readLog, verifyChain } from './evidence.mjs';
import * as RC from './cache.mjs';
import { resolveIsolation, COVERAGE_LIMITS } from './isolate.mjs';

export const KNOWN_LIMITS = [
'Proofline runs on the same machine as the agent: an agent with shell access could edit .proofline/ or proofline.json. The hash chain makes edits detectable, contract weakening vs the base revision is flagged, and CI re-verifies from a clean checkout; protect proofline.json with CODEOWNERS/branch protection for a hard boundary.',
Expand Down Expand Up @@ -93,31 +94,39 @@ export function baseBrief(root, c, t, explicit) {
return L.join('\n');
}

export function verifyTask(root, taskId, { claims, only, skipTypes = [], base: explicitBase, machine, fresh = false } = {}) {
export function verifyTask(root, taskId, opts = {}) {
const { claims, only, skipTypes = [], base: explicitBase, machine, fresh = false } = opts;
const c = C.load(root);
const t = taskById(c, taskId);
const iso = resolveIsolation(c, opts);
const errs = C.validate(c);
// Base is pinned when the task starts, so pushing the work does not move the goalposts.
const { ref: baseRef, source: baseSource, base, problems: baseProblems } = taskBase(root, c, t, explicitBase);
const ctx = { root, contract: c, task: t, base, changed: base ? changedFiles(root, base) : new Map(), measured: {}, machine, baseline: c.baseline?.metrics, tolerancePct: c.defaults?.regression_tolerance_pct, flakyReruns: c.defaults?.flaky_reruns ?? 1 };
const ctx = { root, contract: c, task: t, base, changed: base ? changedFiles(root, base) : new Map(), measured: {}, machine, baseline: c.baseline?.metrics, tolerancePct: c.defaults?.regression_tolerance_pct, flakyReruns: c.defaults?.flaky_reruns ?? 1, sandbox: iso.sandbox };
const results = [];
const reuse = RC.settings(c);
for (const a of t.criteria) {
if (only && !only.includes(a.id)) continue;
if (skipTypes.includes(a.verifier.type)) continue;
let r;
// Reuse (opt-in): a command or metric PASS recorded on this HEAD with a clean tree is not run again; --fresh runs it.
const k = reuse.on && RC.REUSABLE.includes(a.verifier.type) ? RC.keyFor(root, a.verifier, ctx) : null;
const hit = k && !fresh ? RC.lookup(root, k.key, reuse) : null;
if (hit) {
r = RC.reusedResult(hit);
if (a.verifier.type === 'metric') ctx.measured[a.verifier.name || a.verifier.key] = hit.data.evidence.measured;
const sandboxed = ['command', 'test_red_green', 'metric'].includes(a.verifier.type);
if (iso.block && sandboxed) {
r = { status: 'error', detail: iso.block };
} else {
try { r = verifiers[a.verifier.type](a.verifier, ctx); } catch (e) { r = { status: 'error', detail: `verifier crashed: ${e.message}` }; }
// Only a PASS is stored, and only if the tree is still the one the check started on and the log is intact.
if (k && r.status === 'pass' && RC.keyFor(root, a.verifier, ctx)?.key === k.key && verifyChain(root).ok) RC.store(root, k, t.id, a, r);
// Reuse (opt-in): a command or metric PASS recorded on this HEAD with a clean tree is not run again; --fresh runs it.
const k = reuse.on && RC.REUSABLE.includes(a.verifier.type) ? RC.keyFor(root, a.verifier, ctx) : null;
const hit = k && !fresh ? RC.lookup(root, k.key, reuse) : null;
if (hit) {
r = RC.reusedResult(hit);
if (a.verifier.type === 'metric') ctx.measured[a.verifier.name || a.verifier.key] = hit.data.evidence.measured;
} else {
try { r = verifiers[a.verifier.type](a.verifier, ctx); } catch (e) { r = { status: 'error', detail: `verifier crashed: ${e.message}` }; }
// Only a PASS is stored, and only if the tree is still the one the check started on and the log is intact.
if (k && r.status === 'pass' && RC.keyFor(root, a.verifier, ctx)?.key === k.key && verifyChain(root).ok) RC.store(root, k, t.id, a, r);
}
}
results.push({ id: a.id, statement: a.statement, mandatory: a.mandatory !== false, type: a.verifier.type, ...r });
const heuristic = a.verifier.type === 'grep' || a.verifier.type === 'wiring';
results.push({ id: a.id, statement: a.statement, mandatory: a.mandatory !== false, type: a.verifier.type, ...(heuristic ? { heuristic: true } : {}), ...r });
}
const rules = { ...C.DEFAULT_FORBIDDEN, ...(c.forbidden || {}) };
const forbidden = scanForbidden(root, base, rules);
Expand Down Expand Up @@ -170,7 +179,7 @@ export function verifyTask(root, taskId, { claims, only, skipTypes = [], base: e
const pushed = pr ? pr.status === 'pass'
: !!hi.head && !git(['status', '--porcelain'], root).out.split('\n').some((l) => l && !l.includes('.proofline/')) && git(['rev-parse', '--verify', '--quiet', `refs/remotes/${tgt.remote}/${tgt.branch}^{commit}`], root).out === hi.head;
const reused = results.filter((r) => r.reused).map((r) => ({ id: r.id, type: r.type, ts: r.reused.ts, entry: r.reused.entry }));
return { pushed, task: t.id, title: t.title, phase: t.phase, decision, base, base_ref: baseRef, base_source: baseSource, ...hi, contract_hash: C.contractHash(c), results, reuse: !reuse.on ? 'off' : fresh ? 'fresh' : 'on', reused, forbidden, weakenings: weak, contract_change: contractChange, marker, blocked, failing, measured: ctx.measured, claims: claimResults, changed: [...ctx.changed.keys()], ts: new Date().toISOString() };
return { isolated: iso.isolated, env_digest: iso.env_digest, heuristic: true, coverage_limits: COVERAGE_LIMITS, pushed, task: t.id, title: t.title, phase: t.phase, decision, base, base_ref: baseRef, base_source: baseSource, ...hi, contract_hash: C.contractHash(c), results, reuse: !reuse.on ? 'off' : fresh ? 'fresh' : 'on', reused, forbidden, weakenings: weak, contract_change: contractChange, marker, blocked, failing, measured: ctx.measured, claims: claimResults, changed: [...ctx.changed.keys()], ts: new Date().toISOString() };
}

/** Corrective prompt tied to each failed criterion. */
Expand Down
Loading
Loading