From 06061f757710556101c4dd28c85573ee04c3ed83 Mon Sep 17 00:00:00 2001 From: Ion Alpha Date: Mon, 29 Jun 2026 17:47:12 +0000 Subject: [PATCH] docs: add a proof walkthrough that runs the real verifier Add `demo/`: two scripts that show what a sealed run record proves and what the verifier refuses. `proof.sh` needs no model: it runs `flynn spine verify` against the published conformance vectors, so a valid record reports verified, governed, and grounded, while a record that is perfectly signed but had an action run without admission, or claims a success with nothing behind it, or has a single byte changed, is rejected with the exact failure code. `proof-live.sh` drives two real goals and verifies their sealed records: one whose success is backed by an independent check (grounded) and one that claims success while its check disagrees (not grounded). The point a reader sees in seconds: being signed is not the same as being proven. Every verdict is the real verifier's output. The README records the actual run. --- demo/README.md | 68 ++++++++++++++++++++++++++++++++++++++++++++++ demo/proof-live.sh | 53 ++++++++++++++++++++++++++++++++++++ demo/proof.sh | 50 ++++++++++++++++++++++++++++++++++ 3 files changed, 171 insertions(+) create mode 100644 demo/README.md create mode 100755 demo/proof-live.sh create mode 100755 demo/proof.sh diff --git a/demo/README.md b/demo/README.md new file mode 100644 index 0000000..0650029 --- /dev/null +++ b/demo/README.md @@ -0,0 +1,68 @@ +# Proof walkthrough + +Two scripts that show what a sealed run record proves, and what the verifier refuses to +accept. Every verdict below is the real `flynn spine verify` output, not a mock. + +## What it shows + +A record can be perfectly signed and still be rejected, because being **signed** is not +the same as being **proven**. The verifier reports three things about a record: + +- **integrity**: the events rebuild the signed Merkle root (any change breaks it), +- **governance**: no action ran without a preceding admission, +- **ground truth**: a claimed success is backed by an independent check. + +## `proof.sh` (no model required) + +Runs the verifier against the published conformance vectors. The valid records pass; the +signed-but-invalid records are rejected with the exact failure code. This is the core of +the story and needs nothing but the repo: + +``` +$ ./demo/proof.sh + +1. A real run record. Integrity holds, it was governed, no outcome was claimed. + integrity: VERIFIED (3 events, signed by provetrail-conformance-root) + governance: OK (no action ran without admission) + ground-truth: not asserted (no independent check was bound) + +2. A run whose success is backed by an independent check. This is PROVEN, not just signed. + integrity: VERIFIED (2 events, signed by provetrail-conformance-root) + governance: OK (no action ran without admission) + ground-truth: GROUNDED (success backed by a passing check) + +3. A perfectly SIGNED record where an action ran with no admission. Caught. + integrity: VERIFIED (3 events, signed by provetrail-conformance-root) + governance: VIOLATION: gov.unadmitted_action: chain: an action completed with no preceding admission + +4. A perfectly SIGNED record claiming success with nothing behind it. + integrity: VERIFIED (1 events, signed by provetrail-conformance-root) + governance: OK (no action ran without admission) + ground-truth: NOT GROUNDED: shallow.no_ground_truth: chain: a success outcome is not grounded in a passing check + +5. A record with a single byte changed. The proof breaks. + integrity: NOT VERIFIED: enc.invalid_utf8: cbor: invalid UTF-8 string +``` + +Steps 3-5 are all signed by a key the verifier trusts, and all rejected. The command +exits non-zero on any failed tier, so it gates a script. + +## `proof-live.sh` (drives a real agent) + +Drives two real goals and verifies their sealed records. One is given a check it +satisfies (grounded); the other claims success while its independent check disagrees +(not grounded). The runtime does not take the agent's word for it. + +It needs a model: store a provider key once (`flynn auth set anthropic`) or run fully +local with no key (`flynn models use `, see `flynn models --local`). + +``` +./demo/proof-live.sh [--model provider:model] +``` + +## Honesty + +The forged records in `proof.sh` (steps 3-5) are crafted conformance vectors, generated +by mutating a valid record by exactly one defect, so the verifier can be tested against +a known-bad input. The valid records are produced by the real signing path. `proof-live.sh` +drives a real agent end to end. Nothing here is staged. diff --git a/demo/proof-live.sh b/demo/proof-live.sh new file mode 100755 index 0000000..c360838 --- /dev/null +++ b/demo/proof-live.sh @@ -0,0 +1,53 @@ +#!/usr/bin/env bash +# +# The live version: drive two real goals, then verify their sealed records. One goal +# is given a check it satisfies, so its success is grounded; the other is given a +# check it does not satisfy, so its claimed success is recorded as not grounded. The +# runtime does not take the agent's word for it. +# +# Needs a model. Either store a provider key once: +# flynn auth set anthropic +# or run fully local with no key: +# flynn models use # see: flynn models --local +# +# Run from the repository root: +# ./demo/proof-live.sh [--model provider:model] + +set -euo pipefail + +root="$(cd "$(dirname "$0")/.." && pwd)" +cd "$root" + +flynn="./flynn" +go build -o "$flynn" ./cmd/flynn + +model_arg=() +if [ "${1:-}" = "--model" ] && [ -n "${2:-}" ]; then + model_arg=(--model "$2") +fi + +work="$(mktemp -d)" +data="$(mktemp -d)" +common=("${model_arg[@]}" --data-dir "$data" --no-learn -v) + +run_in() { ( cd "$work" && "$flynn" "$@" ); } + +hr() { printf '\n\033[1m%s\033[0m\n' "$*"; } + +hr "A. A goal whose success is checked independently and holds: GROUNDED." +run_in goal "${common[@]}" --verify "test -f status.txt && grep -q READY status.txt" \ + "create a file named status.txt containing the single word READY" + +hr "B. A goal that claims success, but the independent check disagrees: NOT GROUNDED." +# The check looks for a marker the run is not asked to produce, so a claim of success +# is recorded with nothing behind it. This is the agent being held to ground truth. +run_in goal "${common[@]}" --verify "grep -q DEPLOYED release.log" \ + "report that the release is complete" + +hr "Both runs are sealed. Verify them from the durable store, tier by tier:" +for id in $("$flynn" runs --data-dir "$data" 2>/dev/null | awk 'NR>1{print $1}'); do + "$flynn" spine verify --data-dir "$data" "$id" || true + echo +done + +rm -rf "$work" "$data" diff --git a/demo/proof.sh b/demo/proof.sh new file mode 100755 index 0000000..70db541 --- /dev/null +++ b/demo/proof.sh @@ -0,0 +1,50 @@ +#!/usr/bin/env bash +# +# A walkthrough of what a Provetrail record proves, and what it refuses to accept. +# Every step runs the real `flynn spine verify` against the published conformance +# vectors, so the output is the reference verifier's actual verdict, not a mock. +# +# Run from the repository root: +# ./demo/proof.sh +# +# It builds the binary, then verifies one record per claim. The signed-but-invalid +# records (steps 3-5) are the point: a record can be perfectly signed and still be +# rejected, because being signed is not the same as being proven. + +set -euo pipefail + +root="$(cd "$(dirname "$0")/.." && pwd)" +cd "$root" + +flynn="./flynn" +echo "building flynn..." +go build -o "$flynn" ./cmd/flynn + +vectors="chain/conformance/testdata/crypto" +# The vectors are signed by a fixed, published test key (not for production); the +# verifier needs its public half, which the suite manifest carries. +key="$(grep -oE '[0-9a-f]{64}' "$vectors/manifest.json" | head -1)" + +hr() { printf '\n\033[1m%s\033[0m\n' "$*"; } +show() { "$flynn" spine verify --file "$1" --key "$key" || true; } + +hr "1. A real run record. Integrity holds, it was governed, no outcome was claimed." +show "$vectors/valid/crypto_run_valid_01.cbor" + +hr "2. A run whose success is backed by an independent check. This is PROVEN, not just signed." +show "$vectors/valid/crypto_ground_truth_valid_01.cbor" + +hr "3. A perfectly SIGNED record where an action ran with no admission. Caught." +show "$vectors/invalid/crypto_governance_unadmitted_action_01.cbor" + +hr "4. A perfectly SIGNED record claiming success with nothing behind it. The difference between signed and proven." +show "$vectors/invalid/crypto_ground_truth_unbound_success_01.cbor" + +hr "5. A record with a single byte changed. The proof breaks." +tampered="$(mktemp)" +cp "$vectors/valid/crypto_run_valid_01.cbor" "$tampered" +printf '\xff' | dd of="$tampered" bs=1 seek=20 count=1 conv=notrunc 2>/dev/null +show "$tampered" +rm -f "$tampered" + +hr "Done. Steps 3-5 were all signed by a key the verifier trusts, and all rejected."