bigmerge
c6ba0677f0
cycles/ one file per Ishikawa -> scientific method -> Six Sigma loop, named
for the DEFECT not the fix, carrying the commit record as written at
the time
findings/ what the cycles produced, cross-cut: live bugs, architecture answers,
and defects in my own measurement
The organising finding is that predictions which came back FALSE produced every
significant result. Eleven of sixty-one failed, and those eleven found: that the
arity table was not drifted but 40% incomplete; that the AST traversal is
irreducible and only rules and judgments move; that guards could refuse through
the seam after all; and that routing el_bin_lookup through the gate did NOT fix
the SIGSEGV, because the fallback strlen was the hazard -- a wrong fix I would
otherwise have shipped as verified.
One cycle was run without committing predictions first and had to be discarded
as rigged. It is kept, in full, as 18-async-half-expressible.md.
54 lines
2.2 KiB
Markdown
54 lines
2.2 KiB
Markdown
# annotations are never checked
|
|
|
|
**Status: verified on `experiment/annotation-checking`, not merged.**
|
|
|
|
## Ishikawa — why does El silently miscompile?
|
|
|
|
Three bugs 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 but no type CHECKING. The annotation
|
|
feeds dispatch and is never itself verified.
|
|
```
|
|
|
|
## Predictions
|
|
|
|
```
|
|
P1 let x: Int = "hello" compiles clean expect TRUE
|
|
P2 let s: String = 42 compiles clean expect TRUE
|
|
P3 the annotation drives dispatch, unverified expect TRUE
|
|
P4 same root cause as all three bugs found today expect TRUE
|
|
P5 checking literal-vs-annotation catches both expect TRUE
|
|
P6 zero false positives across the compiler's source expect TRUE
|
|
```
|
|
|
|
## Results — 6/6, and worse than a wrong answer
|
|
|
|
```
|
|
let x: Int = "hello"; x + 1 → 4343631981 a string POINTER used as an integer
|
|
let s: String = 42; println(s) → nothing address 42 dereferenced as a string
|
|
```
|
|
|
|
The first **leaks a raw memory address into program output**. The second is an
|
|
**arbitrary-read primitive** if that integer is ever attacker-influenced.
|
|
|
|
Verified: 6/6, zero false positives across the compiler's own source, fixpoint
|
|
ok, 105/105 native.
|
|
|
|
## Six Sigma
|
|
|
|
The emitter only **records** the mismatch; `tools/check/annotations.sh` decides —
|
|
consistent with every other check. Literals are checked because they are
|
|
unambiguous.
|
|
|
|
**Incomplete, stated not hidden:** only literals. `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`.
|