diff --git a/CLAUDE.md b/CLAUDE.md index 534fe9c..3b6bb7e 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -70,7 +70,7 @@ Proof and design history is in `formal/PRESERVATION-DESIGN.adoc`; current status - Formal-proof work spans Coq, Idris2, and the applicable estate policy. Checker output is evidence only for the exact proposition and assumptions run; a green build does not establish general language soundness. - The legacy preservation closure plan is obsolete. `formal/PRESERVATION-DESIGN.adoc` is design/history, not a proof result; `formal/PRESERVATION-HANDOFF.adoc` is historical diagnosis only. - Modality and `linear_to_affine` artifacts are mechanised, but no unconditional L1/L2 preservation theorem is established. The modality-polymorphic L1 statement is refuted as stated; see `PROOF-NEEDS.adoc` and the EXPLAINME ledger. -- All commits GPG-signed (key `4A03639C1EB1F86C7F0C97A91835A14A2867091E`), email `6759885+hyperpolymath@users.noreply.github.com`. Auto-merge ON for every PR. +- Commit signing (owner ruling 2026-11-10). Each commit on `main` is a squash merge made on github.com: GitHub signs it with its own key, and it shows as Verified. The owner key `4A03639C1EB1F86C7F0C97A91835A14A2867091E` (email `6759885+hyperpolymath@users.noreply.github.com`) signs the commits that the owner makes on a local computer. A cloud agent session signs its branch commits with its own session key; never put a private key of the owner into such a session. Auto-merge ON for every PR. --- diff --git a/TEST-NEEDS.adoc b/TEST-NEEDS.adoc index 20cfd5d..a6e1ebb 100644 --- a/TEST-NEEDS.adoc +++ b/TEST-NEEDS.adoc @@ -21,9 +21,9 @@ compliance, 16 tests) performance, correctness, 13 tests) * Benchmarks: `+src/ephapax-parser/benches/parse_bench.rs+`, `+src/ephapax-vram-cache/benches/cache_bench.rs+` -* Total: *620 tests* (`+cargo test --workspace --all-targets+`); +* Total: *621 tests* (`+cargo test --workspace --all-targets+`); pass/fail enforced by `+rust-ci.yml+` -* Documented all-target tests: 620 +* Documented all-target tests: 621 === CRG Testing Taxonomy — Status @@ -83,7 +83,7 @@ eliminator-fork invariant + its gated capstone, per PROOF-NEEDS.adoc §4) ==== Build & Execution * [x] cargo build — compiles -* [x] cargo test –workspace –all-targets — 620 pass, 0 fail +* [x] cargo test –workspace –all-targets — 621 pass, 0 fail * [x] idris2/ephapax-parse-tests.ipkg — compiles AND runs green (2026-07-07, idris2 0.8.0 + zig-built libephapax_tokbuf.so); CI-gated compile-only by abi-verify.yml `+idris2-parse-front+` (runtime run stays diff --git a/src/ephapax-cli/tests/run_wasm.rs b/src/ephapax-cli/tests/run_wasm.rs index 346f631..0c53800 100644 --- a/src/ephapax-cli/tests/run_wasm.rs +++ b/src/ephapax-cli/tests/run_wasm.rs @@ -508,6 +508,105 @@ fn a_module_names_a_data_type_only_through_a_pub_import() { } } +/// A `type` alias and an extern type follow the rule of data types (owner +/// decision 2026-11-10): a module names one when it declares it, or when +/// it imports the module that declares it. An alias must also be `pub`; +/// an extern type is public, as an extern function is. Each module used +/// to see each alias and each extern type of the program. +#[test] +fn a_module_names_an_alias_or_an_extern_type_only_through_an_import() { + let tmp = tempfile::tempdir().expect("tempdir"); + let write = + |name: &str, text: &str| std::fs::write(tmp.path().join(name), text).expect("write module"); + write( + "lib.eph", + "module lib\n\npub type Meters = I32\n\ntype Feet = I32\n\n\ + pub fn double(m: Meters): Meters = m + m\n\n\ + pub fn feet(n: I32): Feet = n\n", + ); + write( + "host.eph", + "module host\n\nextern \"c\" {\n type Handle\n fn open(n: I32): Handle\n \ + fn close(h: Handle): I32\n}\n", + ); + write( + "mid.eph", + "module mid\n\nimport host\n\npub fn via(n: I32): I32 = close(open(n))\n", + ); + let keep = "fn keep(m: Meters): Meters = m\n"; + let pass = "fn pass(h: Handle): Handle = h\n"; + + // (imports and declarations, `main` body, output) + for (head, main, want) in [ + (format!("import lib\n\n{keep}"), "double(keep(4))", "8"), + // An import list names the alias. + ( + format!("import lib(Meters, double)\n\n{keep}"), + "double(keep(4))", + "8", + ), + // A function of `lib` has the private alias in its signature. + ("import lib\n".to_string(), "feet(3)", "3"), + // A declaration of the module shadows an imported alias. + ( + "import lib\n\ndata Meters = M(I32)\n".to_string(), + "match M(5) of | M(n) => n end", + "5", + ), + ] { + write( + "app.eph", + &format!("module app\n\n{head}\nfn main(): I32 = {main}\n"), + ); + for args in [&["run", "app.eph"][..], &["run", "--interp", "app.eph"]] { + assert_eq!(stdout_of(tmp.path(), args), want, "{main} under {args:?}"); + } + } + + // (imports and declarations, text of the load error; `None`: it compiles). + // The host of `run` does not have `open`, so these programs do not run. + let main = "close(pass(open(1)))"; + for (head, error) in [ + (format!("import host\n\n{pass}"), None), + (format!("import host(Handle, open, close)\n\n{pass}"), None), + // The import list does not name the type. + ( + format!("import host(open, close)\n\n{pass}"), + Some("unknown type `Handle`"), + ), + // An extern type of a module that this module does not import. + ( + format!("import mid\n\n{pass}"), + Some("unknown type `Handle`"), + ), + // A private alias, and an alias that the import list does not name. + ( + "import lib\n\nfn keep(f: Feet): Feet = f\n".to_string(), + Some("unknown type `Feet`"), + ), + ( + format!("import lib(double)\n\n{keep}"), + Some("unknown type `Meters`"), + ), + ] { + let body = if head.contains("Handle") { main } else { "0" }; + write( + "app.eph", + &format!("module app\n\n{head}\nfn main(): I32 = {body}\n"), + ); + let out = ephapax(tmp.path(), &["compile", "app.eph"]); + let stderr = String::from_utf8_lossy(&out.stderr); + match error { + None => assert!(out.status.success(), "{head}: stderr:\n{stderr}"), + Some(error) => assert!( + !out.status.success() && stderr.contains(error), + "{head}: exit {:?}, stderr:\n{stderr}", + out.status.code() + ), + } + } +} + /// v2 plan rung E7: an arm with a false guard gives the value to the next /// arm, as wasm and in the interpreter. The desugarer used to take a /// guarded constructor arm without a look at its guard. diff --git a/src/ephapax-desugar/src/lib.rs b/src/ephapax-desugar/src/lib.rs index e386e6d..8e3a3a8 100644 --- a/src/ephapax-desugar/src/lib.rs +++ b/src/ephapax-desugar/src/lib.rs @@ -160,26 +160,46 @@ struct ConstructorInfo { home: SmolStr, } -/// A data type as its module declares it. +/// A named type as its module declares it. #[derive(Debug, Clone)] -struct DataInfo { - params: Vec, - ctors: Vec, - /// Key of the module that declares the type. The names in the - /// fields of `ctors` are names in the scope of that module. +struct TypeInfo { + def: TypeDef, + /// Key of the module that declares the type. The names in `def` are + /// names in the scope of that module. home: SmolStr, - /// `pub data`: a module that imports `home` can name the type. + /// A module that imports `home` can name the type: `pub data`, + /// `pub type`, and each extern type (as each extern function). public: bool, } -/// The data types and the constructors that one module can name: its +/// What a type name stands for. +#[derive(Debug, Clone)] +enum TypeDef { + /// `data Foo(a) = A | B(a)`. + Data { + params: Vec, + ctors: Vec, + }, + /// `type Foo = T`, with `T` in surface form: `desugar_named_type` + /// expands it on demand. Record and sum declarations are already + /// lowered to `Prod`/`Sum`/`Tuple` by `parse_type_decl`. + Alias(SurfaceTy), + /// `extern "abi" { type Foo }`: nominal and opaque. It resolves to + /// `Ty::Var("Foo")`, a rigid type variable that unifies only with + /// itself, so a `Window` is never an `IpcChannel`. + Extern, +} + +/// The named types and the constructors that one module can name: its /// own, and the public ones of the modules that it imports. #[derive(Debug, Clone, Default)] struct Scope { /// Constructor name → info constructors: HashMap, - /// Data type name → declaration - types: HashMap, + /// Type name → declaration. A data type, an alias and an extern + /// type share the one table: a later declaration of a name shadows + /// an earlier one of each kind. + types: HashMap, } /// The key of a module in the registry. `Foo.Bar` and `Foo/Bar` name the @@ -193,31 +213,13 @@ fn module_key(name: &str) -> SmolStr { /// Maps constructor names to their encoding information. This is built /// from `DataDecl` nodes and used to desugar `Construct` and `Match`. /// Each module has its own [`Scope`], as it has for functions: a module -/// names a data type of another module only when it imports that module -/// and the type is `pub`. +/// names a data type, a `type` alias or an extern type of another module +/// only when it imports that module and the type is public. #[derive(Debug, Clone, Default)] pub struct DataRegistry { /// Module key → what the module can name. The key is the empty /// string for declarations registered with no module. scopes: HashMap, - /// Names declared via `extern "abi" { type Foo }` blocks. - /// - /// Extern types are nominal and opaque: the desugar pass resolves - /// `SurfaceTy::Named { name: "Foo", args: [] }` to `Ty::Var("Foo")` - /// rather than emitting an `UnknownType` error. The type checker - /// then treats them as rigid type variables that only unify with - /// themselves (so values of type `Window` cannot be confused with - /// `IpcChannel`, etc.). - extern_types: std::collections::HashSet, - /// `type Foo = T` aliases — captured in their pre-desugar surface - /// form so `desugar_named_type` can recursively expand them on - /// demand. The stored value is whatever the parser produced for the - /// alias body (record/sum decls already pre-lowered to `Prod`/`Sum`/ - /// `Tuple` by `parse_type_decl`). An alias is visible in each module. - /// Each entry has the key of the module that declares the alias: the - /// body expands in the scope of that module, and a module that - /// declares an alias of the same name gets its own. - type_aliases: HashMap>, } impl DataRegistry { @@ -240,31 +242,44 @@ impl DataRegistry { }, ); } - scope.types.insert( - decl.name.clone(), - DataInfo { - params: decl.params.clone(), - ctors: decl.constructors.clone(), - home: home.into(), - public: decl.visibility == SurfaceVisibility::Public, - }, - ); + let def = TypeDef::Data { + params: decl.params.clone(), + ctors: decl.constructors.clone(), + }; + let public = decl.visibility == SurfaceVisibility::Public; + self.register_type(home, &decl.name, def, public); + } + + /// Give the type name `name` its meaning in the module `home`. + fn register_type(&mut self, home: &str, name: &SmolStr, def: TypeDef, public: bool) { + let home: SmolStr = home.into(); + let info = TypeInfo { + def, + home: home.clone(), + public, + }; + let scope = self.scopes.entry(home).or_default(); + scope.types.insert(name.clone(), info); } - /// Bring the public data types that the module `from` declares, with - /// their constructors, into the scope of the module `into`. A list of - /// `names` that is not empty limits the import to the types in it. - /// Returns the names of the imported types. + /// Bring the public types that the module `from` declares, and the + /// constructors of its data types, into the scope of the module + /// `into`. A list of `names` that is not empty limits the import to + /// the types in it. Returns the names of the imported types. fn import(&mut self, into: &str, from: &str, names: &[SmolStr]) -> HashSet { let Some(source) = self.scopes.get(from) else { return HashSet::new(); }; let mut imported = Scope::default(); - for (name, data) in &source.types { - if !data.public || data.home != from || !(names.is_empty() || names.contains(name)) { + for (name, info) in &source.types { + if !info.public || info.home != from || !(names.is_empty() || names.contains(name)) { continue; } - for ctor in &data.ctors { + let TypeDef::Data { ctors, .. } = &info.def else { + imported.types.insert(name.clone(), info.clone()); + continue; + }; + for ctor in ctors { // A later data type of `from` can have a constructor of // the same name: the constructor is then not of `name`. let info = source.constructors.get(&ctor.name); @@ -274,7 +289,7 @@ impl DataRegistry { .insert(ctor.name.clone(), info.clone()); } } - imported.types.insert(name.clone(), data.clone()); + imported.types.insert(name.clone(), info.clone()); } let types = imported.types.keys().cloned().collect(); let scope = self.scopes.entry(into.into()).or_default(); @@ -283,30 +298,16 @@ impl DataRegistry { types } - /// Register an opaque extern type name (from - /// `extern "abi" { type Foo }`). - pub fn register_extern_type(&mut self, name: &SmolStr) { - self.extern_types.insert(name.clone()); - } - - /// Register a `type Foo = T` alias of the module `home` in surface - /// form. Lookups in `desugar_named_type` find the entry and - /// recursively desugar it. - pub fn register_type_alias(&mut self, home: &str, name: SmolStr, ty: SurfaceTy) { - let entries = self.type_aliases.entry(name).or_default(); - entries.retain(|(module, _)| module != home); - entries.push((home.into(), ty)); + /// Register the opaque type `name` of an extern block of the module + /// `home`. + pub fn register_extern_type(&mut self, home: &str, name: &SmolStr) { + self.register_type(home, name, TypeDef::Extern, true); } - /// The alias `name` as the module `scope` sees it, with the key of - /// the module that declares it: the alias of `scope`, or else the - /// alias that was registered last. - fn lookup_type_alias(&self, scope: &str, name: &str) -> Option<&(SmolStr, SurfaceTy)> { - let entries = self.type_aliases.get(name)?; - entries - .iter() - .find(|(module, _)| module == scope) - .or(entries.last()) + /// Register the alias `type name = ty` of the module `home`. `public` + /// is `pub type`: a module that imports `home` can name the alias. + pub fn register_type_alias(&mut self, home: &str, name: SmolStr, ty: SurfaceTy, public: bool) { + self.register_type(home, &name, TypeDef::Alias(ty), public); } /// Look up a constructor by its name in the module `scope`. @@ -314,15 +315,10 @@ impl DataRegistry { self.scopes.get(scope)?.constructors.get(name) } - /// Look up a data type by its name in the module `scope`. - fn get_type_ctors(&self, scope: &str, name: &str) -> Option<&DataInfo> { + /// Look up a type by its name in the module `scope`. + fn get_type(&self, scope: &str, name: &str) -> Option<&TypeInfo> { self.scopes.get(scope)?.types.get(name) } - - /// Is this name a registered extern (opaque) type? - fn is_extern_type(&self, name: &str) -> bool { - self.extern_types.contains(name) - } } // ========================================================================= @@ -402,12 +398,15 @@ impl Desugarer { /// The constructors of the data type of the constructor `info`. fn ctors_of(&self, info: &ConstructorInfo) -> Result, DesugarError> { - self.registry - .get_type_ctors(&info.home, &info.data_name) - .map(|data| data.ctors.clone()) - .ok_or_else(|| DesugarError::UnknownType { + match self.registry.get_type(&info.home, &info.data_name) { + Some(TypeInfo { + def: TypeDef::Data { ctors, .. }, + .. + }) => Ok(ctors.clone()), + _ => Err(DesugarError::UnknownType { name: info.data_name.to_string(), - }) + }), + } } /// Run `f` with the names of the module `home` in scope: the names @@ -433,14 +432,14 @@ impl Desugarer { .map(|i| last_segment(i.module.as_str())) .collect(); - // The public data types of each imported module, in the order of - // the imports: a later one shadows an earlier one, and a - // declaration of this module shadows both. + // The public types of each imported module, in the order of the + // imports: a later one shadows an earlier one, and a declaration + // of this module shadows both. let key = module_key(&module.name); // The imports of the core module: the type checker reads each // name in an import list as a function, so the list keeps only - // the names that are not data types. An import that names only - // data types imports no function. + // the names that are not types. An import that names only types + // imports no function. let mut imports = Vec::with_capacity(module.imports.len()); for import in &module.imports { let types = self @@ -465,13 +464,18 @@ impl Desugarer { SurfaceDecl::Extern { items, .. } => { for item in items { if let SurfaceExternItem::Type { name } = item { - self.registry.register_extern_type(name); + self.registry.register_extern_type(&key, name); } } } - SurfaceDecl::Type { name, ty, .. } => { + SurfaceDecl::Type { + name, + visibility, + ty, + } => { + let public = *visibility == SurfaceVisibility::Public; self.registry - .register_type_alias(&key, name.clone(), ty.clone()); + .register_type_alias(&key, name.clone(), ty.clone(), public); } _ => {} } @@ -955,39 +959,29 @@ impl Desugarer { return Ok(Ty::Base(BaseTy::I32)); } - if self.registry.is_extern_type(name.as_str()) { - return Ok(Ty::Var(name.clone())); - } - - // `type Foo = T` aliases — recursively desugar the stored surface - // form. Aliases are monomorphic here (parameterised aliases would - // carry their args via the body). - let alias = self + let info = self .registry - .lookup_type_alias(&self.scope.borrow(), name.as_str()) - .cloned(); - if let Some((home, aliased)) = alias { - if !args.is_empty() { - return Err(DesugarError::TypeArityMismatch { - name: name.to_string(), - expected: 0, - got: args.len(), - }); - } - return self.with_expansion(name, &home, |this| this.desugar_ty(&aliased)); - } - - let DataInfo { - params, - ctors, - home, - .. - } = self - .registry - .get_type_ctors(&self.scope.borrow(), name.as_str()) + .get_type(&self.scope.borrow(), name.as_str()) .ok_or_else(|| DesugarError::UnknownType { name: name.to_string(), })?; + let home = &info.home; + let (params, ctors) = match &info.def { + TypeDef::Extern => return Ok(Ty::Var(name.clone())), + // Aliases are monomorphic here (parameterised aliases would + // carry their args via the body). + TypeDef::Alias(aliased) => { + if !args.is_empty() { + return Err(DesugarError::TypeArityMismatch { + name: name.to_string(), + expected: 0, + got: args.len(), + }); + } + return self.with_expansion(name, home, |this| this.desugar_ty(aliased)); + } + TypeDef::Data { params, ctors } => (params, ctors), + }; if params.len() != args.len() { return Err(DesugarError::TypeArityMismatch { @@ -2536,6 +2530,7 @@ mod expansion_regressions { } else { named(&format!("A{}", i + 1)) }, + false, ); } let desugarer = Desugarer::with_registry(registry.clone()); @@ -2543,7 +2538,7 @@ mod expansion_regressions { desugarer.desugar_ty(&named("A0")).unwrap(), Ty::Base(BaseTy::I32) ); - registry.register_type_alias("", "A64".into(), named("A0")); + registry.register_type_alias("", "A64".into(), named("A0"), false); assert!(matches!( Desugarer::with_registry(registry).desugar_ty(&named("A0")), Err(DesugarError::RecursiveType { .. }) diff --git a/src/ephapax-driver/src/lib.rs b/src/ephapax-driver/src/lib.rs index 07cb674..14f9b1e 100644 --- a/src/ephapax-driver/src/lib.rs +++ b/src/ephapax-driver/src/lib.rs @@ -224,8 +224,8 @@ pub fn parse_source( )?; // One DataRegistry for all modules: it gives each module its own - // scope, with the `pub data` types of the modules that it imports. - // An `extern type` is visible in each module. + // scope, with the public types of the modules that it imports + // (`pub data`, `pub type`, and each extern type). let mut desugarer = Desugarer::with_registry(DataRegistry::new()); let mut modules = Vec::with_capacity(resolved.len()); for m in resolved {