Skip to content

Commit d0beeb8

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
feat: add truthfulness gate + proof typecheck + trusted-base scripts
Adds three scripts that form the BoJ quality gate: scripts/typecheck-proofs.sh Runs idris2 --find-ipkg --check on every .idr file under src/abi/ and cartridges/*/abi/. Prints PASS/FAIL per file, exits 0 iff FAIL=0. Surfaces pre-existing proof failures in core ABI modules (CartridgeDispatch, SafeCORS, SafePromptInjection) without hiding them; new textkit-mcp proof passes cleanly. scripts/check-trusted-base.sh Counts non-comment believe_me calls in SafetyLemmas.idr. Exits 1 if count differs from EXPECTED (default 5 — charEqSound, charEqSym, unpackLength, appendLengthSum, substrLengthBound). Currently: PASS 5/5. tests/truthfulness_check.sh Truthfulness gate: finds all cartridges with available:true in boj-server/cartridges/ and the sibling boj-server-cartridges repo. Invokes boj-invoke on the first tool of each; fails on stub result. Currently: PASS=1 (textkit-mcp encode_base64), SKIP=264 (stub). Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
1 parent fa14adf commit d0beeb8

3 files changed

Lines changed: 250 additions & 0 deletions

File tree

‎scripts/check-trusted-base.sh‎

Lines changed: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,42 @@
1+
#!/usr/bin/env bash
2+
# SPDX-License-Identifier: MPL-2.0
3+
# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath)
4+
#
5+
# check-trusted-base.sh — Audit believe_me usage in the BoJ ABI proof base.
6+
#
7+
# Counts non-comment believe_me occurrences in src/abi/Boj/SafetyLemmas.idr.
8+
# Prints: "Axiom count: N" and exits 0 if N equals EXPECTED (default 5).
9+
# Any deviation from EXPECTED exits 1 and triggers a review.
10+
#
11+
# The five declared axioms are:
12+
# charEqSound, charEqSym, unpackLength, appendLengthSum, substrLengthBound
13+
# These are load-bearing FFI-boundary axioms (see SafetyLemmas.idr header).
14+
15+
set -euo pipefail
16+
17+
REPO="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)"
18+
SAFETY_LEMMAS="$REPO/src/abi/Boj/SafetyLemmas.idr"
19+
EXPECTED="${EXPECTED_AXIOMS:-5}"
20+
21+
if [[ ! -f "$SAFETY_LEMMAS" ]]; then
22+
echo "ERROR: SafetyLemmas.idr not found at $SAFETY_LEMMAS" >&2
23+
exit 1
24+
fi
25+
26+
# Count believe_me occurrences that are NOT inside ||| docstrings or -- comments.
27+
# Strip comment lines, then count remaining believe_me.
28+
COUNT="$(grep -v '^\s*|||' "$SAFETY_LEMMAS" | grep -v '^\s*--' | grep -c 'believe_me' || true)"
29+
30+
echo "Axiom count: $COUNT (expected $EXPECTED)"
31+
echo "File: src/abi/Boj/SafetyLemmas.idr"
32+
33+
if [[ "$COUNT" -lt "$EXPECTED" ]]; then
34+
echo "WARN: fewer believe_me axioms than expected — was one removed without review?" >&2
35+
exit 1
36+
elif [[ "$COUNT" -gt "$EXPECTED" ]]; then
37+
echo "FAIL: believe_me budget exceeded ($COUNT > $EXPECTED) — triggers estate-wide sweep rule" >&2
38+
exit 1
39+
fi
40+
41+
echo "PASS: trusted-base axiom count correct ($COUNT/$EXPECTED)"
42+
exit 0

‎scripts/typecheck-proofs.sh‎

Lines changed: 79 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,79 @@
1+
#!/usr/bin/env bash
2+
# SPDX-License-Identifier: MPL-2.0
3+
# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath)
4+
#
5+
# typecheck-proofs.sh — Run idris2 --check on every ABI proof in the repo.
6+
#
7+
# Checks:
8+
# - src/abi/Boj/*.idr (core BoJ ABI proofs)
9+
# - cartridges/*/abi/**/*.idr (per-cartridge ABI proofs)
10+
#
11+
# Prints: PASS=N FAIL=N at the end.
12+
# Exit 0 if FAIL=0; exit 1 otherwise.
13+
14+
set -euo pipefail
15+
16+
REPO="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)"
17+
18+
PASS=0
19+
FAIL=0
20+
21+
check_idr() {
22+
local idr_file="$1"
23+
local idr_dir
24+
idr_dir="$(dirname "$idr_file")"
25+
local idr_base
26+
idr_base="$(basename "$idr_file")"
27+
local rel="${idr_file#$REPO/}"
28+
29+
# Run from the directory containing the file so --find-ipkg can locate
30+
# the package descriptor in the same or a parent directory.
31+
local out
32+
if out="$(cd "$idr_dir" && idris2 --find-ipkg --check "$idr_base" 2>&1)"; then
33+
echo "PASS $rel"
34+
PASS=$((PASS + 1))
35+
else
36+
echo "FAIL $rel"
37+
echo " $out" | head -5
38+
FAIL=$((FAIL + 1))
39+
fi
40+
}
41+
42+
# Core ABI proofs: src/abi/Boj/*.idr
43+
ABI_DIR="$REPO/src/abi"
44+
if [[ -d "$ABI_DIR" ]]; then
45+
# Run each file from the abi/ directory root so --find-ipkg finds boj.ipkg
46+
while IFS= read -r -d '' idr_file; do
47+
rel="${idr_file#$ABI_DIR/}"
48+
out="$(cd "$ABI_DIR" && idris2 --find-ipkg --check "$rel" 2>&1)" && {
49+
echo "PASS src/abi/$rel"
50+
PASS=$((PASS + 1))
51+
} || {
52+
echo "FAIL src/abi/$rel"
53+
echo "$out" | head -5
54+
FAIL=$((FAIL + 1))
55+
}
56+
done < <(find "$ABI_DIR" -name "*.idr" -print0 | sort -z)
57+
fi
58+
59+
# Cartridge ABI proofs: cartridges/*/abi/**/*.idr
60+
CART_DIR="$REPO/cartridges"
61+
if [[ -d "$CART_DIR" ]]; then
62+
while IFS= read -r -d '' idr_file; do
63+
local_abi_dir="$(echo "$idr_file" | sed 's|/[^/]*/[^/]*\.idr$||')"
64+
rel_in_abi="${idr_file#$local_abi_dir/}"
65+
rel="${idr_file#$REPO/}"
66+
out="$(cd "$local_abi_dir" && idris2 --find-ipkg --check "$rel_in_abi" 2>&1)" && {
67+
echo "PASS $rel"
68+
PASS=$((PASS + 1))
69+
} || {
70+
echo "FAIL $rel"
71+
echo "$out" | head -5
72+
FAIL=$((FAIL + 1))
73+
}
74+
done < <(find "$CART_DIR" -path "*/abi/*.idr" -print0 | sort -z)
75+
fi
76+
77+
echo ""
78+
echo "PASS=$PASS FAIL=$FAIL"
79+
[[ $FAIL -eq 0 ]]

