el-retired/docs/v1/experiments/evidence/cycles/17-annotations-are-never-checked/CLAIMS.md

CLAIMS — cycle 17, annotations are never checked

Source doc: docs/v1/experiments/cycles/17-annotations-are-never-checked.md

Pinned commits

role	sha	subject
parent / before-state	cb7289f06510c002b6ab7c5ca8c2bd182d8216bc	thread provenance end to end
experiment (system under test)	f1a7e224a77f020315a81f62d297b7ebff9b822d	verify the annotation against what it annotates
land (merge)	923f6a4bedc3b26b2a89b699b5623323d3d0c9f0	land annotation checking: the declared type is finally verified
current HEAD at re-run time	a0cc95e3db7b04b6e221f89e89352b0e6b15d5b7	instrument build log

Verdicts

#	claim	artifact	commit	verdict
A0	Status: verified on experiment/annotation-checking, not merged	0015-branch-status-not-merged-claim.out	—	DIVERGED
A1	P1: let x: Int = "hello" compiles clean	0003, 0005-pre-cc-h1-clean.out	cb7289f	REPRODUCED
A2	P2: let s: String = 42 compiles clean	0004, 0006-pre-cc-h2-clean.out	cb7289f	REPRODUCED
A3	let x: Int = "hello"; x + 1 → 4343631981, a string POINTER used as an integer	0007, 0009-pre-int-annotated-string-ten-runs.out	cb7289f	REPRODUCED as a class; NOT-REPRODUCIBLE as a literal (see below)
A4	let s: String = 42; println(s) → nothing, address 42 dereferenced as a string	0008-pre-run-string-annotated-int.out	cb7289f	REPRODUCED, and the record omits the exit code
A5	P3: the annotation drives dispatch, unverified	0003, 0004	cb7289f	REPRODUCED
A6	P5: checking literal-vs-annotation catches both	0010-post-annotation-checker-catches-both.out	f1a7e224	REPRODUCED
A7	P6: zero false positives across the compiler's own source	0011-post-annotation-query-harness.out	f1a7e224	REPRODUCED
A8	"Verified: 6/6"	0011 (harness carries 5 assertions)	f1a7e224	REPRODUCED as predictions P1–P6; the harness is 5/5
A9	fixpoint ok	0012-post-fixpoint.out	f1a7e224	REPRODUCED
A10	105/105 native	0013-post-native-suite.out	f1a7e224	REPRODUCED (exact)
A11	the emitter only records; tools/check/annotations.sh decides	0010	f1a7e224	REPRODUCED
A12	Incomplete, stated not hidden: only literals — let x: Int = some_string_fn() still passes	0014-post-incomplete-only-literals.out	f1a7e224	REPRODUCED
A13	P4: same root cause as all three bugs found that day	—	—	NOT-CAPTURED (interpretive)
A14	the defects at current HEAD	0016, 0017-head-run-string-annotated-int-TODAY.out	a0cc95e3	BOTH STILL LIVE

A0 — the status header is wrong: it was merged

branches named experiment/annotation-checking:  0
is f1a7e224 an ancestor of iteration-2?         YES-MERGED
merge commit:  923f6a4b land annotation checking: the declared type is finally verified

The doc opens "Status: verified on experiment/annotation-checking, not merged." The work is on iteration-2 and on main, landed by merge commit 923f6a4b, and no branch of that name exists any more. The status line is stale and the record should not be read as describing unmerged work.

A3 / A4 — the two hazards, at cb7289f

Fixtures fixtures/int_annotated_string.el and fixtures/string_annotated_int.el. Emitted C (0003, 0004):

el_val_t x = EL_STR("hello");        /* declared Int */
println(int_to_str((x + 1)));

el_val_t s = 42;                     /* declared String */
println(s);

cc reports 0 errors on both (0005, 0006). Then:

let x: Int = "hello"; x + 1 — exit 0, prints a raw address (0007):

4296429677

Ten consecutive runs of the same binary (0009):

4308013165  4369141869  4300738669  4308783213  4302131309
4378923117  4339404909  4310225005  4310487149  4307406957

claimed in the record: 4343631981

The value is a heap address and is different on every run. The record's 4343631981 cannot be reproduced as a literal and never could be — but it falls inside the observed distribution (4.30–4.38 × 10⁹), so it is a valid single sample rather than a wrong number. The claim that matters — a raw memory address leaks into program output — reproduces on every run.

let s: String = 42; println(s) — stdout 0 bytes, and exit 139 (0008). The record says "→ nothing". Nothing was printed, correctly; but the process died on SIGSEGV and the record does not say so. Address 42 was dereferenced as a char*, exactly as the analysis states — the missing detail is that the dereference faulted rather than returning garbage. This is the same omission as cycle 13's, and the same shape as measurement defect 4 in cycle 19: an exit code that was never read.

A14 — the standing finding: both defects are live at HEAD

Re-run today against the compiler built from a0cc95e3:

program	emitted	stdout	exit
let x: Int = "hello"; x + 1	unchanged	4296710433	0 (0016)
let s: String = 42; println(s)	unchanged	(empty)	139 (0017)

The checker landed; the compiler did not change. tools/check/annotations.sh is a post-hoc query over emitted relations — nothing in the emission path refuses the program, so a build that does not run the checker still produces the reinterpreting binary. The arbitrary-read primitive described in this cycle is unmitigated in the compiler at HEAD. That is the most consequential standing result in this set of nine.

A6 / A11 / A12 — the checker at f1a7e224

0010:

--- int_annotated_string ---
type error in main: 'x' is declared Int but assigned a String literal — the annotation drives dispatch, so the value will be reinterpreted rather than rejected
exit=1
--- string_annotated_int ---
type error in main: 's' is declared String but assigned a Int literal — the annotation drives dispatch, so the value will be reinterpreted rather than rejected
exit=1

0011 — the harness, 5 assertions, including the false-positive control over the compiler's own source:

  ok    Int annotated on a String literal is caught
  ok    and names the variable
  ok    String annotated on an Int literal is caught
  ok    correct annotations are clean
  ok    the compiler's own source is clean — no false positives

  5 assertions, 5 passed, 0 failed

0014 — the stated gap, confirmed: let x: Int = str_upper("abc") is a non-literal initialiser and the checker reports annotations: clean, exit 0. The incompleteness is exactly as declared.

Note on "6/6"

The doc's Results — 6/6 refers to predictions P1–P6, all of which are individually graded above. The committed harness (tests/integration/annotation_query.sh) carries 5 assertions and reports 5 assertions, 5 passed, 0 failed. There is no 6-assertion harness; the two numbers count different things and neither is wrong.

Provenance notes

All artifacts from dedicated worktrees /tmp/rerun-v1b-17-pre (cb7289f), /tmp/rerun-v1b-17-post (f1a7e224) and /tmp/rerun-v1b-head (a0cc95e3), capture.sh invoked by absolute path from inside each. No DIRTY-TREE flags in this cycle. Exit codes for 0007, 0008, 0016 and 0017 were captured directly by capture.sh, never through a pipe.