EXPERIMENT: the capability tier becomes shipped policy plus a query
Capability differs from prohibits_outside in one way that matters: a utility program cannot be trusted to declare its own restrictions, because it would declare none. So the policy comes from OUTSIDE the program -- it ships with the language as data, editable without a compiler release. tools/check/capabilities.rel 18 names that were string literals in codegen tools/check/capabilities.sh the query that decides PREDICTIONS AND RESULTS P1 codegen emits kind + call graph, drops the 4 name tests TRUE zero #errors P2 the 18 literals become a data file TRUE P3 the checker catches capability violations TRUE exit=1 P4 codegen drops ~76 lines TRUE 4963 -> 4881 P5 below the 4661 baseline FALSE ~+230 TWO DEFECTS THE HARNESS FOUND THAT READING WOULD NOT HAVE 1. Calls inside main became invisible. cg_fn returns early for main -- C provides its own -- so hooking the recording there left every call in main unrecorded: a blind spot exactly where a program does its work. The old cap_check_call ran from cg_expr and did see main. Moved the recording to cg_expr. 2. Caller attribution was stale. __cg_current_fn kept whatever cg_fn set last, so a violation in main was reported against the previously emitted function. The test still PASSED, because the violation was detected -- only the name was wrong, and a diagnostic naming the wrong fn is worse than none. Fixed at all three main-emission sites; the first patch missed two because the live path is codegen_streaming. 98/98 native, 7/7 + 4/4 + 5/5 integration, fixpoint ok.
This commit is contained in:
@@ -992,12 +992,14 @@ fn cg_expr(expr: Map<String, Any>) -> String {
|
||||
|
||||
if func_kind == "Ident" {
|
||||
let fn_name: String = func["name"]
|
||||
// Capability-kind enforcement: services can't call
|
||||
// self-formation primitives; utilities can't call any
|
||||
// DHARMA or LLM primitives. cap_check_call records
|
||||
// violations to be emitted as #error directives at the
|
||||
// top of the generated C, so cc fails with a clear msg.
|
||||
cap_check_call(fn_name)
|
||||
// Every call is recorded here, from cg_expr, because this runs for
|
||||
// EVERY expression in every context -- including main's body, which
|
||||
// cg_fn returns early on since C provides its own main. Hooking the
|
||||
// recording to cg_fn instead left every call in main invisible to
|
||||
// the relation graph, a blind spot exactly where a program does its
|
||||
// work. Caught by capability_query.sh, not by reading the code.
|
||||
record_call("program", "is_kind:" + state_get("__program_kind"))
|
||||
record_call(state_get("__cg_current_fn"), fn_name)
|
||||
// Arity check against the builtin table - refuse, with a clear
|
||||
// El-source message, when a known builtin gets the wrong arg
|
||||
// count (e.g. `http_serve(port)` instead of `http_serve(port,
|
||||
@@ -2491,95 +2493,19 @@ fn float_operand_c(expr: Map<String, Any>, expr_c: String) -> String {
|
||||
// The compiler-level rule is structural: the binary either CAN or CANNOT
|
||||
// emit the call. There is no runtime check, no opt-in, no override.
|
||||
|
||||
fn cap_record_violation(kind: String, fn_name: String) -> Bool {
|
||||
let csv: String = state_get("__cap_violations")
|
||||
if str_eq(csv, "") { let csv = "," }
|
||||
let entry: String = kind + ":" + fn_name
|
||||
let key: String = "," + entry + ","
|
||||
if str_contains(csv, key) { return true }
|
||||
state_set("__cap_violations", csv + entry + ",")
|
||||
return true
|
||||
}
|
||||
|
||||
// Self-formation primitives - the cut between CGI and service. A program
|
||||
// that emits these calls IS structurally a CGI; we forbid them everywhere
|
||||
// else.
|
||||
fn is_self_formation_call(fn_name: String) -> Bool {
|
||||
if str_eq(fn_name, "llm_call_agentic") { return true }
|
||||
if str_eq(fn_name, "llm_register_tool") { return true }
|
||||
if str_eq(fn_name, "dharma_emit") { return true }
|
||||
if str_eq(fn_name, "dharma_field") { return true }
|
||||
return false
|
||||
}
|
||||
|
||||
// Any DHARMA primitive - utilities have zero network presence.
|
||||
fn is_dharma_call(fn_name: String) -> Bool {
|
||||
if str_eq(fn_name, "dharma_connect") { return true }
|
||||
if str_eq(fn_name, "dharma_send") { return true }
|
||||
if str_eq(fn_name, "dharma_activate") { return true }
|
||||
if str_eq(fn_name, "dharma_emit") { return true }
|
||||
if str_eq(fn_name, "dharma_field") { return true }
|
||||
if str_eq(fn_name, "dharma_strengthen") { return true }
|
||||
if str_eq(fn_name, "dharma_relationship") { return true }
|
||||
if str_eq(fn_name, "dharma_peers") { return true }
|
||||
return false
|
||||
}
|
||||
|
||||
// Any LLM primitive - utilities have no LLM access at all.
|
||||
fn is_llm_call(fn_name: String) -> Bool {
|
||||
if str_eq(fn_name, "llm_call") { return true }
|
||||
if str_eq(fn_name, "llm_call_system") { return true }
|
||||
if str_eq(fn_name, "llm_call_agentic") { return true }
|
||||
if str_eq(fn_name, "llm_vision") { return true }
|
||||
if str_eq(fn_name, "llm_register_tool") { return true }
|
||||
if str_eq(fn_name, "llm_models") { return true }
|
||||
return false
|
||||
}
|
||||
|
||||
fn cap_check_call(fn_name: String) -> Bool {
|
||||
let kind: String = state_get("__program_kind")
|
||||
if str_eq(kind, "cgi") { return true }
|
||||
if str_eq(kind, "service") {
|
||||
if is_self_formation_call(fn_name) {
|
||||
cap_record_violation("service", fn_name)
|
||||
return false
|
||||
}
|
||||
return true
|
||||
}
|
||||
// utility (default)
|
||||
if is_dharma_call(fn_name) {
|
||||
cap_record_violation("utility", fn_name)
|
||||
return false
|
||||
}
|
||||
if is_llm_call(fn_name) {
|
||||
cap_record_violation("utility", fn_name)
|
||||
return false
|
||||
}
|
||||
return true
|
||||
}
|
||||
|
||||
// Emit collected capability violations as #error directives. Called
|
||||
// from codegen()'s entry point right after the cgi/service-block scan,
|
||||
// so they appear at the very top of the generated C.
|
||||
fn emit_cap_violations() -> Void {
|
||||
let csv: String = state_get("__cap_violations")
|
||||
if str_eq(csv, "") { return }
|
||||
if str_eq(csv, ",") { return }
|
||||
let n: Int = str_len(csv)
|
||||
let i: Int = 1
|
||||
while i < n {
|
||||
let next_comma: Int = str_index_of(str_slice(csv, i, n), ",")
|
||||
if next_comma < 0 { return }
|
||||
let entry: String = str_slice(csv, i, i + next_comma)
|
||||
let colon: Int = str_index_of(entry, ":")
|
||||
if colon > 0 {
|
||||
let kind: String = str_slice(entry, 0, colon)
|
||||
let fn_name: String = str_slice(entry, colon + 1, str_len(entry))
|
||||
emit_line("#error \"capability violation: '" + kind + "' programs may not call '" + fn_name + "' (self-formation primitive - only 'cgi' programs may use it)\"")
|
||||
}
|
||||
let i = i + next_comma + 1
|
||||
}
|
||||
}
|
||||
|
||||
// Surface temporal-type violations as #error directives. The cg_expr BinOp
|
||||
// dispatcher records each violation (Instant + Instant, Duration + Int, -)
|
||||
@@ -3471,9 +3397,15 @@ fn emit_program_init(stmt: Map<String, Any>) -> Void {
|
||||
fn record_call(caller: String, callee: String) -> Void {
|
||||
let path: String = env("EL_RELATIONS_OUT")
|
||||
if str_eq(path, "") { return }
|
||||
// cg_fn returns early for `main` -- C provides its own -- so __cg_current_fn
|
||||
// is unset while main's body is walked. Without this, every call in main is
|
||||
// invisible to the relation graph and both checkers have a blind spot
|
||||
// exactly where a program does its work. Caught by capability_query.sh.
|
||||
let caller2: String = caller
|
||||
if str_eq(caller2, "") { let caller2 = "main" }
|
||||
let prev: String = ""
|
||||
if fs_exists(path) { let prev = fs_read(path) }
|
||||
fs_write(path, prev + caller + " calls " + callee + "\n")
|
||||
fs_write(path, prev + caller2 + " calls " + callee + "\n")
|
||||
}
|
||||
|
||||
|
||||
@@ -3653,7 +3585,6 @@ fn codegen(stmts: [Map<String, Any>], source: String) -> String {
|
||||
if svc_count >= 1 { let kind = "service" }
|
||||
state_set("__program_kind", kind)
|
||||
// Clear capability-violation accumulator from any prior compile.
|
||||
state_set("__cap_violations", "")
|
||||
// Clear arity-violation accumulator from any prior compile.
|
||||
state_set("__arity_violations", "")
|
||||
// Clear temporal-type-violation accumulator from any prior compile.
|
||||
@@ -3818,6 +3749,11 @@ fn codegen(stmts: [Map<String, Any>], source: String) -> String {
|
||||
// main(). Use _argc/_argv so El programs are free to declare their own
|
||||
// local `argv` / `argc` (compiler.el itself does this) without colliding
|
||||
// with the C-side parameters when fn main()'s body is folded in below.
|
||||
// From here the emitter is walking main's body. Without resetting this the
|
||||
// caller attribution is stale from the last cg_fn, so a violation inside
|
||||
// main is reported against whichever function happened to be emitted last
|
||||
// -- a diagnostic naming the wrong fn is worse than none.
|
||||
state_set("__cg_current_fn", "main")
|
||||
emit_line("int main(int _argc, char** _argv) {")
|
||||
emit_line(" el_runtime_init_args(_argc, _argv);")
|
||||
if prog_have {
|
||||
@@ -3914,7 +3850,6 @@ fn codegen(stmts: [Map<String, Any>], source: String) -> String {
|
||||
// will fail on the first one and surface the message; placement at
|
||||
// the bottom is fine - preprocessor errors halt the build wherever
|
||||
// they appear.
|
||||
emit_cap_violations()
|
||||
// Same for builtin-arity violations: cc halts on the first #error,
|
||||
// so a misuse of a known builtin (wrong arg count) fails the build
|
||||
// with a clear message naming the builtin and its expected arity.
|
||||
@@ -4429,7 +4364,6 @@ fn emit_streaming_preamble(sigs: [Map<String, Any>], source: String) -> Void {
|
||||
if cgi_count >= 1 { let kind = "cgi" }
|
||||
if svc_count >= 1 { let kind = "service" }
|
||||
state_set("__program_kind", kind)
|
||||
state_set("__cap_violations", "")
|
||||
state_set("__arity_violations", "")
|
||||
state_set("__time_violations", "")
|
||||
|
||||
@@ -4838,6 +4772,7 @@ fn codegen_streaming(tokens: [Any], sigs: [Map<String, Any>], source: String) ->
|
||||
|
||||
// main() delegates to the El-side runner. Everything above this line is
|
||||
// generated glue; all reporting logic lives in runtime/eltest.el.
|
||||
state_set("__cg_current_fn", "main")
|
||||
emit_line("int main(int _argc, char **_argv) {")
|
||||
emit_line(" el_runtime_init_args(_argc, _argv);")
|
||||
emit_line(" for (int _i = 1; _i < _argc; _i++) {")
|
||||
@@ -4867,6 +4802,7 @@ fn codegen_streaming(tokens: [Any], sigs: [Map<String, Any>], source: String) ->
|
||||
// Emit main() — wrap in arena scope to free intermediate strings.
|
||||
let main_arena_mark: Any = el_arena_push()
|
||||
let kind2: String = state_get("__program_kind")
|
||||
state_set("__cg_current_fn", "main")
|
||||
emit_line("int main(int _argc, char** _argv) {")
|
||||
emit_line(" el_runtime_init_args(_argc, _argv);")
|
||||
// Cross-cutting concerns declared by a `program` block run BEFORE anything
|
||||
@@ -4952,8 +4888,6 @@ fn codegen_streaming(tokens: [Any], sigs: [Map<String, Any>], source: String) ->
|
||||
emit_line(" return 0;")
|
||||
emit_line("}")
|
||||
emit_blank()
|
||||
|
||||
emit_cap_violations()
|
||||
emit_arity_violations()
|
||||
emit_time_violations()
|
||||
el_arena_pop(main_arena_mark)
|
||||
|
||||
Executable
+36
@@ -0,0 +1,36 @@
|
||||
#!/usr/bin/env bash
|
||||
# Control for capability-as-policy: the compiler records the program's kind and
|
||||
# its call graph; the shipped policy file and the checker decide.
|
||||
set -uo pipefail
|
||||
ELC="${1:?usage: capability_query.sh <elc>}"
|
||||
LANG_DIR="${2:-$(cd "$(dirname "${BASH_SOURCE[0]}")/../.." && pwd)}"
|
||||
W=$(mktemp -d); trap 'rm -rf "$W"' EXIT; F=0
|
||||
chk(){ [ "$2" = "$3" ] && printf ' ok %s\n' "$1" || { printf ' FAIL %s\n expected %s got %s\n' "$1" "$2" "$3"; F=$((F+1)); }; }
|
||||
|
||||
cat > "$W/u.el" <<'EOF'
|
||||
fn leaky() -> Int {
|
||||
dharma_emit("x", "y")
|
||||
return 1
|
||||
}
|
||||
fn main() { println("ok") }
|
||||
EOF
|
||||
EL_RELATIONS_OUT="$W/r.txt" "$ELC" "$W/u.el" >/dev/null 2>&1
|
||||
chk "the emitter does not adjudicate" "0" "$("$ELC" "$W/u.el" 2>/dev/null | grep -c 'capability violation')"
|
||||
"$LANG_DIR/tools/check/capabilities.sh" "$W/r.txt" > "$W/o.txt" 2>&1; rc=$?
|
||||
chk "a utility calling a DHARMA primitive is caught" "1" "$rc"
|
||||
chk "the offending fn is named" "1" "$(grep -c 'called from leaky' "$W/o.txt")"
|
||||
|
||||
cat > "$W/c.el" <<'EOF'
|
||||
fn quiet() -> Int { return 1 }
|
||||
fn main() { println("ok") }
|
||||
EOF
|
||||
EL_RELATIONS_OUT="$W/r2.txt" "$ELC" "$W/c.el" >/dev/null 2>&1
|
||||
"$LANG_DIR/tools/check/capabilities.sh" "$W/r2.txt" >/dev/null 2>&1
|
||||
chk "a clean program exits 0" "0" "$?"
|
||||
|
||||
# the policy is DATA: editing it changes enforcement, with no compiler rebuild
|
||||
printf 'utility prohibits_within println\n' > "$W/policy.rel"
|
||||
"$LANG_DIR/tools/check/capabilities.sh" "$W/r2.txt" "$W/policy.rel" >/dev/null 2>&1
|
||||
chk "editing the policy file changes enforcement, no rebuild" "1" "$?"
|
||||
|
||||
echo; echo " 5 assertions, $((5-F)) passed, $F failed"; exit $F
|
||||
@@ -0,0 +1,18 @@
|
||||
# capabilities.rel — the capability policy, as shipped data.
|
||||
#
|
||||
# A program's tier bounds what it may call. This is policy that comes from
|
||||
# OUTSIDE the program: a utility cannot be trusted to declare its own
|
||||
# restrictions, because it would declare none. So unlike prohibits_outside,
|
||||
# which a program declares about itself, this ships with the language and is
|
||||
# editable without a compiler release.
|
||||
#
|
||||
# Previously: four functions and eighteen string literals inside codegen.el.
|
||||
#
|
||||
# <kind> prohibits_within <comma-separated names>
|
||||
|
||||
service prohibits_within llm_call_agentic,llm_register_tool,dharma_emit,dharma_field
|
||||
|
||||
utility prohibits_within dharma_connect,dharma_send,dharma_activate,dharma_emit,dharma_field,dharma_strengthen,dharma_relationship,dharma_peers
|
||||
utility prohibits_within llm_call,llm_call_system,llm_call_agentic,llm_vision,llm_register_tool,llm_models
|
||||
|
||||
# cgi is unrestricted: self-formation is what a cgi program is for.
|
||||
Executable
+24
@@ -0,0 +1,24 @@
|
||||
#!/usr/bin/env bash
|
||||
# capabilities.sh — enforce the capability tier as a QUERY over emitted
|
||||
# relations plus a shipped policy file. The compiler records the program's kind
|
||||
# and its call graph; deciding what that tier may call is not an emitter's job.
|
||||
set -uo pipefail
|
||||
REL="${1:?usage: capabilities.sh <relations-file> [policy]}"
|
||||
POLICY="${2:-$(dirname "${BASH_SOURCE[0]}")/capabilities.rel}"
|
||||
[ -f "$REL" ] || exit 0
|
||||
KIND=$(grep -m1 '^program calls is_kind:' "$REL" | sed 's/.*is_kind://')
|
||||
[ -n "$KIND" ] || KIND=utility
|
||||
V=0
|
||||
while read -r kind rel names; do
|
||||
[ "$kind" = "$KIND" ] && [ "$rel" = "prohibits_within" ] || continue
|
||||
IFS=',' read -ra NAMES <<< "$names"
|
||||
for n in "${NAMES[@]}"; do
|
||||
while read -r caller _ callee; do
|
||||
[ "$callee" = "$n" ] || continue
|
||||
printf "capability violation: '%s' programs may not call '%s' (called from %s)\n" "$KIND" "$n" "$caller"
|
||||
V=$((V+1))
|
||||
done < <(sort -u "$REL")
|
||||
done
|
||||
done < <(grep -v '^#' "$POLICY" | grep -v '^[[:space:]]*$')
|
||||
[ "$V" -eq 0 ] && echo "capabilities: clean ($KIND)"
|
||||
exit "$V"
|
||||
Reference in New Issue
Block a user