✓
Passing This code compiles and runs correctly.
Code
// `assumes` walks the CALL GRAPH: the transitive closure of flows a
// declaration's implementation can reach, graded by the claims each reached
// declaration carries about itself — and conspicuously WITHOUT one when it
// carries none.
//
// koruc <file> assumes <subject>
//
// This program declares a measured CONTRACTED tor that the runner flow calls,
// and an UNCLAIMED middleman between them. The audit of `root` must show:
// - the unclaimed middleman (the finding: a reachable declaration that
// asserts nothing),
// - the claimed leaf, with its stamp,
// and it must NOT fabricate claims for anything else. The absence is the
// test: `mid` is reached and reported `unclaimed`, never silently dropped.
~import std/compiler
~[
- proven contract-honest
Declared by the same shape checker that discharges the obligation.
]tor leaf { v: i64 } -> i64
~tor mid { n: i64 }
~mid = leaf(v: 42)
~tor root { n: i64 }
~root = mid(n: 7)Flows
subflow ~mid click a branch to expand · @labels scroll to their anchor
leaf (v: 42)
subflow ~root click a branch to expand · @labels scroll to their anchor
mid (n: 7)
Test Configuration
Post-validation Script:
#!/bin/bash
# `assumes root` walks root's flow body transitively and reports every
# reachable declaration, graded by its claim — with UNCLAIMED a first-class
# row. The structual point of the audit: a reached declaration without a claim
# is REPORTED, never dropped, and a claimed leaf carries its stamp.
set -e
OUT=$(koruc "$KORU_INPUT" assumes root 2>&1) && RC=0 || RC=$?
[ "$RC" -eq 0 ] \
|| { echo "FAIL: assumes exited $RC"; echo "$OUT"; exit 1; }
echo "$OUT" | grep -q '^📋 assumes — ' \
|| { echo "FAIL: subject header missing"; echo "$OUT"; exit 1; }
# The unclaimed middleman is the finding: reached, reported, stamped unclaimed.
echo "$OUT" | grep -q 'mid \[unclaimed\]' \
|| { echo "FAIL: unclaimed middleman not reported"; echo "$OUT"; exit 1; }
# The claimed leaf carries its stamp and rule.
echo "$OUT" | grep -q 'leaf \[proven\] contract-honest' \
|| { echo "FAIL: claimed leaf not reported with stamp"; echo "$OUT"; exit 1; }
# JSON form: same closure, machine-readable.
OUTJ=$(koruc "$KORU_INPUT" assumes root json 2>&1)
echo "$OUTJ" | grep -q '"subject":"' \
|| { echo "FAIL: json subject missing"; echo "$OUTJ"; exit 1; }
echo "$OUTJ" | grep -q '"stamp":"unclaimed"' \
|| { echo "FAIL: json unclaimed stamp missing"; echo "$OUTJ"; exit 1; }
echo "=== Test passed: transitive closure graded by claims ==="