land annotation checking: the declared type is finally verified

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,

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

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"