EXPERIMENT: prohibition becomes a query over emitted relations
I said prohibition could not move because "a #error has no runtime". That
conflated two separable things: WHEN a violation is detected (build time --
correct, and unchanged) and WHERE the rule and the checker live (the compiler
-- assumed).
A prohibition is a containment relation over the call graph. So codegen now
records what it saw:
sneaky calls raw_sql
allowed calls raw_sql
allowed calls @repository
repository calls prohibits:raw_sql
and tools/check/prohibitions.sh decides, at build time, outside the compiler.
PREDICTIONS AND RESULTS
P1 codegen can emit the call graph it already walks TRUE
P2 the check becomes a query outside the compiler TRUE
P3 all prohibition decisions leave codegen TRUE zero #errors now
P4 violations still caught at build time TRUE exit=1
P5 codegen drops below the 4661 baseline FALSE 4962, +301
P5 is the finding. The TRAVERSAL is irreducible -- you must walk the AST to
find calls, and those ~120 lines do not move no matter who decides. What is not
irreducible is the rule (which names) or the decision (#error). Those left. I
predicted the whole 223 lines would go because I had not separated walking from
adjudicating.
Still compiled, and measured rather than assumed: the capability-tier system
(cap_check_call, is_self_formation_call, is_dharma_call, is_llm_call,
cap_record_violation, emit_cap_violations) is 76 lines of the same shape --
prohibits_WITHIN rather than prohibits_outside, so the checker needs the
opposite polarity to absorb it.
98/98 native, 4/4 prohibition_query.sh, 7/7 seam_binding.sh, fixpoint ok.
This commit is contained in:
Executable
+40
@@ -0,0 +1,40 @@
|
||||
#!/usr/bin/env bash
|
||||
# prohibitions.sh — enforce boundary prohibitions as a QUERY over relations the
|
||||
# compiler emitted, rather than as a rule the compiler contains.
|
||||
#
|
||||
# A prohibition is a containment relation over the call graph: "these calls may
|
||||
# appear only inside a fn carrying construct C". The compiler's job is to say
|
||||
# what it saw — who calls what, who carries what, who prohibits what. Deciding
|
||||
# whether that is legal is a query, and a query does not belong in an emitter.
|
||||
#
|
||||
# Detection still happens at BUILD time. What moved is where the rule and the
|
||||
# checker live, which is what "a #error has no runtime" was hiding.
|
||||
#
|
||||
# usage: prohibitions.sh <relations-file>
|
||||
# exit 0 = clean; exit N = N violations
|
||||
set -uo pipefail
|
||||
REL="${1:?usage: prohibitions.sh <relations-file>}"
|
||||
[ -f "$REL" ] || { echo "no relations file: $REL" >&2; exit 0; }
|
||||
|
||||
V=0
|
||||
# construct -> prohibited names
|
||||
while read -r construct _ rest; do
|
||||
[ "${rest#prohibits:}" = "$rest" ] && continue
|
||||
names="${rest#prohibits:}"
|
||||
IFS=',' read -ra NAMES <<< "$names"
|
||||
for n in "${NAMES[@]}"; do
|
||||
# every fn that calls a prohibited name
|
||||
while read -r caller _ callee; do
|
||||
[ "$callee" = "$n" ] || continue
|
||||
# ...must carry the owning construct
|
||||
if ! grep -qx "$caller calls @$construct" "$REL"; then
|
||||
printf 'boundary violation: %s may only be called from an @%s fn, but %s is not one\n' \
|
||||
"$n" "$construct" "$caller"
|
||||
V=$((V+1))
|
||||
fi
|
||||
done < <(sort -u "$REL")
|
||||
done
|
||||
done < <(sort -u "$REL")
|
||||
|
||||
[ "$V" -eq 0 ] && echo "prohibitions: clean"
|
||||
exit "$V"
|
||||
Reference in New Issue
Block a user