From f1a7e224a77f020315a81f62d297b7ebff9b822d Mon Sep 17 00:00:00 2001
From: bigmerge <agent@neuron>
Date: Mon, 17 Aug 2026 10:53:01 -0500
Subject: [PATCH] verify the annotation against what it annotates

ISHIKAWA: three silent miscompilations found the same day shared one shape.

  method       type tracked by per-function name sets, fed from annotations
  machine      el_val_t erases everything at the C boundary
  material     no propagation through expressions
  measurement  nothing verifies an annotation against what it annotates
  root cause   El has type ANNOTATIONS and no type CHECKING. The annotation
               feeds dispatch and is never itself verified.

MEASURED, and it is not merely a wrong answer

  let x: Int = "hello" ; x + 1   -> printed 4343631981, a string POINTER
                                    interpreted as an integer
  let s: String = 42   ; println -> dereferenced address 42

The first leaks a raw memory address into program output. The second is an
arbitrary-read primitive if the integer is ever attacker-influenced.

PREDICTIONS AND RESULTS
  P1 let x: Int = "hello" compiles clean               TRUE
  P2 let s: String = 42 compiles clean                 TRUE
  P3 the annotation drives dispatch, unverified        TRUE
  P4 same root cause as all three bugs found today     TRUE
  P5 checking literal-vs-annotation catches both       TRUE
  P6 zero false positives across the compiler's source TRUE

The emitter only RECORDS the mismatch; tools/check/annotations.sh decides,
consistent with every other check landed today.

INCOMPLETE, stated rather than hidden: only literals are checked.
let x: Int = some_string_fn() still passes, because signatures.rel carries
Int/Instant/Duration and no String entries. That is a DATA gap, not a capability
limit -- every El function declares its return type in source and codegen
already holds ret_type on every FnDef.

105/105 native, 5/5 annotation_query.sh, fixpoint ok.
---
 lang/el-compiler/src/codegen.el            | 31 ++++++++++++++++++++
 lang/tests/integration/annotation_query.sh | 34 ++++++++++++++++++++++
 lang/tools/check/annotations.sh            | 29 ++++++++++++++++++
 3 files changed, 94 insertions(+)
 create mode 100755 lang/tests/integration/annotation_query.sh
 create mode 100755 lang/tools/check/annotations.sh

