main
1023 Commits
| Author | SHA1 | Message | Date | |
|---|---|---|---|---|
 Brummel
|
c4bee767da |
docs: replace spec-validation parser fact with a project-local directive
The skills plugin no longer carries generic spec-validation machinery. Move the ail/ail-json/ll code-block validation rules into a standalone 'Spec & plan code-block validation' section that instructs specify, grounding-check, and planner directly — same effect, project-local. |
||
|
Brummel
|
2e8dfd8ff9 |
chore: move skills-plugin profile into CLAUDE.md project facts
The skills plugin dropped dev-cycle-profile.yml. Migrate this project's facts into CLAUDE.md under '## Skills plugin: project facts' and remove the profile file. |
||
|
Brummel
|
82d42f1b6b |
docs(design): mark project RETIRED (paused) at the ledger spine
Owner decision, 2026-06-03: pause AILang. Status banner at the top of design/INDEX.md (the sole addressable spine), so any reader — human or agent — sees the state before the framing. The differentiating thesis (a language purpose-built for LLM authorship makes LLM authors measurably more correct) did not find support in the project's own cross-model measurements (experiments/2026-05-12-cross-model-authoring/format-findings.md): - the optimal surface is model-relative — depth-annotated parens help a 3B-active model (6/8 -> 7/8) but HURT a frontier model (7/8 -> 6/8, Llama-3.1-405B hallucinates structure it does not need); - a compiler-in-the-loop is not an equaliser — agentic Qwen collapses into generation repetition before a single valid tree exists, so the oracle never engages; - for a frontier author, AILang is at best neutral vs. a familiar language given a scan-plus-iterate workflow, not an edge. The hallucination-robustness pillar (content-addressed symbols) was separately falsified and removed (#66). What survives, and why this is a pause not a deletion: the language is a sound small ML/effect design, and the measurement harness is the most durable output. main HEAD, git history, and the design ledger are untouched; reversible if a new framing makes the remaining work worthwhile. |
||
|
Brummel
|
fdff6cd613 |
experiment(cma): familiar-vs-unfamiliar — AILang is not harder for a frontier model given a scan (refs #68 #69 #70)
Follows up the SMA controls with the sharper question: does AILang cost a frontier model MORE than a language it knows from training (Rust)? Claude passing SMA is binary and cannot tell "effortless" from "barely". Measured with pass@1 over 6 samples of the same task in AILang (two-example few-shot) vs Rust, single-shot, fresh clueless agents, no tools, oracled afterward. Task 1 (Expr-evaluator — ADT + match + recursion, all in the few-shot): AILang 6/6 = Rust 6/6, no gap; all six AILang answers byte-identical. When every construct is in the few-shot, AILang is not harder. Task 2 (count-greater-than — needs a comparison, OUTSIDE the few-shot): AILang 0/6 vs Rust 6/6. But the logic was correct in all six; they fell on a guessed name (`>`, which AILang lacks). A vocabulary gap, not a reasoning gap — and the single-shot setup is unfair: in Rust Claude implicitly has its training plus the obvious ability to scan an unknown crate, which AILang was denied. The fair test (scan + compiler-loop, how Claude actually works): one Claude context, count-greater-than, given the prelude as a scanned library, then iterated on raw compiler output. Converges in two feedback rounds — gt+match-on-Bool -> (case true ..) -> match (compare h N) .. GT -> green. Decisive contrast: no-scan + terse errors -> Claude DIVERGES (invents gtPos, sub, non-existent pat-var); scan + diagnostic errors -> Claude CONVERGES. Same model; the difference is the discovery affordances, not the model. The 0/6 was the artefact of an unfair test, not an intrinsic AILang weakness — with the scan-plus-iterate workflow, the "language is harder" gap dissolves. Two genuine AILang defects the thread exposed, filed as issues: - #69: `ail builtins` is an incomplete API scan — it lists no comparison operator; gt/lt/le/ge/compare live in the prelude, which builtins does not surface. A model scanning the obvious discovery tool never finds half the comparison stdlib. - #70: `match` on Bool passes `ail check` but codegen rejects it (`match on non-ADT scrutinee (i1); MVP supports only ADTs`); with no `if`, branching on a Bool has no working surface — one must route through compare->Ordering. A check/codegen inconsistency under an "internal:" prefix. Answer, decomposed: cognitively AILang is not harder (the algorithm transfers); vocabulary-without-scan is harder but that is any unfamiliar language; with scan + iteration Claude drives AILang like a foreign crate; where it genuinely is harder is the two fixable tooling/compiler defects above. Caveat: n=6, two small tasks, one model, low sampling variance — exploratory, not a study. Evidence under experiments/2026-05-12-cross-model-authoring/familiar-vs-unfamiliar/. |
||
|
Brummel
|
9c833f65e4 |
experiment(cma): authoring-capability controls — L7 is a model ceiling, not a language ceiling (refs #68)
Every surface run in format-findings.md hit the same L7 (SMA) wall, read so far as a "genuine single-shot complexity ceiling". Three controls on the plain Form-A baseline (identical L7 prompt + ail oracle) pin down what that ceiling actually is. Control 1 — blind frontier model. Ran the full L0–L7 ladder through eight fresh, clueless Claude Opus 4.8 agents, each given verbatim the same prompt the IONOS models got, with no repo access, no compiler, no oracle (all returned tool_uses: 0). Oracled afterward exactly as the harness oracles Qwen/Llama: 8/8 green, including L7. So L7 is not a language ceiling — Form-A is authorable, SMA included, by a strong enough model. The eight modules are kept under clueless-agents/ (one m.ail per dir to satisfy module-name=stem) and re-check green; L7 also runs to the expected output. Claude generalised operators never shown in the few-shot (float +, a / absent from every example, float print). Control 2 — agentic Qwen (qwen_agentic.py). The fairer question: does the compiler-as-a-tool close the gap? Runs the real Claude-Code loop — model proposes a module, harness runs ail, the raw unedited compiler output goes back into the dialogue, up to 8 turns. Result: never solved. From turn 1 Qwen collapses into a repetition loop (~274× "(seq" until max_tokens, completion=1500 every turn); the module is truncated mid-cascade, the oracle returns the correct parse error every turn, and Qwen repeats. Tool access is not an equaliser — it lifts a model only when its reasoning already operates in the right neighbourhood. Also settles the context question: turn 1 collapses at prompt=729 (no accumulated history), so the failure is "can't", not "drowns in context". Raw doc qwen-agentic-sma.md (repetition cascades collapsed to keep the repo small; the collapse marker records the original run length). Control 3 — same SMA in Python (qwen_python_sma.py). Is the AILang failure about coding ability or the unfamiliar surface? Given the same task zero-shot in Python, Qwen returns a clean, idiomatic, correct sliding-window in 113 tokens (verified by inspection + hand-trace; the harness deliberately does not auto-execute LLM code). 113 tokens of correct Python vs a 1500-token collapse in AILang, same model and temperature. Synthesis: the L7 wall is neither an algorithm ceiling nor a "model is weak" ceiling. Qwen owns the algorithm (Python) and a frontier model owns the surface (Claude, blind, first try). Qwen's AILang collapse is specifically the unfamiliar, fully-parenthesised surface it never saw in training, and a compiler-in-the-loop does not rescue it. For an LLM-authored language: making Form-A compiler-driven does not lower the model bar — AILang either targets frontier-class authors, or its surface must drop the structure-tracking load enough for a small model to keep its place. Live IONOS limited to the consented Qwen agentic + Python runs. |
||
|
Brummel
|
ded28e2f75 |
experiment(cma): large-model control on Llama-3.1-405B — the format effect REVERSES (refs #68)
Ran the two core formats (plain Form-A, annotated parens) on Llama-3.1-405B (405B dense, ~135x Qwen3-Coder-Next's 3B active) to separate format-effect from small-model-effect. Scripts parametrized by PROBE_MODEL/PROBE_TAG (Qwen default preserved). Watch-out caught: Llama-3.1 on IONOS leaks its chat template (repeats "assistant", generates endless variants to max_tokens — an IONOS-documented quirk). First run read 0/8; that was the instrument. Fixed with a stop sequence and a balanced-first-module extractor. Result reverses the effect: Qwen3-Coder (3B): plain 6/8, annotated 7/8 Llama-405B (405B): plain 7/8, annotated 6/8 Llama solves L4 (Qwen's bracket wall) with plain parens, so that wall was a small-model effect. Annotated parens help the small model and hurt the large one (at L1 Llama invented a spurious (lit 3) wrapper under the annotated dialect). Both still fail L7 (SMA) — a genuine complexity ceiling. Synthesis: redundant explicit structure is a crutch for weak models. A frontier model tracks plain brackets fine and the unfamiliar scaffolding only adds noise. The right surface is model-relative. Synthesis in format-findings.md; raw ladders llama405-*.md. |
||
|
Brummel
|
ec6efe2cf2 |
docs(cma): add Qwen3-Coder-Next model context to format findings (refs #68)
Researched the model under test. Qwen3-Coder-Next is a 3B-activated MoE (80B total, Feb 2026) trained for AGENTIC coding (codebase + tools + RL on environment feedback), not one-shot generation of unfamiliar syntax — exactly our task, so we tested its weakest discipline. Its tool-calling strength is agentic environment interaction, not emitting deep structured AST JSON, consistent with the tool probe being worst. The format direction is likely general but the magnitude is model-specific; bigger active models on the same IONOS endpoint (Llama-3.1-405B, Llama-3.3-70B) were never tried and are the obvious next step to separate format-effect from small-model-effect. |
||
|
Brummel
|
8391209618 |
experiment(cma): tool-calling re-run at max_tokens=8000 — higher budget does not help, it degenerates (refs #68)
User noted the context window is ~128k and the bad-json failures looked like
truncation, so the max_tokens=2500 cap may have skewed the tool-calling test.
Fair point: the L4/L7 bad-json cases WERE truncation. Verified max_tokens=8000
is accepted, re-ran.
Result: 1/8, slightly worse, not better. The bad-json cases became check
failures (full AST now produced, but semantically wrong), confirming
truncation was a real but secondary factor. And the extra room exposed the
deeper problem: at L2 ("print 7", trivial) Qwen emitted 8000 tokens / ~20KB of
AST JSON and ran off the end — a repetition loop on a one-line program; at L7
it nested JSON deep enough to hit the parser's recursion limit. The verbose
AST-JSON surface is not budget-limited in a recoverable way — more room just
lets it loop or over-nest. Tool-calling stays at the bottom; the higher budget
makes it degenerate, even on trivial tasks. Updated format-findings.md.
|
||
|
Brummel
|
2b9a1083b5 |
experiment(cma): tool-calling / structured-AST tested — worst, and it confirms the rule (refs #68)
User asked whether Qwen's tool-calling could help. Verified tool-calling is
supported on IONOS (a dummy add tool returns a correct tool_call). Then tested
the promising version: submit the program as canonical AST JSON via a forced
submit_program tool — no surface syntax, no converter risk (the tool argument
IS the .ail.json, written and checked directly).
Result: 2/8, tied for worst. Two failure modes, both the model's: valid JSON
but wrong AST (arity etc.), and — at L4/L7 — bad-json: the tool arguments were
not valid JSON at all, because completion hit the 2500-token cap. AST JSON is
so verbose (every leaf is {"t":"var","name":"x"}) that a non-trivial program
overruns the budget and truncates. IONOS does not constrain decoding to the
schema, so the full structure burden stays on the model, and it is the heaviest
of all surfaces (braces+brackets+keys+quotes+commas+"t": per node).
This confirms the rule across six surfaces (annotated-parens 7/8 > plain parens
6/8 > M-expr 4-5/8 > indent 3/8 > YAML 2/8 = tool-AST 2/8): the discriminator is
redundant cue vs extra burden, not explicit vs implicit. Even tool-calling, the
model's home turf, loses because AST JSON maximises bookkeeping with no
redundancy. Lever for an LLM-authored language: redundant self-checking
structure (depth-annotated brackets). Synthesis in format-findings.md.
|
||
|
Brummel
|
7fe08139fb |
experiment(cma): M-expressions tested — middle of the pack; sharpens the finding (refs #68)
Tested McCarthy's head[a; b] notation (user request). Explicit structure (brackets + semicolons) in the function-call shape LLMs know cold. Result 4-5/8 (model variance over two runs): below plain parens, above bracket-free. Two watch-out catches kept it honest: (1) a trailing ';' before ']' — a normal trailing separator Qwen wrote — was rejected by my too-strict parser; fixed to tolerate it, round-trip preserved (without this M-expr looked unfairly bad). (2) L4 then failed with 43 '[' vs 42 ']', a genuine Qwen bracket imbalance (not truncation), the same depth-tracking failure as plain parens. Why worse than plain parens despite being explicit: swapping () for [] does nothing for the balance burden, and the semicolons ADD a second consistency requirement Qwen does not reliably meet. This sharpens the overall finding across five formats (annotated-parens 7/8 > plain parens 6/8 > M-expr 4-5/8 > indent 3/8 > YAML 2/8): the discriminator is not "explicit vs implicit" but REDUNDANT CUE vs EXTRA BURDEN. Depth-annotated parens carry nesting redundantly so the model can't lose its place (best); indentation moves tracking to an implicit channel (worst); M-expr semicolons add bookkeeping on top of bracket balance (middle). Lever for an LLM-authored language: redundant self-checking structure, not a lighter or more familiar surface that carries extra bookkeeping. Synthesis in format-findings.md. |
||
|
Brummel
|
525112e32e |
experiment(cma): bracket-free formats tested — they make Qwen WORSE, not better (refs #68)
Tested the user's bracket-free ideas (indent, YAML) against the annotated-paren result. Hypothesis was that removing the closing token removes the repetition tail. The opposite held. Instrument note (the watch-out paid off twice): a real YAML library auto-quotes and gives *,-,true special meaning, which collides with the AILang operators — Qwen wrote `- *` (multiply), a YAML alias marker, and the library crashed. That is a measurement bug, not a model failure. Rebuilt with a hand-written literal indent parser (atoms verbatim, no quoting); `- *` then round-trips fine. With the instrument fixed, the result is monotone across four formats: format 4 annotated parens 7/8 > plain Form-A parens 6/8 > yamlish indent 3/8 > YAML library 2/8. More explicit structure marking helps this model; less hurts. Qwen's weakness is structure-tracking at depth, and indentation makes it track the nesting itself — as error-prone as matching parens but without the redundant cue. The bracket-free surfaces fail EARLIER (L3/L4), before the L7 repetition ceiling is even reached. Lever for an LLM-authored language: redundant explicit structure (depth- annotated brackets), not a lighter surface. Synthesis in format-findings.md; raw ladders qwen-yaml.md (PyYAML, discarded) and qwen-yamlish.md (own parser). |
||
|
Brummel
|
682b935ba3 |
experiment(cma): annotated-paren format helps Qwen — cracks the bracket wall (refs #68)
Tests the user's hypothesis: if no human reads the surface, lift the paren- counting burden. Format 4 = annotated parens, every paren carries its nesting depth. Discipline: the format has no ail parser, so the converter is round-trip verified (parse-identity on known-good demos) before judging any model output. Result: it helps. Plain Form-A 6/8 -> format 4 7/8 on the same ablation ladder. The depth annotation cracks the bracket-balance wall that broke L4. At the hardest level (L7 SMA) Qwen produced perfectly balanced brackets through the deepest nesting AND correct SMA logic; the only remaining issue was a construct quirk (it treats seq as variadic, but AILang seq is binary). Proof the blocks were right: Qwen's exact logic with a manual binary-seq fix runs and emits the exact expected SMA output. Pushing further (format 4 + explicit seq-binary hint) fixed the seq nesting but L7 still failed on two MODEL-behaviour limits, not encoding: it simplified the logic, and fell into a closing-token repetition tail (hundreds of #0) ). The tail is paren-driven, so the natural next test is a bracket-free format (indent / keyword-delimited) with no closing token to loop on — a deliberate next step needing its own verified converter. Synthesis in format-findings.md. |
||
|
Brummel
|
da99ebaba8 |
experiment(cma): ablation finds WHY Qwen fails at Form-A — two distinct walls (refs #68)
Try-and-error ablation, minimal few-shot context, single shot per level, a ladder L0 (fn returns 42) to L7 (full SMA). Two ladders: base few-shot that only destructures, then one that also constructs (term-ctor). Finding: Qwen is NOT generally incapable. With minimal correct context it writes 6/8 tasks green, including ADTs, match, recursive fns, and Series use. The failures are two specific walls: - Wall 1 (cheap): unfamiliar constructs. It built lists with (app Cons ...) — calling the ctor like a function — because it had only seen match, never term-ctor. Adding ONE term-ctor example flipped L3 and L5 to green and removed the Cons error. The model generalises a construct from one example. - Wall 2 (hard): paren/nesting discipline at depth. The two that stay red (L4, L7) fail purely on bracketing, not knowledge. In L4 the recursive function is flawless; main closes a 4x-nested term-ctor value one paren early so the let body slides inside it — total paren count is BALANCED (43/43), the parens are just misplaced. Green/red tracks nesting depth, not feature. Examples do not fix it. This is the same weakness the full-SMA probes hit (run 2 had correct logic, died on brackets; run 3's long context tipped it into a seq-repetition loop). Takeaway: the bottleneck is the fully-parenthesised surface at depth, not the semantics. Natural next test: the .ail.json authoring form, which removes human paren-counting. Driver qwen_ablation.py; ladders in qwen-ablation-min.md and qwen-ablation-ctor.md; synthesis in qwen-ablation.md. |
||
|
Brummel
|
8b7e683cc9 |
experiment(cma): SMA probe run 3 — full grammar+spec+lib makes Qwen degenerate (refs #68)
Third run of the SMA authoring probe, this time with Qwen fully equipped: a distilled complete Form-A construct grammar (with explicit arity/paren rules), the mini-spec, and the verbatim Series library source. Hypothesis: the formal grammar clears the bracket failures of runs 1-2. It did the opposite. With ~80k prompt tokens the model degenerated into an identical pathological (seq (seq (seq ...))) tower every turn (321 open parens vs 10 close, byte-identical across all 6 turns, indentation exploding). Doubling max_tokens to confirm it was not mere truncation produced HTTP 413 (request too large) — more budget yields an even larger degenerate output, confirming degeneration. Verdict (n=1 model): Qwen3-Coder-Next wrote no working SMA in any of three configurations; more reference material made it WORSE, not better (the lean run 2 got the algorithm right, the fully-equipped run 3 looped); it never converged from ail-check feedback in any run; all failures are Form-A bracket-shape errors, never semantics. Driver + raw logs updated. |
||
|
Brummel
|
577bb6be43 |
experiment(cma): SMA authoring probe against Qwen3-Coder-Next (refs #68)
Probe whether a foreign model can write the Series SMA worked example in
AILang Form-A from the mini-spec + Series API alone. Two live runs, neither
reached green, but a clean progression:
- Run 1 (stock API doc): 6 byte-identical turns, blocked on (app new ...) —
Qwen treats the term head as an ordinary function.
- Run 2 (new clarified as a term head): clears that; ownership threading
comes out idiomatically right (nested let s = Series.push s v), but
S-expression bracketing breaks (push sees 4 args, not 2).
Cross-cutting: Qwen clears a hurdle only with per-quirk guidance and never
converges from the ail check diagnostic (same failure repeated all 6 turns
in both runs); the failures are Form-A bracket-shape errors, not semantic.
n=1 model, single session. Driver: sma_probe.py; raw logs sma-probe-run{1,2}.md.
Live IONOS run, with consent.
|
||
|
Brummel
|
29625e7262 |
feat(cma): revive cross-model harness corpus to current language (refs #68)
The cma authoring-form harness corpus had gone dead against the language as it evolved since May. The plan modelled it as merely schema-dead (missing param_modes/ret_mode); it was also drift-dead in the example BODIES. Fixed in place, with `ail check` + both test suites as the oracle: - Schema: param_modes/ret_mode completed on every fn type; existing borrow annotations preserved (data_with_match's borrow over List). - Symbol drift: `<`/`==` -> `lt`/`eq` (operator-routing); the removed `io/print_int` op -> print_str(int_to_str n) followed by a newline print, preserving the trailing newline the references' expected_stdout needs. - Ownership/ADT restructures: data_simple's reuse-as now wraps the source in a match arm (ctor must be statically visible); data_with_match's count_via_letrec + local go switched borrow->own (consume-while-borrowed under the tightened ownership analysis; head_or_zero still exercises borrow over the boxed List). - param_modes_all rewritten to own (Int) + borrow over a boxed ADT -- (borrow Int) is now a borrow-over-value error. - Two new author-facing examples (loop_sum: Loop/Recur; new_rawbuf: New) cover the Term variants that landed since May. - spec_completeness.rs: drop the deleted ParamMode::Implicit; cover Loop/Recur/New; allowlist the non-authorable Term::Intrinsic out. - spec.md section 4 rewritten to own/borrow (mandatory, no implicit) with the borrow-over-value rule; rendered/ regenerated. - mock_full_run fixture's t3 turn-2 program migrated so the harness score assertions hold; usage fields untouched. Both render/ and harness/ cargo test suites green in mock mode; no live IONOS call. Run the harness budget/reference tests with AIL_BIN pointing at target/debug/ail (ail is not on PATH in the test env). |
||
|
Brummel
|
72d2d9c806 |
test: prune duplicate tests, re-sight two blind coverage guards
Follow-up to a fan-out audit of the whole test suite (742 tests, 21
read-only assessors + synthesis). Two clusters of the audit were
actioned here; the #66 hashing-removal cohort it surfaced is left for
the #66 scope, and the RED-first doc-rot sweep is deferred.
§2 — true duplicates removed (each kept test is a strict superset or
identical fixture+assertions of the deleted one):
- ailang-check param_in_reject_message_names_allowed_set (kept the
_renders_allowed_set_in_ailang_syntax superset)
- ailang-check cross_module_pat_ctor_typedriven_resolves (kept ct2_;
shared cross_module_ws helper retained, 2 other callers)
- ailang-core mq1_qualified_instancedef_class_accepted (kept ct1_)
- ail e2e bool_to_str_emits_true_branch (kept the rc-stats superset)
- ail loop_recur_str adt-leg guard (the standalone heap pin owns it;
dropped the dangling header reference too)
- ailang-check over_strict_mode_silent_when_param_is_borrow (its
assertion is subsumed by explicit_fn_with_no_uses_is_clean; its own
doc claimed a "borrowing body" the Lit body never provided)
§4 — meta-guards that had gone partially blind re-sighted:
- spec_drift::spec_mentions_every_def_kind now pushes Class/Instance
exemplars and asserts their `(class `/`(instance` anchors; the
"wait for 22b.4" exclusion was stale (anchors shipped in
|
||
|
Brummel
|
426ce88d2a |
plan: cma-revival.1 cross-model harness corpus revival (refs #68)
Bite-sized plan for spec 0069. Six tasks: complete schema fields across the 13 examples + 4 references (own default, existing borrow preserved); rewrite param_modes_all + spec.md section 4 (own Int / borrow boxed-ADT, value/boxed rule); add loop_sum + new_rawbuf examples; spec_completeness variant coverage + Intrinsic allowlist; regenerate rendered + green render suite; migrate mock_full_run fixture + green harness suite. All verbatim .ail/.ail.json bodies parse-gate verified this session. The gate caught a real language drift the spec had to absorb: borrow over an unboxed value type (Int) is now a borrow-over-value error, so param_modes_all borrows over a boxed ADT instead. |
||
|
Brummel
|
74849160b7 |
spec: cross-model harness corpus revival (refs #68)
The cma authoring-form harness (experiments/2026-05-12-cross-model-authoring) is milestone-complete but its corpus went schema-dead: the implicit-cutover made param_modes/ret_mode mandatory, so today's ail check rejects 100% of the master examples + reference solutions and the renderer crashes on load. This spec revives the corpus to the current language and gets a mock run green. Scope (corpus-first, method-form-later per #68): minimal field-completion preserving existing modes; two new author-facing examples (loop/recur, new); spec.md section 4 rewritten to own/borrow with the borrow-over-value rule surfaced under the parse-gate; spec_completeness allowlists the non-authorable Term::Intrinsic out; mock fixture migrated so harness score assertions hold. No live IONOS call. Old specs 0017/0018 left intact as closed-milestone history. |
||
|
Brummel
|
54d8f0c660 |
docs(contracts): record the leak-class branch-param drop gate (#63)
Audit of the #63 leg-3 cycle flagged ledger drift: 0008-memory-model.md enumerated the Own-param drop gates as a closed set, but the leak-class branch-param fall-through drop now ships in codegen with no home in the contract. Per the honesty-rule (a contract describes the actual present state), reconcile it. Adds the fourth gate with its three soundness guards — disjointness from the fn-return dec (partition by aggregate: ==0 vs >=1), no-use-after-free (the use-after-consume rejection makes an aggregate>=1 param dead past the construct), and the heap-RC-ADT type precondition (field_drop_call != ailang_rc_dec; closure/static-Str/Var params are skipped to avoid a static-constant underflow). Notes that the pre-tail-call Own-param dec now shares the per-branch model (gate-source = MArm.consume) and updates the binder-name-injectivity precondition to cover the per-branch consume maps carried on MArm / MTerm::If and correlated by the traversal-order cursor. The accepted heap-capturing-closure-in-leak-class leak (soundness over completeness) is recorded in the backlog as Brummel/AILang#67. refs #63 |
||
|
Brummel
|
d72fe0c2e6 |
fix(codegen): drop branch-consume-split owned params (#63 leg 3)
The last leg of the #63 drop-soundness cluster: an (own ...) heap param consumed on one match-arm / if-branch but live on a sibling was never dropped on the live path, leaking one slab per call. This was the residual live=2 leak in series_sma that kept the series headline from being leak-clean. Root: the per-fn aggregate consume_count (the worst-case max over all branches from uniqueness::merge_states) was codegen's only consume signal, and every owned-param drop site gated on it. A param consumed on SOME branch makes the aggregate >= 1, so every site skipped it — including the branch where it stays live. match and if share this root (if is first-class MTerm::If, not desugared to match). Mechanism (spec 0068): - CAPTURE: uniqueness retains the per-branch consume snapshots it already computes per branch and discarded at the max merge — new BranchConsume + infer_module_with_cross_branches (the aggregate-only infer_module_with_cross now delegates and drops the channel). - CARRY: additive MArm.consume / MTerm::If.{then,else}_consume, attached by lower_to_mir via a traversal-order cursor (post-order pop, kind- and exhaustion-asserts make a desync a loud panic; neutral for const bodies which uniqueness does not walk). The AST carries no node id, so the correspondence is the structural pre-order both walks share — pinned by branch_consume_maps_attach_to_matching_arms. - GATE: emit_leakclass_branch_param_drops fires a fall-through drop only for the leak class (branch_consume==0 AND aggregate>=1), in match arms + both if branches; the pre-tail-call dec switches its gate source from the aggregate to per-arm. The fn-return dec and arm-close pattern-binder dec are UNCHANGED. Safety: - Double-free: the drop sites partition by aggregate (==0 -> existing fn-return/pre-tail-call; >=1 -> new per-branch). Disjoint, so no param is dropped twice — no fn-return disable, no tail-position analysis. - Use-after-free: the checker rejects use-after-consume, so an aggregate>=1 param is provably dead past the construct (path-terminal drop, tail position irrelevant). - Type eligibility (found by the full-suite gate during implement; spec 0068 refined): the new agg>=1 site is the FIRST drop site that can reach a STATIC closure-pair param (a top-level fn ref like inc in Either.either, consumed on one arm, live on the other) — a .rodata constant with no rc-header. field_drop_call routes Type::Fn / static-Str / Type::Var to the bare ailang_rc_dec, which underflowed on it. The helper now drops only params with a real per-type heap-ADT drop fn (field_drop_call != "ailang_rc_dec"). Sound (no underflow) and leak-correct (a static closure/Str allocates nothing). Witnessed green by std_either_demo / std_list_demo / poly_rec_capture_demo. Verification: full workspace suite green (116 binaries); both new leak pins (if + match) and series_sma_no_leak_pin green at live=0; legs 1/2 pins still green; INTERCEPTS<->(intrinsic) bijection intact; no Pattern::Lit reject path added. The leg-3 helper's type precondition was applied inline by the orchestrator (a narrowing guard clause in an already-reviewed Task-4 helper, full context loaded) after the implement-orchestrator correctly surfaced the spec gap rather than papering over the regression. This clears the series_sma leak tail; the series milestone (#61) close stays a separate deliberate step (its end-to-end milestone fieldtest). closes #63 |
||
|
Brummel
|
3447ac8039 |
plan: branch-consume-split drop soundness (#63 leg 3)
Five-task plan for spec 0068, decomposed RED-first:
1. RED — new if-branch fixture + pin, un-ignore the committed match pin.
2. CAPTURE — retain per-branch consume snapshots in uniqueness (new
BranchConsume + infer_module_with_cross_branches; old API delegates).
3. CARRY — additive MArm.consume / MTerm::If.{then,else}_consume,
attached by a traversal-order cursor in lower_to_mir (post-order pop,
exhaustion assert, neutral for const bodies) + lock-step test.
4. GATE — emit_leakclass_branch_param_drops helper + :823 gate-source
switch to per-arm; fall-through drops in match arms + if branches.
Disjoint-by-aggregate from the unchanged fn-return dec.
5. VERIFY — series_sma live=0 pin, full workspace suite, lockspair check.
All inlined code lifted from the live source bodies (uniqueness.rs,
lower_to_mir.rs, match_lower.rs, lib.rs) read this session, not from
memory. The one new surface fixture (if-branch) parse-checks clean; the
correspondence test reuses the existing match fixture via the
lower_to_mir_ty.rs elaborate_fixture/body helpers (verified present).
refs #63
|
||
|
Brummel
|
f7226cfba5 |
spec: branch-consume-split drop soundness (#63 leg 3)
Design spec for the last open leg of bug #63: an (own ...) heap param consumed on one branch of a match/if but live on a sibling branch is never dropped on the live branch, leaking one slab per call. This is the residual live=2 leak in series_sma that keeps the series milestone #61 from closing. The leak is general (match AND if, not Series-specific): the per-fn aggregate consume_count — the worst-case max over all branches from uniqueness::merge_states — is codegen's only consume signal, and every owned-param drop site gates on it. A param consumed on some branch makes the aggregate >= 1, so every drop site skips it, including the branch where it stays live. Approach A (chosen, scope = the whole branch-consume-split class): retain the per-branch consume snapshots the uniqueness walker already computes and currently discards at the max merge; carry them additively on MArm.consume and MTerm::If.{then,else}_consume (attached by lower_to_mir in structural traversal-order lock-step, since Term/Match/If/Arm carry no node id); codegen reads them at the branch drop sites. The check pass stays the sole consume authority (the mir.3a direction). Mechanism (refined during planning recon, simpler + provably safe than the first draft's fn-return-disable): the drop sites PARTITION by aggregate consume, so the per-branch map only ever ADDS drops for the leak class and never collides with an existing site: - fn-return dec (lib.rs) and arm-close pattern-binder dec: UNCHANGED. They keep firing for aggregate == 0 (live on every path). - pre-tail-call dec (match_lower.rs): gate source switches from the per-fn aggregate to the per-arm map. Identical decision for legs 1/2 (aggregate 0 => per-arm 0 on every arm); additionally drops a param live on this tail-call arm but consumed on a sibling. - NEW fall-through drop (match arms + if branches), before the br to the join: fires ONLY for the leak class — branch_consume == 0 AND aggregate >= 1. Double-free safety is disjointness by aggregate: the new drop needs aggregate >= 1, fn-return needs aggregate == 0 — mutually exclusive, so no fn-return disable and no tail-position analysis are needed. Use-after-free safety: the checker REJECTS using an owned value after it was consumed on any branch (use-after-consume), pinned green by use_after_consume_on_own_param_is_reported and harden_ownership_heap_double_consume_still_errors — so an aggregate>=1 param is provably never live past the construct, making the per-branch drop path-terminal regardless of tail position. grounding-check PASS (all load-bearing assumptions ratified by green tests / structural fact, incl. the disjointness and use-after-consume claims). Two RED repros carried: the already-committed ignored match pin and a new if-branch pin. refs #63 |
||
|
Brummel
|
d565ed87a3 |
feat(cli): resolve canonical type-scoped describe form
`ail describe <Type>.<op>` is the canonical form for a type-associated
operation (model 0007 §1), but resolve_describe_name only ever looked
up the left segment as a workspace module, so `Series.push` errored
`no module \`Series\`` even though `series.push` and bare `push`
resolved fine.
The dotted branch now falls through on a module miss: if no module is
named by the left segment, scan the workspace for the `Def::Type` named
by it and resolve `<op>` through that type's home module — returning the
identical `Def` the module-scoped and bare forms return (verified: same
hash d5278789db5f267a for `Series.push` / `series.push`). A literal
module still wins (precedence preserved); the bare-name and
ambiguous-name paths are untouched. The genuinely-unknown-prefix
diagnostic is tightened to `no module or type \`X\` in workspace`, and a
type-found-but-op-missing case reports `no def \`op\` in module \`home\`
(home of type \`Type\`)`.
Fix is CLI-local (crates/ail/src/main.rs); ailang-check untouched (a
direct ws.modules scan sufficed, no env.module_types needed). Full
workspace suite green (738); the RED pin describe_resolves_type_scoped_op
(
|
||
|
Brummel
|
8d58c8310b |
test(cli): RED pin for type-scoped describe resolution
`ail describe <Type>.<op>` is the canonical form (model 0007 §1) but currently errors `no module \`Series\` in workspace` because resolve_describe_name (crates/ail/src/main.rs) only looks up the left segment as a MODULE, never as a known TYPE. The module-scoped `series.push` and bare `push` forms already resolve fine. RED pin: describe_resolves_type_scoped_op asserts `ail describe --workspace examples/series_sma.ail Series.push` exits 0 and prints the `series.push` def. Fails today on the exit-0 assertion (feature absent), not on scaffolding. GREEN side follows. refs #64 |
||
|
Brummel
|
a35878154b |
docs(examples): correct rbx_1 ctor-field qualification note
The field-test note on the `Window` ctor claimed that bare
`(con RawBuf (con Float))` in a user ADT ctor field gives a
type-mismatch and that "the only form that checks is the
fully-qualified `raw_buf.RawBuf`". Verified against the current
tool (release at HEAD), that claim is false in every form I could
construct:
- bare `(con RawBuf a)` (type-variable element) in a non-kernel
module: checks ok
- bare `(con RawBuf (con Float))` (concrete element): checks ok
- a `(new RawBuf ...)` value stored via `term-ctor` into a
bare-declared field: checks ok
- the full rbx_1 program with the field switched to bare RawBuf:
checks ok
A ctor field is plain type position, and model 0007 §3
("kernel-module types are accessible bare in type position") already
covers it — the auto-import that makes bare `Series` work at a call
site equally makes bare `RawBuf` resolve in a user ctor field. The
only genuine constraint is that a ctor field carries no mode:
`(own (RawBuf a))` is a surface-parse-error, which model 0007 line
458 already documents.
So there is no qualification asymmetry to add to the ledger; the
ledger is correct as-is. The drift was in this checked-in comment
(a guessed rule recorded as fact), now rewritten to the verified
reality. The qualified spelling is kept in the code as the explicit
form. No ledger change.
closes #65
|
||
|
Brummel
|
a2808a6938 |
test(codegen): ignored RED pin for match-arm consume-split leak (#63 leg 3)
The third and final identified leg of #63: an owned heap param consumed on one match arm but live on a sibling fall-through arm is never dropped, because both codegen drop sites (the fn-return Own-param dec in lib.rs and the pre-tail-call dec in match_lower.rs) gate on the per-fn AGGREGATE consume_count. When the param is consumed on one arm (aggregate >= 1) but live on another, the gate skips the drop on the live arm too. This is the residual that keeps examples/series_sma.ail at live=2 after legs 1 and 2. Series-free minimal repro (a `Box` consumed on the `On` arm, live on the `Off` fall-through arm; main takes the `Off` path): `live=1` today. Committed #[ignore]: unlike legs 1 and 2, this is NOT a contained fix. The per-arm/per-path consume information is destroyed by the worst-case `max` merge in uniqueness.rs (`merge_states`) before MIR — MArm carries only {pat, body}, MirDef.consume is the per-fn aggregate — so codegen has no per-arm liveness to gate a fall-through drop on. Closing it needs a memory-model change (retain per-arm consume, surface it to codegen, emit the drop only on the live arm, never at the post-match join or the consuming arm — a live double-free hazard) and a fresh brainstorm cycle. The pin is committed ignored so the precise symptom and minimal repro are durable; un-ignore when the fix ships. The assertion is a correct symptom pin (live == 0); only the fix mechanism is undecided. refs #63 |
||
|
Brummel
|
e3a9065aa7 |
fix(codegen): drop owned values on let/seq-wrapped tail-call arms (#63 leg 2)
After leg 1, a tail call wrapped in a trailing `(let ...)` / `(seq ...)`
still leaked: `arm_body_is_tail_call` matched only a direct
App/Do{tail:true} arm body, so for an MTerm::Let/Seq body the gate was
false and both pre-tail-call drops (the scrutinee-husk shallow-dec and
the leg-1 owned-param dec) were skipped — while lower_term still
descended through the wrapper and emitted the inner call as musttail.
The fix replaces the one-level match with a local recursive
`tail_position_is_tail_call` that peels through a trailing Let-body /
Seq-rhs chain to its tail-position sub-term. This is a contained fix:
the predicate feeds only the two drop-emission gates, never the
musttail-emission decision (which is independent, in lower_term off
App{tail:true}), so widening it restores the drops without changing
which calls are tail calls. The let-bound value's scope-close drop is
gated on `!block_terminated` and stays correctly skipped, so the
forwarded let binding is not double-freed.
Verified: the leg-2 pin goes green (live=0, was live=4); the leg-1 pin
stays green; full `cargo test --workspace` 0 failures, no double-free /
underflow / IR-snapshot delta; lockstep pairs untouched.
examples/series_sma.ail drops from live=8 to live=2 with unchanged
stdout (3.0 / 5.33333 / 5.66667 / 5.33333).
Not yet leak-clean: the residual live=2 is a THIRD, distinct leg — an
(own) heap param consumed on one match arm but live on a sibling
base-case (non-tail fall-through) arm is not dropped there, because the
fn-return Own-param dec gates on the per-fn AGGREGATE consume_count
(>=1 here, from the recursive arm) rather than per-arm liveness. Routed
as its own RED-first bugfix.
refs #63
|
||
|
Brummel
|
2488d9d345 |
test(codegen): RED pin for let-wrapped tail-call leak (#63 leg 2)
After the leg-1 fix (
|
||
|
Brummel
|
68f500c4b0 |
fix(codegen): drop owned params on tail-call-terminated match arms (#63 leg 1)
An owned heap ADT param that a tail-recursive match arm neither forwards into the tail call nor consumes had no drop site: the fn-return Own-param dec in lib.rs is gated behind `!block_terminated` and so fires only on the fall-through `ret` path, while the per-arm drop in match_lower.rs handled only pattern binders. A `musttail call`-terminated arm therefore leaked one slab per recursion step (#63, leg 1). match_lower.rs now emits a pre-tail-call Own-param dec, gated exactly like the fn-return path: Rc strategy, `arm_body_is_tail_call`, ParamMode::Own, ptr-typed, and uniqueness `consume_count == 0`. For an Own param consume_count==0 also implies "not forwarded into the tail call" — a forwarded Own arg is walked Position::Consume and carries consume_count>=1 — so the gate cannot drop a param the callee took ownership of. The drop routes through the same per-type / partial-drop machinery (honouring moved_slots) as the fn-return path. The match scrutinee param is explicitly skipped: its ownership is already discharged by the pre-tail-call scrutinee-husk shallow-dec plus the moved-out field binders, so dropping it here would dec the same outer cell twice (a double-handling the first cut of this fix introduced and the quality review caught — the pin read live=0 but the IR showed two decs on the scrutinee cell). Verified: the committed RED pin is green (live=0, allocs==frees); full `cargo test --workspace` 0 failures; the fix introduces no under-free (loop_recur_heap_binder / loop_recur_str_binder / loop_str_recur_literal / rc_pin_recurse_implicit / lit_pat_ctor_tail_drop all stay live=0, no underflow to depth 5). No INTERCEPTS/(intrinsic) or pre_desugar_validation change; no IR snapshot refresh needed. Leg 1 only. Leg 2 — a `let`/`seq`-wrapped tail call makes the arm body an MTerm::Let so `arm_body_is_tail_call` is false, skipping both the husk-dec and this new param-dec — still leaks (examples/series_sma.ail stays live=8). It gets its own RED pin and fix next. refs #63 |
||
|
Brummel
|
1be6e49b4f |
test(codegen): RED pin for owned-param leak in tail-recursion (#63)
An owned heap ADT param threaded through a tail-recursive fn whose base-case arm neither forwards nor consumes it is never RC-dec'd, so it leaks one slab per recursion step. Series-free minimal repro (a plain `Box` ADT, no Series/RawBuf), so the pin guards the GENERAL memory-model invariant rather than the Series surface that first surfaced it (examples/series_sma.ail, live=8). The pin builds the fixture with --alloc=rc, runs it under AILANG_RC_STATS=1, and asserts live == 0 (allocs == frees). RED today: `allocs=6 frees=4 live=2`. The fixture passes the replacement ctor directly into the tail call (not let-bound) to isolate leg 1 — the owned-param drop omission — from the second, distinct leg the debugger found (a `let`-wrapped tail call also defeats the scrutinee-husk shallow-dec gate; that leg is what pushes box_ctrl to live=4 and series_sma to live=8, and gets its own pin once leg 1 is green). Cause (debugger, for the GREEN side): the fn-return Own-param dec in crates/ailang-codegen/src/lib.rs (~1444) is gated behind `!block_terminated`, so it fires only on the fall-through ret path; crates/ailang-codegen/src/match_lower.rs (~805) drops only pattern binders, never the fn's owned params. A tail-call-terminated match arm thus has no drop site for an owned param with consume_count==0 that is not forwarded into the tail call. refs #63 |
||
|
Brummel
|
3b3c8c4f07 |
fieldtest(series-step1): 5 examples, 5 findings (1 bug, 1 friction, 1 spec-gap)
Post-ship field test of the shipped `series` library extension as a downstream Form-A author working from the public surface only. Five fixtures under examples/fieldtest/ across the construction/auto-import, ring-buffer/financial-indexing, len/total_count bookkeeping, param-in error-quality, and operator-naming axes; spec at docs/specs/0067-fieldtest-series-step1.md. Wins (carry-on): auto-import works with no `(import series)`; the financial index (0 = newest) maps directly onto the bounded-buffer mental model and stays correct after multiple wraps; the param-in diagnostic for a disallowed element type names the type, the type-variable, the qualified type, and the allowed set. Findings routed: - [bug] An owned ADT threaded through tail-recursion whose base case neither returns nor consumes it is never dropped — a general drop-soundness leak (a plain `Box` control with no Series/RawBuf also leaks). Series surfaces it heavily on the whitepaper's headline streaming pattern, and the committed reference examples/series_sma.ail itself leaks (live=8). Minimal repro: series-step1_5 (live=4). - [friction] `ail describe ... Series.push` (the canonical type-scoped form) reports module-not-found; only `series.push` / bare `push` resolve, and no command lists a type's op set. - [spec_gap] referencing a kernel base type (`RawBuf`) from a user ADT ctor field requires full qualification (`raw_buf.RawBuf`) while bare `Series` works in type-position via auto-import — the asymmetry is undocumented. The fixtures that leak still produce correct output; the leak is a separate observable under AILANG_RC_STATS and an orthogonal, pre-existing bug, not a Series defect. refs #61 |
||
|
Brummel
|
73fbb240be |
docs(model): reconcile 0007 Series with the shipped step-1 reality
The `series` library extension shipped (
|
||
|
Brummel
|
35a9bc67b1 |
feat(series): ship the kernel-tier Series library extension (#61)
Series a is a bounded ring buffer with financial-style indexing (index 0 = newest), shipped as a PURE AILang library extension over RawBuf — zero Rust codegen, zero intercepts, zero (intrinsic) markers. It is the first kernel-tier module that depends on another kernel-tier module (raw_buf). This turns the committed SMA headline pin ( |
||
|
Brummel
|
6b7ee45e49 |
test(series): RED pin for the SMA worked example (#61 headline)
The headline acceptance of #61: the simple-moving-average worked example from design/models/0007-kernel-extensions.md must build via `ail build --alloc=rc`, run, and print the correct moving averages. Green ⇒ the kernel-tier `Series` library extension works end to end (ring-buffer push, financial-style indexing at index 0 = newest, count/total bookkeeping). The fixture is the 0007 worked example with two corrections applied, both verified against the live tool this session: - `>=` is not a surface symbol; the polymorphic Ord helper is `ge` (here on Int operands: total_count vs window size). - `print` on Float emits no trailing newline, so the four averages would concatenate into an unreadable blob. The emit branch now prints the average followed by `io/print_str "\n"`, so each average lands on its own line and the output is deterministic and assertable. (This legibility fix is also queued to be carried back into model 0007.) RED reason (right-for-the-right-reason): `ail check` rejects with [bare-cross-module-type-ref] on `Series` — the kernel-tier module does not exist yet. The fixture itself parses and is otherwise valid. Expected stdout was derived by probing the live %g float formatter independently (the SMA averages are 9/3, 16/3, 17/3, 16/3 over the stream 1,5,3,8,6,2 with window 3): `3.0\n5.33333\n5.66667\n5.33333`. GREEN side (the `series` kernel module + the five ops) is the next mini-mode iteration. |
||
|
Brummel
|
b11a6d9883 |
fix(mono): thread declared return type into mono synth re-entry
GREEN for the series-step-1 base-tier RED (
|
||
|
Brummel
|
e035eff8df |
test(series): RED pin for polymorphic RawBuf element-var forwarding
Base-tier enabling RED for the `series` milestone step 1 (#61). A polymorphic fn that allocates `(new RawBuf n)` with no explicit type-arg — element var solved purely from the enclosing ctor-field type `(con RawBuf a)`, never from a value argument — checks clean but fails `ail build --alloc=rc`: mono drops the check-phase solution for `a`, defaults it to Unit, and codegen mints the unregistered `RawBuf_new__Unit`. The fixture reads the element back via `RawBuf.get` so a wrong specialisation is observable (the program must print the stored `1.0`). This is the precondition the user picked (option B) so Series can ship as a pure AILang library extension over RawBuf while keeping the model-0007 `(new Series (con Float) 3)` caller surface. The #51 fix carried a WRITTEN `(con Int)` type-arg through mono; the variable-via-expected-type case is the untouched gap. RED: `ail check` exits 0; `ail build --alloc=rc` aborts with `RawBuf_new__Unit has no registered intercept`. GREEN target: builds, runs, prints `1.0`. The mono fix must not break the INTERCEPTS↔ (intrinsic) bijection or the Term::New↔pre_desugar_validation lockstep. refs #61 |
||
|
Brummel
|
c747cdf932 |
docs(ledger): fix two coherence gaps surfaced by the project skim
A read-only coherence skim across the project (the contract edits
themselves verified code-true, INDEX bijection exact, all pins green)
surfaced two pre-existing drifts — both predating this audit, neither
from the contract pass. Fixed in the same conservative style.
1. Model 0008 (ownership-totality) §1+§2 narrated the `Implicit`
leak in the PRESENT tense, contradicting the file's own STATUS
header (Implicit deleted via #55,
|
||
|
Brummel
|
4ec8f90b19 |
docs(contracts): finish the honesty pass (0003, 0008, 0013, 0017)
Third tranche, completing the honesty-rule sweep across the remaining
contracts. Same conservative bar: cut unbacked-verification claims,
change/deletion history, and forward-intent; keep present-state design
rationale.
- 0003: drop "sanitiser-verified" — no TSan/sanitiser test exists in
the tree, so the claim asserts a verification that does not happen.
The data-race-freedom property (argued from the non-atomic-but-never-
shared hot path + atomic-relaxed shared counter) stays.
- 0008: the `Type::Con.name` hash paragraph ("the tightening shifted
the hashes ... The new pins ... re-asserts the pre-tightening hashes")
-> present-state: which fixtures carry which hash shape and which test
pins each.
- 0013: drop "the former codegen-side fallback (at ..., and the
now-deleted `synth_with_extras`) is retracted" (deletion history; the
present fact is that codegen does not re-resolve, per the boundary);
"A future refactor that loosens any one of the four breaks ..." ->
present-tense statement that the four are load-bearing and each pinned.
- 0017: drop "a real cost surfaced by the `bench_closure_chain`
regression at the operator-routing-eq-ord milestone" (history) and
"the symmetric extensions are mechanical when the first such workload
appears" (forward-intent); keep the present-state allocation cost, the
pin, and the Int-only-asymmetry rationale.
All 18 contracts now reviewed against the code. Ledger pins green;
honesty sweep clean.
|
||
|
Brummel
|
eaa52ff64f |
docs(contracts): honesty-prose cleanup + ratifier integrity
Second tranche of the contracts-against-code audit. Two threads, both applied conservatively under the over-correction guards in docs_honesty_pin.rs (the self-labelled tiebreaker in 0008 and the Diverge-reserved anchor in 0010 are deliberate honest content and were left untouched; design rationale that explains a present-state design principle — semantic-locality, the reuse-as-wrapper reasons — was also preserved). Honesty-rule (0007): demote clear change/deletion narration to present tense. - 0008: drop "they were promoted from ... to ... Recorded here so"; strip the "Iter A"/"Iter B" iteration labels (the descriptive titles carry the meaning); drop "(no longer a carve-out)". - 0001: "were rewired to use ... was deleted at the same time" -> present tense. (The substance was already correct: `pretty.rs` holds only the diagnostic helpers; an audit agent had misread the line as "pretty.rs was deleted" — the file exists, the printer code does not.) - 0012: drop "Per the tail-call survey of existing fixtures" and "Migration of existing fixtures is partial" -> present-state description of which corpus fixtures carry the tail marker. Ratifier integrity: a contract that names a test which does not ratify it is itself a form of the dishonesty this ledger forbids. - 0014 named `bench/architect_sweeps.sh`, which sweeps honesty-anchors and ratifies none of the six verification mechanisms; and claim 5 cited `tests/expected/`, which never existed (git log empty). Point claim 5 at the real golden mechanism (`crates/ail/tests/snapshots/` via `ir_snapshot.rs`) and the footer at each mechanism's actual test. - 0015's four constraints are guaranteed by absence (no thunk/`ref`/ `IORef` node, non-recursive `let`); the named uniqueness in-source tests only count RC consumes, never the constraints. State the by-construction guarantee and point the ratifier at `ast.rs` (the single source of truth for which nodes exist). - INDEX ratifying-test column updated for both to match. All ledger pins green (docs_honesty_pin, design_index_pin incl. every_contract_names_a_resolvable_ratifying_test, effect_doc_honesty_pin, carve_out_inventory); architect honesty sweep clean. Deferred, recommend-only: 0016-method-dispatch carries no invariant absent from 0013 (merge candidate), but a contract-file merge touches INDEX, the retired-counter convention, and cross-refs — a structural call left for explicit direction. Minor history phrasing in 0008's Type::Con.name hash-shift paragraph (§"FnDef.suppress") also left. |
||
|
Brummel
|
56e076b2ca |
docs(contracts): make 0012 tail-context list code-exhaustive
The §Typecheck enumeration in 0012-tail-calls.md presented the
tail-position rule as exhaustive ("The flag is `false` for: ...") but
omitted `Term::If` entirely — even though `verify_tail_positions`
propagates `is_tail` into both `If` branches (ailang-check/src/lib.rs),
and 0012's own motivating example (`if n == 0 then () else loop(n-1)`)
relies on the `else` branch being a tail position.
Restate the rule by principle (a sub-term is in tail position iff it is
the value of the whole expression) and enumerate the actual checker's
arms: `If` branches, `Match` arms, `Seq` right, `Let`/`LetRec`
in-clause, `Lam` body, and the identity/`Loop` propagators; every
argument position (incl. `If` condition, `Recur`/`New` args) is
non-tail. Matches the present `verify_tail_positions` walker.
|
||
|
Brummel
|
625fe849be |
docs(contracts): reconcile contracts + honesty-pin with shipped reality
First tranche of a contracts-against-code audit (the inverse of the
usual direction: testing the ledger's claims against the code). Each
fix here is a verified factual divergence between a contract and the
code; the direction of the fix follows which side actually drifted.
Code drifted from the stated goal -> fix the code:
- 0014's claim 6 ("`cargo doc --no-deps` runs warning-free") was the
design goal; reality had 6 warnings. Demote the offending intra-doc
links to plain code spans so the docs match the goal:
- ailang-core: `[`load_workspace`]` cannot resolve from core (the
fn lives in ailang-surface, which core may not depend on) — three
sites in workspace.rs.
- ailang-check: three public-item docs linked the `pub(crate)`
helpers `qualify_local_types` / `qualify_workspace_types`.
`cargo doc --no-deps --workspace` is now warning-free.
Contract stale, code legitimately advanced -> fix the contract:
- 0011 stated `float_to_str` "codegen is reserved and not yet
shipped". It is shipped: lowers to `@ailang_float_to_str(double)`,
green under the codegen `float_to_str_no_longer_errors_internal`
unit test and the e2e `float_to_str_smoke`. The docs_honesty_pin
anchor that protected the stale "reserved" wording moved in lockstep
to assert the present-tense lowering instead — the pin had been
guarding a claim the code already falsified.
- 0013 named the diagnostic `ConstraintReferencesUnboundTypeVar`; the
variant is `UnboundConstraintTypeVar` (workspace.rs), and its scope
is a class-method signature whose constraint mentions a tyvar bound
neither by the method's `forall` nor by the class `param`.
- 0017 called the primitive Eq/Ord bodies "placeholder lambdas"; they
carry the `(intrinsic)` marker — the lockstep partner to the
INTERCEPTS registry, not a placeholder.
- 0009 said "seven" `.ail.json` carve-outs and described the inventory
test as pinning seven; the test pins twelve (7 subject-matter + 4
recur + 1 loop-binder, per carve_out_inventory.rs).
Verified separately: 0001's "pretty-printer code in pretty.rs was
deleted, leaving only diagnostic helpers" is factually correct (an
audit agent misread it as "pretty.rs was deleted"); its only issue is
history phrasing, deferred to the honesty-prose tranche.
Deferred to later tranches: honesty-rule prose (history/rationale that
is not a protected honest-reserved/tiebreaker anchor), stale/mislinked
ratifying-tests (0014's `architect_sweeps.sh`, 0015's uniqueness
in-source tests), 0014's never-existent `tests/expected/`, 0012's
non-exhaustive tail-context list, and the 0016<->0013 redundancy.
|
||
|
Brummel
|
69e738d6e6 |
docs(design): close the sma_demo module paren in models/0007 (refs #7)
Verifying the previous commit's surface-syntax fix with `ail parse` (the whitepaper's code blocks are unfenced/untagged, so no spec validation ever parsed them) surfaced a fourth, pre-existing drift the line-by-line signature fix had missed: the §sma_demo `(module …)` was short one closing paren and never balanced — it could not have parsed as written, independent of the mode/con-wrapper drift. Added the missing `)`. With it, both worked-example modules now parse clean: - §sma_demo → `ail parse` ok (4.4 KB JSON) - §series → `ail parse` ok `ail parse` resolves no names, so this verifies surface syntax only, which is the intended scope. The §series listing still leans on kernel-tier polymorphism that `ail check` rejects today; its full compile-verification stays with the pending Series milestone per spec 0059, exactly as the prior commit stated. |
||
|
Brummel
|
5e5b0e1484 |
docs(design): bring models/0007 worked examples onto the shipped surface (refs #7)
The raw-buf milestone fieldtest (spec 0066) surfaced a spec_gap: the kernel-extensions whitepaper teaches RawBuf surface syntax through its §Series worked examples, but those examples were written before three downstream surface decisions landed and never caught up — so an LLM author who pattern-matches them writes programs that fail to parse. Three drift classes, all verified against the HEAD parser: - fn-type slots carried no mode. Post-#55 every value slot needs an explicit `(own …)` / `(borrow …)` (the bare_slot_reject contract). - `(new RawBuf lookback)` omitted the element type. Post-#51 the form is `(new RawBuf (con T) <size>)`; the whitepaper's own spec line (§"allocates") already documents `(new RawBuf (con T) (size: Int))`. - parametrised kernel types were spelled bare `(Series a)` / `(Series (con Float))`, contradicting the whitepaper's OWN prose (`(con Series (con Float))` at the §mechanisms section). Wrapped in `(con …)` to match the documented canonical form. - `len` / `total_count` carried no `(type …)` at all; completed from the obvious neighbour signatures (`borrow (con Series a) → own Int`). Scope is deliberately surface-syntax only. The §Series listing stays a forward-looking sketch of the still-pending library-extension milestone (STATUS header; "not in today's AILang" at the sma_demo block). Its full cross-module compile-verification remains assigned to the Series milestone per spec 0059 — these edits do not claim it compiles today (it leans on kernel-tier polymorphism that is not yet authorable), only that its surface syntax now matches what RawBuf authors must actually write. |
||
|
Brummel
|
9545257333 |
fieldtest: raw-buf milestone — 4 examples, 3 findings (refs #7)
Milestone-close fieldtest for the raw-buf milestone, milestone-scope
variant: four end-to-end scenarios derived top-down from the milestone
promise (construct via (new RawBuf <elem> <size>), fill/read via
set/get, size-only buffers, element variety across {Int,Float,Bool},
forbidden-element reject at check, buffer threading under own/borrow).
Result confirms the milestone-promise hypothesis — RawBuf is clean
end to end, zero bugs:
- mrb_1 Int fill/read loop: check ok, run + native build both print 70
- mrb_2 Float own->own threading + borrow read: prints 3.5
- mrb_3 size-only Bool buffer (#51 legitimate-but-unobserved case): prints 8
- mrb_4 Unit element: rejected at check with a precise
param-not-in-restricted-set diagnostic; build stops at the same
error, codegen never reached (the #51 fix)
Two [working] findings (carry-on) and one [spec_gap]: the
kernel-extensions whitepaper (design/models/0007) teaches bare-mode
fn-type slots that the post-#55 parser rejects. Verified and triaged
separately; the ledger fix follows in its own commit.
|
||
|
Brummel
|
2ca483dbfd |
docs(design): reconcile models 0008/0009 STATUS with the shipped #55 cutover
The 0008 totality core shipped via #55 (spec 0062,
|
||
|
Brummel
|
d8d148224c |
refactor(test): slice the bytes, not the str (sliced_string_as_bytes)
`line[..s].as_bytes()` re-walks UTF-8 boundaries to slice the &str first; `&line.as_bytes()[..s]` slices the byte view directly. `s` is a byte offset from `str::find`, so the two are equivalent here. Clears the last clippy warning in the workspace. |
||
|
Brummel
|
1be2c1f145 |
docs: fix doc_lazy_continuation across the workspace
Eighteen markdown list items in module- and item-doc comments had continuation lines that were not indented to align under the item text, so rustdoc rendered them as separate paragraphs and broke the list. Corrected the indentation (and, at two sites where a general wrap-up sentence followed a sublist, separated it with a blank doc line so it does not mis-attach to the last item). Doc whitespace only; no prose reworded, no code changed. Workspace clippy is now warning-clean. |
||
|
Brummel
|
b5799640f8 |
refactor(core): demote orphaned doc comments in the workspace test module
Two `///` blocks in the in-source test module described tests that were relocated to tests/workspace_pin.rs, leaving doc comments attached to nothing (clippy: empty-lines-after-doc). Converted them to plain `//` notes, matching the already-`//` relocation marker next to them. |
||
|
Brummel
|
5cd2a964e3 |
refactor(surface): collapse the optional-clause duplicate-check onto set_once
Every definition parser repeated the same triplet per optional
attribute — `if slot.is_some() { return duplicate_clause_err(...) }
slot = Some(parse_X()?)`. Factor the check-then-assign into one
helper, set_once(slot, production, subject, clause, value), invoked as
`set_once(&mut doc, prod, subj, "doc", self.parse_doc()?)?`. The match
on peek_head_ident() and the per-clause production/subject/clause
arguments are unchanged, so every duplicate-clause error string stays
byte-identical (the *_rejects_duplicate_*_clause tests pin them).
The helper checks is_some() before the parser runs, so a duplicate
clause still reports at the offending clause's position. Arms that do
more than a plain check+assign (the bool flags drop-iterative/kernel,
the param-in nested map, the suppress/method Vec pushes) are left
inline.
|