006 assumes effective grade

✓ Passing This code compiles and runs correctly.

Code

// `assumes` grades by closure, not by stamp alone. A declaration's EFFECTIVE
// grade is the weakest claim anywhere beneath it (Lean's `#print axioms`
// showing [sorryAx] under a theorem that uses `sorry`). The authored stamp is
// never overridden, but the effective grade tells the truth about what the
// claim rests on:
//
//   claimed  [proven] bought-with-debt      <- authored stamp
//   ↓ effective: unclaimed                 <- the closure contains no claim
//
// This chains: claimed calls bought (unclaimed), which calls stream
// (aspirational — honest admitted debt). The proven claim's effective grade
// must NOT be proven; the aspirational's own effective is aspirational
// (admitted debt shows as itself), and the unclaimed middleman is the silence
// the audit exists to surface.
//
//   koruc <file> assumes claimed

~import std/rules

~[
- aspirational someday-streams
  Honest admitted debt: this slurps, not built yet.
]tor stream { n: i64 } -> i64

~tor bought { n: i64 }
~bought = stream(n: 1)

~[
- proven bought-with-debt
  Claims proven, but its closure rests on the aspirational above.
]tor claimed { n: i64 }
~claimed = bought(n: 2)

input.kz

Flows

subflow ~bought click a branch to expand · @labels scroll to their anchor

stream (n: 1)

subflow ~claimed click a branch to expand · @labels scroll to their anchor

bought (n: 2)

Test Configuration

Post-validation Script:

#!/bin/bash
# The effective grade is the whole point of `assumes`: a `proven` claim whose
# closure contains an aspirational callee must NOT present as effective proven.
# The authored stamp stays honest; the effective line tells what it rests on.
#
#   claimed [proven] bought-with-debt
#   ↓ effective: unclaimed        <- the finding: proof with no claim beneath
#   bought  [unclaimed]
#   ↓ effective: unclaimed       <- silence, first-class
#   stream  [aspirational] someday-streams
#   ↓ effective: aspirational    <- admitted debt shows as itself

set -e

OUT=$(koruc "$KORU_INPUT" assumes claimed 2>&1) && RC=0 || RC=$?
[ "$RC" -eq 0 ] || { echo "FAIL: assumes exited $RC"; echo "$OUT"; exit 1; }

# The proven claim keeps its authored stamp...
echo "$OUT" | grep -q 'claimed  \[proven\] bought-with-debt' \
    || { echo "FAIL: authored proven stamp lost"; echo "$OUT"; exit 1; }

# ...but its effective grade is dragged down by the silent closure.
echo "$OUT" | grep -q 'effective: unclaimed' \
    || { echo "FAIL: proven claim over an unclaimed callee reports a clean effective"; echo "$OUT"; exit 1; }

# The aspirational leaf shows its own debt as itself.
echo "$OUT" | grep -q 'stream  \[aspirational\] someday-streams' \
    || { echo "FAIL: aspirational callee not reached"; echo "$OUT"; exit 1; }

# JSON form carries the effective per row.
OUTJ=$(koruc "$KORU_INPUT" assumes claimed json 2>&1)
echo "$OUTJ" | grep -q '"effective":"unclaimed"' \
    || { echo "FAIL: json effective grade missing"; echo "$OUTJ"; exit 1; }

echo "=== Test passed: effective grade = what the closure rests on ==="

← 005 assumes transitive closure 001 todo declares without executing →