diff --git a/lang/el-compiler/src/codegen.el b/lang/el-compiler/src/codegen.el
index c8e4853..be628f5 100644
--- a/lang/el-compiler/src/codegen.el
+++ b/lang/el-compiler/src/codegen.el
@@ -1526,6 +1526,37 @@ fn cg_stmt(stmt: Map<String, Any>, indent: String, declared: [String]) -> [Strin
         if str_eq(ltype, "Int") {
             add_int_name(name)
         }
+        // ANNOTATION CHECKING. El has type annotations and, until now, no type
+        // checking: the annotation fed dispatch and was never itself verified.
+        // That is the root cause of every silent miscompilation found on
+        // 2026-08-17, and the failure is not merely a wrong answer:
+        //
+        //   let x: Int = "hello"   ; x + 1  -> printed 4343631981, a string
+        //                                     POINTER interpreted as an integer
+        //   let s: String = 42     ; print  -> dereferenced address 42
+        //
+        // The second is an arbitrary-read primitive if the integer is ever
+        // attacker-influenced. Literals are checked here because they are
+        // unambiguous; the emitter only RECORDS the mismatch, the query decides.
+        let vkind: String = val["expr"]
+        if str_eq(ltype, "Int") {
+            if str_eq(vkind, "Str") {
+                record_call(state_get("__cg_current_fn"), "typemismatch:Int:String:" + name)
+            }
+        }
+        if str_eq(ltype, "String") {
+            if str_eq(vkind, "Int") {
+                record_call(state_get("__cg_current_fn"), "typemismatch:String:Int:" + name)
+            }
+            if str_eq(vkind, "Float") {
+                record_call(state_get("__cg_current_fn"), "typemismatch:String:Float:" + name)
+            }
+        }
+        if str_eq(ltype, "Float") {
+            if str_eq(vkind, "Str") {
+                record_call(state_get("__cg_current_fn"), "typemismatch:Float:String:" + name)
+            }
+        }
         // UNANNOTATED let: take the type from what the initialiser RETURNS.
         // Without this, `let a = str_len(s)` loses the Int and a later `a + b`
         // lowers to el_str_concat on two integers -- silently, with no error,
diff --git a/lang/tests/integration/annotation_query.sh b/lang/tests/integration/annotation_query.sh
new file mode 100755
index 0000000..5e6cf70
--- /dev/null
+++ b/lang/tests/integration/annotation_query.sh
@@ -0,0 +1,34 @@
+#!/usr/bin/env bash
+# annotation_query.sh — a declared type must match what it annotates.
+#
+# El had annotations and no checking: the annotation fed dispatch and was never
+# verified against the value, so a mismatch did not fail, it REINTERPRETED
+# MEMORY. let x: Int = "hello" printed 4343631981 (a string pointer used as an
+# integer); let s: String = 42 dereferenced address 42.
+set -uo pipefail
+ELC="${1:?usage: annotation_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)); }; }
+cd "$LANG_DIR"
+
+printf 'fn main() { let x: Int = "hello" println("x") }\n' > "$W/a.el"
+EL_RELATIONS_OUT="$W/r.txt" "$ELC" "$W/a.el" >/dev/null 2>&1
+out=$(./tools/check/annotations.sh "$W/r.txt" 2>&1); rc=$?
+chk "Int annotated on a String literal is caught" "1" "$rc"
+chk "and names the variable" "1" "$(echo "$out" | grep -c "'x' is declared Int")"
+
+printf 'fn main() { let s: String = 42 println(s) }\n' > "$W/b.el"
+EL_RELATIONS_OUT="$W/r2.txt" "$ELC" "$W/b.el" >/dev/null 2>&1
+./tools/check/annotations.sh "$W/r2.txt" >/dev/null 2>&1
+chk "String annotated on an Int literal is caught" "1" "$?"
+
+printf 'fn main() { let n: Int = 42 let s: String = "ok" println(s + int_to_str(n)) }\n' > "$W/c.el"
+EL_RELATIONS_OUT="$W/r3.txt" "$ELC" "$W/c.el" >/dev/null 2>&1
+./tools/check/annotations.sh "$W/r3.txt" >/dev/null 2>&1
+chk "correct annotations are clean" "0" "$?"
+
+EL_RELATIONS_OUT="$W/r4.txt" "$ELC" elc-cli.el >/dev/null 2>&1
+./tools/check/annotations.sh "$W/r4.txt" >/dev/null 2>&1
+chk "the compiler's own source is clean — no false positives" "0" "$?"
+echo; echo "  5 assertions, $((5-F)) passed, $F failed"; exit $F
diff --git a/lang/tools/check/annotations.sh b/lang/tools/check/annotations.sh
new file mode 100755
index 0000000..34e7ce5
--- /dev/null
+++ b/lang/tools/check/annotations.sh
@@ -0,0 +1,29 @@
+#!/usr/bin/env bash
+# annotations.sh — verify that a declared type matches what it annotates.
+#
+# El had annotations and no checking. The annotation fed dispatch (deciding
+# whether `a + b` is arithmetic or concatenation) and was never verified against
+# the value, so a mismatch did not fail -- it reinterpreted memory:
+#
+#   let x: Int = "hello"    a string pointer used as an integer
+#   let s: String = 42      address 42 dereferenced as a string
+#
+# The second is an arbitrary-read primitive if the integer is influenced.
+set -uo pipefail
+REL="${1:?usage: annotations.sh <relations-file>}"
+[ -f "$REL" ] || exit 0
+locate() {
+    awk -v L="$1" '$2=="spans" && $3<=L && $4>=L {printf "%s:%d", $1, L-$3+1; exit}' "$REL" 2>/dev/null
+}
+V=0
+while read -r caller _ rest; do
+    [ "${rest#typemismatch:}" = "$rest" ] && continue
+    body="${rest#typemismatch:}"
+    declared="${body%%:*}"; body="${body#*:}"
+    actual="${body%%:*}";   var="${body#*:}"
+    printf "type error in %s: '%s' is declared %s but assigned a %s literal — the annotation drives dispatch, so the value will be reinterpreted rather than rejected\n" \
+           "$caller" "$var" "$declared" "$actual"
+    V=$((V+1))
+done < <(sort -u "$REL")
+[ "$V" -eq 0 ] && echo "annotations: clean"
+exit "$V"