docs: add a proof walkthrough that runs the real verifier

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 <id>`, 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.

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 <a-local-model-id>      # 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"

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."