‎tests/truthfulness_check.sh‎

Lines changed: 129 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,129 @@
1+
#!/usr/bin/env bash
2+
# SPDX-License-Identifier: MPL-2.0
3+
# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath)
4+
#
5+
# truthfulness_check.sh — Enforce the BoJ truthfulness gate.
6+
#
7+
# A cartridge with "available":true MUST NOT return {"status":"stub"} for any
8+
# of its tools. This gate invokes the first tool of every available cartridge
9+
# and fails if the result is a stub marker.
10+
#
11+
# Scans:
12+
# - $REPO/cartridges/**/cartridge.json (boj-server legacy bundled)
13+
# - $CARTRIDGES_REPO/cartridges/**/cartridge.json (canonical registry)
14+
#
15+
# Set CARTRIDGES_REPO env to override the sibling repo path.
16+
# Set BOJ_INVOKE env to point directly at the boj-invoke binary.
17+
#
18+
# Exit 0 if all available cartridges pass; exit 1 if any stub detected.
19+
20+
set -euo pipefail
21+
22+
REPO="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)"
23+
CARTRIDGES_REPO="${CARTRIDGES_REPO:-$(cd "$REPO/../boj-server-cartridges" 2>/dev/null && pwd || echo "")}"
24+
25+
# Locate boj-invoke
26+
BOJ_INVOKE="${BOJ_INVOKE:-}"
27+
if [[ -z "$BOJ_INVOKE" ]]; then
28+
BOJ_INVOKE="$(find "$REPO/ffi/zig/zig-out/bin" -name "boj-invoke" -maxdepth 1 2>/dev/null | head -1 || echo "")"
29+
fi
30+
if [[ -z "$BOJ_INVOKE" || ! -x "$BOJ_INVOKE" ]]; then
31+
echo "ERROR: boj-invoke not found. Build with: cd ffi/zig && zig build invoke" >&2
32+
echo " Or set BOJ_INVOKE=/path/to/boj-invoke" >&2
33+
exit 1
34+
fi
35+
36+
PASS=0
37+
FAIL=0
38+
SKIP=0
39+
CHECKED=()
40+
41+
check_cartridge() {
42+
local cart_json="$1"
43+
local cart_dir
44+
cart_dir="$(dirname "$cart_json")"
45+
local name
46+
name="$(jq -r '.name // "unknown"' "$cart_json" 2>/dev/null || echo "unknown")"
47+
local available
48+
available="$(jq -r '.available // false' "$cart_json" 2>/dev/null || echo "false")"
49+
50+
if [[ "$available" != "true" ]]; then
51+
SKIP=$((SKIP + 1))
52+
return
53+
fi
54+
55+
# Guard against double-checking the same cartridge from two scan roots
56+
if printf '%s\n' "${CHECKED[@]+" ${CHECKED[*]}"}" | grep -qF " $name "; then
57+
return
58+
fi
59+
CHECKED+=(" $name ")
60+
61+
local so_path
62+
so_path="$(jq -r '.ffi.so_path // empty' "$cart_json" 2>/dev/null || echo "")"
63+
if [[ -z "$so_path" ]]; then
64+
echo " FAIL $name: no ffi.so_path in cartridge.json"
65+
FAIL=$((FAIL + 1))
66+
return
67+
fi
68+
69+
local so_abs="$cart_dir/$so_path"
70+
if [[ ! -f "$so_abs" ]]; then
71+
echo " FAIL $name: .so not found at $so_abs"
72+
FAIL=$((FAIL + 1))
73+
return
74+
fi
75+
76+
local first_tool
77+
first_tool="$(jq -r '.tools[0].name // empty' "$cart_json" 2>/dev/null || echo "")"
78+
if [[ -z "$first_tool" ]]; then
79+
echo " FAIL $name: no tools in cartridge.json"
80+
FAIL=$((FAIL + 1))
81+
return
82+
fi
83+
84+
local result
85+
result="$("$BOJ_INVOKE" "$so_abs" invoke "$first_tool" '{}' 2>/dev/null || echo '{"error":"invoke_failed"}')"
86+
87+
if echo "$result" | grep -q '"status":"stub"'; then
88+
echo " FAIL $name ($first_tool): stub detected — $result"
89+
FAIL=$((FAIL + 1))
90+
elif echo "$result" | grep -qE '"error".*invoke_failed'; then
91+
echo " FAIL $name ($first_tool): invocation failed — $result"
92+
FAIL=$((FAIL + 1))
93+
else
94+
echo " PASS $name ($first_tool): $result"
95+
PASS=$((PASS + 1))
96+
fi
97+
}
98+
99+
echo "BoJ Truthfulness Gate"
100+
echo "====================="
101+
echo "boj-invoke: $BOJ_INVOKE"
102+
echo ""
103+
104+
echo "Scanning: $REPO/cartridges/"
105+
while IFS= read -r -d '' cart_json; do
106+
check_cartridge "$cart_json"
107+
done < <(find "$REPO/cartridges" -name "cartridge.json" -print0 2>/dev/null | sort -z)
108+
109+
if [[ -n "$CARTRIDGES_REPO" && -d "$CARTRIDGES_REPO/cartridges" ]]; then
110+
echo "Scanning: $CARTRIDGES_REPO/cartridges/"
111+
while IFS= read -r -d '' cart_json; do
112+
check_cartridge "$cart_json"
113+
done < <(find "$CARTRIDGES_REPO/cartridges" -name "cartridge.json" -print0 2>/dev/null | sort -z)
114+
fi
115+
116+
echo ""
117+
echo "Results: PASS=$PASS FAIL=$FAIL SKIP=$SKIP (available:false skipped)"
118+
119+
if [[ $FAIL -gt 0 ]]; then
120+
echo "FAIL: $FAIL cartridge(s) failed the truthfulness gate"
121+
exit 1
122+
fi
123+
124+
if [[ $PASS -eq 0 ]]; then
125+
echo "WARN: no available cartridges found — is this expected?"
126+
fi
127+
128+
echo "PASS: all available cartridges are truthful"
129+
exit 0

0 commit comments

Comments
 (0)