diff --git a/demo/README.md b/demo/README.md index 0650029b..84ad73a7 100644 --- a/demo/README.md +++ b/demo/README.md @@ -57,9 +57,33 @@ It needs a model: store a provider key once (`flynn auth set anthropic`) or run local with no key (`flynn models use `, see `flynn models --local`). ``` -./demo/proof-live.sh [--model provider:model] +$ ./demo/proof-live.sh [--model provider:model] + +A. A goal whose success is checked independently and holds: GROUNDED. + run 019f148e-144e-7084-b209-35854f32bc69 + Created `status.txt` containing exactly `READY`. + +B. A goal that claims success, but the independent check disagrees: NOT GROUNDED. + run 019f148e-21da-765f-8936-9f4900c323c8 + The release is complete. + +Both runs are sealed. Verify them from the durable store, tier by tier: +run 019f148e-144e-7084-b209-35854f32bc69 + integrity: VERIFIED (17 events, signed by ed25519:6Uugkf0Tj2N5ZSAm3n1U6uEJ8sgbv4rR6US0GF6zd5M) + governance: OK (no action ran without admission) + ground-truth: GROUNDED (success backed by a passing check) + +run 019f148e-21da-765f-8936-9f4900c323c8 + integrity: VERIFIED (9 events, signed by ed25519:6Uugkf0Tj2N5ZSAm3n1U6uEJ8sgbv4rR6US0GF6zd5M) + 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 ``` +Run B is the agent reporting success that did not happen. It is signed and governed, so +a record that only checked signatures would accept it, and the ground-truth check is +what catches it. The verification command runs in the platform shell (sh on Unix, cmd on +Windows), so the script picks a check the local shell understands. + ## Honesty The forged records in `proof.sh` (steps 3-5) are crafted conformance vectors, generated diff --git a/demo/proof-live.sh b/demo/proof-live.sh index c3608386..1ccb9cfe 100755 --- a/demo/proof-live.sh +++ b/demo/proof-live.sh @@ -18,9 +18,11 @@ set -euo pipefail root="$(cd "$(dirname "$0")/.." && pwd)" cd "$root" -flynn="./flynn" +# Absolute path: the goals run inside a temporary working directory. +flynn="$root/flynn" go build -o "$flynn" ./cmd/flynn +# Flynn's flags are global: they come before the subcommand. model_arg=() if [ "${1:-}" = "--model" ] && [ -n "${2:-}" ]; then model_arg=(--model "$2") @@ -28,25 +30,46 @@ fi work="$(mktemp -d)" data="$(mktemp -d)" -common=("${model_arg[@]}" --data-dir "$data" --no-learn -v) -run_in() { ( cd "$work" && "$flynn" "$@" ); } +# The verification check runs in the platform's shell (sh on Unix, cmd on Windows), so +# pick a check that the local shell understands. +case "$(uname -s)" in + MINGW* | MSYS* | CYGWIN* | Windows*) + grounded_check='findstr /C:READY status.txt >NUL' + ungrounded_check='findstr /C:DEPLOYED release.log >NUL' + ;; + *) + grounded_check='test -f status.txt && grep -q READY status.txt' + ungrounded_check='grep -q DEPLOYED release.log' + ;; +esac hr() { printf '\n\033[1m%s\033[0m\n' "$*"; } +# run_goal CHECK OBJECTIVE: drive one goal in the work directory with an independent +# verification check, and remember its run id. All flags precede the `goal` subcommand. +ids=() +run_goal() { + local out + out="$( cd "$work" && "$flynn" "${model_arg[@]}" --data-dir "$data" --no-learn --verify "$1" goal "$2" 2>&1 )" + printf '%s\n' "$out" + ids+=( "$(printf '%s\n' "$out" | grep -oE 'run [0-9a-f-]{36}' | head -1 | awk '{print $2}')" ) +} + 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" +run_goal "$grounded_check" \ + "create a file named status.txt containing exactly the 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" \ +run_goal "$ungrounded_check" \ "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 +for id in "${ids[@]}"; do + [ -n "$id" ] || continue + "$flynn" --data-dir "$data" spine verify "$id" || true echo done diff --git a/demo/proof.sh b/demo/proof.sh index 70db5415..6c268cb9 100755 --- a/demo/proof.sh +++ b/demo/proof.sh @@ -16,7 +16,7 @@ set -euo pipefail root="$(cd "$(dirname "$0")/.." && pwd)" cd "$root" -flynn="./flynn" +flynn="$root/flynn" echo "building flynn..." go build -o "$flynn" ./cmd/flynn