Record verified retained entry producer gates and independent evidence

2026-09-24 19:42:48 -07:00
parent 7a02333c4a
commit 154bcaf04d
14 changed files with 920 additions and 3 deletions
@@ -687,3 +687,23 @@ general comparison. Compiler prologue observations and existing stack controls
 bound evidence only; this adds no universal heap or stack guarantee.
 Entry/metadata growth timing and the remaining scratch inventory require their
 own explicit decision before actual emitted-output acceptance can be enabled.
+
+## 2026-09-25 — strengthen the existing retained-entry metric at named producers
+
+The [entry producer contract](analysis-entry-producer-contract-20260925.md)
+preserves U's declared grammar events and the conservative M inventory. A new
+explicit route checks C+U+M before selected growth; old routes retain their
+timing. Prefer grammar scalar counts plus a prepaid projector quota to another
+unmetered AST-counting frontier. Seven-slot declaration envelopes already include
+synthetic bodies; actual nested fields/values contribute separately. Quota
+consumption neither recharges nor refunds M, and independent lengths/metadata
+must reconcile. No saturating correction may create a successful witness.
+
+[Windows evidence](experiments/analysis-entry-producer-20260925/README.md)
+preserves both precompile latch fixes, the syntax-cap versus counting-scratch
+evaluator correction and the initial test-only Debug-bound compile failure.
+All six new tests pass with unchanged inherited dispositions and strict Clippy.
+Additional scalar state changes compiler frames, so old stack controls and
+actual prologues remain evidence requirements; a logical slot is not a native
+stack byte. Remaining independently bounded parser scratch requires an explicit
+scope decision, not an inferred universal heap-metering requirement.