Files
AILang/crates/ailang-core/tests/spec_drift.rs
T
Brummel 76b21c00eb feat(lang): eliminate the Implicit ownership default — totality + the drop-soundness it demasks (#55)
Deletes `ParamMode::Implicit`. `ParamMode` is now `{Own, Borrow}`:
every fn-type slot on every signature carries an explicit `own` or
`borrow`, no defaulted position survives anywhere (model 0008 §2,
spec 0062). The parser rejects a bare fn-type slot; `borrow-return`
and `borrow-over-value` reject at the signature; the corpus is
migrated to minimal-ownership modes (consumed ⇒ own, read-only-heap
⇒ borrow, value ⇒ trivial-own). The documented `Implicit`-ret-mode
leak is fixed: an owned heap return now drops exactly once (live=0,
acceptance criterion 5).

This was the easy half. Removing the default ACTIVATED a family of
drop paths that `Implicit` had silently skipped — the pre-cutover
language was leaking (and in places mis-dropping) here rather than
crashing, because an Implicit scrutinee turned the drop off. Making
the modes explicit (Own) turned those paths on and exposed two
latent-bug clusters, all fixed RED-first as part of this cutover:

Drop-soundness family (four legs):
  A. lit-sub-pattern double-free — the desugar re-matched the same
     owned scrutinee in the lit fall-through; fixed by grouping
     consecutive same-ctor arms into one match (bind fields once),
     in ailang-core desugar.
  B. Cons-husk leak on non-tail arm bodies — the lit-sub-pattern
     desugar rebound the owned scrutinee via `Let $mp = xs`, which
     bumped consume_count and suppressed the existing fn-return
     partial_drop. Fixed by not rebinding a bare-Var scrutinee
     (one husk-freeing mechanism, not two).
  C. polymorphic `drop_<T>` rc_dec'd monomorphised value fields —
     the per-ADT drop fn was emitted once from the polymorphic
     TypeDef, defaulting type-var fields to ptr and rc_dec'ing
     inline Ints (segfault). Fixed with per-monomorph drop
     functions (new ailang-codegen::dropmono): the drop set is
     collected from the lowered MIR, value-type fields are skipped,
     heap fields still freed once; monomorphic-concrete ADTs keep
     their byte-identical un-suffixed drop symbol.
  D. static Str literal passed to an `(own Str)` param — the
     literal lowers to a header-less rodata constant; the callee's
     now-active rc_dec read its length field as a refcount and
     freed a static address (segfault). Fixed with the missing
     fourth StrRep::Static→Heap promotion in lower_to_mir's App arm,
     gated on Own mode (borrow args stay static, no regression).

over-strict-mode lint over-fired: it suggested `(borrow V)` for
value-typed params (which `borrow-over-value` rejects — own is the
only legal mode there) and fired on `(intrinsic)` bodies (whose
consumption the linearity walk cannot observe). Tightened to skip
both; contract 0008 updated to the narrowed firing scope.

Irreversible step — canonical-form hash reset (model 0008 §6,
acceptance criterion 6). Every signature now carries explicit modes,
so the hashable canonical JSON changed for every module. RATIFY:
the corpus-wide hash-pin reset (hash_pin, prelude_module_hash_pin,
mono_hash_stability, eq_ord_e2e, embed_export_hash_stable, the
ct4/iter*/loop_recur schema-extension pins) and the list ir_snapshot
golden were regenerated once, deliberately, as the intended one-time
consequence of removing the mode elision from the canonical form —
not a regression. Each regenerated hash verified deterministic across
two runs.

Also fixes a pre-existing latent failure surfaced by the verification
gate, unrelated to this cutover: the `every_contract_names_a_resolvable_
ratifying_test` resolver (design_index_pin) could not resolve the
" + " dual-link ratifying-test form (`uniqueness.rs + linearity.rs`)
that the #57 audit-close (dfdc65f) introduced — it shipped red on that
commit. Resolver taught the dual-link form, mirroring its sibling.

Verification: cargo test --workspace = 731 passed, 0 failed (twice,
stable); e2e 102 passed, no binary exits non-zero (corpus crash-free);
grep-clean for Implicit/fn_implicit/mode_eq across crates; every drop
fix confirmed via emitted IR + AILANG_RC_STATS balance on the head==K,
head!=K, and Nil paths. Three BLOCKEDs en route (the unsound first
husk-dec attempt, the over-strict derivation premise, the leg-B fix
direction) were each treated as a real design/spec gap and rediagnosed,
not patched over.

Supersedes #54 (return-position-only leak patch). Precondition #57
(linearity hardening) was already met. Spec docs/specs/0062, plan
docs/plans/0121.

closes #55
2026-06-02 00:03:46 +02:00

357 lines
12 KiB
Rust

//! Drift detection between the AST and `specs/form_a.md`.
//!
//! The spec is hand-curated, but it cannot silently fall behind the
//! language. Every AST enum (`Term`, `Pattern`, `Type`, `Def`, `Literal`,
//! `ParamMode`) discriminates on a `#[serde(rename = "...")]` tag.
//! These tests construct a sample of every variant, then check that the
//! corresponding tag string (or its parenthesised Form-A keyword) appears
//! in the spec.
//!
//! The exhaustive `match` is the load-bearing piece: adding a new variant
//! without a spec entry fails compilation here long before the test runs.
//! Once the variant is matched, the test asserts the spec mentions it.
use std::collections::BTreeMap;
use ailang_core::ast::{
ConstDef, Ctor, Def, FnDef, Literal, NewArg, Pattern, Suppress, Term, Type, TypeDef,
};
use ailang_core::FORM_A_SPEC;
/// Every `Term` variant must be reachable from the spec. The Form-A
/// keyword for each variant is what the spec is supposed to teach an
/// LLM; if it is missing here, the LLM cannot produce that term.
#[test]
fn spec_mentions_every_term_variant() {
let exemplars: Vec<(&str, Term)> = vec![
("(lit-unit", Term::Lit { lit: Literal::Unit }),
// The Var form has no parenthesised keyword (a bare ident is a
// var-ref). The spec calls it out under "Atom forms"; we look for
// that anchor.
("Atom forms", Term::Var { name: "x".into() }),
(
"(app",
Term::App {
callee: Box::new(Term::Var { name: "f".into() }),
args: vec![Term::Var { name: "x".into() }],
tail: false,
},
),
(
"(let ",
Term::Let {
name: "x".into(),
value: Box::new(Term::Lit { lit: Literal::Int { value: 1 } }),
body: Box::new(Term::Var { name: "x".into() }),
},
),
(
"(let-rec",
Term::LetRec {
name: "f".into(),
ty: Type::fn_owned(vec![], Type::int(), vec![]),
params: vec![],
body: Box::new(Term::Lit { lit: Literal::Int { value: 0 } }),
in_term: Box::new(Term::Var { name: "f".into() }),
},
),
(
"(if",
Term::If {
cond: Box::new(Term::Lit { lit: Literal::Bool { value: true } }),
then: Box::new(Term::Lit { lit: Literal::Int { value: 1 } }),
else_: Box::new(Term::Lit { lit: Literal::Int { value: 0 } }),
},
),
(
"(do ",
Term::Do {
op: "io/print_str".into(),
args: vec![],
tail: false,
},
),
(
"(term-ctor",
Term::Ctor {
type_name: "List".into(),
ctor: "Nil".into(),
args: vec![],
},
),
(
"(match",
Term::Match {
scrutinee: Box::new(Term::Var { name: "x".into() }),
arms: vec![],
},
),
(
"(lam",
Term::Lam {
params: vec![],
param_tys: vec![],
ret_ty: Box::new(Type::int()),
effects: vec![],
body: Box::new(Term::Lit { lit: Literal::Int { value: 0 } }),
},
),
(
"(seq",
Term::Seq {
lhs: Box::new(Term::Var { name: "a".into() }),
rhs: Box::new(Term::Var { name: "b".into() }),
},
),
(
"(clone",
Term::Clone {
value: Box::new(Term::Var { name: "x".into() }),
},
),
(
"(reuse-as",
Term::ReuseAs {
source: Box::new(Term::Var { name: "x".into() }),
body: Box::new(Term::Var { name: "y".into() }),
},
),
(
"(loop",
Term::Loop {
binders: Vec::new(),
body: Box::new(Term::Lit { lit: Literal::Unit }),
},
),
(
"(recur",
Term::Recur { args: vec![] },
),
(
"(new",
Term::New {
type_name: "T".into(),
args: vec![NewArg::Value(Term::Lit {
lit: Literal::Int { value: 0 },
})],
},
),
("(intrinsic", Term::Intrinsic),
];
for (anchor, term) in exemplars {
// Force the exhaustive match: the body is just a tag string that
// we will not actually use, but the compiler will refuse to
// compile this file once a new Term variant is added without a
// matching arm.
let _: &'static str = match term {
Term::Lit { .. } => "lit",
Term::Var { .. } => "var",
Term::App { .. } => "app",
Term::Let { .. } => "let",
Term::LetRec { .. } => "letrec",
Term::If { .. } => "if",
Term::Do { .. } => "do",
Term::Ctor { .. } => "ctor",
Term::Match { .. } => "match",
Term::Lam { .. } => "lam",
Term::Seq { .. } => "seq",
Term::Clone { .. } => "clone",
Term::ReuseAs { .. } => "reuse-as",
Term::Loop { .. } => "loop",
Term::Recur { .. } => "recur",
Term::New { .. } => "new",
Term::Intrinsic => "intrinsic",
};
assert!(
FORM_A_SPEC.contains(anchor),
"spec is missing anchor `{anchor}` for a Term variant — \
update crates/ailang-core/specs/form_a.md"
);
}
}
/// Every `Pattern` variant must appear in the spec.
#[test]
fn spec_mentions_every_pattern_variant() {
let exemplars: Vec<(&str, Pattern)> = vec![
("_", Pattern::Wild),
// pat-var is again the bare-ident form. The spec discusses it
// under "Patterns". Use the heading as the anchor.
("## Patterns", Pattern::Var { name: "x".into() }),
("(pat-lit", Pattern::Lit { lit: Literal::Int { value: 0 } }),
(
"(pat-ctor",
Pattern::Ctor { ctor: "Nil".into(), fields: vec![] },
),
];
for (anchor, pat) in exemplars {
let _: &'static str = match pat {
Pattern::Wild => "wild",
Pattern::Var { .. } => "var",
Pattern::Lit { .. } => "lit",
Pattern::Ctor { .. } => "ctor",
};
assert!(
FORM_A_SPEC.contains(anchor),
"spec is missing anchor `{anchor}` for a Pattern variant"
);
}
}
/// Every `Type` variant must appear in the spec.
#[test]
fn spec_mentions_every_type_variant() {
let exemplars: Vec<(&str, Type)> = vec![
("(con ", Type::int()),
(
"(fn-type",
Type::fn_owned(vec![], Type::unit(), vec![]),
),
(
"TYVAR-NAME",
Type::Var { name: "a".into() },
),
(
"(forall",
Type::Forall {
vars: vec!["a".into()],
constraints: vec![],
body: Box::new(Type::Var { name: "a".into() }),
},
),
];
for (anchor, ty) in exemplars {
let _: &'static str = match ty {
Type::Con { .. } => "con",
Type::Fn { .. } => "fn",
Type::Var { .. } => "var",
Type::Forall { .. } => "forall",
};
assert!(
FORM_A_SPEC.contains(anchor),
"spec is missing anchor `{anchor}` for a Type variant"
);
}
}
/// Every `Literal` variant must appear in the spec.
#[test]
fn spec_mentions_every_literal_variant() {
// Anchors describe how the literal renders in Form-A.
let exemplars: Vec<(&str, Literal)> = vec![
("`INT`", Literal::Int { value: 0 }),
("`true`, `false`", Literal::Bool { value: true }),
("`STRING`", Literal::Str { value: "x".into() }),
("(lit-unit)", Literal::Unit),
("`FLOAT`", Literal::Float { bits: 0 }),
];
for (anchor, lit) in exemplars {
let _: &'static str = match lit {
Literal::Int { .. } => "int",
Literal::Bool { .. } => "bool",
Literal::Str { .. } => "str",
Literal::Unit => "unit",
Literal::Float { .. } => "float",
};
assert!(
FORM_A_SPEC.contains(anchor),
"spec is missing anchor `{anchor}` for a Literal variant"
);
}
}
/// Every `Def` kind must appear in the spec.
#[test]
fn spec_mentions_every_def_kind() {
let fn_def = FnDef {
name: "f".into(),
doc: None,
suppress: vec![],
ty: Type::fn_owned(vec![], Type::int(), vec![]),
params: vec![],
body: Term::Lit { lit: Literal::Int { value: 0 } },
export: None,
};
let const_def = ConstDef {
name: "k".into(),
doc: None,
ty: Type::int(),
value: Term::Lit { lit: Literal::Int { value: 0 } },
};
let type_def = TypeDef {
name: "T".into(),
doc: None,
vars: vec![],
ctors: vec![Ctor {
name: "C".into(),
fields: vec![],
}],
drop_iterative: false,
param_in: BTreeMap::new(),
};
let exemplars: Vec<(&str, Def)> = vec![
("(fn ", Def::Fn(fn_def)),
("(const ", Def::Const(const_def)),
("(data ", Def::Type(type_def)),
];
for (anchor, def) in exemplars {
let _: &'static str = match def {
Def::Fn(_) => "fn",
Def::Const(_) => "const",
Def::Type(_) => "type",
// class/instance Def variants exist but are
// not yet anchored in the prose-spec block. Once 22b.4
// adds prose projection for them, the FORM_A_SPEC text
// gains `(class ` / `(instance ` anchors and this match
// will be exercised. For 22b.1 the exemplars list above
// does not produce these variants.
Def::Class(_) => "class",
Def::Instance(_) => "instance",
};
assert!(
FORM_A_SPEC.contains(anchor),
"spec is missing anchor `{anchor}` for a Def kind"
);
}
}
/// The mode keywords (the RC memory model) must appear so an LLM knows the
/// Form-A wrapper syntax.
#[test]
fn spec_mentions_mode_keywords() {
assert!(FORM_A_SPEC.contains("(own"), "spec missing `(own ...)`");
assert!(FORM_A_SPEC.contains("(borrow"), "spec missing `(borrow ...)`");
}
/// `tail-app` and `tail-do` are distinct keywords from `app`/`do`. The
/// spec must mention both, otherwise an LLM cannot produce tail-correct
/// code at scale.
#[test]
fn spec_mentions_tail_variants() {
assert!(FORM_A_SPEC.contains("tail-app"), "spec missing `tail-app`");
assert!(FORM_A_SPEC.contains("tail-do"), "spec missing `tail-do`");
}
/// `suppress` is part of the surface and the LLM must know how to
/// preserve it. Empty-because is itself a diagnostic; the spec calls
/// it out so the LLM does not produce empty justifications.
#[test]
fn spec_mentions_suppress_clause() {
assert!(FORM_A_SPEC.contains("(suppress"), "spec missing `(suppress ...)`");
assert!(
FORM_A_SPEC.contains("empty-suppress-reason"),
"spec missing the empty-suppress-reason diagnostic"
);
// Make sure `Suppress` in the AST can still be constructed — the
// exhaustive-match property carries through to the surface.
let _ = Suppress {
code: "x".into(),
because: "y".into(),
};
}