diff --git a/README.md b/README.md index 7f42eb67..2b28d1a6 100644 --- a/README.md +++ b/README.md @@ -28,8 +28,9 @@ cargo run -- dump mir examples/basic.purs `build ...` resolves and links every listed module with the standard library from `stdlib/lib` and writes the artifact. `wat ...` renders the text form. `dump ` prints an intermediate IR for -debugging. `main` must be a zero-argument `Int` declaration; its value becomes -the process exit code. +debugging. A selected `main :: Int` returns its value as the process exit code. +A selected `main :: Effect Unit` runs that action once and returns 0; a trap +still propagates. For a guided, interactive walkthrough of P0 through P11, use the React application in [`psrs-explorer/`](psrs-explorer/). It labels compact teaching @@ -45,11 +46,11 @@ what remains in each layer. | Gate | Measured | Scope | | --- | --- | --- | | L0/L1 lexing, layout, parsing | 904/908 | non-FFI `layout`, `passing`, `failing`, `warning` files; the four differences are recorded DEC-16 intentional differences | -| L2 resolution | 54/70 failing, 52/413 passing | official `errorCode`s; 106 `passing` files stop in surface lowering | -| L3 kinds | 27/48 failing | official kind `errorCode`s | -| L4 types | 12/40 failing | official `errorCode`s; most mismatches blocked on a missing library module | -| L5 classes | 41/81 failing | official `errorCode`s; most mismatches blocked on a missing library module | -| L6/M7 runtime | 0/413 passing | 244 blocked on a missing module, 106 in surface lowering | +| L2 resolution | 72/72 failing, 270/413 passing | official `errorCode`s; 53 `passing` files stop on a missing module and 86 at P3 | +| L3 kinds | 35/48 failing | official kind `errorCode`s | +| L4 types | 35/50 failing | official `errorCode`s | +| L5 classes | 53/80 failing | official `errorCode`s | +| L6/M7 runtime | 124/413 passing | all 124 exit 0; 63 have no selected `main`; 53 stop on a missing module | | M8 warnings, optimization | not measured | no scoreboard exists | Run the scoreboards yourself: diff --git a/crates/psrs-backend/src/abi/link/mod.rs b/crates/psrs-backend/src/abi/link/mod.rs index d7dc10f2..0e06a2f3 100644 --- a/crates/psrs-backend/src/abi/link/mod.rs +++ b/crates/psrs-backend/src/abi/link/mod.rs @@ -1,21 +1,23 @@ //! Target-aware linking helpers for source WIT bindings. //! -//! A foreign import's resolved source type is interned into the Core type table -//! so the backend can refer to it by identity. A structurally equal Core type -//! already in the table is reused, so a foreign signature shares the canonical -//! representation of the same type used elsewhere in the module. This replaces -//! recovering the type by structural search at the CC boundary. +//! WIT declarations consume the checked external schemes carried by Core. +//! Structural HIR interning remains available only to isolated ABI fixtures; +//! production linking never reconstructs the checked source type from HIR. +#[cfg(test)] use psrs_core::{Module as CoreModule, Type as CoreType, TypeConstructor, TypeId as CoreTypeId}; +#[cfg(test)] use psrs_hir::{BuiltinType, Type as HirType, TypeKind as HirTypeKind}; /// Interns the resolved source type of a foreign import and returns its /// [`CoreTypeId`]. The type is appended to the module type table when no /// structurally equal type is present. +#[cfg(test)] pub(crate) fn intern_source_type(module: &mut CoreModule, ty: &HirType) -> Option { intern_into(&mut module.types, ty) } +#[cfg(test)] fn intern_into(types: &mut Vec, ty: &HirType) -> Option { let core = match &ty.kind { HirTypeKind::Constructor(BuiltinType::Int) => { @@ -91,6 +93,7 @@ fn intern_into(types: &mut Vec, ty: &HirType) -> Option { Some(intern_core_type(types, core)) } +#[cfg(test)] fn is_array_constructor(types: &[CoreType], id: CoreTypeId) -> bool { matches!( types.get(id.0 as usize), @@ -98,6 +101,7 @@ fn is_array_constructor(types: &[CoreType], id: CoreTypeId) -> bool { ) } +#[cfg(test)] fn is_array_element(types: &[CoreType], id: CoreTypeId) -> bool { match types.get(id.0 as usize) { // `Unit` is a primitive but has no canonical list element. @@ -122,6 +126,7 @@ fn is_array_element(types: &[CoreType], id: CoreTypeId) -> bool { } } +#[cfg(test)] fn is_record(types: &[CoreType], id: CoreTypeId) -> bool { let Some(CoreType::Application(function, _)) = types.get(id.0 as usize) else { return false; @@ -132,6 +137,7 @@ fn is_record(types: &[CoreType], id: CoreTypeId) -> bool { ) } +#[cfg(test)] fn is_user_type(types: &[CoreType], id: CoreTypeId) -> bool { matches!( types.get(id.0 as usize), @@ -139,6 +145,7 @@ fn is_user_type(types: &[CoreType], id: CoreTypeId) -> bool { ) } +#[cfg(test)] fn intern_core_type(types: &mut Vec, core: CoreType) -> CoreTypeId { if let Some(index) = types.iter().position(|existing| *existing == core) { return CoreTypeId(index as u32); diff --git a/crates/psrs-backend/src/abi/link/tests.rs b/crates/psrs-backend/src/abi/link/tests.rs index 150bd72c..91042f63 100644 --- a/crates/psrs-backend/src/abi/link/tests.rs +++ b/crates/psrs-backend/src/abi/link/tests.rs @@ -13,6 +13,7 @@ fn module() -> CoreModule { id: ModuleId(0), name: "Main".into(), externals: Vec::new(), + external_types: Vec::new(), types: vec![ CoreType::Constructor(psrs_core::TypeConstructor::Int), CoreType::Constructor(psrs_core::TypeConstructor::Number), diff --git a/crates/psrs-backend/src/abi/mod.rs b/crates/psrs-backend/src/abi/mod.rs index 9fbf9baf..d4cc20bc 100644 --- a/crates/psrs-backend/src/abi/mod.rs +++ b/crates/psrs-backend/src/abi/mod.rs @@ -23,6 +23,7 @@ use canonical::{ resolve as resolve_canonical, }; pub use handles::{HandleMode, HandleResource}; +#[cfg(test)] pub(crate) use link::intern_source_type; use validation::{unsupported_shape, wasi_interface_enabled}; diff --git a/crates/psrs-backend/src/abi/tests/lists.rs b/crates/psrs-backend/src/abi/tests/lists.rs index 36414ead..030d5f5c 100644 --- a/crates/psrs-backend/src/abi/tests/lists.rs +++ b/crates/psrs-backend/src/abi/tests/lists.rs @@ -18,6 +18,7 @@ fn empty_core() -> CoreModule { id: ModuleId(0), name: "Main".into(), externals: Vec::new(), + external_types: Vec::new(), types: Vec::new(), newtype_ids: Vec::new(), opaque_ids: Vec::new(), diff --git a/crates/psrs-backend/src/abi/tests/mod.rs b/crates/psrs-backend/src/abi/tests/mod.rs index 4ec9b6d8..0affdbce 100644 --- a/crates/psrs-backend/src/abi/tests/mod.rs +++ b/crates/psrs-backend/src/abi/tests/mod.rs @@ -19,6 +19,7 @@ fn empty_core_module() -> psrs_core::Module { id: psrs_hir::ModuleId(0), name: "Main".into(), externals: Vec::new(), + external_types: Vec::new(), types: Vec::new(), newtype_ids: Vec::new(), opaque_ids: Vec::new(), diff --git a/crates/psrs-backend/src/bindings/mod.rs b/crates/psrs-backend/src/bindings/mod.rs index d9df0b89..23002ac9 100644 --- a/crates/psrs-backend/src/bindings/mod.rs +++ b/crates/psrs-backend/src/bindings/mod.rs @@ -3,7 +3,7 @@ use crate::BackendError; use crate::cc; use psrs_core::{Module as CoreModule, TypeId as CoreTypeId}; -use psrs_hir::{ExternalKind, SymbolId, Type as HirType}; +use psrs_hir::{ExternalKind, ModuleId, SymbolId}; use std::collections::{HashMap, HashSet}; /// The complete input consumed by P9. Platform binding metadata is kept beside @@ -23,11 +23,12 @@ pub struct ExternalBindings { impl ExternalBindings { /// Extracts platform binding metadata while crossing the Core boundary. /// CC receives only this side table and therefore never needs to inspect - /// WIT names or HIR external kinds. Each declaration's resolved source type - /// is interned into the Core type table and recorded as a `type_id`, so CC - /// derives its layout from that identity instead of re-deriving it. - pub(crate) fn from_core(module: &mut CoreModule) -> Self { - let declared: Vec<(SymbolId, String, String, Option)> = module + /// WIT names or HIR external kinds. Each declaration's checked, + /// synonym-expanded source scheme is read from Core's external signature + /// table and recorded as a `type_id`, so CC derives its layout from that + /// identity instead of re-deriving it from raw HIR. + pub(crate) fn from_core(module: &CoreModule) -> Self { + let imports = module .externals .iter() .filter_map(|external| { @@ -38,31 +39,24 @@ impl ExternalBindings { else { return None; }; - Some(( - external.symbol, - interface.clone(), - function.clone(), - external.signature.clone(), - )) + let checked = module + .external_types + .iter() + .find(|checked| checked.symbol == external.symbol); + Some(ExternalBinding { + symbol: external.symbol, + source_module: checked.map_or(module.id, |checked| checked.source_module), + interface: interface.clone(), + function: function.clone(), + type_id: checked.map(|checked| checked.ty), + span: external + .signature + .as_ref() + .map(|signature| signature.span) + .unwrap_or(module.span), + }) }) .collect(); - let module_span = module.span; - let mut imports = Vec::with_capacity(declared.len()); - for (symbol, interface, function, signature) in declared { - let span = signature - .as_ref() - .map_or(module_span, |signature| signature.span); - let type_id = signature - .as_ref() - .and_then(|signature| crate::abi::intern_source_type(module, signature)); - imports.push(ExternalBinding { - symbol, - interface, - function, - type_id, - span, - }); - } Self { imports } } @@ -84,7 +78,7 @@ impl ExternalBindings { .map_err(|message| { vec![ BackendError::new("P8 WIT linking", binding.span, message) - .with_module(binding.symbol.module), + .with_module(binding.source_module), ] })?; if let Some(reason) = &import.unsupported { @@ -94,7 +88,7 @@ impl ExternalBindings { binding.span, format!("WIT import `{qualified}` is unsupported: {reason}"), ) - .with_module(binding.symbol.module), + .with_module(binding.source_module), ]); } let Some(type_id) = binding.type_id else { @@ -104,14 +98,14 @@ impl ExternalBindings { binding.span, format!("WIT import `{qualified}` has no resolved source type"), ) - .with_module(binding.symbol.module), + .with_module(binding.source_module), ]); }; crate::abi::link::validate_import_signature(&import, module, type_id).map_err( |message| { vec![ BackendError::new("P8 WIT linking", binding.span, message) - .with_module(binding.symbol.module), + .with_module(binding.source_module), ] }, )?; @@ -225,6 +219,7 @@ impl ExternalBindings { #[derive(Clone, Debug, PartialEq, Eq)] pub struct ExternalBinding { pub symbol: SymbolId, + pub source_module: ModuleId, pub interface: String, pub function: String, /// The declaration's resolved source type, interned in the module type diff --git a/crates/psrs-backend/src/bindings/tests.rs b/crates/psrs-backend/src/bindings/tests.rs index b7d95337..7e11a40d 100644 --- a/crates/psrs-backend/src/bindings/tests.rs +++ b/crates/psrs-backend/src/bindings/tests.rs @@ -26,6 +26,7 @@ fn wit_external(symbol: SymbolId) -> ExternalSymbol { fn binding(symbol: SymbolId) -> ExternalBinding { ExternalBinding { symbol, + source_module: ModuleId(0), interface: "wasi:cli/stdout@0.2.12".into(), function: "log".into(), type_id: None, @@ -39,6 +40,7 @@ fn module(externals: Vec) -> CoreModule { id: ModuleId(1), name: "Main".into(), externals, + external_types: Vec::new(), types: Vec::new(), newtype_ids: Vec::new(), opaque_ids: Vec::new(), diff --git a/crates/psrs-backend/src/cc/case/coverage/tests/mod.rs b/crates/psrs-backend/src/cc/case/coverage/tests/mod.rs index 971bdad9..c02202ad 100644 --- a/crates/psrs-backend/src/cc/case/coverage/tests/mod.rs +++ b/crates/psrs-backend/src/cc/case/coverage/tests/mod.rs @@ -20,6 +20,7 @@ fn module(types: Vec, constructors: Vec) -> Mo id: ModuleId(0), name: "CoverageTest".to_owned(), externals: Vec::new(), + external_types: Vec::new(), types, newtype_ids: Vec::new(), opaque_ids: Vec::new(), diff --git a/crates/psrs-backend/src/cc/case/decision/compile/oracle_record_tests.rs b/crates/psrs-backend/src/cc/case/decision/compile/oracle_record_tests.rs index 3d715ef2..1cb0a0c8 100644 --- a/crates/psrs-backend/src/cc/case/decision/compile/oracle_record_tests.rs +++ b/crates/psrs-backend/src/cc/case/decision/compile/oracle_record_tests.rs @@ -26,6 +26,7 @@ fn module() -> Module { id: ModuleId(0), name: "RecordOracleTest".into(), externals: Vec::new(), + external_types: Vec::new(), types: vec![ Type::Constructor(TypeConstructor::User(u)), Type::Constructor(psrs_core::TypeConstructor::Int), diff --git a/crates/psrs-backend/src/cc/case/decision/compile/oracle_tests.rs b/crates/psrs-backend/src/cc/case/decision/compile/oracle_tests.rs index 4c000f87..834a5b6d 100644 --- a/crates/psrs-backend/src/cc/case/decision/compile/oracle_tests.rs +++ b/crates/psrs-backend/src/cc/case/decision/compile/oracle_tests.rs @@ -33,6 +33,7 @@ fn module() -> Module { id: ModuleId(0), name: "OracleTest".into(), externals: Vec::new(), + external_types: Vec::new(), types: vec![ Type::Constructor(TypeConstructor::User(t)), Type::Constructor(TypeConstructor::User(u)), diff --git a/crates/psrs-backend/src/cc/case/decision/compile/tests/mod.rs b/crates/psrs-backend/src/cc/case/decision/compile/tests/mod.rs index 2e36bfba..af7633b7 100644 --- a/crates/psrs-backend/src/cc/case/decision/compile/tests/mod.rs +++ b/crates/psrs-backend/src/cc/case/decision/compile/tests/mod.rs @@ -14,6 +14,7 @@ fn bool_module() -> (Module, SymbolId, SymbolId) { id: ModuleId(0), name: "DecisionTest".into(), externals: Vec::new(), + external_types: Vec::new(), types: vec![Type::Constructor(TypeConstructor::User(type_id))], newtype_ids: Vec::new(), opaque_ids: Vec::new(), diff --git a/crates/psrs-backend/src/cc/case/decision/realize/tests/mod.rs b/crates/psrs-backend/src/cc/case/decision/realize/tests/mod.rs index 3beda1bd..06a58810 100644 --- a/crates/psrs-backend/src/cc/case/decision/realize/tests/mod.rs +++ b/crates/psrs-backend/src/cc/case/decision/realize/tests/mod.rs @@ -29,6 +29,7 @@ fn compiled_root_switch_resolves_the_realizer_root_slot() { id: module_id, name: "DecisionRealizeTest".into(), externals: Vec::new(), + external_types: Vec::new(), types: vec![Type::Constructor(TypeConstructor::User(type_id))], newtype_ids: Vec::new(), opaque_ids: Vec::new(), diff --git a/crates/psrs-backend/src/cc/case/decision/realize/tests/nested_tests.rs b/crates/psrs-backend/src/cc/case/decision/realize/tests/nested_tests.rs index ab96f6e2..244f3d7b 100644 --- a/crates/psrs-backend/src/cc/case/decision/realize/tests/nested_tests.rs +++ b/crates/psrs-backend/src/cc/case/decision/realize/tests/nested_tests.rs @@ -27,6 +27,7 @@ fn nested_sum_patterns_project_once_per_selected_constructor_and_trap_missing_ta id: module_id, name: "NestedDecisionTest".into(), externals: Vec::new(), + external_types: Vec::new(), types: vec![ Type::Constructor(TypeConstructor::User(outer_type)), Type::Constructor(TypeConstructor::User(bool_type)), diff --git a/crates/psrs-backend/src/cc/case/decision/realize/tests/newtype_tests.rs b/crates/psrs-backend/src/cc/case/decision/realize/tests/newtype_tests.rs index 825e113c..1cb615b9 100644 --- a/crates/psrs-backend/src/cc/case/decision/realize/tests/newtype_tests.rs +++ b/crates/psrs-backend/src/cc/case/decision/realize/tests/newtype_tests.rs @@ -23,6 +23,7 @@ fn newtype_constructor_erases_before_nested_enum_dispatch() { id: module_id, name: "NewtypeDecisionTest".into(), externals: Vec::new(), + external_types: Vec::new(), types: vec![ Type::Constructor(TypeConstructor::User(wrapper_type)), Type::Constructor(TypeConstructor::User(bool_type)), diff --git a/crates/psrs-backend/src/cc/case/decision/realize/tests/parameterized_tests/mod.rs b/crates/psrs-backend/src/cc/case/decision/realize/tests/parameterized_tests/mod.rs index cd2d4d74..bc3414ea 100644 --- a/crates/psrs-backend/src/cc/case/decision/realize/tests/parameterized_tests/mod.rs +++ b/crates/psrs-backend/src/cc/case/decision/realize/tests/parameterized_tests/mod.rs @@ -22,6 +22,7 @@ fn parameterized_array_field_projection_uses_its_stored_canonical_array() { id: module_id, name: "ParameterizedArrayDecisionTest".into(), externals: Vec::new(), + external_types: Vec::new(), types: vec![ Type::Constructor(TypeConstructor::User(wrap_type)), Type::Variable(TypeVariableId(0)), @@ -172,6 +173,7 @@ fn nested_parameterized_projection_keeps_each_canonical_field() { id: module_id, name: "NestedParameterizedDecisionTest".into(), externals: Vec::new(), + external_types: Vec::new(), types: vec![ Type::Constructor(TypeConstructor::User(inner_type)), Type::Constructor(TypeConstructor::User(outer_type)), @@ -320,6 +322,7 @@ fn generic_record_pattern_projects_its_canonical_array_field() { id: module_id, name: "GenericRecordDecisionTest".into(), externals: Vec::new(), + external_types: Vec::new(), types: vec![ Type::Variable(TypeVariableId(0)), Type::Constructor(TypeConstructor::Array), diff --git a/crates/psrs-backend/src/cc/case/decision/realize/tests/product_tests.rs b/crates/psrs-backend/src/cc/case/decision/realize/tests/product_tests.rs index 4f2a0a1b..5636f8a8 100644 --- a/crates/psrs-backend/src/cc/case/decision/realize/tests/product_tests.rs +++ b/crates/psrs-backend/src/cc/case/decision/realize/tests/product_tests.rs @@ -23,6 +23,7 @@ fn single_constructor_product_dispatch_projects_and_binds_first_row_once() { id: module_id, name: "ProductDecisionTest".into(), externals: Vec::new(), + external_types: Vec::new(), types: vec![ Type::Constructor(TypeConstructor::User(type_id)), Type::Constructor(psrs_core::TypeConstructor::Int), diff --git a/crates/psrs-backend/src/cc/case/decision/realize/tests/record_tests.rs b/crates/psrs-backend/src/cc/case/decision/realize/tests/record_tests.rs index 0fa68b48..1970b478 100644 --- a/crates/psrs-backend/src/cc/case/decision/realize/tests/record_tests.rs +++ b/crates/psrs-backend/src/cc/case/decision/realize/tests/record_tests.rs @@ -25,6 +25,7 @@ fn nested_record_patterns_share_one_product_projection_and_keep_source_spans() { id: module_id, name: "RecordDecisionTest".into(), externals: Vec::new(), + external_types: Vec::new(), types: vec![ Type::Constructor(TypeConstructor::User(bool_type)), Type::Constructor(psrs_core::TypeConstructor::Int), diff --git a/crates/psrs-backend/src/cc/layout/tests/mod.rs b/crates/psrs-backend/src/cc/layout/tests/mod.rs index 8f24a81d..57c6da6e 100644 --- a/crates/psrs-backend/src/cc/layout/tests/mod.rs +++ b/crates/psrs-backend/src/cc/layout/tests/mod.rs @@ -23,6 +23,7 @@ fn empty_module(types: Vec) -> Module { id: ModuleId(0), name: "LayoutKeysTest".into(), externals: Vec::new(), + external_types: Vec::new(), types, newtype_ids: Vec::new(), opaque_ids: Vec::new(), @@ -170,6 +171,7 @@ fn equal_normalized_function_signatures_share_one_signature_id() { id: ModuleId(0), name: "SignatureInterningTest".into(), externals: Vec::new(), + external_types: Vec::new(), types, newtype_ids: Vec::new(), opaque_ids: Vec::new(), @@ -287,6 +289,7 @@ fn integer_capture_module(capture: Type) -> Module { id: ModuleId(0), name: "IntegerCaptureTest".into(), externals: Vec::new(), + external_types: Vec::new(), types: vec![capture, Type::Constructor(psrs_core::TypeConstructor::Int)], newtype_ids: Vec::new(), opaque_ids: Vec::new(), @@ -371,6 +374,7 @@ fn an_opaque_handle_and_an_array_of_handles_have_scalar_layouts() { id: module_id, name: "OpaqueHandleLayoutTest".into(), externals: Vec::new(), + external_types: Vec::new(), types: vec![ Type::Constructor(TypeConstructor::User(opaque)), Type::Constructor(TypeConstructor::Array), diff --git a/crates/psrs-backend/src/cc/layout/tests/records.rs b/crates/psrs-backend/src/cc/layout/tests/records.rs index 1fd4401c..436dbfe1 100644 --- a/crates/psrs-backend/src/cc/layout/tests/records.rs +++ b/crates/psrs-backend/src/cc/layout/tests/records.rs @@ -42,6 +42,7 @@ fn parameter_dependent_record_field_keeps_its_canonical_template_in_the_adt_slot id: module_id, name: "RecordPayloadLayoutTest".into(), externals: Vec::new(), + external_types: Vec::new(), types, newtype_ids: Vec::new(), opaque_ids: Vec::new(), @@ -118,6 +119,7 @@ fn a_variant_case_may_carry_a_record_payload() { id: module_id, name: "RecordPayloadVariantLayoutTest".into(), externals: Vec::new(), + external_types: Vec::new(), types, newtype_ids: Vec::new(), opaque_ids: Vec::new(), diff --git a/crates/psrs-backend/src/cc/lower/conversion/tests.rs b/crates/psrs-backend/src/cc/lower/conversion/tests.rs index 94f0c735..d13c233d 100644 --- a/crates/psrs-backend/src/cc/lower/conversion/tests.rs +++ b/crates/psrs-backend/src/cc/lower/conversion/tests.rs @@ -14,6 +14,7 @@ fn unsupported_typed_boundary_reports_its_source_span() { id: ModuleId(0), name: "ConversionDiagnostic".into(), externals: Vec::new(), + external_types: Vec::new(), types: vec![ Type::Constructor(psrs_core::TypeConstructor::Int), Type::Constructor(psrs_core::TypeConstructor::Number), diff --git a/crates/psrs-backend/src/cc/lower/dictionary/tests.rs b/crates/psrs-backend/src/cc/lower/dictionary/tests.rs index 9fdd951a..3ed0f514 100644 --- a/crates/psrs-backend/src/cc/lower/dictionary/tests.rs +++ b/crates/psrs-backend/src/cc/lower/dictionary/tests.rs @@ -277,6 +277,7 @@ fn dictionary_evidence_module() -> thir::Module { id: module_id, name: "DictionaryLayout".into(), externals: Vec::new(), + external_types: Vec::new(), types, newtype_ids: Vec::new(), opaque_ids: Vec::new(), diff --git a/crates/psrs-backend/src/cc/lower/erased/tests.rs b/crates/psrs-backend/src/cc/lower/erased/tests.rs index d7e6ff3d..a96cfab1 100644 --- a/crates/psrs-backend/src/cc/lower/erased/tests.rs +++ b/crates/psrs-backend/src/cc/lower/erased/tests.rs @@ -240,6 +240,7 @@ fn module(types: Vec, declaration: Declaration, entry: SymbolId) -> Module id: entry.module, name: "Main".into(), externals: Vec::new(), + external_types: Vec::new(), types, newtype_ids: Vec::new(), opaque_ids: Vec::new(), diff --git a/crates/psrs-backend/src/cc/lower/letrec/tests.rs b/crates/psrs-backend/src/cc/lower/letrec/tests.rs index 24875473..582528ef 100644 --- a/crates/psrs-backend/src/cc/lower/letrec/tests.rs +++ b/crates/psrs-backend/src/cc/lower/letrec/tests.rs @@ -453,6 +453,7 @@ fn module(types: Vec, declaration: Declaration, entry: SymbolId) -> Module id: entry.module, name: "Main".into(), externals: Vec::new(), + external_types: Vec::new(), types, newtype_ids: Vec::new(), opaque_ids: Vec::new(), diff --git a/crates/psrs-backend/src/cc/lower/record/tests.rs b/crates/psrs-backend/src/cc/lower/record/tests.rs index cf2b4592..80499ab4 100644 --- a/crates/psrs-backend/src/cc/lower/record/tests.rs +++ b/crates/psrs-backend/src/cc/lower/record/tests.rs @@ -191,6 +191,7 @@ fn generic_record_module(include_read: bool, include_build_update: bool) -> Modu id: module_id, name: "SyntheticGenericRecord".into(), externals: Vec::new(), + external_types: Vec::new(), types, newtype_ids: Vec::new(), opaque_ids: Vec::new(), diff --git a/crates/psrs-backend/src/cc/mod.rs b/crates/psrs-backend/src/cc/mod.rs index f874b693..2081c710 100644 --- a/crates/psrs-backend/src/cc/mod.rs +++ b/crates/psrs-backend/src/cc/mod.rs @@ -234,11 +234,12 @@ pub struct TagCase { /// Prefer [`lower_module_with_bindings`] when the caller already owns the /// backend input boundary. /// -/// Effect representation lowering runs here, after the binding table has -/// interned the abstract effect applications and before closure conversion. -pub fn lower_module(mut module: CoreModule) -> Result> { - let mut bindings = ExternalBindings::from_core(&mut module); - crate::effects::lower_effects(&mut module, &mut bindings)?; +/// This entry does not infer an Effect contract. A program that still contains +/// trusted Effect imports must go through [`crate::lower_cc_with_context`] or +/// [`crate::compile_with_context`] so those imports are lowered before WIT +/// linking. +pub fn lower_module(module: CoreModule) -> Result> { + let bindings = ExternalBindings::from_core(&module); lower_module_with_bindings(module, bindings) } @@ -310,7 +311,7 @@ pub fn lower_module_with_bindings( .map_err(|message| { vec![ BackendError::new("P8 closure conversion", module.span, message) - .with_module(binding.symbol.module), + .with_module(binding.source_module), ] })?; if let Some(signature) = &signature { diff --git a/crates/psrs-backend/src/cc/projection.rs b/crates/psrs-backend/src/cc/projection.rs index eaf8e5ef..83bd96c7 100644 --- a/crates/psrs-backend/src/cc/projection.rs +++ b/crates/psrs-backend/src/cc/projection.rs @@ -379,6 +379,7 @@ mod tests { id: module_id, name: "ProjectionTest".into(), externals: Vec::new(), + external_types: Vec::new(), types, newtype_ids: Vec::new(), opaque_ids: Vec::new(), diff --git a/crates/psrs-backend/src/effects.rs b/crates/psrs-backend/src/effects.rs deleted file mode 100644 index 36a19a17..00000000 --- a/crates/psrs-backend/src/effects.rs +++ /dev/null @@ -1,214 +0,0 @@ -//! Suspends effectful foreign imports after [`psrs_core::effect::lower_effects`]. -//! -//! A host call whose source type ends in an effect runs inside the closure -//! that lowering produced. `pure`, `bind`, and `runEffect` are already -//! ordinary declarations by the time this split runs. - -use crate::BackendError; -use crate::bindings::ExternalBindings; -use psrs_core::{Binder, Declaration, Expr, ExprKind, Module as CoreModule, TypeId}; -use psrs_hir::{LocalId, SymbolId}; -use psrs_span::TextRange; - -pub(crate) fn lower_effects( - module: &mut CoreModule, - bindings: &mut ExternalBindings, -) -> Result<(), Vec> { - let lowering = psrs_core::effect::lower_effects(module) - .map_err(|errors| verification_errors(module, &errors))?; - let synthesized = lowering.synthesized.to_vec(); - bindings - .imports - .retain(|binding| !synthesized.contains(&binding.symbol)); - suspend_imports(module, bindings) -} - -/// Representation lowering rejects a closure that is not a token closure before -/// closure conversion, so the backend never encodes one. -fn verification_errors( - module: &CoreModule, - errors: &[psrs_core::VerifyError], -) -> Vec { - errors - .iter() - .map(|error| effect_error(module, error.span, error.message)) - .collect() -} - -struct Suspension { - index: usize, - original: SymbolId, - name: String, - span: TextRange, - parameters: Vec, - closure: TypeId, - payload: TypeId, - source: TypeId, -} - -fn suspend_imports( - module: &mut CoreModule, - bindings: &mut ExternalBindings, -) -> Result<(), Vec> { - let mut plans = Vec::new(); - for (index, binding) in bindings.imports.iter().enumerate() { - let Some(source) = binding.type_id else { - continue; - }; - let Some((parameters, closure, payload)) = - psrs_core::effect::suspended_import(module, source) - else { - continue; - }; - let Some(external) = module - .externals - .iter() - .find(|external| external.symbol == binding.symbol) - else { - return Err(vec![effect_error( - module, - binding.span, - "effectful import has no external symbol", - )]); - }; - plans.push(Suspension { - index, - original: binding.symbol, - name: external.name.clone(), - span: binding.span, - parameters, - closure, - payload, - source, - }); - } - for plan in plans { - let host = psrs_core::effect::fresh_foreign_symbol(module); - let host_type = psrs_core::effect::function_type(module, &plan.parameters, plan.payload); - let Some(external) = module - .externals - .iter_mut() - .find(|external| external.symbol == plan.original) - else { - return Err(vec![effect_error( - module, - plan.span, - "effectful import has no external symbol", - )]); - }; - external.symbol = host; - bindings.imports[plan.index].symbol = host; - bindings.imports[plan.index].type_id = Some(host_type); - module - .declarations - .push(wrapper(module, &plan, host, host_type)?); - } - Ok(()) -} - -fn wrapper( - module: &CoreModule, - plan: &Suspension, - host: SymbolId, - host_type: TypeId, -) -> Result> { - let token_ty = psrs_core::closure_parts(&module.types, plan.closure) - .and_then(|(parameters, _)| parameters.first().copied()) - .ok_or_else(|| { - vec![effect_error( - module, - plan.span, - "effect closure is missing its token parameter", - )] - })?; - let mut next_local = psrs_core::effect::fresh_local(module).0; - let mut fresh = || { - let id = LocalId(next_local); - next_local += 1; - id - }; - let binders = plan - .parameters - .iter() - .copied() - .map(|ty| (fresh(), ty)) - .collect::>(); - let mut call = expr(ExprKind::Global(host), host_type, plan.span); - let mut remaining = host_type; - for (local, ty) in &binders { - let result = psrs_core::arrow_parts(&module.types, remaining) - .map(|(_, result)| result) - .unwrap_or(plan.payload); - call = expr( - ExprKind::Application( - Box::new(call), - Box::new(expr(ExprKind::Local(*local), *ty, plan.span)), - ), - result, - plan.span, - ); - remaining = result; - } - let mut arrow_types = Vec::new(); - let mut current = plan.source; - for _ in &plan.parameters { - arrow_types.push(current); - let Some((_, result)) = psrs_core::arrow_parts(&module.types, current) else { - return Err(vec![effect_error( - module, - plan.span, - "effectful import type is not a function of its payload", - )]); - }; - current = result; - } - let token = fresh(); - let mut value = lambda(token, "token", token_ty, call, plan.closure, plan.span); - for (index, (local, ty)) in binders.iter().enumerate().rev() { - value = lambda(*local, "value", *ty, value, arrow_types[index], plan.span); - } - Ok(Declaration { - symbol: plan.original, - name: plan.name.clone(), - name_span: plan.span, - quantified: Vec::new(), - ty: plan.source, - value, - span: plan.span, - }) -} - -fn lambda( - id: LocalId, - name: &str, - ty: TypeId, - body: Expr, - function_ty: TypeId, - span: TextRange, -) -> Expr { - expr( - ExprKind::Lambda { - binder: Binder { - id, - name: name.to_string(), - ty, - span, - }, - body: Box::new(body), - }, - function_ty, - span, - ) -} - -fn expr(kind: ExprKind, ty: TypeId, span: TextRange) -> Expr { - Expr { kind, ty, span } -} - -fn effect_error(module: &CoreModule, span: TextRange, message: &str) -> BackendError { - let error = BackendError::invalid_ir("P8 effect lowering", span, message.to_string()); - match module.entry { - Some(entry) => error.with_module(entry.module), - None => error, - } -} diff --git a/crates/psrs-backend/src/effects/entry.rs b/crates/psrs-backend/src/effects/entry.rs new file mode 100644 index 00000000..8f142d1e --- /dev/null +++ b/crates/psrs-backend/src/effects/entry.rs @@ -0,0 +1,226 @@ +use super::verify::effect_error; +use crate::BackendError; +use psrs_core::{ + Binder, Binding, Declaration, Expr, ExprKind, Module as CoreModule, Type, TypeConstructor, + TypeId, +}; +use psrs_hir::SymbolId; +use psrs_span::TextRange; + +pub(super) fn validate_source( + module: &CoreModule, + trusted: &psrs_core::effect::TrustedEffect, + entry: psrs_core::effect::EffectCommandEntry, +) -> Result<(), Vec> { + let Some(main) = module + .declarations + .iter() + .find(|declaration| declaration.symbol == entry.symbol) + else { + return Err(vec![effect_error( + module, + module.span, + "Effect command entry has no source declaration", + )]); + }; + if !main.quantified.is_empty() + || psrs_core::effect::effect_application(module, main.ty, trusted.effect_type) + .is_none_or(|(_, payload)| !is_unit(module, payload)) + { + return Err(vec![effect_error( + module, + main.name_span, + "Effect command entry must have type Effect Unit", + )]); + } + Ok(()) +} + +pub(super) fn install( + module: &mut CoreModule, + trusted: &psrs_core::effect::TrustedEffect, + entry: psrs_core::effect::EffectCommandEntry, +) -> Result<(), Vec> { + let Some(main) = module + .declarations + .iter() + .find(|declaration| declaration.symbol == entry.symbol) + .cloned() + else { + return Err(vec![effect_error( + module, + module.span, + "Effect command entry has no source declaration", + )]); + }; + let Some((token_parameters, unit)) = psrs_core::closure_parts(&module.types, main.ty) else { + return Err(vec![effect_error( + module, + main.name_span, + "lowered Effect command entry is not an ordinary token closure", + )]); + }; + if token_parameters.len() != 1 || !is_unit(module, unit) { + return Err(vec![effect_error( + module, + main.name_span, + "lowered Effect command entry must take one token and return Unit", + )]); + } + let Some(run) = trusted + .operations + .iter() + .find(|operation| operation.operation == psrs_core::effect::EffectOperation::Run) + .map(|operation| operation.symbol) + else { + return Err(vec![effect_error( + module, + main.name_span, + "trusted runEffect operation is missing from the Effect contract", + )]); + }; + if !module + .declarations + .iter() + .any(|declaration| declaration.symbol == run) + { + return Err(vec![effect_error( + module, + main.name_span, + "trusted runEffect operation was not lowered", + )]); + } + let int = intern(module, Type::Constructor(TypeConstructor::Int)); + let run_type = psrs_core::effect::function_type(module, &[main.ty], unit); + let result_local = psrs_core::effect::fresh_local(module); + let binder = Binder { + id: result_local, + name: "effectResult".to_string(), + ty: unit, + span: main.name_span, + }; + let run_action = expr( + ExprKind::Application( + Box::new(expr(ExprKind::Global(run), run_type, main.name_span)), + Box::new(expr( + ExprKind::Global(entry.symbol), + main.ty, + main.name_span, + )), + ), + unit, + main.name_span, + ); + let value = expr( + ExprKind::Let { + bindings: vec![Binding { + binder, + quantified: Vec::new(), + value: run_action, + span: main.name_span, + }], + body: Box::new(expr(ExprKind::Integer(0), int, main.name_span)), + }, + int, + main.name_span, + ); + let symbol = fresh_entry_symbol(module, main.symbol.module); + module.declarations.push(Declaration { + symbol, + name: "psrs.command-entry".to_string(), + name_span: main.name_span, + quantified: Vec::new(), + ty: int, + value, + span: main.span, + }); + module.entry = Some(symbol); + if !valid_wrapper(module, symbol, entry.symbol, run, unit, int) { + return Err(vec![effect_error( + module, + main.name_span, + "generated Effect command entry does not run the selected action exactly once", + )]); + } + Ok(()) +} + +fn valid_wrapper( + module: &CoreModule, + wrapper_symbol: SymbolId, + source: SymbolId, + run: SymbolId, + unit: TypeId, + int: TypeId, +) -> bool { + let Some(wrapper) = module + .declarations + .iter() + .find(|declaration| declaration.symbol == wrapper_symbol) + else { + return false; + }; + if wrapper.ty != int || !wrapper.quantified.is_empty() { + return false; + } + let ExprKind::Let { bindings, body } = &wrapper.value.kind else { + return false; + }; + if bindings.len() != 1 || bindings[0].binder.ty != unit || bindings[0].value.ty != unit { + return false; + } + let ExprKind::Application(function, action) = &bindings[0].value.kind else { + return false; + }; + if !matches!(function.kind, ExprKind::Global(symbol) if symbol == run) + || !matches!(action.kind, ExprKind::Global(symbol) if symbol == source) + { + return false; + } + matches!(body.kind, ExprKind::Integer(0)) && body.ty == int +} + +fn is_unit(module: &CoreModule, ty: TypeId) -> bool { + matches!( + module.types.get(ty.0 as usize), + Some(Type::Constructor(TypeConstructor::Unit)) + ) +} + +fn intern(module: &mut CoreModule, ty: Type) -> TypeId { + if let Some(index) = module.types.iter().position(|current| current == &ty) { + TypeId(index as u32) + } else { + module.types.push(ty); + TypeId((module.types.len() - 1) as u32) + } +} + +fn fresh_entry_symbol(module: &CoreModule, owner: psrs_hir::ModuleId) -> SymbolId { + let next = module + .declarations + .iter() + .filter(|declaration| declaration.symbol.module == owner) + .map(|declaration| declaration.symbol.index) + .chain( + module + .externals + .iter() + .filter(|external| external.symbol.module == owner) + .map(|external| external.symbol.index), + ) + .chain( + module + .constructors + .iter() + .filter(|constructor| constructor.symbol.module == owner) + .map(|constructor| constructor.symbol.index), + ) + .max() + .map_or(0, |index| index.saturating_add(1)); + SymbolId::new(owner, next) +} + +fn expr(kind: ExprKind, ty: TypeId, span: TextRange) -> Expr { + Expr { kind, ty, span } +} diff --git a/crates/psrs-backend/src/effects/mod.rs b/crates/psrs-backend/src/effects/mod.rs new file mode 100644 index 00000000..720c09a1 --- /dev/null +++ b/crates/psrs-backend/src/effects/mod.rs @@ -0,0 +1,87 @@ +//! Effect lowering coordinator. Abstract identities and the import plan are +//! checked before the Core type table erases `Effect` applications. + +mod entry; +mod suspension; +mod verify; + +use crate::BackendError; +use crate::bindings::ExternalBindings; +use psrs_core::{Module as CoreModule, effect::EffectCompilation}; + +pub(crate) fn lower_effects( + module: &mut CoreModule, + bindings: &mut ExternalBindings, + context: &EffectCompilation, +) -> Result<(), Vec> { + verify::trusted_contract(module, bindings, &context.trusted)?; + validate_entry_context(module, context)?; + let suspensions = suspension::plan(module, bindings, &context.trusted)?; + let lowering = psrs_core::effect::lower_effects(module, &context.trusted) + .map_err(|errors| verify::verification_errors(&errors))?; + + let applied = suspension::apply(module, bindings, &suspensions)?; + if let Some(entry) = context.command_entry { + entry::install(module, &context.trusted, entry)?; + } + + lowering + .verify(module) + .map_err(|errors| verify::verification_errors(&errors))?; + if let Err(errors) = module.verify() { + return Err(verify::verification_errors(&errors)); + } + suspension::verify(module, bindings, &suspensions, &applied)?; + let synthesized = lowering.synthesized.to_vec(); + bindings + .imports + .retain(|binding| !synthesized.contains(&binding.symbol)); + Ok(()) +} + +fn validate_entry_context( + module: &CoreModule, + context: &EffectCompilation, +) -> Result<(), Vec> { + let selected = module.entry; + match (selected, context.command_entry) { + (Some(selected), Some(entry)) if selected != entry.symbol => { + Err(vec![verify::effect_error( + module, + module.span, + "Effect command entry does not match the selected source entry", + )]) + } + (Some(_), Some(entry)) => entry::validate_source(module, &context.trusted, entry), + (Some(selected), None) => { + let Some(declaration) = module + .declarations + .iter() + .find(|declaration| declaration.symbol == selected) + else { + return Ok(()); + }; + if psrs_core::effect::effect_application( + module, + declaration.ty, + context.trusted.effect_type, + ) + .is_some() + { + Err(vec![verify::effect_error( + module, + declaration.name_span, + "missing Effect command entry metadata for the selected source entry", + )]) + } else { + Ok(()) + } + } + (None, Some(_)) => Err(vec![verify::effect_error( + module, + module.span, + "Effect command entry metadata has no selected source entry", + )]), + (None, None) => Ok(()), + } +} diff --git a/crates/psrs-backend/src/effects/suspension.rs b/crates/psrs-backend/src/effects/suspension.rs new file mode 100644 index 00000000..339d312a --- /dev/null +++ b/crates/psrs-backend/src/effects/suspension.rs @@ -0,0 +1,462 @@ +use super::verify::{effect_error, source_effect_error}; +use crate::BackendError; +use crate::bindings::ExternalBindings; +use psrs_core::{ + Binder, Declaration, Expr, ExprKind, Module as CoreModule, Type, TypeId, closure_parts, +}; +use psrs_hir::{LocalId, ModuleId, SymbolId, TypeVariableId}; +use psrs_span::TextRange; + +#[derive(Clone, Debug, PartialEq, Eq)] +pub(super) struct SuspensionPlan { + index: usize, + original: SymbolId, + source_module: ModuleId, + name: String, + span: TextRange, + source: TypeId, + source_body: TypeId, + quantified: Vec, + parameters: Vec, + application: TypeId, + payload: TypeId, +} + +#[derive(Clone, Debug)] +pub(super) struct AppliedSuspension { + plan: SuspensionPlan, + host: SymbolId, + host_type: TypeId, +} + +fn import_error(module: &CoreModule, plan: &SuspensionPlan, message: &str) -> BackendError { + source_effect_error(module, plan.source_module, plan.span, message) +} + +pub(super) fn plan( + module: &CoreModule, + bindings: &ExternalBindings, + trusted: &psrs_core::effect::TrustedEffect, +) -> Result, Vec> { + let mut plans = Vec::new(); + let operation_symbols = trusted + .operations + .iter() + .map(|operation| operation.symbol) + .collect::>(); + for (index, binding) in bindings.imports.iter().enumerate() { + if operation_symbols.contains(&binding.symbol) { + continue; + } + let Some(source) = binding.type_id else { + continue; + }; + let shape = psrs_core::effect::classify_effect_import(module, source, trusted.effect_type) + .map_err(|message| { + vec![source_effect_error( + module, + binding.source_module, + binding.span, + message, + )] + })?; + let Some(shape) = shape else { + continue; + }; + let Some(external) = module + .externals + .iter() + .find(|external| external.symbol == binding.symbol) + else { + return Err(vec![source_effect_error( + module, + binding.source_module, + binding.span, + "effectful import has no external symbol", + )]); + }; + let source_body = strip_foralls(module, source).ok_or_else(|| { + vec![source_effect_error( + module, + binding.source_module, + binding.span, + "effectful import has an invalid quantified type", + )] + })?; + plans.push(SuspensionPlan { + index, + original: binding.symbol, + source_module: binding.source_module, + name: external.name.clone(), + span: binding.span, + source, + source_body, + quantified: shape.quantified, + parameters: shape.parameters, + application: shape.application, + payload: shape.payload, + }); + } + Ok(plans) +} + +pub(super) fn apply( + module: &mut CoreModule, + bindings: &mut ExternalBindings, + plans: &[SuspensionPlan], +) -> Result, Vec> { + let mut applied = Vec::with_capacity(plans.len()); + for plan in plans { + let Some(binding) = bindings.imports.get(plan.index) else { + return Err(vec![import_error( + module, + plan, + "effect import plan no longer names an external binding", + )]); + }; + if binding.symbol != plan.original + || binding.source_module != plan.source_module + || binding.type_id != Some(plan.source) + { + return Err(vec![import_error( + module, + plan, + "effect import plan no longer matches its source binding", + )]); + } + let Some((parameters, payload)) = closure_parts(&module.types, plan.application) else { + return Err(vec![import_error( + module, + plan, + "planned Effect result was not lowered to a closure", + )]); + }; + if parameters.len() != 1 || payload != plan.payload { + return Err(vec![import_error( + module, + plan, + "planned Effect result has an invalid token closure shape", + )]); + } + let token = parameters[0]; + let host = psrs_core::effect::fresh_foreign_symbol(module); + let host_body = psrs_core::effect::function_type(module, &plan.parameters, plan.payload); + let host_type = quantify(module, &plan.quantified, host_body); + let Some(external) = module + .externals + .iter_mut() + .find(|external| external.symbol == plan.original) + else { + return Err(vec![import_error( + module, + plan, + "effectful import has no external symbol", + )]); + }; + external.symbol = host; + let Some(external_type) = module + .external_types + .iter_mut() + .find(|external| external.symbol == plan.original) + else { + return Err(vec![import_error( + module, + plan, + "effectful import has no checked source signature", + )]); + }; + external_type.symbol = host; + external_type.ty = host_type; + bindings.imports[plan.index].symbol = host; + bindings.imports[plan.index].type_id = Some(host_type); + let wrapper = build_wrapper(module, plan, host, host_body, token)?; + module.declarations.push(wrapper); + applied.push(AppliedSuspension { + plan: plan.clone(), + host, + host_type, + }); + } + Ok(applied) +} + +pub(super) fn verify( + module: &CoreModule, + bindings: &ExternalBindings, + plans: &[SuspensionPlan], + applied: &[AppliedSuspension], +) -> Result<(), Vec> { + if plans.len() != applied.len() { + return Err(vec![effect_error( + module, + module.span, + "effect import plan and wrapper counts differ", + )]); + } + for (plan, applied) in plans.iter().zip(applied) { + if &applied.plan != plan { + return Err(vec![import_error( + module, + plan, + "effect import wrapper was built from different lowering evidence", + )]); + } + let Some(binding) = bindings.imports.get(plan.index) else { + return Err(vec![import_error( + module, + plan, + "effect wrapper has no host binding", + )]); + }; + if binding.symbol != applied.host + || binding.source_module != plan.source_module + || binding.type_id != Some(applied.host_type) + { + return Err(vec![import_error( + module, + plan, + "effect wrapper and host binding signatures differ", + )]); + } + let Some(host_external) = module + .externals + .iter() + .find(|external| external.symbol == applied.host) + else { + return Err(vec![import_error( + module, + plan, + "effect wrapper host import is missing", + )]); + }; + if host_external.signature.is_none() { + return Err(vec![import_error( + module, + plan, + "effect wrapper host import has no source signature", + )]); + } + let Some(wrapper) = module + .declarations + .iter() + .find(|declaration| declaration.symbol == plan.original) + else { + return Err(vec![import_error( + module, + plan, + "effect import wrapper declaration is missing", + )]); + }; + if wrapper.ty != plan.source_body + || wrapper.quantified != plan.quantified + || !wrapper_matches(module, wrapper, plan, applied.host) + { + return Err(vec![import_error( + module, + plan, + "effect import wrapper does not preserve its planned signature and suspension", + )]); + } + let Some((token_parameters, result)) = closure_parts(&module.types, plan.application) + else { + return Err(vec![import_error( + module, + plan, + "planned Effect result is no longer a closure", + )]); + }; + if token_parameters.len() != 1 || result != plan.payload { + return Err(vec![import_error( + module, + plan, + "planned Effect result no longer matches its recorded payload", + )]); + } + } + Ok(()) +} + +fn build_wrapper( + module: &CoreModule, + plan: &SuspensionPlan, + host: SymbolId, + host_body: TypeId, + token: TypeId, +) -> Result> { + let mut next_local = psrs_core::effect::fresh_local(module).0; + let mut fresh = || { + let id = LocalId(next_local); + next_local += 1; + id + }; + let binders = plan + .parameters + .iter() + .copied() + .map(|ty| (fresh(), ty)) + .collect::>(); + let mut call = expr(ExprKind::Global(host), host_body, plan.span); + let mut remaining = host_body; + for (local, ty) in &binders { + let Some((_, result)) = psrs_core::arrow_parts(&module.types, remaining) else { + return Err(vec![import_error( + module, + plan, + "planned host import type has fewer arguments than its source binding", + )]); + }; + call = expr( + ExprKind::Application( + Box::new(call), + Box::new(expr(ExprKind::Local(*local), *ty, plan.span)), + ), + result, + plan.span, + ); + remaining = result; + } + if remaining != plan.payload { + return Err(vec![import_error( + module, + plan, + "planned host import result differs from its Effect payload", + )]); + } + let mut arrow_types = Vec::new(); + let mut current = plan.source_body; + for _ in &plan.parameters { + arrow_types.push(current); + let Some((_, result)) = psrs_core::arrow_parts(&module.types, current) else { + return Err(vec![import_error( + module, + plan, + "effectful import type is not a function of its planned payload", + )]); + }; + current = result; + } + if current != plan.application { + return Err(vec![import_error( + module, + plan, + "effect import source signature changed after planning", + )]); + } + let token_local = fresh(); + let mut value = lambda( + token_local, + "token", + token, + call, + plan.application, + plan.span, + ); + for (index, (local, ty)) in binders.iter().enumerate().rev() { + value = lambda(*local, "value", *ty, value, arrow_types[index], plan.span); + } + Ok(Declaration { + symbol: plan.original, + name: plan.name.clone(), + name_span: plan.span, + quantified: plan.quantified.clone(), + ty: plan.source_body, + value, + span: plan.span, + }) +} + +fn wrapper_matches( + module: &CoreModule, + wrapper: &Declaration, + plan: &SuspensionPlan, + host: SymbolId, +) -> bool { + let mut expression = &wrapper.value; + let mut locals = Vec::with_capacity(plan.parameters.len() + 1); + for parameter in &plan.parameters { + let ExprKind::Lambda { binder, body } = &expression.kind else { + return false; + }; + if binder.ty != *parameter { + return false; + } + locals.push(binder.id); + expression = body; + } + let ExprKind::Lambda { binder, body } = &expression.kind else { + return false; + }; + let Some((tokens, result)) = closure_parts(&module.types, plan.application) else { + return false; + }; + if tokens != [binder.ty] || result != plan.payload || expression.ty != plan.application { + return false; + } + locals.push(binder.id); + let mut call = body.as_ref(); + for local in locals.iter().take(plan.parameters.len()).rev() { + let ExprKind::Application(function, argument) = &call.kind else { + return false; + }; + if !matches!(argument.kind, ExprKind::Local(id) if id == *local) { + return false; + } + call = function; + } + matches!(call.kind, ExprKind::Global(symbol) if symbol == host) +} + +fn strip_foralls(module: &CoreModule, mut ty: TypeId) -> Option { + let mut remaining = module.types.len(); + while let Some(Type::ForAll { body, .. }) = module.types.get(ty.0 as usize) { + if remaining == 0 { + return None; + } + remaining -= 1; + ty = *body; + } + Some(ty) +} + +fn quantify(module: &mut CoreModule, variables: &[TypeVariableId], body: TypeId) -> TypeId { + if variables.is_empty() { + return body; + } + let ty = Type::ForAll { + variables: variables.to_vec(), + body, + }; + if let Some(index) = module.types.iter().position(|candidate| candidate == &ty) { + TypeId(index as u32) + } else { + module.types.push(ty); + TypeId((module.types.len() - 1) as u32) + } +} + +fn lambda( + id: LocalId, + name: &str, + ty: TypeId, + body: Expr, + function_ty: TypeId, + span: TextRange, +) -> Expr { + expr( + ExprKind::Lambda { + binder: Binder { + id, + name: name.to_string(), + ty, + span, + }, + body: Box::new(body), + }, + function_ty, + span, + ) +} + +fn expr(kind: ExprKind, ty: TypeId, span: TextRange) -> Expr { + Expr { kind, ty, span } +} diff --git a/crates/psrs-backend/src/effects/verify.rs b/crates/psrs-backend/src/effects/verify.rs new file mode 100644 index 00000000..af89e06d --- /dev/null +++ b/crates/psrs-backend/src/effects/verify.rs @@ -0,0 +1,277 @@ +use crate::BackendError; +use crate::bindings::ExternalBindings; +use psrs_core::{Module as CoreModule, Type, TypeConstructor}; +use psrs_hir::{ExternalKind, TypeId as HirTypeId, TypeVariableId}; +use psrs_span::TextRange; +use std::collections::HashSet; + +const EFFECT_INTERFACE: &str = "psrs:effect"; + +pub(super) fn trusted_contract( + module: &CoreModule, + bindings: &ExternalBindings, + trusted: &psrs_core::effect::TrustedEffect, +) -> Result<(), Vec> { + if !module.opaque_ids.contains(&trusted.effect_type) + || !module.types.iter().any(|ty| { + matches!(ty, Type::Constructor(TypeConstructor::User(id)) if *id == trusted.effect_type) + }) + { + return Err(vec![effect_error( + module, + module.span, + "trusted Effect identity is missing or is not an opaque type", + )]); + } + let mut symbols = HashSet::new(); + let mut operations = HashSet::new(); + for operation in &trusted.operations { + if !symbols.insert(operation.symbol) || !operations.insert(operation.operation) { + return Err(vec![effect_error( + module, + module.span, + "trusted Effect operation bindings are duplicated", + )]); + } + let Some(external) = module + .externals + .iter() + .find(|external| external.symbol == operation.symbol) + else { + return Err(vec![effect_error( + module, + module.span, + "trusted Effect operation binding has no external declaration", + )]); + }; + let expected = operation.operation.wit_function(); + if !matches!( + &external.kind, + ExternalKind::Wit { interface, function } + if interface == EFFECT_INTERFACE && function == expected + ) { + return Err(vec![source_effect_error( + module, + external_source_module(module, operation.symbol), + external + .signature + .as_ref() + .map_or(module.span, |ty| ty.span), + "trusted Effect operation identity does not match its WIT binding", + )]); + } + let Some(binding) = bindings + .imports + .iter() + .find(|binding| binding.symbol == operation.symbol) + else { + return Err(vec![source_effect_error( + module, + external_source_module(module, operation.symbol), + external + .signature + .as_ref() + .map_or(module.span, |ty| ty.span), + "trusted Effect operation has no external binding metadata", + )]); + }; + let Some(signature) = binding.type_id else { + return Err(vec![source_effect_error( + module, + binding.source_module, + binding.span, + "trusted Effect operation has no checked source signature", + )]); + }; + if !valid_core_operation_signature( + module, + signature, + trusted.effect_type, + operation.operation, + ) { + return Err(vec![source_effect_error( + module, + binding.source_module, + binding.span, + &format!( + "trusted Effect operation `{expected}` has an invalid checked source signature" + ), + )]); + } + } + if [ + psrs_core::effect::EffectOperation::Pure, + psrs_core::effect::EffectOperation::Bind, + psrs_core::effect::EffectOperation::Run, + psrs_core::effect::EffectOperation::Trap, + ] + .into_iter() + .any(|required| !operations.contains(&required)) + { + return Err(vec![effect_error( + module, + module.span, + "trusted Effect contract is missing a required operation binding", + )]); + } + for external in &module.externals { + if matches!( + &external.kind, + ExternalKind::Wit { interface, .. } if interface == EFFECT_INTERFACE + ) && !symbols.contains(&external.symbol) + { + return Err(vec![source_effect_error( + module, + external_source_module(module, external.symbol), + external + .signature + .as_ref() + .map_or(module.span, |ty| ty.span), + "Effect WIT import is missing from the trusted operation bindings", + )]); + } + } + Ok(()) +} + +fn valid_core_operation_signature( + module: &CoreModule, + ty: psrs_core::TypeId, + effect: HirTypeId, + operation: psrs_core::effect::EffectOperation, +) -> bool { + let Some((variables, parameters, result)) = core_function_signature(module, ty) else { + return false; + }; + match operation { + psrs_core::effect::EffectOperation::Pure => { + variables.len() == 1 + && parameters.len() == 1 + && core_variable(module, parameters[0]) == Some(variables[0]) + && core_effect_payload(module, result, effect) + .is_some_and(|payload| core_variable(module, payload) == Some(variables[0])) + } + psrs_core::effect::EffectOperation::Bind => { + if variables.len() != 2 || parameters.len() != 2 { + return false; + } + let first = core_effect_payload(module, parameters[0], effect); + let continuation = psrs_core::arrow_parts(&module.types, parameters[1]); + let result = core_effect_payload(module, result, effect); + matches!((first, continuation, result), + (Some(first), Some((input, output)), Some(output_result)) + if core_variable(module, first) == Some(variables[0]) + && core_variable(module, input) == Some(variables[0]) + && core_effect_payload(module, output, effect) + .is_some_and(|payload| core_variable(module, payload) == Some(variables[1])) + && core_variable(module, output_result) == Some(variables[1])) + } + psrs_core::effect::EffectOperation::Run => { + variables.len() == 1 + && parameters.len() == 1 + && core_effect_payload(module, parameters[0], effect) + .is_some_and(|payload| core_variable(module, payload) == Some(variables[0])) + && core_variable(module, result) == Some(variables[0]) + } + psrs_core::effect::EffectOperation::Trap => { + parameters.is_empty() + && variables.is_empty() + && core_effect_payload(module, result, effect).is_some_and(|payload| { + matches!( + module.types.get(payload.0 as usize), + Some(Type::Constructor(TypeConstructor::Unit)) + ) + }) + } + } +} + +fn core_function_signature( + module: &CoreModule, + ty: psrs_core::TypeId, +) -> Option<( + Vec, + Vec, + psrs_core::TypeId, +)> { + let mut quantified = Vec::new(); + let mut body = ty; + let mut seen = HashSet::new(); + while seen.insert(body) { + let Some((variables, inner)) = psrs_core::forall_parts(&module.types, body) else { + break; + }; + quantified.extend_from_slice(variables); + body = inner; + } + if !seen.insert(body) && psrs_core::forall_parts(&module.types, body).is_some() { + return None; + } + let mut parameters = Vec::new(); + let mut arrow_seen = HashSet::new(); + loop { + if !arrow_seen.insert(body) { + return None; + } + let Some((parameter, result)) = psrs_core::arrow_parts(&module.types, body) else { + break; + }; + parameters.push(parameter); + body = result; + } + Some((quantified, parameters, body)) +} + +fn core_variable(module: &CoreModule, ty: psrs_core::TypeId) -> Option { + match module.types.get(ty.0 as usize) { + Some(Type::Variable(variable)) => Some(*variable), + _ => None, + } +} + +fn core_effect_payload( + module: &CoreModule, + ty: psrs_core::TypeId, + effect: HirTypeId, +) -> Option { + psrs_core::effect::effect_application(module, ty, effect).map(|(_, payload)| payload) +} + +pub(super) fn verification_errors(errors: &[psrs_core::VerifyError]) -> Vec { + errors + .iter() + .map(|error| { + BackendError::invalid_ir("P8 effect lowering", error.span, error.message.to_string()) + .with_module(error.module) + }) + .collect() +} + +pub(super) fn effect_error(module: &CoreModule, span: TextRange, message: &str) -> BackendError { + let error = BackendError::invalid_ir("P8 effect lowering", span, message.to_string()); + match module.entry { + Some(entry) => error.with_module(entry.module), + None => error, + } +} + +pub(super) fn source_effect_error( + _module: &CoreModule, + source_module: psrs_hir::ModuleId, + span: TextRange, + message: &str, +) -> BackendError { + BackendError::invalid_ir("P8 effect lowering", span, message.to_string()) + .with_module(source_module) +} + +pub(super) fn external_source_module( + module: &CoreModule, + symbol: psrs_hir::SymbolId, +) -> psrs_hir::ModuleId { + module + .external_types + .iter() + .find(|external| external.symbol == symbol) + .map_or(module.id, |external| external.source_module) +} diff --git a/crates/psrs-backend/src/lib.rs b/crates/psrs-backend/src/lib.rs index b8db9bef..40629f36 100644 --- a/crates/psrs-backend/src/lib.rs +++ b/crates/psrs-backend/src/lib.rs @@ -126,6 +126,32 @@ pub fn compile(module: psrs_core::Module) -> Result> Ok(compile_with_stages(module)?.artifact) } +/// Compiles linked Core using the trusted Effect identities issued by the +/// driver. Core-only callers that do not provide this contract receive no +/// library-specific Effect lowering. +pub fn compile_with_effect_context( + module: psrs_core::Module, + effect_context: psrs_core::effect::EffectCompilation, +) -> Result> { + Ok(compile_with_context(module, Some(effect_context), TargetCapabilities::default())?.artifact) +} + +/// Lowers Core to CC after applying an explicit Effect contract. +/// +/// Callers that already removed trusted Effect imports, or that have no +/// trusted contract, pass `None` and get the same binding extraction as +/// [`cc::lower_module`]. +pub fn lower_cc_with_context( + mut module: psrs_core::Module, + effect_context: Option<&psrs_core::effect::EffectCompilation>, +) -> Result> { + let mut external_bindings = ExternalBindings::from_core(&module); + if let Some(context) = effect_context { + effects::lower_effects(&mut module, &mut external_bindings, context)?; + } + cc::lower_module_with_bindings(module, external_bindings) +} + /// The default-profile validator, retained for backend unit tests. #[allow(dead_code)] pub(crate) fn validator() -> wasmparser::Validator { @@ -144,6 +170,8 @@ pub(crate) fn validator_for(target: TargetCapabilities) -> wasmparser::Validator pub struct Stages { /// Verified Typed Core after P7 and before P8. pub core: psrs_core::Module, + /// The explicit trusted Effect context needed to compile `core` again. + pub effect_context: Option, pub cc: cc::Module, pub mir: mir::Module, pub wasm: wasm::Module, @@ -158,6 +186,14 @@ pub fn compile_with_stages(module: psrs_core::Module) -> Result Result> { + compile_with_context(module, None, target) +} + +pub fn compile_with_context( + module: psrs_core::Module, + effect_context: Option, + target: TargetCapabilities, ) -> Result> { let owner = module.entry.map(|entry| entry.module); let mut module = @@ -167,14 +203,17 @@ pub fn compile_with_target( .into_iter() .map(|error| { BackendError::new("P7 Core optimization", error.span, error.message) + .with_module(error.module) }) .collect(), owner, ) })?; let optimized_core = module.clone(); - let mut external_bindings = ExternalBindings::from_core(&mut module); - effects::lower_effects(&mut module, &mut external_bindings)?; + let mut external_bindings = ExternalBindings::from_core(&module); + if let Some(context) = effect_context.as_ref() { + effects::lower_effects(&mut module, &mut external_bindings, context)?; + } external_bindings.validate_conformance(&module, target)?; let lowered_cc = cc::lower_module_with_bindings(module, external_bindings)?; let cc = lowered_cc.cc; @@ -238,6 +277,7 @@ pub fn compile_with_target( })?; Ok(Stages { core: optimized_core, + effect_context, cc, mir, wasm, diff --git a/crates/psrs-backend/src/mir/binding_tests.rs b/crates/psrs-backend/src/mir/binding_tests.rs index 889dbaf1..7e0ae893 100644 --- a/crates/psrs-backend/src/mir/binding_tests.rs +++ b/crates/psrs-backend/src/mir/binding_tests.rs @@ -56,6 +56,7 @@ fn input(call: bool) -> (cc::Module, ExternalBindings) { let bindings = ExternalBindings { imports: vec![ExternalBinding { symbol: external, + source_module: ModuleId(0), interface: crate::abi::names::STDOUT.into(), function: crate::abi::names::GET_STDOUT.into(), type_id: None, @@ -164,6 +165,7 @@ fn p9_exposes_an_owned_handle_without_dropping_it() { let bindings = ExternalBindings { imports: vec![ExternalBinding { symbol: external, + source_module: ModuleId(0), interface: crate::abi::names::STDOUT.into(), function: crate::abi::names::GET_STDOUT.into(), type_id: None, diff --git a/crates/psrs-backend/src/mir/gc_tests/rank_n/mod.rs b/crates/psrs-backend/src/mir/gc_tests/rank_n/mod.rs index 861d3da1..e8f86558 100644 --- a/crates/psrs-backend/src/mir/gc_tests/rank_n/mod.rs +++ b/crates/psrs-backend/src/mir/gc_tests/rank_n/mod.rs @@ -387,6 +387,7 @@ pub(super) fn module(types: Vec, declarations: Vec, entry: Sy id: entry.module, name: "RankNBackendTest".into(), externals: Vec::new(), + external_types: Vec::new(), types, newtype_ids: Vec::new(), opaque_ids: Vec::new(), diff --git a/crates/psrs-backend/src/mir/indirect_tests/aggregate/collections.rs b/crates/psrs-backend/src/mir/indirect_tests/aggregate/collections.rs index a3326573..991932dd 100644 --- a/crates/psrs-backend/src/mir/indirect_tests/aggregate/collections.rs +++ b/crates/psrs-backend/src/mir/indirect_tests/aggregate/collections.rs @@ -102,6 +102,7 @@ fn base( let bindings = ExternalBindings { imports: vec![ExternalBinding { symbol: external_symbol, + source_module: ModuleId(0), interface: "wasi:io/streams".into(), function: function.into(), type_id: None, diff --git a/crates/psrs-backend/src/mir/indirect_tests/aggregate/fixtures.rs b/crates/psrs-backend/src/mir/indirect_tests/aggregate/fixtures.rs index bde23029..51302b74 100644 --- a/crates/psrs-backend/src/mir/indirect_tests/aggregate/fixtures.rs +++ b/crates/psrs-backend/src/mir/indirect_tests/aggregate/fixtures.rs @@ -134,6 +134,7 @@ pub(super) fn fixture_with_representations( let bindings = ExternalBindings { imports: vec![ExternalBinding { symbol: external_symbol, + source_module: ModuleId(0), interface: "wasi:io/streams".into(), function: function.into(), type_id: None, @@ -270,6 +271,7 @@ pub(super) fn parameter_fixture() -> (cc::Module, ExternalBindings, Resolve) { let bindings = ExternalBindings { imports: vec![ExternalBinding { symbol: external_symbol, + source_module: ModuleId(0), interface: "wasi:io/streams".into(), function: "take".into(), type_id: None, diff --git a/crates/psrs-backend/src/mir/indirect_tests/aggregate/indirect.rs b/crates/psrs-backend/src/mir/indirect_tests/aggregate/indirect.rs index 8c210917..be513667 100644 --- a/crates/psrs-backend/src/mir/indirect_tests/aggregate/indirect.rs +++ b/crates/psrs-backend/src/mir/indirect_tests/aggregate/indirect.rs @@ -163,6 +163,7 @@ pub(super) fn indirect_aggregate_fixture() -> (cc::Module, ExternalBindings, Res let bindings = ExternalBindings { imports: vec![ExternalBinding { symbol: external_symbol, + source_module: ModuleId(0), interface: "wasi:io/streams".into(), function: "take".into(), type_id: None, diff --git a/crates/psrs-backend/src/mir/indirect_tests/aggregate/large.rs b/crates/psrs-backend/src/mir/indirect_tests/aggregate/large.rs index 6479798c..4cae5c7c 100644 --- a/crates/psrs-backend/src/mir/indirect_tests/aggregate/large.rs +++ b/crates/psrs-backend/src/mir/indirect_tests/aggregate/large.rs @@ -110,6 +110,7 @@ pub(super) fn large_record_fixture() -> (cc::Module, ExternalBindings, Resolve) let bindings = ExternalBindings { imports: vec![ExternalBinding { symbol: external_symbol, + source_module: ModuleId(0), interface: "wasi:io/streams".into(), function: "get".into(), type_id: None, @@ -215,6 +216,7 @@ pub(super) fn large_unit_result_fixture() -> (cc::Module, ExternalBindings, Reso let bindings = ExternalBindings { imports: vec![ExternalBinding { symbol: external_symbol, + source_module: ModuleId(0), interface: "wasi:io/streams".into(), function: "get".into(), type_id: None, diff --git a/crates/psrs-backend/src/mir/indirect_tests/aggregate/list_record.rs b/crates/psrs-backend/src/mir/indirect_tests/aggregate/list_record.rs index d97b8100..0f4c1557 100644 --- a/crates/psrs-backend/src/mir/indirect_tests/aggregate/list_record.rs +++ b/crates/psrs-backend/src/mir/indirect_tests/aggregate/list_record.rs @@ -87,6 +87,7 @@ fn finish( let bindings = ExternalBindings { imports: vec![ExternalBinding { symbol: external_symbol, + source_module: ModuleId(0), interface: "wasi:io/streams".into(), function: "get".into(), type_id: None, diff --git a/crates/psrs-backend/src/mir/indirect_tests/aggregate/nested.rs b/crates/psrs-backend/src/mir/indirect_tests/aggregate/nested.rs index e23e963b..cd719ede 100644 --- a/crates/psrs-backend/src/mir/indirect_tests/aggregate/nested.rs +++ b/crates/psrs-backend/src/mir/indirect_tests/aggregate/nested.rs @@ -117,6 +117,7 @@ pub(super) fn nested_variant_fixture() -> (cc::Module, ExternalBindings, Resolve let bindings = ExternalBindings { imports: vec![ExternalBinding { symbol: external_symbol, + source_module: ModuleId(0), interface: "wasi:io/streams".into(), function: "get".into(), type_id: None, @@ -222,6 +223,7 @@ pub(super) fn nested_record_fixture() -> (cc::Module, ExternalBindings, Resolve) let bindings = ExternalBindings { imports: vec![ExternalBinding { symbol: external_symbol, + source_module: ModuleId(0), interface: "wasi:io/streams".into(), function: "get".into(), type_id: None, @@ -380,6 +382,7 @@ pub(super) fn nested_record_parameter_fixture() -> (cc::Module, ExternalBindings let bindings = ExternalBindings { imports: vec![ExternalBinding { symbol: external_symbol, + source_module: ModuleId(0), interface: "wasi:io/streams".into(), function: "take".into(), type_id: None, diff --git a/crates/psrs-backend/src/mir/indirect_tests/aggregate/record_fields.rs b/crates/psrs-backend/src/mir/indirect_tests/aggregate/record_fields.rs index 1856639b..cb7ab113 100644 --- a/crates/psrs-backend/src/mir/indirect_tests/aggregate/record_fields.rs +++ b/crates/psrs-backend/src/mir/indirect_tests/aggregate/record_fields.rs @@ -125,6 +125,7 @@ pub(super) fn record_with_aggregate_field_fixture() -> (cc::Module, ExternalBind let bindings = ExternalBindings { imports: vec![ExternalBinding { symbol: external_symbol, + source_module: ModuleId(0), interface: "wasi:io/streams".into(), function: "get".into(), type_id: None, @@ -348,6 +349,7 @@ pub(super) fn record_with_aggregate_field_parameter_fixture() let bindings = ExternalBindings { imports: vec![ExternalBinding { symbol: external_symbol, + source_module: ModuleId(0), interface: "wasi:io/streams".into(), function: "take".into(), type_id: None, diff --git a/crates/psrs-backend/src/mir/indirect_tests/aggregate/resource_result.rs b/crates/psrs-backend/src/mir/indirect_tests/aggregate/resource_result.rs index 39795612..4ccfb193 100644 --- a/crates/psrs-backend/src/mir/indirect_tests/aggregate/resource_result.rs +++ b/crates/psrs-backend/src/mir/indirect_tests/aggregate/resource_result.rs @@ -98,6 +98,7 @@ pub(super) fn resource_result_fixture() -> (cc::Module, ExternalBindings, Resolv let bindings = ExternalBindings { imports: vec![ExternalBinding { symbol: external_symbol, + source_module: ModuleId(0), interface: "wasi:io/streams".into(), function: "get".into(), type_id: None, diff --git a/crates/psrs-backend/src/mir/indirect_tests/aggregate/scalars.rs b/crates/psrs-backend/src/mir/indirect_tests/aggregate/scalars.rs index 1c1418e2..ab0a6711 100644 --- a/crates/psrs-backend/src/mir/indirect_tests/aggregate/scalars.rs +++ b/crates/psrs-backend/src/mir/indirect_tests/aggregate/scalars.rs @@ -109,6 +109,7 @@ pub(super) fn wide_scalar_fixture() -> (cc::Module, ExternalBindings, Resolve) { let bindings = ExternalBindings { imports: vec![ExternalBinding { symbol: external_symbol, + source_module: ModuleId(0), interface: "wasi:io/streams".into(), function: "get".into(), type_id: None, @@ -246,6 +247,7 @@ pub(super) fn wide_scalar_parameter_fixture() -> (cc::Module, ExternalBindings, let bindings = ExternalBindings { imports: vec![ExternalBinding { symbol: external_symbol, + source_module: ModuleId(0), interface: "wasi:io/streams".into(), function: "take".into(), type_id: None, diff --git a/crates/psrs-backend/src/mir/indirect_tests/composite/fixture.rs b/crates/psrs-backend/src/mir/indirect_tests/composite/fixture.rs index 2cc95d75..8369eca2 100644 --- a/crates/psrs-backend/src/mir/indirect_tests/composite/fixture.rs +++ b/crates/psrs-backend/src/mir/indirect_tests/composite/fixture.rs @@ -246,6 +246,7 @@ pub(super) fn composite_indirect_fixture() -> (cc::Module, ExternalBindings, Res let bindings = ExternalBindings { imports: vec![ExternalBinding { symbol: external_symbol, + source_module: ModuleId(0), interface: "wasi:io/streams".into(), function: "take-shapes".into(), type_id: None, diff --git a/crates/psrs-backend/src/mir/indirect_tests/mod.rs b/crates/psrs-backend/src/mir/indirect_tests/mod.rs index 903d891d..e5d61c59 100644 --- a/crates/psrs-backend/src/mir/indirect_tests/mod.rs +++ b/crates/psrs-backend/src/mir/indirect_tests/mod.rs @@ -91,6 +91,7 @@ fn indirect_fixture() -> (cc::Module, ExternalBindings, Resolve) { let bindings = ExternalBindings { imports: vec![ExternalBinding { symbol: external_symbol, + source_module: ModuleId(0), interface: "wasi:io/streams".into(), function: "take".into(), type_id: None, diff --git a/crates/psrs-backend/src/mir/indirect_tests/record_list/fixtures/aggregate.rs b/crates/psrs-backend/src/mir/indirect_tests/record_list/fixtures/aggregate.rs index ae376199..a91166a7 100644 --- a/crates/psrs-backend/src/mir/indirect_tests/record_list/fixtures/aggregate.rs +++ b/crates/psrs-backend/src/mir/indirect_tests/record_list/fixtures/aggregate.rs @@ -121,6 +121,7 @@ pub(crate) fn flags_fixture() -> (cc::Module, ExternalBindings, Resolve) { let bindings = ExternalBindings { imports: vec![ExternalBinding { symbol: external_symbol, + source_module: ModuleId(0), interface: "wasi:io/streams".into(), function: "take".into(), type_id: None, @@ -215,6 +216,7 @@ pub(crate) fn handle_fixture() -> (cc::Module, ExternalBindings, Resolve) { let bindings = ExternalBindings { imports: vec![ExternalBinding { symbol: external_symbol, + source_module: ModuleId(0), interface: "wasi:io/streams".into(), function: "take".into(), type_id: None, @@ -339,6 +341,7 @@ pub(crate) fn tuple_fixture() -> (cc::Module, ExternalBindings, Resolve) { let bindings = ExternalBindings { imports: vec![ExternalBinding { symbol: external_symbol, + source_module: ModuleId(0), interface: "wasi:io/streams".into(), function: "take".into(), type_id: None, @@ -425,6 +428,7 @@ fn handle_result(result: &str) -> (cc::Module, ExternalBindings, Resolve) { let bindings = ExternalBindings { imports: vec![ExternalBinding { symbol: external_symbol, + source_module: ModuleId(0), interface: "wasi:io/streams".into(), function: "get".into(), type_id: None, diff --git a/crates/psrs-backend/src/mir/indirect_tests/record_list/fixtures/fixed.rs b/crates/psrs-backend/src/mir/indirect_tests/record_list/fixtures/fixed.rs index 200104af..cb36b0b4 100644 --- a/crates/psrs-backend/src/mir/indirect_tests/record_list/fixtures/fixed.rs +++ b/crates/psrs-backend/src/mir/indirect_tests/record_list/fixtures/fixed.rs @@ -110,6 +110,7 @@ pub(crate) fn fixed_list_fixture() -> (cc::Module, ExternalBindings, Resolve) { let bindings = ExternalBindings { imports: vec![ExternalBinding { symbol: external_symbol, + source_module: ModuleId(0), interface: "wasi:io/streams".into(), function: "take".into(), type_id: None, @@ -186,6 +187,7 @@ pub(crate) fn fixed_list_result_fixture() -> (cc::Module, ExternalBindings, Reso let bindings = ExternalBindings { imports: vec![ExternalBinding { symbol: external_symbol, + source_module: ModuleId(0), interface: "wasi:io/streams".into(), function: "get".into(), type_id: None, diff --git a/crates/psrs-backend/src/mir/indirect_tests/record_list/fixtures/mod.rs b/crates/psrs-backend/src/mir/indirect_tests/record_list/fixtures/mod.rs index 243e9560..63794799 100644 --- a/crates/psrs-backend/src/mir/indirect_tests/record_list/fixtures/mod.rs +++ b/crates/psrs-backend/src/mir/indirect_tests/record_list/fixtures/mod.rs @@ -145,6 +145,7 @@ pub(super) fn fixture() -> (cc::Module, ExternalBindings, Resolve) { let bindings = ExternalBindings { imports: vec![ExternalBinding { symbol: external_symbol, + source_module: ModuleId(0), interface: "wasi:io/streams".into(), function: "take".into(), type_id: None, @@ -230,6 +231,7 @@ pub(super) fn result_fixture() -> (cc::Module, ExternalBindings, Resolve) { let bindings = ExternalBindings { imports: vec![ExternalBinding { symbol: external_symbol, + source_module: ModuleId(0), interface: "wasi:io/streams".into(), function: "get".into(), type_id: None, @@ -356,6 +358,7 @@ pub(super) fn string_fixture() -> (cc::Module, ExternalBindings, Resolve) { let bindings = ExternalBindings { imports: vec![ExternalBinding { symbol: external_symbol, + source_module: ModuleId(0), interface: "wasi:io/streams".into(), function: "take".into(), type_id: None, diff --git a/crates/psrs-backend/src/mir/indirect_tests/record_list/fixtures/variants.rs b/crates/psrs-backend/src/mir/indirect_tests/record_list/fixtures/variants.rs index 1df31fb0..237f1ce6 100644 --- a/crates/psrs-backend/src/mir/indirect_tests/record_list/fixtures/variants.rs +++ b/crates/psrs-backend/src/mir/indirect_tests/record_list/fixtures/variants.rs @@ -151,6 +151,7 @@ fn parameter_fixture( let bindings = ExternalBindings { imports: vec![ExternalBinding { symbol: external_symbol, + source_module: ModuleId(0), interface: "wasi:io/streams".into(), function: "take".into(), type_id: None, @@ -320,6 +321,7 @@ pub(crate) fn option_string_list_result_fixture() -> (cc::Module, ExternalBindin let bindings = ExternalBindings { imports: vec![ExternalBinding { symbol: external_symbol, + source_module: ModuleId(0), interface: "wasi:io/streams".into(), function: "get".into(), type_id: None, @@ -469,6 +471,7 @@ pub(crate) fn option_list_list_fixture() -> (cc::Module, ExternalBindings, Resol let bindings = ExternalBindings { imports: vec![ExternalBinding { symbol: external_symbol, + source_module: ModuleId(0), interface: "wasi:io/streams".into(), function: "take".into(), type_id: None, diff --git a/crates/psrs-backend/src/mir/indirect_tests/record_list/fixtures/wide_flags.rs b/crates/psrs-backend/src/mir/indirect_tests/record_list/fixtures/wide_flags.rs index 002b04af..48cd2ab3 100644 --- a/crates/psrs-backend/src/mir/indirect_tests/record_list/fixtures/wide_flags.rs +++ b/crates/psrs-backend/src/mir/indirect_tests/record_list/fixtures/wide_flags.rs @@ -389,6 +389,7 @@ fn finish( let bindings = ExternalBindings { imports: vec![ExternalBinding { symbol: external_symbol, + source_module: ModuleId(0), interface: "wasi:io/streams".into(), function: function.into(), type_id: None, diff --git a/crates/psrs-backend/src/mir/mod.rs b/crates/psrs-backend/src/mir/mod.rs index a1f476fe..2e39decf 100644 --- a/crates/psrs-backend/src/mir/mod.rs +++ b/crates/psrs-backend/src/mir/mod.rs @@ -227,7 +227,7 @@ fn lower_module_after_binding_validation( let import = wasi.import(interface, function).map_err(|message| { vec![ BackendError::new("P9 MIR lowering", external.span, message) - .with_module(external.symbol.module), + .with_module(external.source_module), ] })?; if let Some(reason) = &import.unsupported { @@ -237,7 +237,7 @@ fn lower_module_after_binding_validation( external.span, format!("WIT import `{interface}#{function}` is unsupported: {reason}"), ) - .with_module(external.symbol.module), + .with_module(external.source_module), ]); } let Some(signature) = abstract_signatures.get(&external.symbol).cloned() else { @@ -247,7 +247,7 @@ fn lower_module_after_binding_validation( external.span, format!("WIT import `{interface}#{function}` has no abstract signature"), ) - .with_module(external.symbol.module), + .with_module(external.source_module), ]); }; wit_imports.insert( diff --git a/crates/psrs-backend/src/mir/wit/tests/primitive.rs b/crates/psrs-backend/src/mir/wit/tests/primitive.rs index 1847f83c..6b2e9ddd 100644 --- a/crates/psrs-backend/src/mir/wit/tests/primitive.rs +++ b/crates/psrs-backend/src/mir/wit/tests/primitive.rs @@ -30,6 +30,7 @@ fn validate( id: ModuleId(0), name: "Main".into(), externals: Vec::new(), + external_types: Vec::new(), types: Vec::new(), newtype_ids: Vec::new(), opaque_ids: Vec::new(), @@ -137,6 +138,7 @@ fn option_string_validates_and_lowers_as_a_discriminant_and_string() { id: ModuleId(0), name: "Main".into(), externals: Vec::new(), + external_types: Vec::new(), types: Vec::new(), newtype_ids: Vec::new(), opaque_ids: Vec::new(), @@ -185,6 +187,7 @@ fn option_string_validates_and_lowers_as_a_discriminant_and_string() { id: ModuleId(0), name: "Main".into(), externals: Vec::new(), + external_types: Vec::new(), types: Vec::new(), newtype_ids: Vec::new(), opaque_ids: Vec::new(), diff --git a/crates/psrs-core/src/dictionary.rs b/crates/psrs-core/src/dictionary.rs index fb667824..a0af853d 100644 --- a/crates/psrs-core/src/dictionary.rs +++ b/crates/psrs-core/src/dictionary.rs @@ -222,6 +222,7 @@ mod tests { id: ModuleId(0), name: "DictionaryLayout".into(), externals: Vec::new(), + external_types: Vec::new(), types, newtype_ids: Vec::new(), opaque_ids: Vec::new(), diff --git a/crates/psrs-core/src/effect/mod.rs b/crates/psrs-core/src/effect/mod.rs index ebb3994b..db0657a4 100644 --- a/crates/psrs-core/src/effect/mod.rs +++ b/crates/psrs-core/src/effect/mod.rs @@ -12,12 +12,70 @@ mod supplies; use crate::{Module, Type, TypeConstructor, TypeId, VerifyError, closure_parts}; use psrs_hir::{LocalId, ModuleId, SymbolId, TypeId as HirTypeId}; +use std::collections::HashSet; use operations::synthesize_operations; use supplies::LocalSupply; const EFFECT_INTERFACE: &str = "psrs:effect"; +/// The resolved identity of the trusted effect library interface. The driver +/// creates this only from its trusted library prefix and carries it to P8. +/// Consumers must not reconstruct trust from qualified names or opacity. +#[derive(Clone, Debug, PartialEq, Eq)] +pub struct TrustedEffect { + pub effect_type: HirTypeId, + pub operations: Vec, +} + +/// A source command entry that the frontend has checked to have type +/// `Effect Unit`. P8 wraps it after lowering the abstract effect type. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub struct EffectCommandEntry { + pub symbol: SymbolId, +} + +#[derive(Clone, Debug, PartialEq, Eq)] +pub struct EffectCompilation { + pub trusted: TrustedEffect, + pub command_entry: Option, +} + +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub struct EffectOperationBinding { + pub operation: EffectOperation, + pub symbol: SymbolId, +} + +#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)] +pub enum EffectOperation { + Pure, + Bind, + Run, + Trap, +} + +impl EffectOperation { + pub fn wit_function(self) -> &'static str { + match self { + Self::Pure => "pure", + Self::Bind => "bind", + Self::Run => "run", + Self::Trap => "trap", + } + } +} + +/// An import signature classified while its result still names the abstract +/// trusted Effect constructor. +#[derive(Clone, Debug, PartialEq, Eq)] +pub struct EffectImportType { + pub quantified: Vec, + pub parameters: Vec, + pub application: TypeId, + pub payload: TypeId, +} + /// One representation closure written for an `Effect` application. #[derive(Clone, Copy, Debug, PartialEq, Eq)] pub struct EffectClosure { @@ -78,24 +136,87 @@ impl EffectLowering { /// Lowers library effects in a linked Core module. /// /// Programs that do not contain the opaque `Prelude.Effect` type are unchanged. -pub fn lower_effects(module: &mut Module) -> Result> { - let Some(effect) = library_effect(module) else { - return Ok(EffectLowering::default()); - }; +pub fn lower_effects( + module: &mut Module, + trusted: &TrustedEffect, +) -> Result> { + let effect = trusted.effect_type; + if !module.opaque_ids.contains(&effect) { + return Err(vec![verification_error( + module, + "trusted Effect identity is missing or is not an opaque type", + )]); + } let token = intern(module, Type::Constructor(TypeConstructor::Int)); let closures = rewrite_effect_applications(module, effect, token); + let synthesized = synthesize_operations(module, token, trusted)?; let lowering = EffectLowering { - synthesized: synthesize_operations(module, token), + synthesized, closures, }; lowering.verify(module)?; Ok(lowering) } -fn library_effect(module: &Module) -> Option { - module.type_names.iter().find_map(|(id, name)| { - (*name == "Prelude.Effect" && module.opaque_ids.contains(id)).then_some(*id) - }) +/// Classifies a WIT source signature by its abstract result type. The returned +/// structure is evidence for a later wrapper; no closure shape is inspected. +pub fn classify_effect_import( + module: &Module, + ty: TypeId, + effect: HirTypeId, +) -> Result, &'static str> { + let mut current = ty; + let mut quantified = Vec::new(); + let mut parameters = Vec::new(); + let mut visited = HashSet::new(); + loop { + if !visited.insert(current) { + return Err("cyclic type spine in effect import signature"); + } + let Some(node) = module.types.get(current.0 as usize) else { + return Err("effect import signature references an invalid type id"); + }; + if let Type::ForAll { variables, body } = node { + quantified.extend_from_slice(variables); + current = *body; + continue; + } + if let Type::Application(function, argument) = node + && (module.types.get(function.0 as usize).is_none() + || module.types.get(argument.0 as usize).is_none()) + { + return Err("effect import signature contains an invalid application spine"); + } + if let Some((function, payload)) = effect_application(module, current, effect) { + return Ok(Some(EffectImportType { + quantified, + parameters, + application: function, + payload, + })); + } + let Some((parameter, result)) = crate::arrow_parts(&module.types, current) else { + return Ok(None); + }; + if module.types.get(parameter.0 as usize).is_none() + || module.types.get(result.0 as usize).is_none() + { + return Err("effect import signature contains an invalid function spine"); + } + parameters.push(parameter); + current = result; + } +} + +pub fn effect_application( + module: &Module, + id: TypeId, + effect: HirTypeId, +) -> Option<(TypeId, TypeId)> { + let Type::Application(function, payload) = module.types.get(id.0 as usize)? else { + return None; + }; + is_effect_constructor(module, *function, effect).then_some((id, *payload)) } /// Writes `Type::Closure` over each `Effect` application and records the shape @@ -154,30 +275,6 @@ fn intern(module: &mut Module, ty: Type) -> TypeId { TypeId((module.types.len() - 1) as u32) } -/// A suspended import: source parameters, the closure type, and its payload. -pub fn suspended_import(module: &Module, ty: TypeId) -> Option<(Vec, TypeId, TypeId)> { - let mut current = ty; - let mut seen = 0; - while seen <= module.types.len() - && let Some((_, body)) = crate::forall_parts(&module.types, current) - { - current = body; - seen += 1; - } - let mut parameters = Vec::new(); - loop { - if let Some((closure_parameters, result)) = closure_parts(&module.types, current) { - if closure_parameters.len() != 1 { - return None; - } - return Some((parameters, current, result)); - } - let (parameter, result) = crate::arrow_parts(&module.types, current)?; - parameters.push(parameter); - current = result; - } -} - /// Builds `parameters -> result` in the module type table. pub fn function_type(module: &mut Module, parameters: &[TypeId], result: TypeId) -> TypeId { let mut ty = result; diff --git a/crates/psrs-core/src/effect/operations.rs b/crates/psrs-core/src/effect/operations.rs index 3285811d..7af14f12 100644 --- a/crates/psrs-core/src/effect/operations.rs +++ b/crates/psrs-core/src/effect/operations.rs @@ -6,37 +6,73 @@ //! integer `0`, and `trap` is the effect that escapes instead of returning. use super::supplies::{LocalSupply, VariableSupply}; -use super::{EFFECT_INTERFACE, intern}; +use super::{EFFECT_INTERFACE, TrustedEffect, intern}; use crate::{Binder, Declaration, Expr, ExprKind, Module, Type, TypeConstructor, TypeId}; use psrs_hir::{ExternalKind, LocalId, SymbolId, TypeVariableId}; use psrs_span::TextRange; /// Synthesizes `pure`, `bind`, `run`, and `trap`, dropping the abstract imports /// they replace. Returns the symbols that became ordinary declarations. -pub(super) fn synthesize_operations(module: &mut Module, token: TypeId) -> Vec { - let operations = module - .externals - .iter() - .enumerate() - .filter_map(|(index, external)| { - let ExternalKind::Wit { - interface, - function, - } = &external.kind - else { - return None; - }; - (*interface == EFFECT_INTERFACE).then_some(( - index, - external.symbol, - external.name.clone(), - function.clone(), - external_span(external), - )) - }) - .collect::>(); - if operations.is_empty() { - return Vec::new(); +pub(super) fn synthesize_operations( + module: &mut Module, + token: TypeId, + trusted: &TrustedEffect, +) -> Result, Vec> { + let mut operations = Vec::new(); + let mut seen_symbols = std::collections::HashSet::new(); + let mut seen_operations = std::collections::HashSet::new(); + for binding in &trusted.operations { + if !seen_symbols.insert(binding.symbol) || !seen_operations.insert(binding.operation) { + return Err(vec![verification_error( + module, + "trusted Effect operation bindings are duplicated", + )]); + } + let Some((index, external)) = module + .externals + .iter() + .enumerate() + .find(|(_, external)| external.symbol == binding.symbol) + else { + return Err(vec![verification_error( + module, + "trusted Effect operation binding has no external declaration", + )]); + }; + let ExternalKind::Wit { + interface, + function, + } = &external.kind + else { + return Err(vec![verification_error( + module, + "trusted Effect operation is not a WIT import", + )]); + }; + if interface != EFFECT_INTERFACE || function != binding.operation.wit_function() { + return Err(vec![verification_error( + module, + "trusted Effect operation identity does not match its WIT binding", + )]); + } + operations.push(( + index, + binding.symbol, + external.name.clone(), + function.clone(), + external_span(external), + )); + } + if module.externals.iter().any(|external| { + matches!( + &external.kind, + ExternalKind::Wit { interface, .. } if interface == EFFECT_INTERFACE + ) && !seen_symbols.contains(&external.symbol) + }) { + return Err(vec![verification_error( + module, + "Effect WIT import is missing from the trusted operation bindings", + )]); } let mut locals = LocalSupply::new(module); let mut variables = VariableSupply::new(module); @@ -82,7 +118,10 @@ pub(super) fn synthesize_operations(module: &mut Module, token: TypeId) -> Vec None, }; let Some(declaration) = declaration else { - continue; + return Err(vec![verification_error( + module, + "trusted Effect operation has no lowering rule", + )]); }; module.declarations.push(declaration); synthesized.push(symbol); @@ -92,7 +131,18 @@ pub(super) fn synthesize_operations(module: &mut Module, token: TypeId) -> Vec crate::VerifyError { + crate::VerifyError { + module: module.id, + span: module.span, + message, + } } fn pure_declaration( diff --git a/crates/psrs-core/src/lib.rs b/crates/psrs-core/src/lib.rs index 2af93254..54d64aec 100644 --- a/crates/psrs-core/src/lib.rs +++ b/crates/psrs-core/src/lib.rs @@ -36,11 +36,27 @@ pub struct ConstructorInfo { pub parameters: Vec, } +/// The checked, synonym-expanded signature of a WIT value import. Compiler +/// intrinsics use registry-owned contracts and do not appear in this table. +#[derive(Clone, Debug, PartialEq, Eq)] +pub struct ExternalType { + pub symbol: SymbolId, + /// Source module that declared this import. External symbols themselves + /// live in the reserved intrinsic namespace, so their symbol ID cannot + /// carry diagnostic origin. + pub source_module: ModuleId, + pub ty: TypeId, +} + #[derive(Clone, Debug, PartialEq, Eq)] pub struct Module { pub id: ModuleId, pub name: String, pub externals: Vec, + /// Checked WIT import signatures projected from THIR. Backend binding and + /// representation lowering must consume these schemes rather than + /// reconstructing types from raw HIR annotations. + pub external_types: Vec, pub types: Vec, /// Nominal newtypes that are represented by their single field below Core. /// This is representation metadata, not a change to the source type. diff --git a/crates/psrs-core/src/link/mod.rs b/crates/psrs-core/src/link/mod.rs index 5351b0c4..ca4fdcae 100644 --- a/crates/psrs-core/src/link/mod.rs +++ b/crates/psrs-core/src/link/mod.rs @@ -1,5 +1,6 @@ use crate::{ - Binding, ConstructorInfo, Declaration, Expr, ExprKind, Module, PatternKind, Type, TypeId, + Binding, ConstructorInfo, Declaration, Expr, ExprKind, ExternalType, Module, PatternKind, Type, + TypeId, }; use psrs_hir::{ModuleId, SymbolId, TypeVariableId}; use psrs_span::TextRange; @@ -29,6 +30,8 @@ pub fn link(modules: Vec) -> Module { let mut declarations = Vec::new(); let mut externals = Vec::new(); let mut seen_externals = std::collections::HashSet::new(); + let mut external_types = Vec::new(); + let mut seen_external_types = HashSet::new(); let mut type_names = Vec::new(); let mut seen_type_names = HashSet::new(); let mut type_variable_offset = 0u32; @@ -76,6 +79,15 @@ pub fn link(modules: Vec) -> Module { externals.push(external); } } + for external in module.external_types { + if seen_external_types.insert(external.symbol) { + external_types.push(ExternalType { + symbol: external.symbol, + source_module: external.source_module, + ty: shift_id(external.ty, offset), + }); + } + } for (id, name) in module.type_names { if seen_type_names.insert(id) { type_names.push((id, name)); @@ -86,6 +98,7 @@ pub fn link(modules: Vec) -> Module { id: ModuleId(0), name, externals, + external_types, types, newtype_ids, opaque_ids, @@ -250,9 +263,23 @@ pub fn prune_unreachable(module: &mut Module, root: SymbolId) { // never constructs or matches, such as a newtype resource wrapper. Its // constructors are still needed to resolve and lay out the binding, so keep // every type the external signatures mention. - for external in &module.externals { - if let Some(signature) = &external.signature { - collect_type_ids(signature, &mut used_types); + let mut visited = HashSet::new(); + for external in &module.external_types { + collect_core_type_ids(external.ty, module, &mut used_types, &mut visited); + } + loop { + let before = used_types.len(); + let field_types = module + .constructors + .iter() + .filter(|constructor| used_types.contains(&constructor.type_id)) + .flat_map(|constructor| constructor.field_types.iter().copied()) + .collect::>(); + for field_type in field_types { + collect_core_type_ids(field_type, module, &mut used_types, &mut visited); + } + if used_types.len() == before { + break; } } module @@ -260,29 +287,35 @@ pub fn prune_unreachable(module: &mut Module, root: SymbolId) { .retain(|constructor| used_types.contains(&constructor.type_id)); } -fn collect_type_ids(ty: &psrs_hir::Type, out: &mut HashSet) { - match &ty.kind { - psrs_hir::TypeKind::Named(id) | psrs_hir::TypeKind::Opaque(id) => { - out.insert(*id); +fn collect_core_type_ids( + id: TypeId, + module: &Module, + out: &mut HashSet, + visited: &mut HashSet, +) { + if !visited.insert(id) { + return; + } + match module.types.get(id.0 as usize) { + Some(Type::Constructor(crate::TypeConstructor::User(type_id))) => { + out.insert(*type_id); } - psrs_hir::TypeKind::Application(function, argument) => { - collect_type_ids(function, out); - collect_type_ids(argument, out); + Some(Type::Application(function, argument)) => { + collect_core_type_ids(*function, module, out, visited); + collect_core_type_ids(*argument, module, out, visited); } - psrs_hir::TypeKind::Function { parameter, result } => { - collect_type_ids(parameter, out); - collect_type_ids(result, out); + Some(Type::ForAll { body, .. }) => { + collect_core_type_ids(*body, module, out, visited); } - psrs_hir::TypeKind::Forall { body, .. } | psrs_hir::TypeKind::Constrained { body, .. } => { - collect_type_ids(body, out) + Some(Type::RowExtend { ty, tail, .. }) => { + collect_core_type_ids(*ty, module, out, visited); + collect_core_type_ids(*tail, module, out, visited); } - psrs_hir::TypeKind::Row { fields, tail } | psrs_hir::TypeKind::Record { fields, tail } => { - for field in fields { - collect_type_ids(&field.ty, out); - } - if let Some(tail) = tail { - collect_type_ids(tail, out); + Some(Type::Closure { parameters, result }) => { + for parameter in parameters { + collect_core_type_ids(*parameter, module, out, visited); } + collect_core_type_ids(*result, module, out, visited); } _ => {} } diff --git a/crates/psrs-core/src/lower/module.rs b/crates/psrs-core/src/lower/module.rs index b0514806..9af7177a 100644 --- a/crates/psrs-core/src/lower/module.rs +++ b/crates/psrs-core/src/lower/module.rs @@ -84,6 +84,15 @@ pub(super) fn lower_module_inner(module: psrs_thir::Module) -> Result, declaration_type: u32, value: Expr) -> Module { id: ModuleId(0), name: "Main".into(), externals: Vec::new(), + external_types: Vec::new(), types, newtype_ids: Vec::new(), opaque_ids: Vec::new(), @@ -78,6 +79,19 @@ fn module(types: Vec, declaration_type: u32, value: Expr) -> Module { } fn with_trace(mut module: Module) -> Module { + let int = TypeId( + module + .types + .iter() + .position(|ty| matches!(ty, Type::Constructor(TypeConstructor::Int))) + .expect("trace fixture has an integer type") as u32, + ); + let ty = arrow_type(&mut module.types, int, int); + module.external_types.push(crate::ExternalType { + symbol: SymbolId::new(ModuleId(0), 0), + source_module: module.id, + ty, + }); module.externals.push(ExternalSymbol { symbol: SymbolId::new(ModuleId(0), 0), name: "trace".into(), diff --git a/crates/psrs-core/src/opt/tests/patterns.rs b/crates/psrs-core/src/opt/tests/patterns.rs index 7a040a85..572e0207 100644 --- a/crates/psrs-core/src/opt/tests/patterns.rs +++ b/crates/psrs-core/src/opt/tests/patterns.rs @@ -111,6 +111,7 @@ fn nested_record_case(second: i32) -> Module { id: ModuleId(0), name: "PatternOptimization".into(), externals: Vec::new(), + external_types: Vec::new(), types: std::mem::take(&mut types), newtype_ids: Vec::new(), opaque_ids: Vec::new(), diff --git a/crates/psrs-core/src/tests/dictionaries.rs b/crates/psrs-core/src/tests/dictionaries.rs index 6b311a75..1cbf9d06 100644 --- a/crates/psrs-core/src/tests/dictionaries.rs +++ b/crates/psrs-core/src/tests/dictionaries.rs @@ -67,6 +67,7 @@ fn lowering_erases_instance_and_superclass_evidence_to_calls_and_projections() { id: module_id, name: "Main".into(), externals: Vec::new(), + external_types: Vec::new(), types, newtype_ids: Vec::new(), opaque_ids: Vec::new(), @@ -199,6 +200,7 @@ fn lowering_erases_global_dictionary_evidence_to_a_core_global() { id: module_id, name: "Main".into(), externals: Vec::new(), + external_types: Vec::new(), types: vec![ thir::Type::Constructor(thir::TypeConstructor::Int), thir::Type::RowEmpty, diff --git a/crates/psrs-core/src/tests/effects.rs b/crates/psrs-core/src/tests/effects.rs index e84147fe..9f90da3b 100644 --- a/crates/psrs-core/src/tests/effects.rs +++ b/crates/psrs-core/src/tests/effects.rs @@ -5,7 +5,7 @@ //! runtime token alone and returns the lowered effect result. use super::*; -use crate::effect::{EffectClosure, lower_effects}; +use crate::effect::{EffectClosure, TrustedEffect, classify_effect_import, lower_effects}; use psrs_hir::{ModuleId, SymbolId, TypeId as HirTypeId, TypeVariableId}; const SPAN: TextRange = TextRange::new(0, 8); @@ -16,6 +16,14 @@ const B: TypeId = TypeId(2); const ARROW: TypeId = TypeId(5); const EFFECT: TypeId = TypeId(6); const EFFECT_APPLICATION: TypeId = TypeId(7); +const EFFECT_HIR: HirTypeId = HirTypeId::new(ModuleId(0), 3); + +fn trusted_effect() -> TrustedEffect { + TrustedEffect { + effect_type: EFFECT_HIR, + operations: Vec::new(), + } +} /// A linked module whose only effect is `Effect (a -> b)`. /// @@ -29,11 +37,12 @@ const EFFECT_APPLICATION: TypeId = TypeId(7); /// | 6 | `Prelude.Effect` | /// | 7 | `Effect (a -> b)`, the node lowering replaces | fn effect_module() -> Module { - let effect = HirTypeId::new(ModuleId(0), 3); + let effect = EFFECT_HIR; Module { id: ModuleId(0), name: "Main".into(), externals: Vec::new(), + external_types: Vec::new(), types: vec![ Type::Constructor(TypeConstructor::Int), Type::Variable(TypeVariableId(0)), @@ -60,7 +69,8 @@ fn effect_module() -> Module { #[test] fn lowered_effect_closures_are_one_token_closure_over_the_effect_result() { let mut module = effect_module(); - let lowering = lower_effects(&mut module).expect("the written closure keeps its shape"); + let lowering = + lower_effects(&mut module, &trusted_effect()).expect("the written closure keeps its shape"); assert_eq!( lowering.closures, vec![EffectClosure { @@ -89,7 +99,8 @@ fn lowered_effect_closures_are_one_token_closure_over_the_effect_result() { #[test] fn a_lowered_effect_closure_flattened_to_arity_two_is_rejected() { let mut module = effect_module(); - let lowering = lower_effects(&mut module).expect("the written closure starts in its shape"); + let lowering = lower_effects(&mut module, &trusted_effect()) + .expect("the written closure starts in its shape"); module.types[EFFECT_APPLICATION.0 as usize] = Type::Closure { parameters: vec![TOKEN, A], result: ARROW, @@ -110,7 +121,8 @@ fn a_lowered_effect_closure_flattened_to_arity_two_is_rejected() { #[test] fn a_lowered_effect_closure_with_the_wrong_result_is_rejected() { let mut module = effect_module(); - let lowering = lower_effects(&mut module).expect("the written closure starts in its shape"); + let lowering = lower_effects(&mut module, &trusted_effect()) + .expect("the written closure starts in its shape"); module.types[EFFECT_APPLICATION.0 as usize] = Type::Closure { parameters: vec![TOKEN], result: B, @@ -126,7 +138,8 @@ fn a_lowered_effect_closure_with_the_wrong_result_is_rejected() { #[test] fn a_lowered_effect_that_is_not_a_closure_is_rejected() { let mut module = effect_module(); - let lowering = lower_effects(&mut module).expect("the written closure starts in its shape"); + let lowering = lower_effects(&mut module, &trusted_effect()) + .expect("the written closure starts in its shape"); module.types[EFFECT_APPLICATION.0 as usize] = Type::Application(EFFECT, ARROW); let errors = lowering .verify(&module) @@ -141,13 +154,109 @@ fn a_lowered_effect_that_is_not_a_closure_is_rejected() { /// A module without the opaque library type is left alone and passes the check. #[test] -fn a_module_without_the_library_effect_has_no_lowered_closures() { +fn lowering_rejects_missing_trusted_effect_identity() { let mut module = effect_module(); module.type_names.clear(); module.opaque_ids.clear(); - let lowering = lower_effects(&mut module).expect("nothing to lower"); - assert!(lowering.closures.is_empty()); - assert!(lowering.verify(&module).is_ok()); + let errors = lower_effects(&mut module, &trusted_effect()) + .expect_err("missing trusted identity metadata is an error"); + assert_eq!( + errors[0].message, + "trusted Effect identity is missing or is not an opaque type" + ); +} + +#[test] +fn effect_import_classification_rejects_a_cyclic_arrow_result() { + let mut module = effect_module(); + module.types = vec![ + Type::Constructor(TypeConstructor::Function), + Type::Constructor(TypeConstructor::Int), + Type::Application(TypeId(0), TypeId(1)), + Type::Application(TypeId(2), TypeId(3)), + ]; + let error = classify_effect_import(&module, TypeId(3), EFFECT_HIR) + .expect_err("a recursive arrow spine is malformed"); + assert_eq!(error, "cyclic type spine in effect import signature"); +} + +#[test] +fn a_checked_foreign_effect_signature_must_quantify_its_type_variables() { + let mut module = effect_module(); + let symbol = SymbolId::new(ModuleId(0), 9); + let free = TypeId(module.types.len() as u32); + module.types.push(Type::Variable(TypeVariableId(99))); + module.externals.push(psrs_hir::ExternalSymbol { + symbol, + name: "foreignEffect".into(), + kind: psrs_hir::ExternalKind::Wit { + interface: "test:effect".into(), + function: "foreign-effect".into(), + }, + signature: None, + }); + module.external_types.push(crate::ExternalType { + symbol, + source_module: module.id, + ty: free, + }); + + let errors = module + .verify() + .expect_err("free external variables are invalid"); + assert!( + errors + .iter() + .any(|error| { error.message == "type variable is outside its quantifier scope" }) + ); +} + +#[test] +fn another_foreign_effect_identity_is_not_the_trusted_effect_constructor() { + let mut module = effect_module(); + let other_effect = HirTypeId::new(ModuleId(1), 3); + let other = TypeId(module.types.len() as u32); + module + .types + .push(Type::Constructor(TypeConstructor::User(other_effect))); + let application = TypeId(module.types.len() as u32); + module.types.push(Type::Application(other, A)); + module.opaque_ids.push(other_effect); + module + .type_names + .push((other_effect, "Prelude.Effect".into())); + + assert_eq!( + classify_effect_import(&module, application, EFFECT_HIR).unwrap(), + None, + "matching spelling and opacity do not substitute for trusted identity" + ); + + lower_effects(&mut module, &trusted_effect()).unwrap(); + assert!(matches!( + module.types.get(application.0 as usize), + Some(Type::Application(_, _)) + )); + assert!(matches!( + module.types.get(EFFECT_APPLICATION.0 as usize), + Some(Type::Closure { .. }) + )); +} + +#[test] +fn an_ordinary_closure_shaped_import_is_not_an_effect_import() { + let mut module = effect_module(); + let ordinary = TypeId(module.types.len() as u32); + module.types.push(Type::Closure { + parameters: vec![A], + result: B, + }); + + assert_eq!( + classify_effect_import(&module, ordinary, EFFECT_HIR).unwrap(), + None, + "suspension is planned from the checked abstract Effect result, not closure shape" + ); } fn messages(result: Result<(), Vec>) -> Vec<&'static str> { diff --git a/crates/psrs-core/src/tests/external_types.rs b/crates/psrs-core/src/tests/external_types.rs new file mode 100644 index 00000000..731fed88 --- /dev/null +++ b/crates/psrs-core/src/tests/external_types.rs @@ -0,0 +1,168 @@ +use crate::{ExternalType, Module, Type, TypeConstructor, TypeId}; +use psrs_hir::{ExternalKind, ExternalSymbol, ModuleId, SymbolId, TypeVariableId}; +use psrs_span::TextRange; + +fn fixture() -> Module { + let symbol = SymbolId::new(ModuleId::INTRINSICS, 3); + Module { + id: ModuleId(2), + name: "ExternalScheme".into(), + externals: vec![ExternalSymbol { + symbol, + name: "clock".into(), + kind: ExternalKind::Wit { + interface: "wasi:clocks/monotonic-clock".into(), + function: "now".into(), + }, + signature: None, + }], + external_types: vec![ExternalType { + symbol, + source_module: ModuleId(2), + ty: TypeId(0), + }], + types: vec![Type::Constructor(TypeConstructor::Int)], + newtype_ids: Vec::new(), + opaque_ids: Vec::new(), + callable_types: Vec::new(), + constructors: Vec::new(), + declarations: Vec::new(), + type_names: Vec::new(), + entry: None, + span: TextRange::new(0, 5), + } +} + +fn rejects(module: &Module, fragment: &str) { + let errors = module + .verify() + .expect_err("malformed checked external scheme must fail"); + assert!( + errors.iter().any(|error| error.message.contains(fragment)), + "{errors:?}" + ); +} + +#[test] +fn a_wit_scheme_is_required_even_without_a_raw_annotation() { + let mut module = fixture(); + module.verify().unwrap(); + module.external_types.clear(); + rejects(&module, "no checked signature"); +} + +#[test] +fn checked_external_schemes_are_unique_and_have_an_external_owner() { + let mut module = fixture(); + module.external_types.push(module.external_types[0].clone()); + rejects(&module, "more than one checked signature"); + let mut module = fixture(); + module.externals.clear(); + rejects(&module, "no external declaration"); +} + +#[test] +fn checked_external_schemes_reject_invalid_type_references() { + let mut module = fixture(); + module.external_types[0].ty = TypeId(99); + rejects(&module, "type"); +} + +#[test] +fn external_quantifiers_scope_their_variables() { + let mut module = fixture(); + let variable = TypeVariableId(7); + module.types = vec![Type::Variable(variable)]; + rejects(&module, "quantifier scope"); + module.types.push(Type::ForAll { + variables: vec![variable], + body: TypeId(0), + }); + module.external_types[0].ty = TypeId(1); + module + .verify() + .expect("a properly quantified external scheme is valid"); + module.types[1] = Type::ForAll { + variables: vec![variable, variable], + body: TypeId(0), + }; + rejects(&module, "unique"); +} + +#[test] +fn cyclic_external_schemes_are_rejected() { + let mut module = fixture(); + module.types[0] = Type::ForAll { + variables: Vec::new(), + body: TypeId(0), + }; + rejects(&module, "cycle"); +} + +#[test] +fn linking_preserves_external_type_ids_and_distinct_quantifier_scopes() { + let mut left = fixture(); + let variable = TypeVariableId(7); + left.types = vec![ + Type::Variable(variable), + Type::ForAll { + variables: vec![variable], + body: TypeId(0), + }, + ]; + left.external_types[0].ty = TypeId(1); + let mut right = left.clone(); + right.id = ModuleId(3); + right.externals[0].symbol = SymbolId::new(ModuleId::INTRINSICS, 4); + right.external_types[0].symbol = right.externals[0].symbol; + right.external_types[0].source_module = right.id; + let linked = crate::link(vec![left, right]); + linked.verify().unwrap(); + assert_eq!( + linked + .external_types + .iter() + .map(|external| external.source_module) + .collect::>(), + vec![ModuleId(2), ModuleId(3)] + ); + let mut variables = Vec::new(); + for external in &linked.external_types { + let Type::ForAll { + variables: bound, + body, + } = &linked.types[external.ty.0 as usize] + else { + panic!("linked external lost its quantifier"); + }; + assert_eq!(bound.len(), 1); + assert_eq!(linked.types[body.0 as usize], Type::Variable(bound[0])); + variables.push(bound[0]); + } + assert_eq!(variables.len(), 2); + assert_ne!(variables[0], variables[1]); +} + +#[test] +fn linked_external_signature_errors_keep_the_declaring_source_module() { + let mut external = fixture(); + external.id = ModuleId(9); + external.external_types[0].source_module = external.id; + external.types[0] = Type::Variable(TypeVariableId(42)); + let linked = crate::link(vec![external]); + let errors = linked.verify().unwrap_err(); + let scope_error = errors + .iter() + .find(|error| error.message.contains("quantifier scope")) + .unwrap(); + assert_eq!(scope_error.module, ModuleId(9)); + + let mut external = fixture(); + external.id = ModuleId(9); + external.external_types[0].source_module = external.id; + external.external_types[0].ty = TypeId(99); + let linked = crate::link(vec![external]); + let errors = linked.verify().unwrap_err(); + assert!(errors.iter().any(|error| error.module == ModuleId(9) + && error.message.contains("outside the Core type table"))); +} diff --git a/crates/psrs-core/src/tests/link.rs b/crates/psrs-core/src/tests/link.rs index 2deb783b..84b0d7cf 100644 --- a/crates/psrs-core/src/tests/link.rs +++ b/crates/psrs-core/src/tests/link.rs @@ -14,6 +14,7 @@ fn module_with( id: ModuleId(id), name: format!("M{id}"), externals: Vec::new(), + external_types: Vec::new(), types, newtype_ids: Vec::new(), opaque_ids: Vec::new(), @@ -156,3 +157,82 @@ fn link_reserves_ids_for_forall_binders_that_have_no_variable_node() { linked.verify().unwrap_err() ); } + +#[test] +fn pruning_keeps_nominal_types_through_a_checked_wit_alias_and_nested_fields() { + let resource = HirTypeId::new(ModuleId(0), 1); + let nested = HirTypeId::new(ModuleId(0), 2); + let alias = HirTypeId::new(ModuleId(1), 7); + let import = SymbolId::new(ModuleId(0), 10); + let mut module = module_with( + 0, + vec![ + Type::Constructor(TypeConstructor::Int), + Type::Constructor(TypeConstructor::User(nested)), + Type::Constructor(TypeConstructor::User(resource)), + ], + vec![Declaration { + symbol: SymbolId::new(ModuleId(0), 0), + name: "main".into(), + name_span: SPAN, + quantified: Vec::new(), + ty: TypeId(0), + value: Expr { + kind: ExprKind::Integer(0), + ty: TypeId(0), + span: SPAN, + }, + span: SPAN, + }], + vec![ + ConstructorInfo { + symbol: SymbolId::new(ModuleId(0), 2), + name: "Nested".into(), + type_id: nested, + tag: 0, + field_count: 0, + field_types: Vec::new(), + parameters: Vec::new(), + }, + ConstructorInfo { + symbol: SymbolId::new(ModuleId(0), 3), + name: "Resource".into(), + type_id: resource, + tag: 0, + field_count: 1, + field_types: vec![TypeId(1)], + parameters: Vec::new(), + }, + ], + ); + module.entry = Some(SymbolId::new(ModuleId(0), 0)); + module.externals.push(psrs_hir::ExternalSymbol { + symbol: import, + name: "read".into(), + kind: psrs_hir::ExternalKind::Wit { + interface: "test:resource".into(), + function: "read".into(), + }, + signature: Some(psrs_hir::Type { + kind: psrs_hir::TypeKind::Named(alias), + span: SPAN, + }), + }); + module.external_types.push(crate::ExternalType { + symbol: import, + source_module: module.id, + ty: TypeId(2), + }); + + prune_unreachable(&mut module, SymbolId::new(ModuleId(0), 0)); + + assert_eq!( + module + .constructors + .iter() + .map(|constructor| constructor.type_id) + .collect::>(), + [nested, resource], + "the checked alias and its constructor field both retain their nominal layouts" + ); +} diff --git a/crates/psrs-core/src/tests/mod.rs b/crates/psrs-core/src/tests/mod.rs index 99a804f2..0ed11b44 100644 --- a/crates/psrs-core/src/tests/mod.rs +++ b/crates/psrs-core/src/tests/mod.rs @@ -2,6 +2,7 @@ use super::*; use psrs_hir::{Intrinsic, LocalId, ModuleId, SymbolId}; mod effects; +mod external_types; mod link; mod patterns; mod rank_n; @@ -26,6 +27,7 @@ fn verifier_rejects_out_of_range_types() { id: ModuleId(0), name: "Main".into(), externals: Vec::new(), + external_types: Vec::new(), types: vec![Type::Constructor(crate::TypeConstructor::Int)], newtype_ids: Vec::new(), opaque_ids: Vec::new(), @@ -61,6 +63,7 @@ fn verifier_attributes_declaration_errors_to_their_source_module() { id: ModuleId(0), name: "Linked".into(), externals: Vec::new(), + external_types: Vec::new(), types: vec![Type::Constructor(crate::TypeConstructor::Int)], newtype_ids: Vec::new(), opaque_ids: Vec::new(), @@ -93,6 +96,7 @@ fn single_declaration(types: Vec, declaration_type: TypeId, value: Expr) - id: ModuleId(0), name: "Main".into(), externals: Vec::new(), + external_types: Vec::new(), types, newtype_ids: Vec::new(), opaque_ids: Vec::new(), diff --git a/crates/psrs-core/src/tests/patterns.rs b/crates/psrs-core/src/tests/patterns.rs index d30b5b66..72c6d421 100644 --- a/crates/psrs-core/src/tests/patterns.rs +++ b/crates/psrs-core/src/tests/patterns.rs @@ -67,6 +67,7 @@ fn case_module( id: ModuleId(0), name: "PatternVerifier".into(), externals: Vec::new(), + external_types: Vec::new(), types, newtype_ids: Vec::new(), opaque_ids: Vec::new(), diff --git a/crates/psrs-core/src/tests/rank_n.rs b/crates/psrs-core/src/tests/rank_n.rs index 538778c4..766ec086 100644 --- a/crates/psrs-core/src/tests/rank_n.rs +++ b/crates/psrs-core/src/tests/rank_n.rs @@ -38,6 +38,7 @@ fn module(types: Vec, declarations: Vec) -> Module { id: ModuleId(0), name: "RankN".into(), externals: Vec::new(), + external_types: Vec::new(), types, newtype_ids: Vec::new(), opaque_ids: Vec::new(), diff --git a/crates/psrs-core/src/tests/rows.rs b/crates/psrs-core/src/tests/rows.rs index 2e317754..2859f17d 100644 --- a/crates/psrs-core/src/tests/rows.rs +++ b/crates/psrs-core/src/tests/rows.rs @@ -81,6 +81,7 @@ fn packaged(types: Vec, declarations: Vec) -> Module { id: ModuleId(0), name: "Rows".into(), externals: Vec::new(), + external_types: Vec::new(), types, newtype_ids: Vec::new(), opaque_ids: Vec::new(), diff --git a/crates/psrs-core/src/verify/mod.rs b/crates/psrs-core/src/verify/mod.rs index b8227831..1cd9c6f4 100644 --- a/crates/psrs-core/src/verify/mod.rs +++ b/crates/psrs-core/src/verify/mod.rs @@ -1,5 +1,5 @@ use crate::{Module, Type, TypeId, VerifyError}; -use psrs_hir::LocalId; +use psrs_hir::{ExternalKind, LocalId}; use std::collections::HashMap; mod expr; @@ -36,14 +36,64 @@ pub(crate) fn module(module: &Module) -> Result<(), Vec> { }), ) }) - .chain( - module - .externals + .chain(module.externals.iter().map(|external| { + let signature = module + .external_types .iter() - .map(|external| (external.symbol, None)), - ) + .find(|checked| checked.symbol == external.symbol) + .and_then(|checked| external_scheme(module, checked.ty)); + (external.symbol, signature) + })) .collect::>(); let mut errors = Vec::new(); + let mut external_type_symbols = std::collections::HashSet::new(); + for external_type in &module.external_types { + let span = module + .externals + .iter() + .find(|external| external.symbol == external_type.symbol) + .and_then(|external| external.signature.as_ref()) + .map_or(module.span, |signature| signature.span); + if !external_type_symbols.insert(external_type.symbol) { + errors.push(error( + external_type.source_module, + span, + "a foreign symbol has more than one checked signature", + )); + } + if !module + .externals + .iter() + .any(|external| external.symbol == external_type.symbol) + { + errors.push(error( + external_type.source_module, + span, + "a checked foreign signature has no external declaration", + )); + } + verify_type( + external_type.ty, + module, + external_type.source_module, + span, + &mut errors, + ); + } + for external in &module.externals { + if matches!(&external.kind, ExternalKind::Wit { .. }) + && !external_type_symbols.contains(&external.symbol) + { + errors.push(error( + external.symbol.module, + external + .signature + .as_ref() + .map_or(module.span, |ty| ty.span), + "a foreign declaration has no checked signature", + )); + } + } for (index, ty) in module.types.iter().enumerate() { let id = TypeId(index as u32); match ty { @@ -107,3 +157,20 @@ pub(crate) fn module(module: &Module) -> Result<(), Vec> { Err(errors) } } + +fn external_scheme(module: &Module, ty: TypeId) -> Option { + let mut current = ty; + let mut quantified = Vec::new(); + let mut seen = std::collections::HashSet::new(); + while seen.insert(current) { + let Some((variables, body)) = crate::forall_parts(&module.types, current) else { + return Some(SchemeType { + ty: current, + quantified, + }); + }; + quantified.extend_from_slice(variables); + current = body; + } + None +} diff --git a/crates/psrs-core/src/verify/scopes/mod.rs b/crates/psrs-core/src/verify/scopes/mod.rs index 81d6449a..7d6cd09c 100644 --- a/crates/psrs-core/src/verify/scopes/mod.rs +++ b/crates/psrs-core/src/verify/scopes/mod.rs @@ -40,6 +40,26 @@ pub(super) fn verify_module(module: &Module) -> Vec { ); } } + for external in &module.external_types { + let span = module + .externals + .iter() + .find(|declaration| declaration.symbol == external.symbol) + .and_then(|declaration| declaration.signature.as_ref()) + .map_or(module.span, |signature| signature.span); + let first_error = errors.len(); + types::scoped_type( + external.ty, + module, + &HashSet::new(), + span, + &mut HashSet::new(), + &mut errors, + ); + for error in &mut errors[first_error..] { + error.module = external.source_module; + } + } for declaration in &module.declarations { let mut scope = HashSet::new(); enter( diff --git a/crates/psrs-driver/src/lib.rs b/crates/psrs-driver/src/lib.rs index 49cd0444..e74874c1 100644 --- a/crates/psrs-driver/src/lib.rs +++ b/crates/psrs-driver/src/lib.rs @@ -110,10 +110,16 @@ pub struct Compilation { } pub fn compile_source(source_name: &str, source_text: &str) -> Result> { - let (core, trusted_prefix, mut warnings) = - lower_source_with_prelude_to_core(source_name, source_text)?; - let output = psrs_backend::compile(core).map_err(backend_diagnostics)?; - warnings.extend(backend_warnings(output.warnings, trusted_prefix)); + let lowered = lower_source_with_prelude_to_core(source_name, source_text)?; + let mut warnings = lowered.warnings; + let output = psrs_backend::compile_with_context( + lowered.core, + lowered.effect_context, + psrs_backend::TargetCapabilities::default(), + ) + .map_err(backend_diagnostics)? + .artifact; + warnings.extend(backend_warnings(output.warnings, lowered.trusted_prefix)); Ok(Artifact { wasm: output.wasm, wat: output.wat, @@ -121,21 +127,29 @@ pub fn compile_source(source_name: &str, source_text: &str) -> Result, + effect_context: Option, +} + /// Parses the standard library and a program module and links both into one /// Core module. Library declarations the program does not reach are pruned. fn lower_source_with_prelude_to_core( source_name: &str, source_text: &str, -) -> Result<(psrs_core::Module, usize, Vec), Vec> { +) -> Result> { let (sources, trusted_prefix) = prepend_stdlib(&[(source_name, source_text)])?; - let (module, warnings) = - program::lower_program_to_core_with_trusted_prefix_and_warnings(&sources, trusted_prefix) + let (core, warnings, effect_context) = + program::lower_program_to_core_and_effect_context(&sources, trusted_prefix) .map_err(program_diagnostics_from_hidden_prelude)?; - Ok(( - module, + Ok(LoweredSource { + core, trusted_prefix, - program::typecheck_warnings(warnings, trusted_prefix), - )) + warnings: program::typecheck_warnings(warnings, trusted_prefix), + effect_context, + }) } fn prepend_stdlib<'a>( @@ -165,17 +179,73 @@ pub(crate) fn lower_source_to_core( source_name: &str, source_text: &str, ) -> Result> { - lower_source_with_prelude_to_core(source_name, source_text).map(|(module, _, _)| module) + lower_source_with_prelude_to_core(source_name, source_text).map(|lowered| lowered.core) +} + +/// Linked Core plus the trusted Effect contract required to lower it. +#[cfg(test)] +pub(crate) struct PreparedSource { + pub core: psrs_core::Module, + pub effect_context: Option, +} + +#[cfg(test)] +pub(crate) fn prepare_main(source: &str) -> Result> { + prepare_sources(&[("Main.purs", source)]) +} + +#[cfg(test)] +pub(crate) fn prepare_sources(sources: &[(&str, &str)]) -> Result> { + let (sources, trusted_prefix) = prepend_stdlib(sources)?; + let (core, _warnings, effect_context) = + program::lower_program_to_core_and_effect_context(&sources, trusted_prefix) + .map_err(program_diagnostics_from_hidden_prelude)?; + Ok(PreparedSource { + core, + effect_context, + }) +} + +#[cfg(test)] +pub(crate) fn compile_main_stages(source: &str) -> Result> { + compile_main_with_target(source, psrs_backend::TargetCapabilities::default()) +} + +#[cfg(test)] +pub(crate) fn compile_main_with_target( + source: &str, + target: psrs_backend::TargetCapabilities, +) -> Result> { + let prepared = prepare_main(source)?; + psrs_backend::compile_with_context(prepared.core, prepared.effect_context, target) + .map_err(backend_diagnostics) +} + +#[cfg(test)] +pub(crate) fn lower_main_to_cc( + source: &str, +) -> Result> { + let prepared = prepare_main(source)?; + psrs_backend::lower_cc_with_context(prepared.core, prepared.effect_context.as_ref()) + .map_err(backend_diagnostics) } pub fn compile_source_with_dumps( source_name: &str, source_text: &str, ) -> Result> { - let (core, trusted_prefix, mut warnings) = - lower_source_with_prelude_to_core(source_name, source_text)?; - let stages = psrs_backend::compile_with_stages(core).map_err(backend_diagnostics)?; - warnings.extend(backend_warnings(stages.artifact.warnings, trusted_prefix)); + let lowered = lower_source_with_prelude_to_core(source_name, source_text)?; + let mut warnings = lowered.warnings; + let stages = psrs_backend::compile_with_context( + lowered.core, + lowered.effect_context, + psrs_backend::TargetCapabilities::default(), + ) + .map_err(backend_diagnostics)?; + warnings.extend(backend_warnings( + stages.artifact.warnings, + lowered.trusted_prefix, + )); Ok(Compilation { artifact: Artifact { wasm: stages.artifact.wasm, diff --git a/crates/psrs-driver/src/program/effects.rs b/crates/psrs-driver/src/program/effects.rs index ebb7c5a7..5bc52a47 100644 --- a/crates/psrs-driver/src/program/effects.rs +++ b/crates/psrs-driver/src/program/effects.rs @@ -1,41 +1,190 @@ use super::{DiagnosticOrigin, ProgramDiagnostic, diagnostic}; -use psrs_hir::{Expr, ExprKind, Module, SymbolId}; +use psrs_core::effect::EffectOperation; +use psrs_hir::{Expr, ExprKind, ExternalKind, Module, SymbolId, TypeDeclarationKind}; use psrs_span::TextRange; -/// Restricts references to the trusted `Prelude.runEffect` value to the -/// selected command entry. This runs on resolved HIR, before type inference. -pub(super) fn check_run_effect_scope( - modules: &[Module], - trusted_prefix: usize, -) -> Result<(), Vec> { - let Some(runner) = modules +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub(super) struct EntrySelection { + pub symbol: SymbolId, + pub source: usize, + pub span: TextRange, +} + +#[derive(Clone, Debug, PartialEq, Eq)] +pub(super) enum EntryResolution { + Selected(EntrySelection), + Missing, + Ambiguous { + entries: Vec, + main_modules: bool, + }, +} + +pub(super) fn select_entry(modules: &[Module]) -> EntryResolution { + let candidates = modules .iter() - .take(trusted_prefix) - .find(|module| module.name == "Prelude") - .and_then(|module| { + .enumerate() + .flat_map(|(source, module)| { module .declarations .iter() - .find(|declaration| declaration.name == "runEffect") - .map(|declaration| declaration.symbol) - .or_else(|| { - module - .externals - .iter() - .find(|external| external.name == "runEffect") - .map(|external| external.symbol) + .filter(|declaration| declaration.name == "main") + .map(move |declaration| EntrySelection { + symbol: declaration.symbol, + source, + span: declaration.name_span, + }) + }) + .collect::>(); + let main_modules = candidates + .iter() + .filter(|entry| modules[entry.source].name == "Main") + .copied() + .collect::>(); + match main_modules.as_slice() { + [entry] => EntryResolution::Selected(*entry), + [] if candidates.len() == 1 => EntryResolution::Selected(candidates[0]), + [] if candidates.is_empty() => EntryResolution::Missing, + _ if !main_modules.is_empty() => EntryResolution::Ambiguous { + entries: main_modules, + main_modules: true, + }, + _ => EntryResolution::Ambiguous { + entries: candidates, + main_modules: false, + }, + } +} + +pub(super) fn require_unambiguous_entry( + resolution: EntryResolution, +) -> Result, Vec> { + match resolution { + EntryResolution::Selected(entry) => Ok(Some(entry)), + EntryResolution::Missing => Ok(None), + EntryResolution::Ambiguous { + entries, + main_modules, + } => { + let message = if main_modules { + "multiple `main` declarations exist in modules named `Main`" + } else { + "program has multiple `main` declarations; define one `main` in `Main`" + }; + Err(entries + .into_iter() + .map(|entry| ProgramDiagnostic { + source: DiagnosticOrigin::Source(entry.source), + diagnostic: diagnostic("P7 entry selection", entry.span, message), }) + .collect()) + } + } +} + +pub(super) fn trusted_effect( + modules: &[Module], + trusted_prefix: usize, +) -> Result, Vec> { + let preludes = modules + .iter() + .take(trusted_prefix) + .enumerate() + .filter(|(_, module)| module.name == "Prelude") + .collect::>(); + if preludes.is_empty() { + return Ok(None); + } + if preludes.len() != 1 { + return Err(vec![ProgramDiagnostic { + source: DiagnosticOrigin::Program, + diagnostic: diagnostic( + "P7 Effect contract", + preludes[1].1.span, + "trusted program contains multiple Prelude modules", + ), + }]); + } + let (source, prelude) = preludes[0]; + let Some(effect) = prelude.types.iter().find(|declaration| { + declaration.name == "Effect" && declaration.kind == TypeDeclarationKind::Foreign + }) else { + return Ok(None); + }; + let mut operations = Vec::new(); + for (name, operation, wit_name) in [ + ("pure", EffectOperation::Pure, "pure"), + ("bind", EffectOperation::Bind, "bind"), + ("runEffect", EffectOperation::Run, "run"), + ("trap", EffectOperation::Trap, "trap"), + ] { + let Some(external) = prelude + .externals + .iter() + .find(|external| external.name == name) + else { + return Err(vec![ProgramDiagnostic { + source: DiagnosticOrigin::Source(source), + diagnostic: diagnostic( + "P7 Effect contract", + prelude.span, + "trusted Prelude is missing a required Effect operation binding", + ), + }]); + }; + if !matches!( + &external.kind, + ExternalKind::Wit { interface, function } + if interface == "psrs:effect" && function == wit_name + ) { + return Err(vec![ProgramDiagnostic { + source: DiagnosticOrigin::Source(source), + diagnostic: diagnostic( + "P7 Effect contract", + external + .signature + .as_ref() + .map_or(prelude.span, |ty| ty.span), + "trusted Prelude Effect operation has the wrong WIT identity", + ), + }]); + } + operations.push(psrs_core::effect::EffectOperationBinding { + operation, + symbol: external.symbol, + }); + } + Ok(Some(psrs_core::effect::TrustedEffect { + effect_type: effect.id, + operations, + })) +} + +/// Enforces the source compatibility rule: `runEffect` may be referenced only +/// inside the selected declaration. Passing it from that declaration to a +/// helper is allowed; this is a lexical rule, not capability confinement. +pub(super) fn check_run_effect_scope( + modules: &[Module], + entry: Option, + trusted: Option<&psrs_core::effect::TrustedEffect>, +) -> Result<(), Vec> { + let Some(runner) = trusted + .and_then(|trusted| { + trusted + .operations + .iter() + .find(|operation| operation.operation == EffectOperation::Run) }) + .map(|operation| operation.symbol) else { return Ok(()); }; - let entry = selected_entry_symbol(modules); let mut errors = Vec::new(); for (source, module) in modules.iter().enumerate() { for declaration in &module.declarations { let mut references = Vec::new(); collect_runner_references(&declaration.value, runner, &mut references); - if Some(declaration.symbol) == entry { + if entry.is_some_and(|entry| declaration.symbol == entry.symbol) { continue; } for span in references { @@ -49,6 +198,22 @@ pub(super) fn check_run_effect_scope( }); } } + for instance in &module.instances { + for member in &instance.members { + let mut references = Vec::new(); + collect_runner_references(&member.value, runner, &mut references); + for span in references { + errors.push(ProgramDiagnostic { + source: DiagnosticOrigin::Source(source), + diagnostic: diagnostic( + "P7 entry selection", + span, + "the trusted `runEffect` binding may only be referenced from the selected command entry `main`", + ), + }); + } + } + } } if errors.is_empty() { Ok(()) @@ -57,28 +222,6 @@ pub(super) fn check_run_effect_scope( } } -fn selected_entry_symbol(modules: &[Module]) -> Option { - let candidates = modules - .iter() - .flat_map(|module| { - module - .declarations - .iter() - .filter(|declaration| declaration.name == "main") - .map(move |declaration| (module.name.as_str(), declaration.symbol)) - }) - .collect::>(); - let main_module = candidates - .iter() - .filter(|(module_name, _)| *module_name == "Main") - .collect::>(); - match main_module.as_slice() { - [(_, symbol)] => Some(*symbol), - [] if candidates.len() == 1 => Some(candidates[0].1), - _ => None, - } -} - fn collect_runner_references(expression: &Expr, runner: SymbolId, spans: &mut Vec) { match &expression.kind { ExprKind::Global(symbol) if *symbol == runner => spans.push(expression.span), diff --git a/crates/psrs-driver/src/program/mod.rs b/crates/psrs-driver/src/program/mod.rs index 004d9aad..e5dcb152 100644 --- a/crates/psrs-driver/src/program/mod.rs +++ b/crates/psrs-driver/src/program/mod.rs @@ -55,9 +55,13 @@ fn compile_program_sources_with_trusted_prefix( sources: &[(&str, &str)], trusted_prefix: usize, ) -> Result> { - let (core, source_warnings) = - lower_program_to_core_with_trusted_prefix_and_warnings(sources, trusted_prefix)?; - let output = psrs_backend::compile(core).map_err(|errors| { + let (core, source_warnings, effect_context) = + lower_program_to_core_and_effect_context(sources, trusted_prefix)?; + let output = match effect_context { + Some(context) => psrs_backend::compile_with_effect_context(core, context), + None => psrs_backend::compile(core), + } + .map_err(|errors| { errors .into_iter() .map(|error| ProgramDiagnostic { @@ -93,13 +97,32 @@ pub(crate) fn lower_program_to_core_with_trusted_prefix( .map(|(core, _warnings)| core) } +#[cfg(test)] pub(crate) fn lower_program_to_core_with_trusted_prefix_and_warnings( sources: &[(&str, &str)], trusted_prefix: usize, ) -> Result<(psrs_core::Module, Vec), Vec> { - let (typed, warnings) = - typecheck_program_sources_with_trusted_prefix_and_warnings(sources, trusted_prefix)?; - let entry = select_entry(&typed)?; + lower_program_to_core_and_effect_context(sources, trusted_prefix) + .map(|(core, warnings, _context)| (core, warnings)) +} + +pub(super) fn lower_program_to_core_and_effect_context( + sources: &[(&str, &str)], + trusted_prefix: usize, +) -> Result< + ( + psrs_core::Module, + Vec, + Option, + ), + Vec, +> { + let resolved = resolve_program_sources(sources)?; + let entry = effects::require_unambiguous_entry(effects::select_entry(&resolved))?; + let trusted = effects::trusted_effect(&resolved, trusted_prefix)?; + effects::check_run_effect_scope(&resolved, entry, trusted.as_ref())?; + let (typed, warnings) = typecheck_resolved_program_with_warnings(resolved)?; + let command_entry = classify_command_entry(&typed, entry, trusted.as_ref())?; let mut modules = Vec::with_capacity(typed.len()); for (index, module) in typed.into_iter().enumerate() { match psrs_core::lower_module_unverified(module) { @@ -117,8 +140,8 @@ pub(crate) fn lower_program_to_core_with_trusted_prefix_and_warnings( } let mut linked = psrs_core::link(modules); if let Some(entry) = entry { - linked.entry = Some(entry); - psrs_core::prune_unreachable(&mut linked, entry); + linked.entry = Some(entry.symbol); + psrs_core::prune_unreachable(&mut linked, entry.symbol); } if let Err(errors) = linked.verify() { return Err(errors @@ -129,69 +152,84 @@ pub(crate) fn lower_program_to_core_with_trusted_prefix_and_warnings( }) .collect()); } - Ok((linked, warnings)) + let context = trusted.map(|trusted| psrs_core::effect::EffectCompilation { + trusted, + command_entry, + }); + Ok((linked, warnings, context)) } -/// Selects one deterministic program entry before linking. A command program -/// uses `Main.main` when that module is present; otherwise a source list with a -/// single `main` declaration is accepted. Ambiguous entries are frontend-facing -/// diagnostics instead of being resolved by input order; a missing entry is -/// left for the backend to diagnose after Core lowering so earlier backend -/// limitation diagnostics remain useful. -fn select_entry( - modules: &[psrs_thir::Module], -) -> Result, Vec> { - let candidates = modules - .iter() - .enumerate() - .flat_map(|(source, module)| { - module - .declarations - .iter() - .filter(|declaration| declaration.name == "main") - .map(move |declaration| (source, module, declaration)) - }) - .collect::>(); - let main_module = candidates +fn classify_command_entry( + typed: &[psrs_thir::Module], + selected: Option, + trusted: Option<&psrs_core::effect::TrustedEffect>, +) -> Result, Vec> { + let Some(selected) = selected else { + return Ok(None); + }; + let Some(module) = typed.get(selected.source) else { + return Err(vec![ProgramDiagnostic { + source: DiagnosticOrigin::Source(selected.source), + diagnostic: diagnostic( + "P7 entry selection", + selected.span, + "selected command entry was not type checked", + ), + }]); + }; + let Some(main) = module + .declarations .iter() - .filter(|(_, module, _)| module.name == "Main") - .collect::>(); - let selected = if main_module.len() == 1 { - Some(main_module[0].2.symbol) - } else if main_module.len() > 1 { - return Err(main_module - .into_iter() - .map(|(source, _, declaration)| ProgramDiagnostic { - source: DiagnosticOrigin::Source(*source), - diagnostic: diagnostic( - "P7 entry selection", - declaration.name_span, - "multiple `main` declarations exist in modules named `Main`", - ), - }) - .collect()); - } else if candidates.len() == 1 { - Some(candidates[0].2.symbol) - } else { - None + .find(|declaration| declaration.symbol == selected.symbol) + else { + return Err(vec![ProgramDiagnostic { + source: DiagnosticOrigin::Source(selected.source), + diagnostic: diagnostic( + "P7 entry selection", + selected.span, + "selected command entry has no typed declaration", + ), + }]); }; - if let Some(symbol) = selected { - return Ok(Some(symbol)); - } - if candidates.is_empty() { + if matches!( + module.types.get(main.ty.0 as usize), + Some(psrs_thir::Type::Constructor( + psrs_thir::TypeConstructor::Int + )) + ) { return Ok(None); } - Err(candidates - .into_iter() - .map(|(source, _, declaration)| ProgramDiagnostic { - source: DiagnosticOrigin::Source(source), + let is_effect_unit = trusted.is_some_and(|trusted| { + let Some(psrs_thir::Type::Application(function, payload)) = + module.types.get(main.ty.0 as usize) + else { + return false; + }; + matches!( + module.types.get(function.0 as usize), + Some(psrs_thir::Type::Constructor(psrs_thir::TypeConstructor::User(id))) + if *id == trusted.effect_type + ) && matches!( + module.types.get(payload.0 as usize), + Some(psrs_thir::Type::Constructor( + psrs_thir::TypeConstructor::Unit + )) + ) && main.quantified.is_empty() + }); + if is_effect_unit { + Ok(Some(psrs_core::effect::EffectCommandEntry { + symbol: selected.symbol, + })) + } else { + Err(vec![ProgramDiagnostic { + source: DiagnosticOrigin::Source(selected.source), diagnostic: diagnostic( "P7 entry selection", - declaration.name_span, - "program has multiple `main` declarations; define one `main` in `Main`", + main.name_span, + "command entry must have type `Int` or `Effect Unit`", ), - }) - .collect()) + }]) + } } /// Resolves a program from a list of `(source_name, source_text)` pairs. Module @@ -263,6 +301,18 @@ fn typecheck_program_sources_with_trusted_prefix_and_warnings( pub(super) fn typecheck_program_with_warnings( modules: Vec, trusted_prefix: usize, +) -> Result<(Vec, Vec), Vec> { + let entry = match effects::select_entry(&modules) { + effects::EntryResolution::Selected(entry) => Some(entry), + effects::EntryResolution::Missing | effects::EntryResolution::Ambiguous { .. } => None, + }; + let trusted = effects::trusted_effect(&modules, trusted_prefix)?; + effects::check_run_effect_scope(&modules, entry, trusted.as_ref())?; + typecheck_resolved_program_with_warnings(modules) +} + +fn typecheck_resolved_program_with_warnings( + modules: Vec, ) -> Result<(Vec, Vec), Vec> { let true_symbols = psrs_desugar::true_symbols(&modules); let mut desugared = Vec::with_capacity(modules.len()); @@ -285,7 +335,6 @@ pub(super) fn typecheck_program_with_warnings( return Err(errors); } let modules = desugared; - effects::check_run_effect_scope(&modules, trusted_prefix)?; // Kind checking runs once for the whole program and produces the one // environment every module's type check consumes. Its diagnostics are // reported here rather than dropped: a conflict in module A is reported @@ -310,17 +359,6 @@ pub(super) fn typecheck_program_with_warnings( ), }); } - let effect_type = modules - .iter() - .take(trusted_prefix) - .find(|module| module.name == "Prelude") - .and_then(|module| { - module - .types - .iter() - .find(|declaration| declaration.name == "Effect") - .map(|declaration| declaration.id) - }); let mut known_types = modules .iter() .flat_map(|module| module.types.iter().cloned()) @@ -377,29 +415,12 @@ pub(super) fn typecheck_program_with_warnings( &instance_sets, &exported_instances, ); - let trusted_effect_representation = index < trusted_prefix - && matches!( - module.name.as_str(), - "Prelude" - | "Effect" - | "Effect.Console" - | "Test.Assert" - | "WASI.Resource" - | "WASI.IO" - | "WASI.Clock" - | "WASI.Random" - | "WASI.Console" - | "WASI.Process" - | "WASI.FileSystem" - | "WASI.Network" - | "WASI" - ); let check = psrs_typecheck::typecheck_module_with_checked_kinds_and_module_names_and_warnings( module, &imported, - effect_type, - trusted_effect_representation, + None, + false, psrs_typecheck::TypecheckContext { known_types: &known_types, imported_instances: &imported_instances, diff --git a/crates/psrs-driver/src/tests/adts.rs b/crates/psrs-driver/src/tests/adts.rs index 1b43d265..740d3acd 100644 --- a/crates/psrs-driver/src/tests/adts.rs +++ b/crates/psrs-driver/src/tests/adts.rs @@ -86,9 +86,7 @@ fn runs_a_case_on_nullary_constructors_when_wasmtime_is_available() { #[test] fn lowers_enum_case_to_mir_switch_and_wasm_br_table() { - let stages = - psrs_backend::compile_with_stages(lower_source_to_core("Main.purs", ENUM_SOURCE).unwrap()) - .unwrap(); + let stages = crate::compile_main_stages(ENUM_SOURCE).unwrap(); let has_tag_switch = stages .cc .functions diff --git a/crates/psrs-driver/src/tests/backend.rs b/crates/psrs-driver/src/tests/backend.rs index be2bebca..372e37e6 100644 --- a/crates/psrs-driver/src/tests/backend.rs +++ b/crates/psrs-driver/src/tests/backend.rs @@ -4,8 +4,7 @@ use super::*; fn structures_wasm_ir_with_a_structured_region() { let source = "module Main where\nchoose condition = if condition then 9 else 2\nmain = choose true\n"; - let core = lower_source_to_core("Main.purs", source).unwrap(); - let stages = psrs_backend::compile_with_stages(core).unwrap(); + let stages = crate::compile_main_stages(source).unwrap(); assert!( stages.wasm.functions.iter().any(|function| function .body diff --git a/crates/psrs-driver/src/tests/cc_ir_audit.rs b/crates/psrs-driver/src/tests/cc_ir_audit.rs index f54134f3..b9b416ee 100644 --- a/crates/psrs-driver/src/tests/cc_ir_audit.rs +++ b/crates/psrs-driver/src/tests/cc_ir_audit.rs @@ -71,8 +71,7 @@ fn expect_prelude_program_exit(name: &str, sources: &[(&str, &str)], expected: i } fn cc_stages(source: &str) -> psrs_backend::Stages { - let core = lower_source_to_core("Main.purs", source).expect("source lowers to Core"); - psrs_backend::compile_with_stages(core).expect("Core lowers through CC to Wasm") + crate::compile_main_stages(source).expect("Core lowers through CC to Wasm") } const RECURSIVE_SUM: &str = "module Main where\nimport Prelude\ng :: Int -> Int -> Int\ng n acc = if n == 0 then acc else g (n - 1) (acc + 1)\n"; diff --git a/crates/psrs-driver/src/tests/dictionary_audit/fixtures/evidence.rs b/crates/psrs-driver/src/tests/dictionary_audit/fixtures/evidence.rs index 68d23f4b..35eaf70d 100644 --- a/crates/psrs-driver/src/tests/dictionary_audit/fixtures/evidence.rs +++ b/crates/psrs-driver/src/tests/dictionary_audit/fixtures/evidence.rs @@ -153,6 +153,7 @@ pub(crate) fn dictionary_module() -> (thir::Module, SymbolId) { id: module_id, name: "Main".into(), externals: Vec::new(), + external_types: Vec::new(), types, newtype_ids: Vec::new(), opaque_ids: Vec::new(), @@ -324,6 +325,7 @@ pub(crate) fn escaping_method_module() -> (thir::Module, SymbolId) { id: module_id, name: "Main".into(), externals: Vec::new(), + external_types: Vec::new(), types, newtype_ids: Vec::new(), opaque_ids: Vec::new(), diff --git a/crates/psrs-driver/src/tests/dictionary_audit/fixtures/generic.rs b/crates/psrs-driver/src/tests/dictionary_audit/fixtures/generic.rs index 78783e51..b5ed4b45 100644 --- a/crates/psrs-driver/src/tests/dictionary_audit/fixtures/generic.rs +++ b/crates/psrs-driver/src/tests/dictionary_audit/fixtures/generic.rs @@ -123,6 +123,7 @@ pub(crate) fn erased_dictionary_module() -> (thir::Module, SymbolId) { id: module_id, name: "Main".into(), externals: Vec::new(), + external_types: Vec::new(), types, newtype_ids: Vec::new(), opaque_ids: Vec::new(), @@ -241,6 +242,7 @@ pub(crate) fn polymorphic_method_module() -> (thir::Module, SymbolId) { id: module_id, name: "Main".into(), externals: Vec::new(), + external_types: Vec::new(), types, newtype_ids: Vec::new(), opaque_ids: Vec::new(), diff --git a/crates/psrs-driver/src/tests/dictionary_audit/fixtures/methods.rs b/crates/psrs-driver/src/tests/dictionary_audit/fixtures/methods.rs index 86340326..cc13a951 100644 --- a/crates/psrs-driver/src/tests/dictionary_audit/fixtures/methods.rs +++ b/crates/psrs-driver/src/tests/dictionary_audit/fixtures/methods.rs @@ -84,6 +84,7 @@ pub(crate) fn default_method_module() -> (thir::Module, SymbolId) { id: module_id, name: "Main".into(), externals: Vec::new(), + external_types: Vec::new(), types, newtype_ids: Vec::new(), opaque_ids: Vec::new(), @@ -334,6 +335,7 @@ pub(crate) fn recursive_instance_module() -> (thir::Module, SymbolId) { intrinsic(int_sub, "intSub", Intrinsic::I32Sub), intrinsic(int_le, "intLe", Intrinsic::I32LeS), ], + external_types: Vec::new(), types, newtype_ids: Vec::new(), opaque_ids: Vec::new(), diff --git a/crates/psrs-driver/src/tests/dictionary_audit/fixtures/ordering.rs b/crates/psrs-driver/src/tests/dictionary_audit/fixtures/ordering.rs index 2152a956..bb595aa7 100644 --- a/crates/psrs-driver/src/tests/dictionary_audit/fixtures/ordering.rs +++ b/crates/psrs-driver/src/tests/dictionary_audit/fixtures/ordering.rs @@ -153,6 +153,7 @@ pub(crate) fn ordered_dictionaries_module() -> (thir::Module, SymbolId) { id: module_id, name: "Main".into(), externals: Vec::new(), + external_types: Vec::new(), types, newtype_ids: Vec::new(), opaque_ids: Vec::new(), @@ -345,6 +346,7 @@ pub(crate) fn shared_dictionary_module() -> (thir::Module, SymbolId) { id: module_id, name: "Main".into(), externals: Vec::new(), + external_types: Vec::new(), types, newtype_ids: Vec::new(), opaque_ids: Vec::new(), diff --git a/crates/psrs-driver/src/tests/dictionary_audit/negative.rs b/crates/psrs-driver/src/tests/dictionary_audit/negative.rs index d0298b7d..27f37ea7 100644 --- a/crates/psrs-driver/src/tests/dictionary_audit/negative.rs +++ b/crates/psrs-driver/src/tests/dictionary_audit/negative.rs @@ -52,6 +52,7 @@ fn module_with(bad: thir::Declaration, span: TextRange) -> thir::Module { id: ModuleId(0), name: "Main".into(), externals: Vec::new(), + external_types: Vec::new(), types: types.list(), newtype_ids: Vec::new(), opaque_ids: Vec::new(), diff --git a/crates/psrs-driver/src/tests/effect_arity.rs b/crates/psrs-driver/src/tests/effect_arity.rs index 57e6dd81..88480fbf 100644 --- a/crates/psrs-driver/src/tests/effect_arity.rs +++ b/crates/psrs-driver/src/tests/effect_arity.rs @@ -9,8 +9,7 @@ use super::run_with_wasmtime; #[test] fn an_effect_of_a_function_is_not_arity_two_and_log_is_saturated() { let source = "module Main where\nimport Prelude\nimport WASI.Clock\nimport WASI.Console\nmk :: Effect (Int -> Int)\nmk = pure (\\x -> x + 1)\nmain = let stored = now in let message = log \"message\" in runEffect (bind mk (\\f -> pure (f 41)))\n"; - let core = crate::lower_source_to_core("Main.purs", source).expect("source lowers to Core"); - let stages = psrs_backend::compile_with_stages(core).expect("Core lowers through CC"); + let stages = crate::compile_main_stages(source).expect("Core lowers through CC"); let function = |name: &str| { stages .cc @@ -75,10 +74,7 @@ fn an_effect_of_a_function_is_not_arity_two_and_log_is_saturated() { #[test] fn a_partial_source_application_captures_once_and_defers_the_effect() { let stored = "module Main where\nimport Prelude\nimport WASI.Console\npick :: Boolean -> String -> Effect Unit\npick choice message = if choice then log message else log \"other\"\nmain = let partial = pick true in 0\n"; - let stages = psrs_backend::compile_with_stages( - crate::lower_source_to_core("Main.purs", stored).expect("source lowers to Core"), - ) - .expect("Core lowers through CC"); + let stages = crate::compile_main_stages(stored).expect("Core lowers through CC"); let pick = stages .cc .functions diff --git a/crates/psrs-driver/src/tests/effects/contract.rs b/crates/psrs-driver/src/tests/effects/contract.rs new file mode 100644 index 00000000..2cd8bd8b --- /dev/null +++ b/crates/psrs-driver/src/tests/effects/contract.rs @@ -0,0 +1,187 @@ +use psrs_core::effect::{EffectCommandEntry, EffectCompilation, EffectOperation}; + +fn fixture() -> (psrs_core::Module, EffectCompilation) { + let lowered = crate::lower_source_with_prelude_to_core( + "Main.purs", + "module Main where\nimport Prelude\nmain = 0\n", + ) + .unwrap(); + let core = lowered.core; + let context = lowered.effect_context; + ( + core, + context.expect("embedded Prelude supplies the trusted contract"), + ) +} + +fn rejects(core: psrs_core::Module, context: EffectCompilation, message: &str) { + let errors = psrs_backend::compile_with_context( + core, + Some(context), + psrs_backend::TargetCapabilities::default(), + ) + .expect_err("a malformed explicit Effect contract must fail before encoding"); + assert!( + errors.iter().any(|error| error.message.contains(message)), + "{errors:?}" + ); +} + +#[test] +fn the_backend_rejects_partial_and_duplicate_trusted_operation_metadata() { + let (core, mut context) = fixture(); + context + .trusted + .operations + .retain(|binding| binding.operation != EffectOperation::Trap); + rejects(core, context, "missing a required operation binding"); + + let (core, mut context) = fixture(); + context + .trusted + .operations + .push(context.trusted.operations[0]); + rejects(core, context, "duplicated"); +} + +#[test] +fn the_backend_rejects_operation_identity_and_checked_signature_mismatches() { + let (core, mut context) = fixture(); + context.trusted.operations[0].symbol = core.entry.unwrap(); + rejects(core, context, "no external declaration"); + + let (mut core, context) = fixture(); + let pure = context + .trusted + .operations + .iter() + .find(|binding| binding.operation == EffectOperation::Pure) + .unwrap() + .symbol; + let integer = psrs_core::TypeId( + core.types + .iter() + .position(|ty| { + matches!( + ty, + psrs_core::Type::Constructor(psrs_core::TypeConstructor::Int) + ) + }) + .unwrap() as u32, + ); + core.external_types + .iter_mut() + .find(|external| external.symbol == pure) + .unwrap() + .ty = integer; + rejects(core, context, "invalid checked source signature"); +} + +#[test] +fn the_backend_rejects_an_effect_entry_context_for_an_integer_source_entry() { + let (core, mut context) = fixture(); + context.command_entry = Some(EffectCommandEntry { + symbol: core.entry.unwrap(), + }); + rejects(core, context, "must have type Effect Unit"); +} + +fn action_fixture() -> (psrs_core::Module, EffectCompilation) { + let lowered = crate::lower_source_with_prelude_to_core( + "Main.purs", + "module Main where\nimport Prelude\nmain :: Effect Unit\nmain = pure unit\n", + ) + .unwrap(); + (lowered.core, lowered.effect_context.unwrap()) +} + +#[test] +fn effect_command_metadata_must_name_the_selected_source_entry() { + let (mut core, mut context) = action_fixture(); + let selected = core.entry.unwrap(); + let mut decoy = core + .declarations + .iter() + .find(|decl| decl.symbol == selected) + .unwrap() + .clone(); + decoy.symbol = psrs_hir::SymbolId::new(selected.module, 1_000_000); + decoy.name = "decoy".into(); + context.command_entry = Some(EffectCommandEntry { + symbol: decoy.symbol, + }); + core.declarations.push(decoy); + rejects(core, context, "selected source entry"); +} + +#[test] +fn an_effect_source_entry_requires_command_metadata() { + let (core, mut context) = action_fixture(); + context.command_entry = None; + rejects(core, context, "missing Effect command entry"); +} + +#[test] +fn checked_import_verification_keeps_the_foreign_source_module() { + let prepared = crate::prepare_sources(&[ + ( + "Clock.purs", + "module Clock where\nimport Prelude\nforeign import \"wasi:clocks/monotonic-clock#now\" keep :: Int\n", + ), + ( + "Main.purs", + "module Main where\nimport Prelude\nimport Clock\nmain = keep\n", + ), + ]) + .expect("the clock import links before its checked signature is damaged"); + let mut core = prepared.core; + let context = prepared.effect_context.expect("trusted effect"); + let entry = core.entry.expect("selected main"); + let keep = core + .externals + .iter() + .find(|external| external.name == "keep") + .expect("clock import") + .symbol; + let source_module = core + .external_types + .iter() + .find(|external| external.symbol == keep) + .expect("checked clock signature") + .source_module; + assert_ne!(source_module, entry.module); + core.types + .push(psrs_core::Type::Variable(psrs_hir::TypeVariableId(900_001))); + let free = psrs_core::TypeId((core.types.len() - 1) as u32); + core.external_types + .iter_mut() + .find(|external| external.symbol == keep) + .expect("checked clock signature") + .ty = free; + let context = Some(context); + let optimized = psrs_backend::compile_with_context( + core.clone(), + context.clone(), + psrs_backend::TargetCapabilities::default(), + ) + .expect_err("optimization must reject an unbound variable in a checked import"); + let lowered = psrs_backend::lower_cc_with_context(core, context.as_ref()) + .expect_err("effect lowering must reject an unbound variable in a checked import"); + for errors in [optimized, lowered] { + assert!( + errors.iter().any(|error| { + error.module == Some(source_module) + && error + .message + .contains("type variable is outside its quantifier scope") + }), + "{errors:?}" + ); + assert!( + errors + .iter() + .all(|error| error.module != Some(entry.module)), + "the entry module must not own the import's verification failure: {errors:?}" + ); + } +} diff --git a/crates/psrs-driver/src/tests/effects/entry.rs b/crates/psrs-driver/src/tests/effects/entry.rs new file mode 100644 index 00000000..b47ec88e --- /dev/null +++ b/crates/psrs-driver/src/tests/effects/entry.rs @@ -0,0 +1,287 @@ +use super::super::super::*; +use std::process::Output; + +#[test] +fn both_single_source_apis_compile_int_main_with_the_trusted_effect_library() { + let source = "module Main where\nimport Prelude\nmain = 0\n"; + compile_source("Main.purs", source).expect("compile_source must lower trusted Effect imports"); + compile_source_with_dumps("Main.purs", source) + .expect("compile_source_with_dumps must lower trusted Effect imports"); +} + +#[test] +fn an_effect_unit_entry_executes_its_action_once_through_both_source_apis() { + let source = "module Main where\nimport Prelude\nimport WASI.Console\nmain = log \"command\"\n"; + let artifact = compile_source("Main.purs", source).expect("inferred Effect Unit main"); + let dumped = compile_source_with_dumps("Main.purs", source) + .expect("the dump API must preserve Effect lowering context"); + for wasm in [&artifact.wasm, &dumped.artifact.wasm] { + let Some(output) = run_wasm(wasm) else { return }; + assert_eq!(output.status.code(), Some(0)); + assert_eq!(output.stdout, b"command\n"); + } +} + +#[test] +fn effect_unit_entry_runs_strict_construction_effects_before_its_action() { + let source = "module Main where\nimport Prelude\nimport WASI.Console\nmain = let ignored = runEffect (log \"construct\") in log \"action\"\n"; + let artifact = compile_source("Main.purs", source).expect("the selected main owns runEffect"); + let Some(output) = run_wasm(&artifact.wasm) else { + return; + }; + assert_eq!(output.status.code(), Some(0)); + assert_eq!(output.stdout, b"construct\naction\n"); +} + +#[test] +fn effect_unit_entry_propagates_a_trap_from_the_action() { + let source = "module Main where\nimport Prelude\nimport WASI.Console\nmain :: Effect Unit\nmain = bind (log \"before\") (\\_ -> bind trap (\\_ -> log \"after\"))\n"; + let artifact = compile_source("Main.purs", source).expect("the effect entry should compile"); + let Some(output) = run_wasm(&artifact.wasm) else { + return; + }; + assert!( + !output.status.success(), + "the action trap must escape: {output:?}" + ); + assert!( + String::from_utf8_lossy(&output.stderr).contains("wasm trap:") + || String::from_utf8_lossy(&output.stderr).contains("wasm backtrace"), + "the action trap should include a Wasmtime trap marker: {output:?}" + ); + assert_eq!( + output.stdout, b"before\n", + "the trap must suppress later output" + ); +} + +#[test] +fn the_effect_context_survives_backend_stage_recompilation() { + let source = "module Main where\nimport Prelude\nimport WASI.Console\nmain :: Effect Unit\nmain = log \"recompiled\"\n"; + let lowered = crate::lower_source_with_prelude_to_core("Main.purs", source).unwrap(); + let core = lowered.core; + let context = lowered.effect_context; + let stages = psrs_backend::compile_with_context( + core, + context, + psrs_backend::TargetCapabilities::default(), + ) + .unwrap(); + let replay = psrs_backend::compile_with_context( + stages.core.clone(), + stages.effect_context.clone(), + psrs_backend::TargetCapabilities::default(), + ) + .expect("P8 context must be retained with the returned Core"); + let Some(output) = run_wasm(&replay.artifact.wasm) else { + return; + }; + assert_eq!(output.status.code(), Some(0)); + assert_eq!(output.stdout, b"recompiled\n"); +} + +#[test] +fn a_quantified_effect_import_lowers_to_a_monotype_wrapper() { + let clock = ( + "Clock.purs", + "module Clock where\nimport Prelude\nforeign import \"wasi:clocks/monotonic-clock#now\" now :: forall a. Effect Int\n", + ); + let main = ( + "Main.purs", + "module Main where\nimport Prelude\nimport WASI.Console\nimport Clock\nmain :: Effect Unit\nmain = bind now (\\_ -> log \"quantified\")\n", + ); + let artifact = compile_program_sources_with_prelude(&[clock, main]) + .expect("a rank-1 effect import must lower without repeating its forall"); + let Some(output) = run_wasm(&artifact.wasm) else { + return; + }; + assert_eq!(output.status.code(), Some(0)); + assert_eq!(output.stdout, b"quantified\n"); +} + +#[test] +fn effect_import_alias_is_expanded_before_suspension_planning() { + let types = ( + "Types.purs", + "module Types where\nimport Prelude\ntype ClockTick = Effect Int\n", + ); + let clock = ( + "Clock.purs", + "module Clock where\nimport Prelude\nimport Types\nforeign import \"wasi:clocks/monotonic-clock#now\" clock :: ClockTick\n", + ); + let main = ( + "Main.purs", + "module Main where\nimport Prelude\nimport WASI.Console\nimport Clock\nmain :: Effect Unit\nmain = bind clock (\\_ -> log \"clock completed\")\n", + ); + let artifact = compile_program_sources_with_prelude(&[types, clock, main]) + .expect("an imported alias in a WIT signature must be classified from checked types"); + let Some(output) = run_wasm(&artifact.wasm) else { + return; + }; + assert_eq!(output.status.code(), Some(0)); + assert_eq!(output.stdout, b"clock completed\n"); +} + +#[test] +fn effect_suspension_conformance_errors_keep_the_imports_source_origin() { + let clock = ( + "Clock.purs", + "module Clock where\nimport Prelude\nforeign import \"wasi:clocks/monotonic-clock#now\" clock :: Effect String\n", + ); + let main = ( + "Main.purs", + "module Main where\nimport Prelude\nimport WASI.Console\nimport Clock\nmain = bind clock (\\_ -> log \"unreachable\")\n", + ); + let errors = compile_program_sources_with_prelude(&[clock, main]) + .expect_err("a suspended host import must still match its WIT result"); + assert!( + errors.iter().any(|error| { + error.source == DiagnosticOrigin::Source(0) + && error.diagnostic.stage == "P8 WIT linking" + && error + .diagnostic + .message + .contains("source result type incompatible") + }), + "{errors:#?}" + ); +} + +#[test] +fn class_constrained_wit_imports_are_rejected_with_a_source_diagnostic() { + let source = "module Main where\nimport Prelude\nforeign import \"wasi:clocks/monotonic-clock#now\" clock :: forall a. Eq a => a\nmain = 0\n"; + let errors = compile_program_sources_with_prelude(&[("Main.purs", source)]) + .expect_err("the canonical WIT ABI cannot carry class dictionaries"); + assert!( + errors.iter().any(|error| { + error.source == DiagnosticOrigin::Source(0) + && error.diagnostic.stage == "P5 typecheck" + && error + .diagnostic + .message + .contains("class-constrained WIT imports are not supported") + }), + "{errors:#?}" + ); +} + +#[test] +fn instance_member_references_do_not_bypass_the_run_effect_scope() { + let source = "module Main where\nimport Prelude\nclass Runner a where\n run :: a -> Int\ninstance Runner Int where\n run _ = runEffect (pure 42)\nmain = run 0\n"; + let errors = compile_program_sources_with_prelude(&[("Main.purs", source)]) + .expect_err("instance methods are executable declarations too"); + assert!( + errors.iter().any(|error| { + error.source == DiagnosticOrigin::Source(0) + && error.diagnostic.stage == "P7 entry selection" + && error + .diagnostic + .message + .contains("may only be referenced from the selected command entry") + }), + "{errors:#?}" + ); +} + +#[test] +fn the_selected_entry_may_pass_run_effect_to_a_higher_order_helper() { + let source = "module Main where\nimport Prelude\nrunWith :: (Effect Int -> Int) -> Int\nrunWith runner = runner (pure 42)\nmain = runWith runEffect\n"; + let artifact = compile_source("Main.purs", source) + .expect("the selected declaration may pass its lexically scoped runner"); + let Some(output) = run_wasm(&artifact.wasm) else { + return; + }; + assert_eq!(output.status.code(), Some(42)); +} + +#[test] +fn effect_unit_entry_accepts_a_type_synonym_and_cross_module_value() { + let producer = ( + "Producer.purs", + "module Producer where\nimport Prelude\nimport WASI.Console\ntype Action = Effect Unit\naction :: Action\naction = log \"linked\"\n", + ); + let main = ( + "Main.purs", + "module Main where\nimport Prelude\nimport Producer\nmain = action\n", + ); + let artifact = compile_program_sources_with_prelude(&[producer, main]) + .expect("an inferred entry may return an imported aliased Effect Unit"); + let Some(output) = run_wasm(&artifact.wasm) else { + return; + }; + assert_eq!(output.status.code(), Some(0)); + assert_eq!(output.stdout, b"linked\n"); +} + +#[test] +fn an_effect_int_entry_remains_invalid() { + let source = "module Main where\nimport Prelude\nmain :: Effect Int\nmain = pure 42\n"; + let errors = compile_source("Main.purs", source) + .expect_err("the command entry must return Int or Effect Unit"); + assert!(errors.iter().any(|error| { + error.stage == "P7 entry selection" && error.message.contains("Effect Unit") + })); +} + +#[test] +fn typechecking_does_not_require_a_unique_command_entry() { + let left = ("Left.purs", "module Left where\nmain = 0\n"); + let right = ("Right.purs", "module Right where\nmain = 0\n"); + crate::typecheck_program_sources(&[left, right]) + .expect("ordinary typechecking does not select a command entry"); + let errors = compile_program_sources_with_prelude(&[left, right]) + .expect_err("compilation requires one command entry"); + assert!(errors.iter().any(|error| { + error.diagnostic.stage == "P7 entry selection" + && error + .diagnostic + .message + .contains("multiple `main` declarations") + })); +} + +#[test] +fn a_main_in_the_main_module_takes_precedence_and_unique_main_is_the_fallback() { + let other = ("Other.purs", "module Other where\nmain = 1\n"); + let main = ("Main.purs", "module Main where\nmain = 42\n"); + let preferred = compile_program_sources(&[other, main]).unwrap(); + let Some(output) = run_wasm(&preferred.wasm) else { + return; + }; + assert_eq!(output.status.code(), Some(42)); + + let unique = ("Runner.purs", "module Runner where\nmain = 7\n"); + let fallback = compile_program_sources(&[unique]).unwrap(); + let Some(output) = run_wasm(&fallback.wasm) else { + return; + }; + assert_eq!(output.status.code(), Some(7)); +} + +fn run_wasm(wasm: &[u8]) -> Option { + if std::process::Command::new("wasmtime") + .arg("--version") + .output() + .is_err() + { + if std::env::var("PSRS_REQUIRE_WASMTIME").as_deref() == Ok("1") { + panic!("PSRS_REQUIRE_WASMTIME=1 but wasmtime is not installed"); + } + eprintln!("skipping: wasmtime is not installed"); + return None; + } + static COUNTER: std::sync::atomic::AtomicU32 = std::sync::atomic::AtomicU32::new(0); + let id = COUNTER.fetch_add(1, std::sync::atomic::Ordering::Relaxed); + let path = std::env::temp_dir().join(format!( + "psrs-effect-entry-{}-{id}.wasm", + std::process::id() + )); + std::fs::write(&path, wasm).unwrap(); + let output = std::process::Command::new("wasmtime") + .arg("run") + .arg(&path) + .output() + .unwrap(); + let _ = std::fs::remove_file(path); + Some(output) +} diff --git a/crates/psrs-driver/src/tests/effects.rs b/crates/psrs-driver/src/tests/effects/mod.rs similarity index 95% rename from crates/psrs-driver/src/tests/effects.rs rename to crates/psrs-driver/src/tests/effects/mod.rs index f2ad4d51..7c2951d6 100644 --- a/crates/psrs-driver/src/tests/effects.rs +++ b/crates/psrs-driver/src/tests/effects/mod.rs @@ -1,3 +1,6 @@ +mod contract; +mod entry; + use super::super::*; use std::sync::atomic::{AtomicU32, Ordering}; @@ -121,11 +124,11 @@ fn transitive_effect_types_keep_their_closure_representation() { fn an_untrusted_prelude_effect_remains_an_ordinary_user_type() { let prelude_source = ( "Prelude.purs", - "module Prelude where\ndata Effect a = MkEffect a\nidentity :: Effect Int\nidentity = MkEffect 42\n", + "module Prelude where\nforeign import data Effect :: Type -> Type\nforeign import \"wasi:clocks/monotonic-clock#now\" foreignEffect :: Effect Int\n", ); let main_source = ( "Main.purs", - "module Main where\nimport Prelude\nforward :: Effect Int\nforward = identity\nmain = 0\n", + "module Main where\nimport Prelude\nforward :: Effect Int\nforward = foreignEffect\nmain = 0\n", ); let typed = crate::program::typecheck_program_sources(&[prelude_source, main_source]).unwrap(); let main = typed.iter().find(|module| module.name == "Main").unwrap(); @@ -142,7 +145,18 @@ fn an_untrusted_prelude_effect_remains_an_ordinary_user_type() { main.types[effect_constructor.0 as usize], psrs_thir::Type::Constructor(psrs_thir::TypeConstructor::User(_)) )); - assert!(compile_program_sources(&[prelude_source, main_source]).is_ok()); + let errors = compile_program_sources(&[prelude_source, main_source]) + .expect_err("the untrusted nominal Effect remains an ordinary WIT result type"); + assert!( + errors.iter().any(|error| { + error.diagnostic.stage == "P8 WIT linking" + && error + .diagnostic + .message + .contains("source result type incompatible") + }), + "{errors:#?}" + ); } #[test] @@ -390,7 +404,9 @@ fn ado_notation_combines_effectful_arguments_in_order() { #[test] fn ado_notation_runs_effects_left_to_right() { - let source = "module Main where\nimport Prelude\nimport WASI.Console\nmain = runEffect (ado\n first <- log \"first\"\n second <- log \"second\"\n in first)\n"; + // The `ado` block stays outside `let`: its `in` closes the nearest + // layout `let`, so the Int entry is the block's own result. + let source = "module Main where\nimport Prelude\nimport WASI.Console\nmain = runEffect (ado\n first <- log \"first\"\n second <- log \"second\"\n in 0)\n"; let Some(output) = run_effect_program(source) else { eprintln!("skipping: wasmtime is not installed"); return; diff --git a/crates/psrs-driver/src/tests/generic_aggregate_audit.rs b/crates/psrs-driver/src/tests/generic_aggregate_audit.rs index 90142e3f..1c59130b 100644 --- a/crates/psrs-driver/src/tests/generic_aggregate_audit.rs +++ b/crates/psrs-driver/src/tests/generic_aggregate_audit.rs @@ -127,8 +127,7 @@ fn retained_generic_capture_executes_through_a_closure() { } fn assert_retained_capture(name: &str, source: &str) { - let core = lower_source_to_core("Main.purs", source).expect("closure source should lower"); - let stages = psrs_backend::compile_with_stages(core).expect("closure should compile"); + let stages = crate::compile_main_stages(source).expect("closure should compile"); assert!( stages .mir @@ -152,8 +151,7 @@ fn assert_retained_capture(name: &str, source: &str) { #[test] fn p9_reuses_helpers_for_equal_complete_conversion_plans() { let source = "module Main where\nimport Prelude\ncopy :: forall a. Array a -> Array a\ncopy values = values\nmain = arrayIndex (copy [1, 2]) 0 + arrayIndex (copy [3, 4]) 1\n"; - let core = lower_source_to_core("Main.purs", source).unwrap(); - let backend_input = psrs_backend::cc::lower_module(core).unwrap(); + let backend_input = crate::lower_main_to_cc(source).unwrap(); let (mir, _) = psrs_backend::mir::lower_module_with_bindings( backend_input.cc, backend_input.externals, @@ -399,7 +397,8 @@ use fixtures::{array_new_default_count, clear_array_literals}; #[test] fn empty_array_reconstruction_executes() { let source = "module Main where\ndata Wrap a = Wrap (Array a)\nwrap :: forall a. Array a -> Wrap a\nwrap values = Wrap values\nunwrap :: forall a. Wrap a -> Array a\nunwrap value = case value of\n Wrap values -> values\nmain = arrayLength (unwrap (wrap [0]))\n"; - let mut core = lower_source_to_core("Main.purs", source).expect("source should lower to Core"); + let mut prepared = crate::prepare_main(source).expect("source should lower to Core"); + let core = &mut prepared.core; let mut cleared = false; for declaration in &mut core.declarations { cleared |= clear_array_literals(&mut declaration.value); @@ -408,8 +407,12 @@ fn empty_array_reconstruction_executes() { cleared, "the fixture should contain an array literal to empty" ); - let stages = psrs_backend::compile_with_stages(core) - .expect("an empty concrete array must still lower through the conversion path"); + let stages = psrs_backend::compile_with_context( + prepared.core, + prepared.effect_context, + psrs_backend::TargetCapabilities::default(), + ) + .expect("an empty concrete array must still lower through the conversion path"); assert!( array_new_default_count(&stages.mir) >= 1, "the empty array should still allocate its canonical destination" diff --git a/crates/psrs-driver/src/tests/integration.rs b/crates/psrs-driver/src/tests/integration.rs index 81f78fab..eecc4aa2 100644 --- a/crates/psrs-driver/src/tests/integration.rs +++ b/crates/psrs-driver/src/tests/integration.rs @@ -118,8 +118,7 @@ fn exposes_readable_core_and_backend_ir_dumps() { #[test] fn backend_stages_expose_core_after_p7() { - let core = lower_source_to_core("Main.purs", "module Main where\nmain = 3\n").unwrap(); - let stages = psrs_backend::compile_with_stages(core).unwrap(); + let stages = crate::compile_main_stages("module Main where\nmain = 3\n").unwrap(); let main = stages .core .declarations @@ -232,7 +231,12 @@ fn rejects_ambiguous_program_entries_instead_of_using_source_order() { #[test] fn attributes_backend_errors_to_their_declaring_module() { - let a = ("A.purs", "module A where\nmain = let x = x in x\n"); + // The result uses `x`, so dead-binding cleanup cannot delete the cycle + // before closure conversion. The entry stays `Int`. + let a = ( + "A.purs", + "module A where\nmain :: Int\nmain = let x = x in x\n", + ); let b = ("B.purs", "module B where\nanswer = 0\n"); let errors = compile_program_sources(&[a, b]).unwrap_err(); assert!(errors.iter().any(|error| { diff --git a/crates/psrs-driver/src/tests/mod.rs b/crates/psrs-driver/src/tests/mod.rs index f1f97c97..8a8bf0c5 100644 --- a/crates/psrs-driver/src/tests/mod.rs +++ b/crates/psrs-driver/src/tests/mod.rs @@ -20,8 +20,7 @@ mod semigroup; mod show; fn lower_source_to_mir(source: &str) -> psrs_backend::mir::Module { - let core = lower_source_to_core("Main.purs", source).expect("source should lower to Core"); - let backend_input = psrs_backend::cc::lower_module(core).expect("Core should lower to CC"); + let backend_input = crate::lower_main_to_cc(source).expect("Core should lower to CC"); psrs_backend::mir::lower_module_with_bindings( backend_input.cc, backend_input.externals, diff --git a/crates/psrs-driver/src/tests/parameterized_shapes.rs b/crates/psrs-driver/src/tests/parameterized_shapes.rs index 719d9674..e0e24fcd 100644 --- a/crates/psrs-driver/src/tests/parameterized_shapes.rs +++ b/crates/psrs-driver/src/tests/parameterized_shapes.rs @@ -12,10 +12,13 @@ unwrap value = case value of Wrap values -> values main = arrayIndex (unwrap (wrap [40, 42])) 1 "; - let core = lower_source_to_core("Main.purs", source).expect("source should lower to Core"); - let generic_cc = psrs_backend::cc::lower_module(core.clone()) - .expect("generic source Core should lower to CC before P7") - .cc; + let prepared = crate::prepare_main(source).expect("source should lower to Core"); + let generic_cc = psrs_backend::lower_cc_with_context( + prepared.core.clone(), + prepared.effect_context.as_ref(), + ) + .expect("generic source Core should lower to CC before P7") + .cc; let generic_array_maps = aggregate_conversions(&generic_cc) .iter() .map(|conversion| array_map_count(&conversion.plan)) @@ -24,8 +27,12 @@ main = arrayIndex (unwrap (wrap [40, 42])) 1 generic_array_maps >= 2, "expected pre-P7 concrete/generic boundary maps; found {generic_array_maps}" ); - let stages = psrs_backend::compile_with_stages(core) - .expect("generic Array a must map at concrete call boundaries"); + let stages = psrs_backend::compile_with_context( + prepared.core, + prepared.effect_context, + psrs_backend::TargetCapabilities::default(), + ) + .expect("generic Array a must map at concrete call boundaries"); let erased = psrs_backend::cc::ValueShape::Reference(psrs_backend::cc::Reference { nullable: false, heap: psrs_backend::cc::RefShape::Erased, @@ -100,10 +107,13 @@ copy :: forall a. { items :: Array a, value :: a } -> { items :: Array a, value copy record = record { value = record.value } main = arrayIndex ((copy { items: [40, 42], value: 7 }).items) 1 "; - let core = lower_source_to_core("Main.purs", source).expect("source should lower to Core"); - let generic_cc = psrs_backend::cc::lower_module(core.clone()) - .expect("generic source Core should lower to CC before P7") - .cc; + let prepared = crate::prepare_main(source).expect("source should lower to Core"); + let generic_cc = psrs_backend::lower_cc_with_context( + prepared.core.clone(), + prepared.effect_context.as_ref(), + ) + .expect("generic source Core should lower to CC before P7") + .cc; let generic_conversions = aggregate_conversions(&generic_cc); assert!( generic_conversions @@ -111,8 +121,12 @@ main = arrayIndex ((copy { items: [40, 42], value: 7 }).items) 1 .any(|conversion| { contains_canonical_record_array_map(&conversion.plan) }), "expected a pre-P7 canonical closed-record map containing a nested array map" ); - let stages = psrs_backend::compile_with_stages(core) - .expect("closed generic records should map across concrete instantiations"); + let stages = psrs_backend::compile_with_context( + prepared.core, + prepared.effect_context, + psrs_backend::TargetCapabilities::default(), + ) + .expect("closed generic records should map across concrete instantiations"); assert!(stages.artifact.wat.contains("struct.new")); assert!(stages.artifact.wat.contains("struct.get")); assert!(stages.artifact.wat.contains("array.new_fixed")); @@ -136,10 +150,13 @@ duplicate :: forall a. Array (Array a) -> Array (Array a) duplicate values = values main = arrayIndex (arrayIndex (duplicate [[40, 42]]) 0) 1 "; - let core = lower_source_to_core("Main.purs", source).expect("source should lower to Core"); - let generic_cc = psrs_backend::cc::lower_module(core.clone()) - .expect("generic source Core should lower to CC before P7") - .cc; + let prepared = crate::prepare_main(source).expect("source should lower to Core"); + let generic_cc = psrs_backend::lower_cc_with_context( + prepared.core.clone(), + prepared.effect_context.as_ref(), + ) + .expect("generic source Core should lower to CC before P7") + .cc; let conversions = aggregate_conversions(&generic_cc); let maximum_nested_array_maps = conversions .iter() @@ -150,8 +167,12 @@ main = arrayIndex (arrayIndex (duplicate [[40, 42]]) 0) 1 maximum_nested_array_maps >= 2, "expected pre-P7 recursively nested ArrayMap plans; found depth {maximum_nested_array_maps}" ); - let stages = psrs_backend::compile_with_stages(core) - .expect("nested generic arrays should map recursively"); + let stages = psrs_backend::compile_with_context( + prepared.core, + prepared.effect_context, + psrs_backend::TargetCapabilities::default(), + ) + .expect("nested generic arrays should map recursively"); assert!(stages.artifact.wat.contains("array.get")); let Some(output) = run_wasmtime(source) else { eprintln!("skipping execution: wasmtime is not installed"); @@ -174,10 +195,13 @@ concrete :: Array Int -> Array Int concrete values = values main = arrayIndex (applyArray concrete [40, 42]) 1 "; - let core = lower_source_to_core("Main.purs", source).expect("source should lower to Core"); - let generic_cc = psrs_backend::cc::lower_module(core.clone()) - .expect("generic source Core should lower to CC before P7") - .cc; + let prepared = crate::prepare_main(source).expect("source should lower to Core"); + let generic_cc = psrs_backend::lower_cc_with_context( + prepared.core.clone(), + prepared.effect_context.as_ref(), + ) + .expect("generic source Core should lower to CC before P7") + .cc; let array_maps = aggregate_conversions(&generic_cc) .iter() .map(|conversion| array_map_count(&conversion.plan)) @@ -186,8 +210,12 @@ main = arrayIndex (applyArray concrete [40, 42]) 1 array_maps >= 2, "expected pre-P7 higher-order argument and result ArrayMap plans; found {array_maps}" ); - let stages = psrs_backend::compile_with_stages(core) - .expect("higher-order adapters should convert generic aggregate arguments and results"); + let stages = psrs_backend::compile_with_context( + prepared.core, + prepared.effect_context, + psrs_backend::TargetCapabilities::default(), + ) + .expect("higher-order adapters should convert generic aggregate arguments and results"); assert!(stages.artifact.wat.contains("array.get")); let Some(output) = run_wasmtime(source) else { eprintln!("skipping execution: wasmtime is not installed"); diff --git a/crates/psrs-driver/src/tests/pattern_matching_audit.rs b/crates/psrs-driver/src/tests/pattern_matching_audit.rs index a5ceae4a..b00802b4 100644 --- a/crates/psrs-driver/src/tests/pattern_matching_audit.rs +++ b/crates/psrs-driver/src/tests/pattern_matching_audit.rs @@ -10,8 +10,7 @@ use super::*; use psrs_backend::cc::AssignmentKind; fn stages(source: &str) -> psrs_backend::Stages { - let core = lower_source_to_core("Main.purs", source).expect("source lowers to Core"); - psrs_backend::compile_with_stages(core).expect("Core lowers through CC to Wasm") + crate::compile_main_stages(source).expect("Core lowers through CC to Wasm") } fn flatten_cc(assignments: &[psrs_backend::cc::Assignment]) -> Vec<&psrs_backend::cc::Assignment> { diff --git a/crates/psrs-driver/src/tests/polymorphism_erasure_audit.rs b/crates/psrs-driver/src/tests/polymorphism_erasure_audit.rs index 4a25bd0b..bd743c1a 100644 --- a/crates/psrs-driver/src/tests/polymorphism_erasure_audit.rs +++ b/crates/psrs-driver/src/tests/polymorphism_erasure_audit.rs @@ -61,8 +61,7 @@ fn expect_exit(name: &str, source: &str, expected: i32) { } fn pre_optimization_mir(source: &str) -> psrs_backend::mir::Module { - let core = lower_source_to_core("Main.purs", source).expect("source should lower to Core"); - let backend_input = psrs_backend::cc::lower_module(core).expect("Core should lower to CC"); + let backend_input = crate::lower_main_to_cc(source).expect("Core should lower to CC"); psrs_backend::mir::lower_module_with_bindings( backend_input.cc, backend_input.externals, @@ -89,9 +88,7 @@ fn function_type_keys(types: &[RecGroup]) -> Vec<(Vec, Vec #[test] fn equal_normalized_function_signatures_allocate_one_mir_function_type() { let source = "module Main where\nimport Prelude\nfInt :: Array Int -> Array Int\nfInt values = values\nfStr :: Array String -> Array String\nfStr values = values\nuseInt :: (Array Int -> Array Int) -> Int\nuseInt function = arrayLength (function [1, 2])\nuseStr :: (Array String -> Array String) -> Int\nuseStr function = arrayLength (function [\"a\", \"b\"])\nmain = useInt fInt + useStr fStr\n"; - let core = lower_source_to_core("Main.purs", source).expect("source should lower to Core"); - let stages = - psrs_backend::compile_with_stages(core).expect("the two function types should compile"); + let stages = crate::compile_main_stages(source).expect("the two function types should compile"); let keys = function_type_keys(&stages.mir.types); assert!( !keys.is_empty(), diff --git a/crates/psrs-driver/src/tests/scalars.rs b/crates/psrs-driver/src/tests/scalars.rs index ebe7d16c..151d5f87 100644 --- a/crates/psrs-driver/src/tests/scalars.rs +++ b/crates/psrs-driver/src/tests/scalars.rs @@ -122,9 +122,7 @@ main = pick First #[test] fn generates_floor_helpers_for_division_nested_in_case_branches() { - let core = lower_source_to_core("Main.purs", CASE_HELPER_SOURCE) - .expect("typechecking a case with nested division"); - let stages = psrs_backend::compile_with_stages(core) + let stages = crate::compile_main_stages(CASE_HELPER_SOURCE) .expect("case-nested division must generate its helper before MIR lowering"); assert!( stages.cc.functions.iter().any(|function| { diff --git a/crates/psrs-driver/src/tests/tail_calls.rs b/crates/psrs-driver/src/tests/tail_calls.rs index bd4c9802..9434ce5a 100644 --- a/crates/psrs-driver/src/tests/tail_calls.rs +++ b/crates/psrs-driver/src/tests/tail_calls.rs @@ -5,7 +5,6 @@ //! `return_call_ref` only when the target enables the tail-call proposal; the //! stable profile keeps them as ordinary calls plus return. -use super::*; use psrs_backend::TargetCapabilities; use psrs_backend::mir::Terminator; @@ -42,8 +41,7 @@ fn execute_component(name: &str, wasm: &[u8]) -> Result psrs_backend::Stages { - let core = lower_source_to_core("Main.purs", source).expect("source should lower to Core"); - psrs_backend::compile_with_target(core, target).expect("the program should compile") + crate::compile_main_with_target(source, target).expect("the program should compile") } fn has_tail_call(mir: &psrs_backend::mir::Module) -> bool { diff --git a/crates/psrs-driver/src/tests/typecheck.rs b/crates/psrs-driver/src/tests/typecheck/mod.rs similarity index 89% rename from crates/psrs-driver/src/tests/typecheck.rs rename to crates/psrs-driver/src/tests/typecheck/mod.rs index 7e1329ba..0adcc725 100644 --- a/crates/psrs-driver/src/tests/typecheck.rs +++ b/crates/psrs-driver/src/tests/typecheck/mod.rs @@ -1,5 +1,7 @@ use super::*; +mod opaque; + #[test] fn typechecks_a_polymorphic_array_signature() { let source = "module Main where\nfoo :: forall a. Array a -> Array a\nfoo x = x\n"; @@ -152,58 +154,6 @@ main = runEffect action assert!(check_source("Main.purs", source).is_err()); } -#[test] -fn lowers_an_opaque_foreign_type_to_core_without_collapsing_it_to_int() { - let source = "\ -module Main where -foreign import data Handle :: Type -foreign import data Other :: Type -keep :: Handle -> Handle -keep h = h -main = keep -"; - let core = lower_source_to_core("Main.purs", source).expect("opaque types lower to Core"); - let main = core - .declarations - .iter() - .find(|declaration| declaration.name == "main") - .expect("main"); - let Some((parameter, result)) = psrs_core::arrow_parts(&core.types, main.ty) else { - panic!( - "main should be a function, got {:?}", - core.types[main.ty.0 as usize] - ); - }; - let mut handle = None; - for end in [parameter, result] { - match &core.types[end.0 as usize] { - psrs_core::Type::Constructor(psrs_core::TypeConstructor::User(id)) => { - assert!( - core.opaque_ids.contains(id), - "Handle must be recorded as opaque" - ); - assert!( - core.constructors - .iter() - .all(|constructor| constructor.type_id != *id), - "an opaque type has no constructors" - ); - match handle { - None => handle = Some(*id), - Some(previous) => assert_eq!(previous, *id), - } - } - other => panic!("Handle must not become {other:?}"), - } - } - let handle = handle.expect("Handle"); - assert!( - core.opaque_ids.iter().any(|id| *id != handle), - "Other must stay a distinct opaque type, got {:?}", - core.opaque_ids - ); -} - #[test] fn typechecks_ado_notation_over_effect() { // `ado` desugars to `map`/`apply`/`pure`; inference must see through the diff --git a/crates/psrs-driver/src/tests/typecheck/opaque.rs b/crates/psrs-driver/src/tests/typecheck/opaque.rs new file mode 100644 index 00000000..70e50144 --- /dev/null +++ b/crates/psrs-driver/src/tests/typecheck/opaque.rs @@ -0,0 +1,55 @@ +use super::*; + +#[test] +fn lowers_an_opaque_foreign_type_to_core_without_collapsing_it_to_int() { + let source = "\ +module Main where +foreign import data Handle :: Type +foreign import data Other :: Type +keep :: Handle -> Handle +keep h = h +use :: (Handle -> Handle) -> Int +use _ = 0 +main = use keep +"; + let core = lower_source_to_core("Main.purs", source).expect("opaque types lower to Core"); + let keep = core + .declarations + .iter() + .find(|declaration| declaration.name == "keep") + .expect("keep"); + let Some((parameter, result)) = psrs_core::arrow_parts(&core.types, keep.ty) else { + panic!( + "keep should be a function, got {:?}", + core.types[keep.ty.0 as usize] + ); + }; + let mut handle = None; + for end in [parameter, result] { + match &core.types[end.0 as usize] { + psrs_core::Type::Constructor(psrs_core::TypeConstructor::User(id)) => { + assert!( + core.opaque_ids.contains(id), + "Handle must be recorded as opaque" + ); + assert!( + core.constructors + .iter() + .all(|constructor| constructor.type_id != *id), + "an opaque type has no constructors" + ); + match handle { + None => handle = Some(*id), + Some(previous) => assert_eq!(previous, *id), + } + } + other => panic!("Handle must not become {other:?}"), + } + } + let handle = handle.expect("Handle"); + assert!( + core.opaque_ids.iter().any(|id| *id != handle), + "Other must stay a distinct opaque type, got {:?}", + core.opaque_ids + ); +} diff --git a/crates/psrs-thir/src/external_type_tests.rs b/crates/psrs-thir/src/external_type_tests.rs new file mode 100644 index 00000000..c7023d31 --- /dev/null +++ b/crates/psrs-thir/src/external_type_tests.rs @@ -0,0 +1,99 @@ +use crate::{ExternalType, Module, Type, TypeConstructor, TypeId}; +use psrs_hir::{ExternalKind, ExternalSymbol, ModuleId, SymbolId, TypeVariableId}; +use psrs_span::TextRange; + +fn fixture() -> Module { + let symbol = SymbolId::new(ModuleId::INTRINSICS, 3); + Module { + id: ModuleId(2), + name: "ExternalScheme".into(), + externals: vec![ExternalSymbol { + symbol, + name: "clock".into(), + kind: ExternalKind::Wit { + interface: "wasi:clocks/monotonic-clock".into(), + function: "now".into(), + }, + signature: None, + }], + external_types: vec![ExternalType { + symbol, + source_module: ModuleId(2), + ty: TypeId(0), + }], + types: vec![Type::Constructor(TypeConstructor::Int)], + newtype_ids: Vec::new(), + opaque_ids: Vec::new(), + callable_types: Vec::new(), + constructors: Vec::new(), + declarations: Vec::new(), + type_names: Vec::new(), + span: TextRange::new(0, 5), + } +} + +fn rejects(module: &Module, fragment: &str) { + let errors = module + .verify() + .expect_err("malformed checked external scheme must fail"); + assert!( + errors.iter().any(|error| error.message.contains(fragment)), + "{errors:?}" + ); +} + +#[test] +fn a_wit_scheme_is_required_even_without_a_raw_annotation() { + let mut module = fixture(); + module.verify().unwrap(); + module.external_types.clear(); + rejects(&module, "no checked signature"); +} + +#[test] +fn checked_external_schemes_are_unique_and_have_an_external_owner() { + let mut module = fixture(); + module.external_types.push(module.external_types[0].clone()); + rejects(&module, "more than one checked signature"); + let mut module = fixture(); + module.externals.clear(); + rejects(&module, "no external declaration"); +} + +#[test] +fn checked_external_schemes_reject_invalid_type_references() { + let mut module = fixture(); + module.external_types[0].ty = TypeId(99); + rejects(&module, "type"); +} + +#[test] +fn external_quantifiers_scope_their_variables() { + let mut module = fixture(); + let variable = TypeVariableId(7); + module.types = vec![Type::Variable(variable)]; + rejects(&module, "quantifier scope"); + module.types.push(Type::ForAll { + variables: vec![variable], + body: TypeId(0), + }); + module.external_types[0].ty = TypeId(1); + module + .verify() + .expect("a properly quantified external scheme is valid"); + module.types[1] = Type::ForAll { + variables: vec![variable, variable], + body: TypeId(0), + }; + rejects(&module, "unique"); +} + +#[test] +fn cyclic_external_schemes_are_rejected() { + let mut module = fixture(); + module.types[0] = Type::ForAll { + variables: Vec::new(), + body: TypeId(0), + }; + rejects(&module, "cycle"); +} diff --git a/crates/psrs-thir/src/lib.rs b/crates/psrs-thir/src/lib.rs index 6eaa7cd3..192819de 100644 --- a/crates/psrs-thir/src/lib.rs +++ b/crates/psrs-thir/src/lib.rs @@ -177,11 +177,26 @@ pub struct ConstructorInfo { pub parameters: Vec, } +/// The normalized checked scheme for one WIT value import. Unlike the HIR +/// signature kept for names and diagnostics, `ty` has had type synonyms +/// expanded by the type checker and uses this module's type table. Intrinsics +/// use registry-owned contracts and do not appear in this table. +#[derive(Clone, Debug, PartialEq, Eq)] +pub struct ExternalType { + pub symbol: SymbolId, + /// Source module that declared this import. External symbols themselves + /// live in the reserved intrinsic namespace, so their symbol ID cannot + /// carry diagnostic origin. + pub source_module: ModuleId, + pub ty: TypeId, +} + #[derive(Clone, Debug, PartialEq, Eq)] pub struct Module { pub id: ModuleId, pub name: String, pub externals: Vec, + pub external_types: Vec, pub types: Vec, /// Nominal types whose single constructor is erased at runtime. The type /// checker keeps these types distinct; later lowering uses this metadata @@ -354,6 +369,8 @@ impl Module { } } +#[cfg(test)] +mod external_type_tests; #[cfg(test)] mod rank_n_tests; #[cfg(test)] diff --git a/crates/psrs-thir/src/rank_n_tests.rs b/crates/psrs-thir/src/rank_n_tests.rs index 5647a157..ec2705af 100644 --- a/crates/psrs-thir/src/rank_n_tests.rs +++ b/crates/psrs-thir/src/rank_n_tests.rs @@ -54,6 +54,7 @@ fn module(types: Vec, declarations: Vec) -> Module { id: ModuleId(0), name: "RankN".into(), externals: Vec::new(), + external_types: Vec::new(), types, newtype_ids: Vec::new(), opaque_ids: Vec::new(), diff --git a/crates/psrs-thir/src/scope/mod.rs b/crates/psrs-thir/src/scope/mod.rs index 00d77d7a..83984fc2 100644 --- a/crates/psrs-thir/src/scope/mod.rs +++ b/crates/psrs-thir/src/scope/mod.rs @@ -41,6 +41,16 @@ pub(super) fn verify_module(module: &Module) -> Vec { ); } } + for external in &module.external_types { + verify_type_scope( + external.ty, + &module.types, + &HashSet::new(), + module.span, + &mut HashSet::new(), + &mut errors, + ); + } for declaration in &module.declarations { let mut scope = HashSet::new(); enter_binders( diff --git a/crates/psrs-thir/src/tests.rs b/crates/psrs-thir/src/tests.rs index 222be9f4..edc82c8d 100644 --- a/crates/psrs-thir/src/tests.rs +++ b/crates/psrs-thir/src/tests.rs @@ -7,6 +7,7 @@ fn verifier_rejects_invalid_type_references() { id: ModuleId(0), name: "Main".into(), externals: Vec::new(), + external_types: Vec::new(), types: vec![Type::Constructor(TypeConstructor::Int)], newtype_ids: Vec::new(), opaque_ids: Vec::new(), @@ -44,6 +45,7 @@ fn verifier_checks_instance_context_against_constructor_parameters() { id: ModuleId(0), name: "Main".into(), externals: Vec::new(), + external_types: Vec::new(), types: vec![ Type::Constructor(TypeConstructor::Int), Type::Constructor(TypeConstructor::Record), @@ -101,6 +103,7 @@ fn verifier_requires_superclass_evidence_to_name_a_well_typed_field() { id: ModuleId(0), name: "Main".into(), externals: Vec::new(), + external_types: Vec::new(), types: vec![ Type::Constructor(TypeConstructor::Int), Type::RowEmpty, @@ -166,6 +169,7 @@ fn literal_reference_module(reference_type: TypeId) -> Module { id: ModuleId(0), name: "Main".into(), externals: Vec::new(), + external_types: Vec::new(), types: vec![ Type::Constructor(TypeConstructor::User(proxy)), Type::TypeLevelString("a".into()), @@ -253,6 +257,7 @@ fn verifier_rejects_coercion_evidence_for_a_different_boundary() { id: ModuleId(0), name: "Main".into(), externals: Vec::new(), + external_types: Vec::new(), types: vec![ Type::Constructor(TypeConstructor::Int), Type::Constructor(TypeConstructor::Boolean), diff --git a/crates/psrs-thir/src/verify/mod.rs b/crates/psrs-thir/src/verify/mod.rs index 029e5c95..20e2a369 100644 --- a/crates/psrs-thir/src/verify/mod.rs +++ b/crates/psrs-thir/src/verify/mod.rs @@ -1,12 +1,51 @@ use crate::{ Evidence, EvidenceKind, Expr, ExprKind, Module, Pattern, PatternKind, Type, TypeId, VerifyError, }; +use psrs_hir::ExternalKind; use psrs_span::TextRange; mod semantics; pub(super) fn verify_module(module: &Module) -> Result<(), Vec> { let mut errors = Vec::new(); + let mut external_type_symbols = std::collections::HashSet::new(); + for external_type in &module.external_types { + if !external_type_symbols.insert(external_type.symbol) { + errors.push(VerifyError { + span: module.span, + message: "a foreign symbol has more than one checked signature", + }); + } + if !module + .externals + .iter() + .any(|external| external.symbol == external_type.symbol) + { + errors.push(VerifyError { + span: module.span, + message: "a checked foreign signature has no external declaration", + }); + } + verify_type_id( + external_type.ty, + module.types.len(), + module.span, + &mut errors, + ); + } + for external in &module.externals { + if matches!(&external.kind, ExternalKind::Wit { .. }) + && !external_type_symbols.contains(&external.symbol) + { + errors.push(VerifyError { + span: external + .signature + .as_ref() + .map_or(module.span, |ty| ty.span), + message: "a foreign declaration has no checked signature", + }); + } + } for ty in &module.types { match ty { Type::Application(parameter, result) => { diff --git a/crates/psrs-thir/src/verify/semantics/matching/tests.rs b/crates/psrs-thir/src/verify/semantics/matching/tests.rs index d5947958..0b1cf2ed 100644 --- a/crates/psrs-thir/src/verify/semantics/matching/tests.rs +++ b/crates/psrs-thir/src/verify/semantics/matching/tests.rs @@ -41,6 +41,7 @@ fn module(types: Vec, declarations: Vec) -> Module { id: ModuleId(0), name: "Main".into(), externals: Vec::new(), + external_types: Vec::new(), types, newtype_ids: Vec::new(), opaque_ids: Vec::new(), diff --git a/crates/psrs-typecheck/src/typecheck/entry.rs b/crates/psrs-typecheck/src/typecheck/entry.rs index 71b0dae3..06643a04 100644 --- a/crates/psrs-typecheck/src/typecheck/entry.rs +++ b/crates/psrs-typecheck/src/typecheck/entry.rs @@ -163,6 +163,31 @@ pub fn typecheck_module_with_checked_kinds_and_module_names_and_warnings( let mut types = TypeInterner::default(); let mut generics = checker.state.generic_variables.clone(); + let external_types = module + .externals + .iter() + .filter_map(|external| { + if !matches!(external.kind, hir::ExternalKind::Wit { .. }) { + return None; + } + let signature = external.signature.as_ref()?; + let inferred = checker.elaborate_type_mode(signature, &mut HashMap::new(), true); + if contains_constraint(&inferred) { + checker.state.errors.push(TypeCheckError::new( + TypeCheckErrorKind::UnsupportedType, + signature.span, + "class-constrained WIT imports are not supported by the WASI binding ABI", + )); + return None; + } + let ty = checker.finalize_type(&inferred, signature.span, &mut types, &generics)?; + Some(thir::ExternalType { + symbol: external.symbol, + source_module: module.id, + ty, + }) + }) + .collect::>(); let declarations = inferred .into_iter() .filter_map(|declaration| { @@ -261,6 +286,7 @@ pub fn typecheck_module_with_checked_kinds_and_module_names_and_warnings( id: module.id, name: module.name, externals: module.externals, + external_types, types: types.values, newtype_ids, opaque_ids, @@ -287,3 +313,21 @@ pub fn typecheck_module_with_checked_kinds_and_module_names_and_warnings( .collect()), } } + +fn contains_constraint(ty: &InferType) -> bool { + match ty { + InferType::Constrained { .. } => true, + InferType::Application(function, argument) => { + contains_constraint(function) || contains_constraint(argument) + } + InferType::ForAll { body, .. } => contains_constraint(body), + InferType::RowExtend { ty, tail, .. } => { + contains_constraint(ty) || contains_constraint(tail) + } + InferType::Variable(_) + | InferType::Constructor(_) + | InferType::RowEmpty + | InferType::TypeLevelString(_) + | InferType::TypeLevelInt(_) => false, + } +} diff --git a/docs/design/D-04-suite-roadmap.md b/docs/design/D-04-suite-roadmap.md index 1635c837..cfcbe96d 100644 --- a/docs/design/D-04-suite-roadmap.md +++ b/docs/design/D-04-suite-roadmap.md @@ -250,8 +250,8 @@ total falls. Across both halves, 24 cases stop at another P3 name the library still owns — 8 on `$`, 2 each on `negate`, `_`, and the deliberately absent `assertEqual`, 2 on `logShow`, and singles on `Monad`, `Eq`, `Unit`'s import site, `append`, `show`, `Foo.Bar`, and `<>` — and 8 stop later in the pipeline -(4 at P10 entry selection, 4 at P5 type checking). No case reaches execution, so -the runtime board stays 0/413; the `unit` half also moves no case past P0, +(4 at P10 entry selection, 4 at P5 type checking). No case reached execution in +that measurement, so its runtime board stayed 0/413; the `unit` half also moves no case past P0, because the four DEC-16 surrogate files are unaffected. `Test.Assert` is landed as the four checks that need no class surface @@ -307,8 +307,8 @@ landed) and after it, with L2 `passing` resolution moves from 245/413 to **253/413**, first-stage blockers from 168 to 160, and other P3 blockers from 107 to 99. The missing-module count stays 57. Eight files leave L2; `show` and `Show` are no longer first-blocker -names. The same after-run is the L6 table below (still 0/413 executing) and the -gate rows. `Number`'s digits are not a correctly rounded ECMAScript conversion, +names. That after-run is the Show L6 table below, which was still 0/413 +executing. It is not the current gate row. `Number`'s digits are not a correctly rounded ECMAScript conversion, so a file that compares `show` of a non-dyadic fraction with the official text can still disagree once it runs. `logShow` and `assertEqual` stay with #95. @@ -556,8 +556,9 @@ obligation to FE-13, and accepted mismatches still need type-checking fixes. - **Acceptance:** Agreement on the `errorCode`s above. - **Prerequisite:** M4. -**Measured current result (2026-10-04, annotations oracle, remeasured with -`Show`):** **53/84** failing cases agree. Per-code agreement is +**Measured current result (2026-10-04, annotations oracle, remeasured with the +Effect-entry run):** **53/80** failing cases agree. An earlier headline said +53/84; the per-code totals sum to 80, and this run confirms 80. Per-code agreement is `OverlappingInstances` 8/8, `NoInstanceFound` 41/52, `MissingClassMember` 2/2, `DuplicateInstance` 1/1, `InvalidInstanceHead` 1/5, and 0 for `PossiblyInfiniteInstance` (1), `OrphanInstance` (6), `InvalidNewtypeInstance` @@ -578,8 +579,8 @@ its custom error instead of `TypesDoNotUnify`. because a visible type application on a class-method head is not yet resolved. That is the FE-17 class-head limit, and it is the one place #87's work costs agreement rather than gaining it. -M2 remains 72/72, and parse 904/908 and corpus runtime 0/413 are unchanged. -These six results were remeasured together on the integrated tree with +On that earlier integrated tree, M2 remained 72/72, parse remained 904/908, and +corpus runtime remained 0/413. These six results were remeasured together with `PSRS_ORACLE=annotations cargo test -p psrs-driver --test suite -- --ignored --nocapture`. The remaining mismatches are accounted for by those per-code results; they @@ -696,15 +697,17 @@ the code reference and an immutable capture array. file. - **Prerequisite:** M2–M6. -**Progress (measured by `runtime::l6_runtime_scoreboard`):** **0 of 413** -non-FFI `passing` files compile, validate, and run, with 26 excluded as FFI. The -board compiles each case with the on-disk standard library on the module path, -so "no scoreboard" is no longer the blocker; the compiler and the library are. -No corpus case reaches Wasmtime in this board. Separate vertical execution -tests run under mandatory Wasmtime for GC strings, arrays, closed records, -erased newtypes, parameterized ADTs, closures, dictionaries, effects, the -component path, and pattern-matrix behavior including the value-sensitive -`1185.purs` and `2049.purs` shapes. +**Progress (measured by `runtime::l6_runtime_scoreboard`):** **124 of 413** +non-FFI `passing` files compile, validate, and run, with 26 excluded as FFI. +All 124 exit 0 and print a first stdout line. They are the same 124 files whose +previous first blocker was a `main` that was not a zero-argument `Int`. The 63 +files with no selected `main` stay blocked at P10. This measurement does not +emit an empty main and does not change the 413 denominator. The board compiles +each case with the on-disk standard library on the module path. Separate +vertical execution tests run under mandatory Wasmtime for GC strings, arrays, +closed records, erased newtypes, parameterized ADTs, closures, dictionaries, +effects, the component path, and pattern-matrix behavior including the +value-sensitive `1185.purs` and `2049.purs` shapes. Agreement here means the pipeline compiles the file, the component passes Wasm validation, and the guest runs to completion without trapping. The corpus @@ -715,15 +718,30 @@ failure must reach the guest as a trap to be visible, which is the only execution signal the corpus can express. Nothing in the corpus needs argv, stdin, or a preopened directory, so the runner passes none. -The 413 rejections, by the first phase that blocks them. The current figures come +The 289 rejections, by the first phase that blocks them. The current figures come from one `PSRS_REQUIRE_WASMTIME=1 PSRS_ORACLE=annotations` run of all five boards -on 2026-10-04 at `071fb11` plus the `logShow` slice, so they are a single -consistent measurement. The two tables after it are earlier measurements taken -independently on `6f66524` and are **not** additive with it or with each other; -they are kept because the M2 paragraphs cite them. +on 2026-10-04 (Wasmtime 49.0.2, `purs` 0.15.16). L1–L5 did not move in that run. +The tables after the current one are earlier measurements and are **not** +additive with it or with each other; they are kept because the M2 paragraphs +cite them. -After `Effect.Console.logShow` (`PSRS_REQUIRE_WASMTIME=1` L6/M7 scoreboard run on -2026-10-04 at `071fb11` plus this slice): +After the `Effect Unit` command entry (the same run): + +| Blocker | Cases | Recovered by | +| --- | --- | --- | +| Missing library module | 53 | Phase 3: #94 `Prelude`, #95 `Effect`/`Effect.Console`/`Test.Assert`, #96 `Proxy`/`Partial.Unsafe`, and #124 the unowned `Data.*` modules. | +| P10 Wasm structuring | 63 | No selected `main`. The 124 files that previously stopped because `main` was not a zero-argument `Int` now run and exit 0. | +| P3 resolve | 86 | Another resolution error behind the library gap; the library surface owns most of them. | +| P5 typecheck | 46 | A type error behind the other blockers. | +| P5 kind check | 17 | A kind error behind the other blockers. | +| P8 closure conversion | 14 | A representation behind the other blockers. | +| P0 lex | 4 | The DEC-16 lone-surrogate cases, which are also L1 differences. | +| P6 Core lowering | 6 | `Prim.undefined` has no runtime representation, plus partially applied field constructors. | +| P2 surface lowering | 0 | No `passing` file stops in surface lowering; Phase 2 closed this row. | +| Harness loading | 0 | Nothing: every case assembles. | + +Earlier, after `Effect.Console.logShow` (`PSRS_REQUIRE_WASMTIME=1` L6/M7 scoreboard run on +2026-10-04 at `071fb11` plus that slice): | Blocker | Cases | Recovered by | | --- | --- | --- | @@ -801,8 +819,8 @@ The failure path is now landed rather than assumed: `Prelude.trap` is a `psrs:effect` external whose body is an unreachable path, `Test.Assert` writes a message and then escapes through it, and the vertical tests assert the trap rather than an exit code (`PSRS_REQUIRE_WASMTIME=1 cargo test -p psrs-driver ---lib tests::assertions`). No corpus case reaches Wasmtime yet, so the board -stays 0/413. +--lib tests::assertions`). That measurement's board was still 0/413. The +current board is the 124/413 table above. The L2 run reports 19 sibling modules loaded and no case blocked because the loader could not use an on-disk sibling. Before #86, two such cases were @@ -929,14 +947,15 @@ concrete slice issues as sub-issues; this table is the index. | 2 | [#75](https://github.com/biuld/purescript-rs/issues/75) Frontend surface lowering — **complete** | [#84](https://github.com/biuld/purescript-rs/issues/84) ascription, [#85](https://github.com/biuld/purescript-rs/issues/85) patterns, [#86](https://github.com/biuld/purescript-rs/issues/86) operator aliases, [#87](https://github.com/biuld/purescript-rs/issues/87) type wildcards and rows, [#88](https://github.com/biuld/purescript-rs/issues/88) guards and multi-scrutinee `case`, [#89](https://github.com/biuld/purescript-rs/issues/89) `Prim` and unary minus, [#90](https://github.com/biuld/purescript-rs/issues/90) instance resolution | **No `passing` file stops in surface lowering.** From the 61-case `5298aad` baseline, #88 moved 22 past P2, the 34 fixed pattern paths plus 22 type, kind, instance, and declaration forms brought it to 5, and [#87](https://github.com/biuld/purescript-rs/pull/122) removed the last five. All six slices are `Done`. | | 3 | [#76](https://github.com/biuld/purescript-rs/issues/76) Standard library — **next** | [#94](https://github.com/biuld/purescript-rs/issues/94) `Prelude` (77 measured after the `logShow` slice: the 7 cases that stopped on `logShow` stop instead on a `Prelude` name #94 also owns), [#95](https://github.com/biuld/purescript-rs/issues/95) `Effect`/`Effect.Console`/`Test.Assert` (305), [#96](https://github.com/biuld/purescript-rs/issues/96) `Proxy`/`Partial.Unsafe` (17), [#124](https://github.com/biuld/purescript-rs/issues/124) the `Data` modules no slice owned (27) | **342 of the 354** files L2 originally could not resolve were blocked on a missing library module. #95's first slice landed `Effect` and `Effect.Console`, dropping that to **83** and `passing` resolution from 59/413 to **199/413**; its second slice landed the `unit` value and `Test.Assert`, dropping the missing-module count to **62** and `passing` resolution to **209/413**. #94's first slice then landed `Data.Function` and the `$`/`#` operators, taking resolution to **225/413** and the missing-module count to **61**; its next slice landed `Data.Semigroup` and `<>`, taking resolution to **235/413**. `Eq`, `Ord`, and `Semiring` then landed with the intrinsic layer. The `Show` slice, measured on that master, moves resolution from 245/413 to **253/413**. `Data.Monoid` and `Data.Foldable`, measured independently on `6f66524` before `Show`, leave lenient resolution at **245/413** and move the compile-path missing-module count from 57 to 55. The figures were measured independently on `6f66524` and are not additive. The `Data.Tuple` slice, re-measured with the L2 scoreboard on `6f66524`, leaves resolution at **245/413** and moves the missing-module count from 57 to **56**, with other P3 blockers from 107 to **108**. That measurement is independent of the Show and Foldable figures and is not additive with them. Tuple's row said `logShow` and `assertEqual` were still waiting on the `Show`/`Eq` class surface, and that the GitHub `Corpus cases` field records the measured count; Show later recorded that the classes are declared and that the field was not written. What #95 still owns is `assertEqual` and `assertEqual'`; `logShow` has since landed as `log` of `show`, taking resolution to **270/413**. Depends on Phase 2, now complete: the library itself uses ascriptions, guards, sections, and instances. #94 measures 0 by first blocking stage only because `stdlib/lib/Prelude.purs` resolves; its missing surface is latent, surfacing as the P3 `Monad`, `identity`, `Functor`, and `negate` blockers *behind* the library modules. After the `logShow` slice, the 86 files blocked first at P3 on a name split as 77 to the `Prelude`/class surface #94 owns, 4 to #124 (`Unit` 2, `P.Unit` 1, `between` 1), 3 to #96 (`Partial`), and 2 to #95 (`assertEqual`). The 77 are `Monad` 13, `identity` 9, `_` 8, `negate` 6, `Functor` 6, `Eq1` 4, `<<<` 4, `otherwise` 3, `<$>` 3, `&&` 3, `when` 2, `mod` 2, `compare` 2, and one each of `P.identity`, `Applicative`, `||`, `>>>`, `not`, `-`, and `Foo.Bar`. `show` and `Show` are not in that set, and neither is `logShow` any longer. Show recorded that the GitHub `Corpus cases` field was not written because `gh` is not authenticated on that machine; Foldable's row said the field records the measured count, and that claim was not rechecked here. | | 4 | [#77](https://github.com/biuld/purescript-rs/issues/77) L4 and L5 to 100% | [#97](https://github.com/biuld/purescript-rs/issues/97) missing class checks, [#98](https://github.com/biuld/purescript-rs/issues/98) deriving and fundeps, [#99](https://github.com/biuld/purescript-rs/issues/99) hole inference, [#100](https://github.com/biuld/purescript-rs/issues/100) M3 kind gate, [#123](https://github.com/biuld/purescript-rs/issues/123) `forall` binder visibility | Turns "measurable" into "passing". #81 makes 153 cases trackable; the rest need rules. #123 is the shared root cause behind the three visible-type-application limits #87 recorded, and #100's polykind instantiation needs the same machinery, so it is filed as one foundational change rather than three patches. | -| 5 | [#78](https://github.com/biuld/purescript-rs/issues/78) Backend on real programs | [#73](https://github.com/biuld/purescript-rs/issues/73) aggregate fixture execution, [#101](https://github.com/biuld/purescript-rs/issues/101) CC/MIR coverage | Consumes the output of Phases 2–4. The backend rows are `Partial` on source coverage, not on design. | +| 5 | [#78](https://github.com/biuld/purescript-rs/issues/78) Backend on real programs | [#73](https://github.com/biuld/purescript-rs/issues/73) aggregate fixture execution, [#101](https://github.com/biuld/purescript-rs/issues/101) CC/MIR coverage, [#139](https://github.com/biuld/purescript-rs/issues/139) `Effect Unit` command entry | [#139](https://github.com/biuld/purescript-rs/issues/139) is an independent slice taken while Phase 3 and Phase 4 are still open. It does not complete those phases and it does not close #78. The other backend rows stay `Partial` on source coverage. | | 6 | [#79](https://github.com/biuld/purescript-rs/issues/79) M8 warnings and optimization | [#91](https://github.com/biuld/purescript-rs/issues/91) warning scoreboard, [#92](https://github.com/biuld/purescript-rs/issues/92) optimize comparison | Last, because both need a harness first and neither blocks another phase. | Two dependencies are worth stating because they are not visible in the table: Phase 3 cannot start before Phase 2, because the standard library is itself a -large client of the forms Phase 2 lands; and Phase 5 cannot start before Phase -3, because no corpus program is end-to-end comparable until the library -exists. +large client of the forms Phase 2 lands; and Phase 5 normally waits for Phase +3, because most corpus programs are not end-to-end comparable until the library +exists. #139 is the recorded exception: the command-entry slice above, taken +while Phase 3 and Phase 4 remain open. Wasm proposal families outside the current target — BC-04 through BC-09, multi-value signatures, bulk memory, SIMD, exceptions, threads, memory64, and @@ -1014,11 +1033,11 @@ for matrix status. | L3 | Kinds and higher-kinded types | 35/48 failing cases on the `Show` remeasurement (`KindsDoNotUnify` 15/24, `PartiallyAppliedSynonym` 10/12, and the other mapped code totals as measured in M3). The gate row Tuple left in place still said 34/48; Tuple did not remeasure L3, so 34/48 and 35/48 are not a combined result. | 100% agreement for the mapped kind cases. | | L4 | Core type checking | 35/50 failing cases; `TypesDoNotUnify` 32/41, `IntOutOfRange` 1/1, `InfiniteType` 2/2, `CannotApplyExpressionOfTypeOnType` 1/2, `EscapedSkolem` 0/2, `ExpectedType` 0/2, `AmbiguousTypeVariables` 0/1. | 100% agreement for the mapped type cases. | | L5 | Classes and instances | 53/80 failing cases; `OverlappingInstances` 8/8, `NoInstanceFound` 41/52, `MissingClassMember` 2/2, `DuplicateInstance` 1/1, `InvalidInstanceHead` 1/5, and 0 for the other mapped codes. The row previously said 84; the per-code totals sum to 80 and the remeasurement confirms 80. | 100% agreement for the mapped class cases. | -| L6/M7 | Runtime and standard library | 0/413 non-FFI passing files compile, validate, and run; 53 stop on missing modules, 187 at P10, 86 at P3, 46 at P5 typecheck, 17 at P5 kind checking, 14 at P8, 6 at P6, and 4 at P0; no P2 surface-lowering blockers and no harness-loading blockers. | Every in-scope passing file for the feature compiles, validates, and runs with the expected result. | +| L6/M7 | Runtime and standard library | 124/413 non-FFI passing files compile, validate, and run, all with exit code 0. Of the other 289, 53 stop on missing modules, 63 at P10 because no `main` was selected, 86 at P3, 46 at P5 typecheck, 17 at P5 kind checking, 14 at P8, 6 at P6, and 4 at P0; no P2 surface-lowering blockers and no harness-loading blockers. One `PSRS_REQUIRE_WASMTIME=1 PSRS_ORACLE=annotations` run of all boards on 2026-10-04 (Wasmtime 49.0.2, `purs` 0.15.16). L1–L5 in this table were unchanged in that run. | Every in-scope passing file for the feature compiles, validates, and runs with the expected result. | | M8-W | Warnings | 67 non-FFI warning files are in scope; no warning-code scoreboard exists | Warning-code agreement reaches 100% for the tracked warning corpus. | | M8-O | Optimization | 10 optimize files are in scope; they are not vendored and their goldens are JavaScript output | Expected optimize/CoreFn output agrees for all tracked optimize files. | -The L2 and L6/M7 rows that name 253/413, 57 missing modules, 99 other P3 blockers, or 177 at P10 are the `Show` measurement on `6f66524`. `Data.Foldable`'s compile-path measurement of the same counters is the second M7 table and was taken independently on `6f66524`; the figures are not additive. Foldable did not rewrite these gate rows. The L5 53/84 figure is the `Show` remeasurement; Foldable left the earlier 51/92. `Data.Tuple`'s L2 figures (245/413, 56 missing modules, 108 at P3) were measured independently on `6f66524` and are not additive with either of those. Tuple did not re-run L6. +The gate rows above are the 2026-10-04 measurement. Earlier M7 tables in the progress section record the `logShow`, `Show`, and Foldable runs; those figures are historical and are not added to this table. L5 is 53/80. An older headline of 53/84 does not match the per-code totals. ### Feature-to-gate crosswalk @@ -1073,7 +1092,7 @@ resolved, type checked, and represented in Typed Core as required. | FE-17 | Visible type application, typed binders, type wildcards, holes, and advanced annotations | Typed binders preserve and check scoped annotations, and each source type wildcard receives fresh kind/type variables through the shared type spine. Type-level `String` and `Int` literals are ordinary spine nodes: a signature may contain them, they unify by value, and they survive into THIR where the verifier compares them. A wildcard in a value signature is solved by unification and is accepted in every shape `purs` accepts; a wildcard in an instance head is rejected as `InvalidInstanceHead`, while one in an instance context stays legal. The `1664.purs` wildcard binder lowers through P2. Visible term type application, wildcard warning/error behavior, higher-kinded application, and non-generalized hole diagnostics remain incomplete. The `Type`, `Constraint`, and `Symbol` heads are accepted as ordinary type constructors with their declared primitive kinds. Official's CST has no kind-application node; its kind checker synthesizes `KindApp` while instantiating a polymorphic kind, and this compiler performs that instantiation in the kind solver, so its source type spine needs no `KindApplication` node. The source forms that do name a kind or type explicitly are separate nodes. #87 lands both of the forms that blocked P2: a negative type-level integer prefix is the negative literal on the shared spine, and a visible type application `e @T` is elaborated by the checker, which substitutes the written argument for the operand's outermost quantifier after checking it against that quantifier's kind, and is erased at runtime. No P2 surface-lowering case remains. Three limits are recorded rather than approximated. A chained application `f @A @B` is reported, because the quantifiers an application leaves behind are scheme variables here and choosing between them needs the scheme to record which variables a visible application has consumed. A visible application on a class-method head is unresolved, which is `failing/ClassHeadNoVTA3.purs`. And this compiler's CST does not carry the binder visibility that official's `CST/Convert.hs` derives from `forall @a.`, so a plain `forall a.` binder is selectable where `purs` rejects it — the permissive direction, and the remaining half of `failing/VisibleTypeApplications1.purs`. `CannotApplyExpressionOfTypeOnType` and `CannotSkipTypeApplication` are the mapped codes. The primitive row relations themselves all have rules, and the row-side gap that remains is the rigid-tail unification defect under FE-13. | Partial | Model `forall` binder visibility so a visible application matches official, then resolve chained applications and class-method heads. | | FE-18 | Higher-rank types, subsumption, impredicativity, and higher-rank `forall` | Bidirectional checking preserves nested quantifiers, checks directional function/record subsumption, and rejects escaping skolems and specialized universal arguments. Source and GC execution cases cover rank-2 through rank-4, fields, returned and captured values, recursive annotations, higher-kinded parameters, and nested constraints. See the [rank-N acceptance record](../implementation/frontend/rank-n.md) for verification evidence and the official differential battery. | Partial | Reconcile the complete official higher-rank/skolem corpus, including its library dependencies and separate higher-rank kind requirements; track visible type application and diagnostic agreement. | | FE-19 | Foreign declarations and target-aware external names | Source-declared WIT bindings are resolved for the supported backend path. `foreign import data` is a nominal opaque type with no constructors; a nullary one maps to a WIT resource. THIR and Core keep it as `Constructor(User(id))` plus `opaque_ids`, distinct from `Int` (`lowers_an_opaque_foreign_type_to_core_without_collapsing_it_to_int`). JavaScript FFI is not a frontend target. CC/MIR handle layout is not done. | Partial | Finish target-aware foreign value rules beyond the supported WIT subset. Resource lifetime and handle layout stay in the backend. | -| FE-20 | Warnings, holes, source spans, and official diagnostic codes | Source spans exist and resolution, kind, type, and class `errorCode`s are measured: L1 904/908, L2 72/72, L3 35/48, L4 35/50, L5 53/84. The L4/L5 denominators count cases reaching their owner stage; 16 cases in the combined run are blocked earlier. Pattern-binder diagnostics match the annotated duplicate-name cases; warning coverage and complete diagnostic agreement remain open. Non-generalized hole diagnostics remain tracked under FE-17. | Partial | Add the missing class checks (#97) and track warning-code agreement separately from acceptance errors. | +| FE-20 | Warnings, holes, source spans, and official diagnostic codes | Source spans exist and resolution, kind, type, and class `errorCode`s are measured: L1 904/908, L2 72/72, L3 35/48, L4 35/50, L5 53/80. Pattern-binder diagnostics match the annotated duplicate-name cases; warning coverage and complete diagnostic agreement remain open. Non-generalized hole diagnostics remain tracked under FE-17. | Partial | Add the missing class checks (#97) and track warning-code agreement separately from acceptance errors. | | FE-21 | Typed Core normalization and CoreFn/optimization compatibility | Typed Core lowering and verification work for the supported subset; official optimize output is not yet a target. | Partial | Add Core optimization passes and an explicit optimize compatibility track. | The frontend landing order is: @@ -1113,13 +1132,13 @@ Wasm is the target encoding, and WIT/WASI are the platform integration layers. | BE-18 | Generic source-declared WIT imports | Compatible `Int`/`Boolean`/`Number` scalars, handles, and `list`/`string` imports lower through the canonical ABI with signature validation. A WIT `string` is a source `String` and a WIT `list` is `Array Int`, so the two no longer share a source type ([DEC-16](../decision/DEC-16-scalar-strings-and-utf8-storage.md)). Closed, directly flattened WIT records can contain nested `list` fields. | Partial | Add other aggregate WIT values, richer results, and user-library loading. | | BE-19 | WIT aggregate values and resources | Resource handles lower under [DEC-14](../decision/DEC-14-resource-handle-ownership.md): the compiler drops no handle on its own and exposes `resource.drop` to source, so the standard library owns the lifetime discipline; byte lists and closed WIT records with nested byte-list fields are classified and lowered in WIT field order. Indirect parameter tuples are allocated through `cabi_realloc`. Non-byte `list` of scalars, `bool`, `char`, strings, nullary enums, flags, resource handles, and directly flattened records of scalar or string fields is copied between a source GC array and the canonical buffer, with a driver execution test for `list` and synthesized Wasm fixtures for `list`, `list`, and `list` ([ABI-08](../implementation/backend/linear-memory-and-canonical-abi.md) In progress). `option`, `result`, and non-unit `variant` are classified and validated against `Data.Maybe.Maybe`, `Data.Either.Either`, and a source data type, CC derives their variant representation and a concrete payload tree, and MIR branches on each tag and rebuilds the source value recursively for a scalar payload of any width (`s8`..`u64`, `f32`/`f64`), a byte or non-byte list, `flags`, a closed record, and a nested `option`/`result`/`variant`, recursing through record fields and a `list`/`list` element, with synthesized Wasm fixtures ([DEC-13](../decision/DEC-13-wit-to-source-type-mapping.md)); a large aggregate return area is allocated through `cabi_realloc`, a handle in a result is an ordinary value the standard library drops explicitly, and an indirect parameter record carries a mapped aggregate. The aggregate ABI is generated from one normalized canonical type ([compositional canonical ABI lowering](backend/wasm/canonical-abi-compositional.md)); the descriptor types and per-shape plans are removed. `list>`/`list`/`list` elements, nested `list>`, multi-word flags as list elements and in aggregates, non-byte `list`, and `list>` results are classified and lowered, and a unit-success `result<_, E>` maps to `Either E Unit` (the error on `Left`) and sizes its return area from the error payload. | Partial | Add general aggregate layouts beyond the list-and-handle subset. | | BE-20 | Component Model packaging and capability-based imports | `wit-component` lifts the core module to a WASI 0.2 component and prunes unused imports. | Partial | Add component import/export regression cases beyond the CLI path and pass the L6/M7 gate. | -| BE-21 | WASI CLI entry, exit, stdout, and stderr | `wasi:cli/run`, exit codes, console output, and error output work in the component path. Source `Effect` values remain inert until the selected entry calls `runEffect`; focused execution tests cover source order and repeated runs ([WASI-02/03](../implementation/backend/wasi-platform.md) Verified). | Partial | Expand source-level runtime cases and pass the L6/M7 gate. | +| BE-21 | WASI CLI entry, exit, stdout, and stderr | `wasi:cli/run`, exit codes, console output, and error output work in the component path. A selected `Int` entry returns its value as the exit code. A selected `Effect Unit` entry runs that action once, returns 0 after normal completion, and propagates a trap. Creating an action does not run its deferred operation. Focused Wasmtime tests assert output, status, and trap markers ([WASI-02/03](../implementation/backend/wasi-platform.md) Verified). The official board is 124/413, so this row stays Partial. | Partial | Pass the L6/M7 gate. The 63 files with no selected `main` stay explicit blockers. | | BE-22 | WASI clocks and randomness | Monotonic time and random bytes are wired through WASI and tested. | Partial | Expose the remaining clock/random library surface and pass the L6/M7 gate. | | BE-23 | WASI arguments, environment, and filesystem | WIT descriptions are vendored, but the source library and aggregate lowering are not complete ([WASI-07](../implementation/backend/wasi-platform.md) In progress). | Planned | Add module loading and aggregate/list support, then expose these services. | | BE-24 | WASI sockets and HTTP | Not part of the current synchronous portable-program target. | Excluded | Revisit as a separate platform scope after the core target is stable. | | BE-25 | WASI 0.3 async streams and futures | The current compiler targets synchronous WASI 0.2. | Planned | Revisit only with an explicit platform decision and async language/library plan. | | BE-26 | Standard library and user module loading | User modules are discovered from the entry files' directories and linked transitively ([WASI-09](../implementation/backend/wasi-platform.md) Verified); the PureScript-facing standard library is loaded from `stdlib/lib` in trusted-prefix order ([WASI-10](../implementation/backend/wasi-platform.md) Verified). | Partial | Pass the L6/M7 module-loading scoreboard. | -| BE-27 | Wasm/WASI execution and official passing-suite runtime coverage | Vertical execution tests pass for the bootstrap slice, and the `l6_runtime_scoreboard` harness compiles, validates, and runs the 413 non-FFI `passing` files; it measures 0/413 today. The first blockers are 53 missing library modules, 187 P10 entry-point-selection failures, 86 P3 resolution failures, 46 P5 type errors, 17 P5 kind errors, 14 P8 representation errors, 6 P6 Core-lowering failures, and 4 P0 lexing failures; there are 0 harness-loading blockers. The library surface this row was waiting on is landed: `Effect`/`Effect.Console` — including `logShow` over the library `show` — and `Test.Assert`, whose failure path is a real guest trap (`Prelude.trap`). The remaining library work is the `Prelude` class and value surface (#94), the unowned `Data.*` modules (#124), and `Test.Assert.assertEqual` (#95), which #137 blocks because a constraint on a variable inside a record type is elaborated against the record. P10 is the largest single blocker at 187 and is not a library gap, so this row cannot move above 0/413 until Phase 5 selects an entry for `main :: Effect Unit`. The 26 FFI files are excluded. | Partial | Land the `Prelude` class surface, then track per-feature runtime cases against the board. | +| BE-27 | Wasm/WASI execution and official passing-suite runtime coverage | Vertical execution tests pass for the bootstrap slice, and the `l6_runtime_scoreboard` harness compiles, validates, and runs the 413 non-FFI `passing` files; it measures **124/413** on 2026-10-04 (Wasmtime 49.0.2, `purs` 0.15.16). All 124 exit 0 and are the files whose previous first blocker was a non-`Int` entry. The first blockers of the other 289 are 53 missing library modules, 63 P10 files with no selected `main`, 86 P3 resolution failures, 46 P5 type errors, 17 P5 kind errors, 14 P8 representation errors, 6 P6 Core-lowering failures, and 4 P0 lexing failures; there are 0 harness-loading blockers and 0 P2 blockers. The library surface this row was waiting on is landed: `Effect`/`Effect.Console` — including `logShow` over the library `show` — and `Test.Assert`, whose failure path is a real guest trap (`Prelude.trap`). The remaining library work is the `Prelude` class and value surface (#94), the unowned `Data.*` modules (#124), and `Test.Assert.assertEqual` (#95), which #137 blocks because a constraint on a variable inside a record type is elaborated against the record. The remaining P10 files have no selected `main` and stay explicit blockers; this row does not emit an empty main. The 26 FFI files are excluded. The row stays Partial because L6 is not complete. | Partial | Land the `Prelude` class surface, then track per-feature runtime cases against the board. | | BE-28 | JavaScript/Node.js FFI compatibility | Not emitted or executed by this backend. | Excluded | No work planned under this decision. | ### Topic implementation acceptance @@ -1137,7 +1156,7 @@ acceptance result. | Polymorphism and erasure | BE-02, BE-08; FE-09 input | Re-baselined by DEC-10: PE-01..PE-11 are Verified, including GC-string erasure and capture. | [PE-01..PE-11](../implementation/backend/polymorphism-and-erasure.md) | | Scalars and primitives | BE-04; FE-08 input | Re-baselined by DEC-10: SP-01..SP-12 are Verified, including the GC-string representation. | [SP-01..SP-12](../implementation/backend/scalars-and-primitives.md) | | Pattern matching | BE-05, BE-06; supporting BE-08, BE-09 | PM-01..PM-15 have implementation, verifier, and required execution evidence. PM-14 includes source-spanned Boolean redundancy and guarded fallthrough; broader feature rows retain their separate gates. | [PM-01..PM-15](../implementation/backend/pattern-matching.md) | -| Effects | BE-21; supporting BE-02, BE-26 | Representation lowering is in place. `Effect` stays an opaque user application through Typed Core, and `lower_effects` emits a one-parameter closure before closure conversion. EF-01..EF-12 are verified on that encoding; EF-12 covers `trap`, the `Effect Unit` whose application ends the guest, which is how the standard library reports an assertion that did not hold. The negative fixtures call `EffectLowering::verify` after replacing a recorded node with an arity-two `Effect (a -> b)` closure or a closure whose result is wrong; they fail in Core. The backend maps a `VerifyError` that `lower_effects` itself returns. A type table changed after the pass returns is not checked again. BE-21 stays the broader landing gate. `callable_types` remains and is always empty. | [EF-01..EF-11](../implementation/backend/effects.md) | +| Effects | BE-21; supporting BE-02, BE-26 | Trusted Effect identities and checked WIT schemes are passed explicitly. Source `Effect a` stays abstract through Typed Core; P8 lowers it to a generic one-parameter closure. EF-01..EF-13 are Verified, including the `Effect Unit` command adapter and the lexical `runEffect` rule. A type table changed after `lower_effects` returns is not checked again. The official runtime board is 124/413. The 63 files with no selected `main` remain blocked, and BE-21 stays Partial. | [EF-01..EF-13](../implementation/backend/effects.md) | | Type classes and dictionaries | BE-02, BE-09; FE-14/15 input | Backend acceptance complete from verified Typed Core fixtures: DICT-01..DICT-11 have implementation, verifier, and required execution evidence. Source constrained calls, contextual/imported generic instances, superclasses, fundeps, and ordered instance chains execute; FE-14/15 remain partial for remaining source class/fundep coverage, the constrained instance-member specialization limit, and official-suite acceptance. Class-method local constraints are covered under FE-18; deriving is tracked under FE-16. | [DICT-01..DICT-11](../implementation/backend/type-classes-and-dictionaries.md) | | Generic aggregate erasure | BE-08, BE-09, BE-10; supporting BE-02, BE-03, BE-13, BE-15 | Topic acceptance complete: all GA-01..GA-20 checks have implementation, verifier and required execution evidence. Broader feature rows retain their separate gates. | [Requirements, repair evidence, and validation](../implementation/backend/generic-aggregate-erasure.md) | | Optimization | BE-12 | Topic acceptance complete: OPT-01..OPT-14 have implementation, verifier, and required execution evidence. The official M8-O gate stays on the broader BE-12 row. | [OPT-01..OPT-14](../implementation/backend/optimization.md) | diff --git a/docs/design/backend/00-ir-boundaries.md b/docs/design/backend/00-ir-boundaries.md index 0adeb99a..4f0791b2 100644 --- a/docs/design/backend/00-ir-boundaries.md +++ b/docs/design/backend/00-ir-boundaries.md @@ -95,9 +95,10 @@ established theory decides it, and the topic documents own the details: [Control flow](fp/control-flow-and-tail-calls.md) represents self tail recursion as a loop and other tail calls as `return_call*`. - **Effects.** Wadler's monadic translation; Levy's call-by-push-value. Source - and Typed Core keep `Effect a` abstract. One representation lowering then - produces an ordinary closure; later stages do not recover an effect arity - from the library type ([effects](fp/effects.md)). + and Typed Core keep `Effect a` abstract. Trusted-library binding supplies + stable constructor and operation identities; lowering plans effectful imports + before erasure and produces generic closures. Later stages do not infer + Effect semantics from closure shape ([effects](fp/effects.md)). Deliberately not used: lazy evaluation and strictness analysis (the source is strict), typed low-level IRs such as FLINT/TAL (this design verifies each @@ -289,11 +290,16 @@ mechanical encoding of already-verified signatures. ### Boundary validation -External binding validation runs in both directions. P8 checks that the side -table is exactly the source WIT externals (`validate_core`); P9 checks that -every binding has one CC external with a matching abstract signature -(`validate_cc`). This prevents a caller from making a target binding disappear -or disagree with the representation CC used while type-checking calls. +External binding validation runs in both directions. P8 builds the side table +from Core's checked `ExternalType` schemes and checks that every source WIT +external has exactly one binding (`validate_core`). P9 checks that every binding +has one CC external with a matching abstract signature (`validate_cc`). The +checked schemes originate in THIR, where aliases are expanded and `ForAll` +quantifiers are preserved, and their `TypeId`s are remapped through Core +linking and optimization. WIT conformance and Effect classification consume +these checked types; the backend does not reconstruct them from raw HIR +annotations. This prevents a target binding from disappearing or disagreeing +with the representation CC used while type-checking calls. ## Code map @@ -311,7 +317,7 @@ crates/psrs-backend/src/ lib.rs crate surface: `compile` / `compile_with_target`, `ExternalBindings` capability.rs `TargetCapabilities` and validator feature mapping types.rs shared Wasm value/type model -abi.rs, abi/ WIT registry, canonical ABI classification, source signatures +abi/ WIT registry, canonical ABI classification, checked source signatures component.rs component packaging cc/ CC IR (functional) mod.rs `Module`, `Function`, `Assignment`, `AssignmentKind`, lowering entry @@ -411,8 +417,10 @@ B0: Return v2 ``` -with `main : () -> i32`. The verifier checks SSA, dominance, and the primitive's -operand and result types. +with `main : () -> i32` for the integer example. A source `Effect Unit` entry is +normalized earlier to an ordinary zero-argument integer command function; the +wrapper runs the action once, then returns zero. The verifier checks SSA, +dominance, and the primitive's operand and result types. **P10 structured Wasm.** The structurer emits a function type `() -> i32`, then `i32.const 1`, `i32.const 2`, `i32.add`, and a return of the result. It assigns @@ -431,13 +439,21 @@ and P10/P11 would name it from the ABI registry; CC would be unchanged. ## Boundaries and interfaces -- **Frontend to P7.** The front end produces linked, pruned Typed Core with an - `entry` `SymbolId`. The backend may not infer semantic identity from source - text; no stage above MIR may depend on memory offsets, Wasm indices, or - target calling conventions ([D-01](../D-01-frontend-and-ir-boundaries.md), [Wasm - encoding](wasm/encoding-and-structuring.md)). -- **P7 to P8.** A verified Core module plus the external binding side table. - See [functional core](../frontend/semantics/functional-core.md) and [CC IR](fp/cc-ir.md). +- **Frontend and driver to P7.** The front end produces linked, pruned Typed + Core with checked WIT `ExternalType` schemes plus explicit trusted-library + binding metadata for `Effect` and an + `EffectCommandEntry` holding the selected source `SymbolId`. Select + `Main.main` when present; otherwise require a unique top-level `main`. The + same source identity feeds lexical runner checks and any generated wrapper. + The backend may not infer semantic identity from source text; no stage above + MIR may depend on memory offsets, Wasm indices, or target calling conventions + ([D-01](../D-01-frontend-and-ir-boundaries.md), + [Wasm encoding](wasm/encoding-and-structuring.md)). +- **P7 to P8.** Verified Core plus explicit trusted-effect and selected-entry + metadata. P8 builds WIT bindings from Core's checked `ExternalType` + schemes before erasure. See + [functional core](../frontend/semantics/functional-core.md) and + [CC IR](fp/cc-ir.md). - **P8 to P9.** A `BackendInput { cc, externals }` plus an explicit `TargetCapabilities` profile. See [CC IR](fp/cc-ir.md) and [capability profile](wasm/capability-profile.md). diff --git a/docs/design/backend/fp/cc-ir.md b/docs/design/backend/fp/cc-ir.md index 9727a776..7fa9c3ce 100644 --- a/docs/design/backend/fp/cc-ir.md +++ b/docs/design/backend/fp/cc-ir.md @@ -236,10 +236,13 @@ ExternalBinding = { symbol: SymbolId, interface: String, function: String, ``` The Rust names are `BackendInput`, `ExternalBindings`, and `ExternalBinding` -(`crates/psrs-backend/src/bindings.rs`); `ExternalBindings` is the concrete side +(`crates/psrs-backend/src/bindings/mod.rs`); `ExternalBindings` is the concrete side table. Its `imports` map a symbol to its source declaration and platform binding. For the WASI target the binding contains the WIT interface and function names and -the declaration's resolved Core type identity required by the +the declaration's checked Core type identity from `Module.external_types`. That +scheme has type synonyms expanded and retains `ForAll` quantifiers. The raw HIR +annotation is source metadata, not an input from which the backend rebuilds the +type. The binding's checked type identity is required by the [canonical ABI](../wasm/canonical-abi-and-wit.md). P9 resolves these bindings through the ABI registry, emits canonical calls and adapters for referenced symbols, and keeps unused runtime imports out of MIR. Consequently, WIT names do diff --git a/docs/design/backend/fp/effects.md b/docs/design/backend/fp/effects.md index 6f59b795..6687b8d6 100644 --- a/docs/design/backend/fp/effects.md +++ b/docs/design/backend/fp/effects.md @@ -6,12 +6,12 @@ [type classes and dictionaries](type-classes-and-dictionaries.md); monads, closures, and the distinction between a value and a computation. Read [IR boundaries](../00-ir-boundaries.md) first. -**Summary:** `Effect a` stays an abstract library type through type checking and -Typed Core. One representation lowering then replaces each effect value with a -closure that takes the runtime token and returns the lowered result. That -closure is not a source arrow, so a function or another effect inside the -result stays a separate call. `pure`, `bind`, and `runEffect` are ordinary -source functions; only this lowering threads the token. +**Summary:** `Effect a` stays abstract through type checking and Typed Core, with +its trusted constructor and operation identities resolved once and carried to +the representation boundary. Lowering uses those identities to create generic +closures and to plan suspended foreign imports before erasing the abstract type. +The command entry accepts `Int` or `Effect Unit`; an internal wrapper runs an +effectful entry once and returns zero after normal completion. ## Scope @@ -66,19 +66,22 @@ runEffect :: forall a. Effect a -> a trap :: Effect Unit ``` -`runEffect` is provided only to the selected command entry as specified by -[F-02](../../../feature/F-02-portable-programs.md). It has an ordinary function -type; entry authorization is a driver rule, not an inference rule. +`runEffect` is a trusted library operation with an ordinary source function +type. A direct reference is permitted only in the selected command entry +declaration. This is a lexical reference check, not a capability or +non-escape guarantee: the entry may pass the function value to a helper, which +may then call it. For `main :: Effect Unit`, the compiler-generated command +wrapper is the primary route for running the selected action. `trap` is the effect whose result never exists: an uncaught failure on this target is a guest trap, and this is the one operation that says so. It takes no argument because the failure has already been reported through an ordinary service such as `Effect.Console.error` before it is used; a library that has a message to carry writes it first and then escapes. It is -`Effect Unit` rather than `forall a. Effect a`: the polymorphic form would need -the backend to produce a value of a type that is only known at the use site, -and no library caller needs it — the standard library's assertion surface is -its only consumer. +`Effect Unit` because that is the assertion and platform API the current +library needs. This API choice is not forced by the lowering: a non-returning +trap produces no result value, so the backend does not need to invent a value +of the use-site type. The equations below are the representation translation, not source equalities. `Token` does not occur in a source type, and `Effect a` does not unify with @@ -90,16 +93,24 @@ pure v = RepClosure(token) { v } bind m k = RepClosure(token) { call (call k (call m token)) token } runEffect m = call m runtimeToken trap = RepClosure(token) { unreachable } + +commandEntry(main : Effect Unit) = + let action = call main [] + runEffect action + 0 ``` -- **Construction is inert.** Building an `Effect` value allocates a closure and - performs no operation; merely storing or passing it does not run it. -- **Running is explicit.** The elaborated `runEffect` supplies the token. Only - the selected command entry can reference `runEffect`; an effect invoked twice - there runs twice. +- **Construction is inert.** Building an `Effect` value does not perform the + operation deferred in its closure; storing or passing the value does not run + it. Source arguments are evaluated strictly as usual and may themselves have + observable behavior. +- **Running is explicit.** The selected entry may call `runEffect` explicitly + where its source type permits. For an `Effect Unit` entry, the generated + command wrapper runs its returned action exactly once and yields zero after + normal completion. A trap propagates. - **Sequencing is left to right.** Elaborated `bind` runs the first computation, - then feeds its result to the continuation with the same token, so operations - keep source order. + then feeds its result to the continuation with the same token. Ordering comes + from the calls and strict evaluation order, not from the token's bits. - **The token is not a source value.** No source program names it, applies an effect to it, or passes an ordinary function where an effect is required. - **Escaping is not returning.** Applying `trap` to the token reaches an @@ -109,11 +120,14 @@ trap = RepClosure(token) { unreachable } ### Two callable forms -A source function and an effect closure are different callable values. +A source function and a representation closure are different callable +values. `RepClosure` is notation for the existing generic `Closure` +representation with fixed parameters. It is not an Effect-specific closure +kind or runtime object. ```text SourceArrow a b = the curried Function spine a -> b -RepClosure params r = a closure created with a fixed parameter list and a +RepClosure params r = a generic closure with a fixed parameter list and a result value ``` @@ -139,26 +153,34 @@ parameter, not a second parameter of `log`. ### Elaboration and invariants -The frontend resolves `Effect` as an imported abstract type constructor and -checks it by ordinary kind, application, and subsumption rules. It adds no -effect flag, private constructor, or representation mode. +The frontend resolves `Effect` through the trusted library binding and checks +it by ordinary kind, application, and subsumption rules. It adds no effect +flag, private constructor, or representation mode. - `Effect a` is `Application(Constructor(User(effect_id)), a)` on the uniform application spine ([DEC-15](../../../decision/DEC-15-unified-type-representation.md)). THIR and Typed Core keep that type. Unification, subsumption, and arity flattening do not treat it as a function. -- No stage stores an "effect" flag on an expression. Effects compose through - `pure`, `bind`, `runEffect`, and `trap`. -- Exactly one pass recognizes `effect_id`: the representation lowering below. - After it, CC and MIR see ordinary closures and calls. They do not consult a - callable-constructor table and they do not match `Effect`. -- The token's physical type is chosen by that pass. The synchronous runtime - uses an `i32` placeholder. Changing it changes the pass and the runtime, not - the source API or the Core type of `pure` and `bind`. -- Reusing a value never reorders or merges observably distinct `runEffect` - calls; each elaborated call receives a token. -- The driver identifies the selected command entry and checks the scope of - `runEffect` references before ordinary type inference. +- Trusted-library binding resolves the semantic identity of `Effect` and the + `pure`, `bind`, `runEffect`, and `trap` operations once. The linked Core input + carries those resolved identities to the lowering that consumes them. No + later stage reconstructs trust from a qualified source name or opacity flag. +- Before replacing abstract applications, the lowering classifies each + effectful foreign import from that identity and its checked, synonym-expanded + external scheme in Core. `Effect` remains abstract at this point. The pass + records an immutable suspension plan for that exact import. + After erasure, only imports in those plans receive a delayed wrapper; a + generic one-parameter closure shape is not evidence of an effect. +- No stage stores an "effect" flag on an expression or adds a dedicated Effect + IR node, closure kind, or runtime object. After representation lowering, CC + and MIR see generic closures and calls. +- The synchronous token may be the integer zero. It carries no scheduling or + ordering guarantee. Call order and multiplicity are preserved by the + evaluation and optimizer contracts. +- Entry selection produces one resolved command-entry `SymbolId`: use + `Main.main` when present, otherwise require one unique top-level `main`. + The lexical `runEffect` reference check and generated entry wrapper use that + same identity. - Calls, including calls reached through closures, may perform effects. Core, CC, and MIR optimizations preserve their order and multiplicity unless a separate purity proof establishes that a particular call is inert. @@ -178,10 +200,21 @@ abstract, and produces CC closures with explicit parameter lists. - `trap`'s closure body is an unreachable path, so applying it ends the guest. It is a Core expression type, not a new CC or MIR instruction: the existing trap assignment already ends a path for an unmatched pattern. -- A foreign import whose source type is `Effect τ` becomes a closure that - performs the host call when the token is supplied. In a strict language the - call must not happen when the effect value is built. `pure foreignCall` would - evaluate the call too early, so the suspension is this closure, not `pure`. +- Before effect applications are rewritten, each imported operation is + classified from the trusted `Effect` identity in its checked, synonym-expanded + external scheme. `Effect` remains abstract until this lowering. + The plan records the checked source scheme, source parameters, and effect + payload. When applying it, lowering derives the host function type from those + parameters and the payload. The generated wrapper keeps the scheme's binders + on `Declaration.quantified` and the monotype, after `Effect` has been rewritten + to a closure, on `Declaration.ty`. Core enters those binders before checking + `ty`, so the declaration type must not repeat the leading `ForAll`. The + quantified host scheme stays on the checked external type. The wrapper + performs the host call when the returned effect closure is run; an unrelated + import returning an ordinary closure is left unchanged. + In a strict language, the host operation itself must not happen when the + effect value is built. `pure foreignCall` would evaluate that call too early, + so the import wrapper provides the suspension. - A source function such as `log :: String -> Effect Unit` keeps one source parameter. Its body is ordinary `bind` over effect-typed operations. The returned value is the `RepClosure` produced for that `Effect`. @@ -254,8 +287,8 @@ lower_effect(Effect τ) = RepClosure([Token], lower(τ)) lower_pure = \value -> RepClosure(token) { value } lower_bind = \first -> \next -> RepClosure(token) { - result = call (call first token) - rest = call (call next result) + result = call first token + rest = call next result call rest token } lower_run = \action -> call action runtimeToken @@ -266,6 +299,46 @@ lower_trap = RepClosure(token) { unreachable } not continue into a function or effect stored in the result. Sequencing is the order of these calls: `call first token` completes before `call next result`. +### Planning suspended imports + +Before lowering replaces `Effect` in an import signature, the backend reads the +external's checked scheme from `Module.external_types` and records an immutable +plan for that resolved external. The scheme has aliases already expanded and +retains its `ForAll` quantifiers. A plan retains the original checked source +`TypeId`, its quantified variables and stripped body, the source parameters, +the exact Effect application and payload/result types, and the source symbol +and span. When applying the plan, lowering derives the host function type from +the recorded source parameters and payload, retargets the external binding to +that host symbol and type, and builds a wrapper under the original source +symbol used by Core calls. The applied record retains the derived host symbol +and type; verification checks the host binding and generated wrapper against +that type and the original plan. The host operation executes only when the +closure body is called; an ordinary one-parameter closure in another import +has no such plan and is not suspended. +Structural verification compares each plan with its generated wrapper and the +complete transformed Core. Focused execution tests separately establish +inertness and ordering. + +### Normalizing the command entry + +Entry selection is shared with the lexical `runEffect` check and produces one +resolved `SymbolId`. The selected source declaration is `Main.main` when it is +present; otherwise the program must have exactly one top-level declaration +named `main`. The selected declaration must take no arguments and return either +`Int` or the trusted `Effect Unit` type. Before erasure, the backend checks +that an Effect command-entry record names exactly the selected Core entry; +missing or stale metadata is an invalid compiler contract. + +An `Int` entry retains the existing zero-argument integer command +convention, and its result remains the process exit code. For `Effect Unit`, +the compiler generates an ordinary Core adapter that evaluates the selected +declaration to an action, runs it exactly once through the trusted effect +runner, then returns zero. A guest trap escapes before normal completion and +is not translated into zero. The adapter is placed in the selected source +module, retains source origin for diagnostics, and becomes the Core module +entry before CC. The selected source `SymbolId` remains available for lexical +runner checks. The adapter lowers to generic closure and call forms. + ### Partial application of a source arrow ```text @@ -309,96 +382,138 @@ rewrites to `bind` before Core, so the backend sees only `pure`, `bind`, ## Code map -The effect vocabulary is frontend source and the lowering path is the ordinary -closure and partial-application path. The implementation must conform to this -organization. +Trusted source bindings and ordinary closure lowering jointly own the +representation. The implementation must conform to this organization. ```text -crates/psrs-typecheck/src/ ordinary checking of User(effect_id) -crates/psrs-core/src/effect/ lower_effects(module) -> EffectLowering -crates/psrs-driver/src/prelude.rs entry-only runEffect -crates/psrs-backend/src/cc/ closures and calls, with no Effect match -crates/psrs-backend/src/mir/ +crates/psrs-driver/src/program/effects.rs + resolve TrustedEffect; select EffectCommandEntry { symbol }; + enforce the lexical runEffect reference rule +crates/psrs-thir/src/lib.rs and crates/psrs-core/src/lib.rs + carry WIT ExternalType { symbol, source_module, ty } checked schemes through P6/P7; + preserve those IDs while linking and optimizing Core +crates/psrs-backend/src/bindings/mod.rs + build ExternalBindings from checked Core external schemes +crates/psrs-core/src/effect/ + lower abstract Effect applications using trusted identities +crates/psrs-backend/src/effects.rs + classify abstract imports and retain their suspension plans; + build planned wrappers and the Effect Unit command adapter; + verify the complete transformed Core +crates/psrs-backend/src/cc/ and crates/psrs-backend/src/mir/ + lower generic closures, calls, and command ABI ``` - Responsibilities and required types: -- The effect library supplies `foreign import data Effect :: Type -> Type`, - `pure`, `bind`, and the trusted `runEffect` binding, all at the abstract - signatures in the model. The driver enforces entry-only `runEffect`. -- `psrs-hir` retains the resolved `Effect` type identity. No CST, AST, HIR, or - Core node carries an effect flag or a token type. +- Trusted library binding resolves a `TrustedEffect` record with the resolved + `Effect` constructor identity and the `pure`, `bind`, `runEffect`, and + `trap` operation identities. The driver passes this record alongside linked + Core. +- Each WIT external import has an `ExternalType { symbol, source_module, ty }` in THIR and Core. + `ty` indexes the checked module type table; type synonyms are expanded during + checking and `ForAll` quantifiers remain in the scheme. Linking and Core + optimization remap the type ID with that table. The raw HIR external + annotation remains source metadata, not the authority for WIT semantics. + The recorded `source_module` identifies the declaring module independently + of the foreign symbol namespace and remains authoritative for diagnostics. +- `ExternalBindings::from_core` consumes the checked Core external scheme table. + Effect classification, WIT conformance, and trusted WIT operation-signature + validation use these checked type IDs; backend stages do not re-elaborate HIR + annotations or reconstruct aliases. Compiler intrinsics keep their explicit + `Intrinsic` descriptor contracts and do not use `ExternalType`. + When trusted operation imports become synthesized declarations, their + external scheme entries are removed with those imports. - `psrs-typecheck` checks `Effect a` as an ordinary abstract application. It has no `Effect` constructor, no mode that opens an effect into an arrow, and no unification of `Effect a` with a function. -- `lower_effects(module)` is the only function that matches `effect_id`. It - replaces `Effect τ` with `RepClosure([Token], lower(τ))`, replaces `pure`, - `bind`, and `runEffect`, and suspends a foreign import of type `Effect τ` - inside that closure. It records every closure it wrote and checks that record - before returning. `EffectLowering::verify` rejects a recorded node whose - parameter list is not `[Token]` or whose result is not `lower(τ)`. It does - not add a Core or CC effect node. -- CC and MIR lower the resulting closures through `FunctionRef` and direct or - indirect calls. Curried-arrow flattening reads source `Function` spines only. - Partial application (`lower_partial_global_application`) applies to - under-applied source arrows, not to the token of an effect. +- Before rewriting abstract effect applications, the lowering pipeline records + an `EffectImportPlan` for each semantically effectful WIT import, using its + checked external scheme and trusted Effect identity. The plan retains the + original checked `TypeId`, quantified variables, decomposed source arguments + and payload/result types, and the source symbol/span. Applying the plan derives + the host type from the source parameters and payload; the applied record keeps + the derived host symbol/type for verification. Lowering replaces `Effect τ` + with generic + `Closure([Token], lower(τ))` types and synthesizes operation bodies and + wrappers only from the explicit identities and plans. +- The wrapper and rewritten Core are structurally verified before CC. This + checks binding and type-shape contracts; it does not add a Core or CC Effect + node or prove runtime behavior. +- CC and MIR lower the resulting generic closures through `FunctionRef` and + direct or indirect calls. Curried-arrow flattening reads source `Function` + spines only. Partial application + (`lower_partial_global_application`) applies to under-applied source arrows, + not to the token of an effect. - The representation may later grow into dictionary passing ([type classes and dictionaries](type-classes-and-dictionaries.md)). The token - stays inside `lower_effects`; its type is chosen there. + stays inside effect lowering; its type is chosen there. - WASI operations are owned by the [WASI platform library](../wasm/wasi-platform-library.md) and the - [canonical ABI and WIT](../wasm/canonical-abi-and-wit.md). An operation whose - source type is `Effect` is suspended by `lower_effects` and performs its host - call only when that closure runs. + [canonical ABI and WIT](../wasm/canonical-abi-and-wit.md). A host call is + suspended only when its checked scheme returns an application of the trusted + Effect constructor and import classification records a suspension plan; + generic closure shape does not classify an import. ## Invariants and verification -- Constructing an effect performs no call into a WASI import; this is tested by - observing no output when an effect is built and never run. -- Running effects preserves source order; the ordering derives from ANF - assignment order, so the CC verifier's ordering checks cover it. -- A stored effect runs once per explicit `runEffect`; two runs produce two - observable effects. -- Dictionaries or closures carrying effects have ordinary shapes; the CC and MIR - verifiers check them as products and closures, not as effects. -- Execution evidence requires `wasmtime`; the tests skip when the runtime is - absent and run in CI under `PSRS_REQUIRE_WASMTIME=1`, as required by - [DEC-05](../../../decision/DEC-05-wasmtime-feature-set.md). +The structural verifier checks that the trusted constructor and operation +identities match their binding metadata; each planned external still matches +its checked Core scheme, and each applied plan matches its derived host type and +generated wrapper; each rewritten effect application has one token parameter +and the lowered result; +and the transformed Core module, including wrappers, is valid. These checks +establish structure and identity only. + +Behavioral guarantees require source-level execution. Tests must show that +building the deferred action does not call its external, that strict argument +evaluation remains in source order, that `bind` runs each continuation action +once and left to right, and that the `Effect Unit` command wrapper returns zero +only after normal completion. A trap must escape the wrapper without a normal +exit result. CC/MIR shape verification does not establish these behaviors. + +Execution evidence requires `wasmtime`. A scoreboard's runtime-completion +classification is not a golden stdout comparison and cannot distinguish every +host CLI failure from a guest exit. Focused tests must assert expected output, +process status, or an explicit trap marker with `PSRS_REQUIRE_WASMTIME=1` +([DEC-05](../../../decision/DEC-05-wasmtime-feature-set.md)). ## Worked example ```purescript -main = - let first = runEffect (log "first") - in let second = runEffect (log "second") - in 0 +main :: Effect Unit +main = do + log "first" + log "second" ``` -`log :: String -> Effect Unit` has one source parameter. Lowering proceeds as: +`log :: String -> Effect Unit` has one source parameter. The selected +declaration returns an effect closure. The compiler-generated command wrapper +calls the selected declaration once, applies the returned closure once, and +returns zero after the action finishes: ```text -// runEffect (log "first") -action1 = DirectCall(log, ["first"]) - // result: RepClosure([Token], Unit) -result1 = call action1 runtimeToken +action = DirectCall(Main.main, []) + // result: Closure([Token], Unit) +ignored = call action runtimeToken +result = 0 ``` -`log`'s body is `bind` over effect-typed writes. Each `bind` has already become -a `RepClosure`; running `action1` is what performs the writes. Building -`action1` allocates that closure and prints nothing. - -The second `runEffect` lowers identically into the following assignment, so the -ANF order runs `"first\n"` before `"second\n"`. Constructing `action1` alone -would allocate a closure and print nothing, which is exactly the test -`constructing_an_effect_does_not_execute_it`. - +The writes occur inside the action closure, so the wrapper prints +`first\nsecond\n` once and exits with code zero. If the action traps, the +wrapper does not reach its normal zero result. A wrapper verifier checks the +generated call types and selected symbol; Wasmtime execution tests establish +that the writes happen once and that a trap escapes. ## Boundaries and interfaces -- **From the frontend.** `Effect` is an imported abstract type constructor. - `do`/`ado` desugars to library `bind`. No effect flag is added to CST, AST, - HIR, or Core nodes, and P5 does not open the representation. -- **Through `lower_effects`.** This is the conversion from the abstract Core - type to a CC closure. Downstream stages receive closures, not `Effect`. +- **From the frontend and driver.** The driver passes a `TrustedEffect` + binding and an `EffectCommandEntry` with the selected source `SymbolId` + alongside linked Core. `do`/`ado` desugars to library `bind`. No effect flag + is added to CST, AST, HIR, or Core nodes, and P5 does not open the + representation. +- **Through effect lowering.** This converts abstract Core types to generic + closures. It verifies an `Effect Unit` entry and inserts its ordinary adapter + before CC. Import plans survive long enough to generate and verify wrappers; + downstream stages receive closures, not `Effect`. - **To CC.** An effect is a closure whose parameter list is `[Token]`. Source partial application remains available for under-applied source arrows. - **To MIR/Wasm.** Ordinary closure creation and calls. The token's MIR type is @@ -425,52 +540,20 @@ would allocate a closure and print nothing, which is exactly the test [Core optimization](../opt/core.md); token elimination after representation lowering belongs to [MIR optimization](../opt/mir.md). Both must preserve the run-once-per-`runEffect` behavior. -- **Diagnostics.** A source program that refers to `runEffect` outside the - selected command entry receives a frontend diagnostic before Core lowering. +- **Diagnostics.** A direct source reference to `runEffect` outside the + selected command-entry declaration receives a source diagnostic. Passing the + runner from within that declaration to a helper is permitted; this rule does + not prevent escape or invocation through a passed value. ## Implementation notes -`lower_effects` in `crates/psrs-core/src/effect/` is the representation -conversion. Prelude declares `foreign import data Effect :: Type -> Type`. -`pure`, `bind`, and `runEffect` are abstract `psrs:effect` imports. The pass -returns `EffectLowering`, whose `synthesized` symbols are those three -declarations and whose `closures` are the `EffectClosure` entries it wrote. It -matches the opaque `Prelude.Effect` type id, replaces each application with -`Type::Closure` whose parameter list is Core `Int`, and suspends a foreign import -whose type ends in that application so the host call runs inside the closure. -`crates/psrs-backend/src/effects.rs` drops the abstract imports and performs -that suspension. The entry check lives in -`crates/psrs-driver/src/program/effects.rs` and looks up `runEffect` on -declarations and externals. `runEffect`'s synthesized body applies the integer -`0`. - -`callable_types` remains a field on the typed module and is always empty. -Closure conversion and MIR do not read it. Calling convention uses the closure's -parameter list: `log` has one parameter, `log "message"` is a saturated call, -and `Effect (Int -> Int)` is not a two-parameter function -(`an_effect_of_a_function_is_not_arity_two_and_log_is_saturated`). A partial -application of `Boolean -> String -> Effect Unit` captures the Boolean once and -does not run the write (`a_partial_source_application_captures_once_and_defers_the_effect`). - -Typed Core still shows `Effect Int` as a user-type application. A source -function is rejected by ordinary unification, and a user-declared `data Effect` -is not opaque, so the pass leaves it nominal. Order, inertness, and the -entry-only runner are recorded in -[the effects checklist](../../../implementation/backend/effects.md). -`EffectLowering::verify` rejects a recorded closure whose parameter list is not -`[Token]` or whose result is not the lowered effect result. The executed -fixtures rewrite the node after `lower_effects` returns and call `verify` again -(`a_lowered_effect_closure_flattened_to_arity_two_is_rejected`, -`a_lowered_effect_closure_with_the_wrong_result_is_rejected`). They fail with a -Core `VerifyError` and do not enter the backend. `lower_effects` also calls -`verify` before it returns, and -`crates/psrs-backend/src/effects.rs` maps that returned error to -`InvalidCompilerIr` under `P8 effect lowering`. The closures the pass writes -already match the record, so the fixtures do not take that mapping. A type -table changed after the pass returns is not checked again on the compile path. -`Type::Closure` remains a general representation, and only the recorded nodes -are constrained. The optimizer's effectful-call preservation rules remain in -the Core and MIR optimization documents. +Implementation and test status, including stage-specific evidence, are +maintained in the [effects acceptance record](../../../implementation/backend/effects.md). +That record retains historical results and marks the expanded identity, +import-plan, transformed-Core, and command-entry requirements pending until +their focused tests and required runtime execution are recorded. This design +specifies the intended contracts; closure-shaped IR alone does not establish +the behavioral guarantees above. ## References diff --git a/docs/design/backend/wasm/canonical-abi-and-wit.md b/docs/design/backend/wasm/canonical-abi-and-wit.md index 0b909c7c..6493c492 100644 --- a/docs/design/backend/wasm/canonical-abi-and-wit.md +++ b/docs/design/backend/wasm/canonical-abi-and-wit.md @@ -42,15 +42,26 @@ type-directedly, so the library is ordinary source code. ## Model -Two side tables carry the boundary. Neither is part of CC or MIR. A -target-aware linking stage (see [Design](#design)) resolves each import once and -produces one [`ResolvedExternal`](#resolved-externals) per declaration, pairing -the resolved source type with the WIT descriptor. +Two side tables carry the boundary. Neither is part of CC or MIR. The type +checker produces a checked `ExternalType` for each WIT external import; aliases +are expanded there, and `ForAll` quantifiers remain in the checked type graph. +P8 joins that scheme to the raw external's target binding and produces one +[`ResolvedExternal`](#resolved-externals) per WIT declaration, pairing the +checked source type with the WIT descriptor. The declaring `source_module` +is captured before linking and preserved in the external binding: foreign +symbols use the reserved intrinsic namespace, which is not their source owner. +Binding diagnostics use this explicit owner and the original source span. + +Class-constrained WIT value signatures are currently unsupported: the checker +reports `UnsupportedType` on the source signature rather than dropping its +constraint evidence or inventing a canonical ABI for dictionary parameters. +Quantified signatures without class constraints retain their `ForAll` structure. ```text +ExternalType = { symbol: SymbolId, source_module: ModuleId, ty: TypeId } ExternalBindings = { imports: [ResolvedExternal] } ResolvedExternal = { symbol: SymbolId, interface: String, function: String, - type_id: TypeId, import: WasiImport } + checked_type: TypeId, import: WasiImport } WasiRegistry = { resolve: wit_parser::Resolve, imports: [WasiImport], @@ -80,11 +91,12 @@ WasiResultKind = None | Scalar | Boolean | Enum { cases: [String] } WasiField = { name: String, kind: WasiParamKind } ``` -The linking stage resolves an `ExternalKind::Wit { interface, function }` against -the vendored WIT once and produces a `ResolvedExternal`. `type_id` is the -declaration's resolved source type, interned in the module type table, so CC can -derive its layout from the shared representation table instead of re-deriving it -from a source-type mirror. `import` is the WIT descriptor that carries the ABI +P8 joins each `ExternalKind::Wit { interface, function }` to its checked +`ExternalType` by `SymbolId`, resolves the vendored WIT once, and produces a +`ResolvedExternal`. `checked_type` is the synonym-expanded source scheme from +the Core type table, with its `ForAll` quantifiers preserved, so CC can derive +its layout from the shared representation table instead of re-elaborating the +raw HIR annotation. `import` is the WIT descriptor that carries the ABI facts the source type cannot: numeric width, `string` versus `list`, flattening, `retptr`, and `own`/`borrow` ownership. A declaration the source ABI cannot express yields no `ResolvedExternal` and is rejected. @@ -126,11 +138,12 @@ foreign import "wasi:clocks/monotonic-clock#now" now :: Int ``` The string is `#`. The declaration's source name is -unrelated to the WIT name, and its declared type is mapped to the canonical +unrelated to the WIT name, and its checked external type is mapped to the canonical signature through the standard type mapping. There is a single external kind, -`Wit`; the compiler has no per-function host registry. `ExternalBindings` is a -lossless projection of the source externals, checked against Core -(`validate_core`) and against CC's abstract signatures (`validate_cc`). +`Wit`; the compiler has no per-function host registry. `ExternalBindings` is +built from Core's checked `ExternalType` schemes and target-binding metadata, +then checked against Core (`validate_core`) and CC's abstract signatures +(`validate_cc`). It never re-elaborates the raw HIR type annotation. ### Source type mapping @@ -200,15 +213,17 @@ WASI 0.2.12 WIT once, before CC lowering. Resolution: - finds the package and interface, then the WIT function; - computes the canonical signature with `Resolve::wasm_signature`; - classifies each WIT parameter and the result into the WIT descriptor; -- interns the declaration's resolved source type in the module type table; +- joins the external's checked `ExternalType` by symbol instead of rebuilding + its source scheme from the HIR annotation; - records an `unsupported` reason when the shape has no source mapping, when a list is not byte-valued, when flattening does not agree with the canonical signature, or when the interface's package is disabled by the target; and - interns the import and returns a `ResolvedExternal`. -The stage validates the resolved source type against the WIT descriptor. A -failure is reported against the declaration's span; a declaration fails even -when dead code never calls it, because the side table is validated eagerly. +The stage validates the checked source type against the WIT descriptor. A +failure is reported against the declaration's source location; a declaration +fails even when dead code never calls it, because the side table is validated +eagerly. ### Lowering a call @@ -448,12 +463,14 @@ the crate-level tree. The implementation must conform to this organization: ```text backend/src/ - abi.rs WasiRegistry, WasiImport, package gating abi/ + mod.rs WasiRegistry, WasiImport, package gating classification.rs WIT type classification and value types - link.rs target-aware linking: intern the resolved type and - validate conformance - bindings.rs ExternalBindings side table and boundary checks + link/ + mod.rs target binding lookup and conformance entry + conformance.rs checked Core type versus WIT signature + bindings/ + mod.rs ExternalBindings side table and boundary checks mir/ wit/ mod.rs canonical call lowering and result recovery @@ -467,14 +484,15 @@ backend/src/ - `ExternalBindings` — the side table of the Model section, holding one `ResolvedExternal` per `ExternalKind::Wit` binding. `ResolvedExternal` pairs - the declaration's resolved source `TypeId` with its resolved `WasiImport` + the declaration's checked Core `TypeId` from `Module.external_types` with its + resolved `WasiImport` descriptor. It must provide `validate_core` and `validate_cc` for the P8/P9 boundary checks, and `validate_conformance`, which resolves and validates every binding against the resolved Core type where Core is available. -- `abi/link.rs` — the target-aware linking stage. It interns each declaration's - resolved source type in the module type table, resolves the WIT import once, - and validates the two sides with `validate_import_signature(import, module, - type_id)`. +- `abi/link/` — the target-aware conformance stage. It consumes the checked + Core type ID, resolves the WIT import once, and validates the two sides with + `validate_import_signature(import, module, checked_type)`. It does not parse + or re-intern raw HIR type annotations. - `WasiRegistry` — the interned `(interface, function)` registry, holding the `TargetCapabilities` it was loaded with. It must provide: - `load() -> Result` and @@ -580,8 +598,8 @@ synthesize and export `cabi_realloc` ([linear memory boundary](linear-memory-and ## Boundaries and interfaces -- **Input:** Typed Core externals projected into `ExternalBindings`, the vendored - WASI WIT, and the target profile. +- **Input:** Core `ExternalType` schemes joined with target-binding metadata to + produce `ExternalBindings`, the vendored WASI WIT, and the target profile. - **Output:** a set of `ResolvedExternal`s and the `WasiRegistry` P9 hands to P10; MIR imports carry only the canonical symbol, parameters, and result. - **To MIR:** canonical calls and adaptation instructions. The ABI layer decides @@ -733,19 +751,20 @@ implementation coverage, not design choices. The allocator, buffer free, and supported element is lowered. Resolved bindings ([DEC-12](../../../decision/DEC-12-resolved-wit-bindings.md)): -each foreign import's resolved source type is interned into the Core type table -by the linking boundary (`abi/link.rs`) and carried as an -`ExternalBinding::type_id`. CC derives its whole abstract signature, including -record and array representations, directly from that Core type; the structural -re-search (`core_type_matches_source`) and the source-signature comparison are -removed. WIT conformance validation runs at the linking boundary against the -resolved Core type (`ExternalBindings::validate_conformance`, -`abi/link::validate_import_signature`). MIR lowering reads the declaration's CC -`Signature` (`ValueShape`) and projects record and flags fields by label from -the planned representation table; the WIT descriptor drives canonical -adaptation. `SourceType` and `SourceSignature` are deleted; the ABI unit tests -validate against the resolved Core type. The refactor is behavior preserving and -does not change the source language. +each external's checked, synonym-expanded scheme is produced during type +checking and carried in `Module.external_types`, with `ForAll` quantifiers +preserved. `ExternalBindings::from_core` joins it to the WIT target binding and +carries its Core type identity beside that binding. CC derives its whole +abstract signature, including record and array representations, directly from +that Core type; the structural re-search (`core_type_matches_source`) and the +source-signature comparison are removed. WIT conformance validation runs at P8 +against the checked Core type (`ExternalBindings::validate_conformance`, +`abi/link::conformance::validate_import_signature`). MIR lowering reads the +declaration's CC `Signature` (`ValueShape`) and projects record and flags fields +by label from the planned representation table; the WIT descriptor drives +canonical adaptation. `SourceType` and `SourceSignature` are deleted; the ABI +unit tests validate against the resolved Core type. The refactor is behavior +preserving and does not change the source language. Implemented today: direct mappings for `bool`, `s32`, `s64`/`u64`, `f32`/`f64`, `char`, narrowed/unsigned integers, nullary enums, byte lists (`String`), direct diff --git a/docs/design/backend/wasm/encoding-and-structuring.md b/docs/design/backend/wasm/encoding-and-structuring.md index 0849f85f..36c5bc04 100644 --- a/docs/design/backend/wasm/encoding-and-structuring.md +++ b/docs/design/backend/wasm/encoding-and-structuring.md @@ -223,11 +223,15 @@ aligned blocks ([linear memory boundary](linear-memory-and-canonical-abi-boundar ### Command entry synthesis -The selected entry declaration must be a zero-argument function returning `Int` -(`i32`). P10 synthesizes a `run` entry with type `() -> i32` whose body calls -`main`, then calls `wasi:cli/exit.exit-with-code` with `main`'s result, then -returns `0`, the canonical `ok` discriminant of the `run` result. The core -module exports this entry under the name `wit-component` expects +The selected `Int` entry retains the existing zero-argument integer command +convention and preserves its result. An `Effect Unit` entry is normalized by an +ordinary Core adapter that runs the selected action exactly once, then returns +zero; a guest trap propagates before normal completion. Both forms reach P10 as +a zero-argument integer command function, with no generated adapter around the +`Int` entry. P10 synthesizes a `run` entry with type `() -> i32` that calls this +function, passes its result to `wasi:cli/exit.exit-with-code`, then returns `0`, +the canonical `ok` discriminant of the `run` result. The core module exports +this entry under the name `wit-component` expects (`wasi:cli/run@0.2.12#run`) and exports its linear memory as `memory`. The component lift and world are described in [WASI platform library](wasi-platform-library.md). diff --git a/docs/design/backend/wasm/wasi-platform-library.md b/docs/design/backend/wasm/wasi-platform-library.md index 5ef2b4a5..07c74b4d 100644 --- a/docs/design/backend/wasm/wasi-platform-library.md +++ b/docs/design/backend/wasm/wasi-platform-library.md @@ -148,7 +148,7 @@ consolidated capability layout: `WASI.Resource`, `WASI.IO`, `WASI.Console`, | On-disk `stdlib/lib` and the trusted prefix | WASI-10 | Done. The driver reads `stdlib/lib/trusted`. | | Exported wrappers | This library, [DEC-11](../../../decision/DEC-11-primitive-ffi-stdlib-wrappers.md) | Every service wrapper, plus the `WASI` umbrella. Raw imports stay unexported. | | `wasi:cli/exit.exit` (`status: result`) | Not wrapped | One canonical `i32`, and still not a library wrapper. See below. | -| `Effect` as `foreign import data` | [Effects](../fp/effects.md) | `Prelude` declares `foreign import data Effect` and the `psrs:effect` externals `pure`, `bind`, `run`, and `trap`. `lower_effects` turns the opaque application into a one-parameter closure after Typed Core and supplies those four bodies. | +| `Effect` as `foreign import data` | [Effects](../fp/effects.md) | Trusted library binding carries the resolved constructor and operation identities. Effect lowering turns applications into generic one-parameter closures, and import wrappers come only from plans formed from checked external schemes before `Effect` erasure. | | `Maybe`, `Either`, records, and data types as wrappers | [DEC-13](../../../decision/DEC-13-wit-to-source-type-mapping.md) | Library types, not compiler types; every `result` is an `Either E O` with the error on `Left`. | | **WASI-07 Arguments, environment, and filesystem** | #59 | Verified. `WASI.Process.arguments`/`environment` and `WASI.FileSystem` wrap `wasi:cli/environment` and `wasi:filesystem`; a file round-trip, a directory walk, and an environment read execute under Wasmtime. | | **WASI-08 Sockets** | #59 | In progress. `WASI.Network` wraps the socket services and the wrapper surface lowers; no socket execution test yet. HTTP/TLS are excluded. | @@ -210,15 +210,25 @@ WASI 0.2 families to be enabled in the target profile ### Entry and exit -The selected entry declaration is a zero-argument `Int` function. P10 -synthesizes the `run` entry that calls `main`, passes the result to -`wasi:cli/exit.exit-with-code`, and returns `0`, the canonical `ok` -discriminant of the `run` result. That synthesized call is how `main`'s -integer code exits. `WASI.Process.exitWithCode` is a separate effectful call to -the same WIT function; it does not replace the entry. A runtime that -implements `exit-with-code` as process termination never observes the trailing -constant, which exists to give the entry its declared `i32` result -([Wasm encoding](encoding-and-structuring.md)). +The driver selects one source declaration by resolved identity: `Main.main` +when present, otherwise the unique top-level declaration named `main`. The +selected declaration takes no arguments and returns `Int` or the trusted +`Effect Unit` type. An `Int` declaration keeps the existing zero-argument +integer command convention and preserves its result. For `Effect Unit`, P8 +generates an ordinary Core adapter that evaluates the selected declaration, +runs the returned action once, and returns zero after normal completion. The +adapter becomes the Core entry before CC; no adapter is added around an `Int` +entry. + +The `Effect Unit` wrapper propagates a guest trap instead of producing a +successful zero exit. P10's `run` entry calls the selected or generated +zero-argument integer function, passes its result to +`wasi:cli/exit.exit-with-code`, and returns `0`, +the canonical `ok` discriminant of the `run` result. `WASI.Process.exitWithCode` +is a separate effectful call to the same WIT function; it does not replace the +entry. A runtime that implements `exit-with-code` as process termination never +observes the trailing constant, which exists to give the entry its declared +`i32` result ([Wasm encoding](encoding-and-structuring.md)). ### The platform library @@ -395,18 +405,18 @@ sufficient ([IR boundaries](../00-ir-boundaries.md)). ## Worked example -Take `main = log "hello"`. The platform library defines `log` over the WIT -imports `wasi:cli/stdout#get-stdout` and +Take `main = log "hello"` with the inferred type `Effect Unit`. The platform +library defines `log` over the WIT imports `wasi:cli/stdout#get-stdout` and `wasi:io/streams#[method]output-stream.blocking-write-and-flush`. Linking keeps those imports because `main` reaches them, and prunes them otherwise. Lowering produces the Canonical ABI call shown in -[canonical ABI and WIT](canonical-abi-and-wit.md), the string literal lives in a -data segment ([linear memory boundary](linear-memory-and-canonical-abi-boundary.md)), -and P10 synthesizes the entry that calls `main` and exits. `componentize` then -lifts the core module: the component imports `wasi:cli/stdout@0.2.12` and -`wasi:io/streams@0.2.12` (plus their support interfaces) and exports -`wasi:cli/run@0.2.12`. `wasmtime run hello.wasm` calls `run`, which writes -`hello\n` and exits with `main`'s code. +[canonical ABI and WIT](canonical-abi-and-wit.md), and the string literal lives +in a data segment ([linear memory boundary](linear-memory-and-canonical-abi-boundary.md)). +The generated command wrapper runs the selected action once and returns zero. +`componentize` lifts the core module: the component imports +`wasi:cli/stdout@0.2.12` and `wasi:io/streams@0.2.12` (plus their support +interfaces) and exports `wasi:cli/run@0.2.12`. `wasmtime run hello.wasm` calls +`run`, which writes `hello\n` and exits successfully. ## Boundaries and interfaces diff --git a/docs/design/frontend/semantics/functional-core.md b/docs/design/frontend/semantics/functional-core.md index 6e9f81cb..dbe4a818 100644 --- a/docs/design/frontend/semantics/functional-core.md +++ b/docs/design/frontend/semantics/functional-core.md @@ -109,18 +109,40 @@ constructors is fixed: The primitive constructors name the source primitives; their concrete runtime representation is fixed later at MIR, not in Core. +Every WIT external import also has a checked, normalized scheme in +`Module.external_types`: + +```text +ExternalType = { symbol: SymbolId, ty: TypeId } +``` + +The type checker elaborates each WIT external annotation into the checked type +table, expanding type synonyms while preserving `ForAll` quantifiers. The raw +HIR external declaration remains for its source name and WIT binding metadata; +its annotation is not a later-stage semantic input. Compiler intrinsics keep +their explicit `Intrinsic` descriptor contracts and do not use this table. +Linking and optimization remap `ExternalType.ty` with the module type table. +Core verification requires one valid checked scheme for every WIT import. +Consumers such as effect lowering and target binding use this scheme and never +reconstruct it from HIR. + A data type's cases are not part of its `Type`; they are `ConstructorInfo` records naming a tag, a field count, and field types. A sum is therefore an ordered set of cases with stable tags, not a nested pair of constructors. `Effect a` is `Application(Constructor(User(effect_id)), a)`: an ordinary imported abstract type constructor applied on the uniform spine. Core has no -`Effect` node, no token type, and no side table that makes this constructor -callable. After Core, one representation lowering replaces each `Effect τ` -value with a closure whose parameter list is the runtime token and whose result -is the lowering of `τ`. That closure is not a source arrow, so curried-arrow -flattening does not absorb a function or a nested effect inside `τ`. The -translation and the execution boundary are specified in +`Effect` node, token type, or callable-type side table. Trusted library binding +resolves the constructor and operation identities once and passes that metadata +alongside linked Core. Each WIT import also carries its checked, +synonym-expanded scheme in `Module.external_types`; `ForAll` quantification is +preserved and `Effect` remains abstract in the scheme. The effect-lowering +pipeline uses the trusted identities and checked WIT schemes to classify +effectful imports before representation lowering, then replaces each `Effect τ` +value with a generic closure whose parameter list is the runtime token and +whose result is the lowering of `τ`. That closure is not a source arrow, so +curried-arrow flattening does not absorb a function or a nested effect inside +`τ`. The translation and execution boundary are specified in [effects](../../backend/fp/effects.md). `Module.newtype_ids` records single-field newtypes that are represented by their @@ -314,7 +336,9 @@ must preserve that scope when replacing the expression. ```text verify_module(module): - build globals = declarations -> checked type, externals -> unknown + build globals = declarations -> checked type, + WIT externals -> checked scheme from Module.external_types, + compiler intrinsics -> Intrinsic descriptor contract for each type in module.types: verify_type for each declaration: verify_type(declaration.ty) @@ -341,12 +365,15 @@ The required modules and the values they provide are: - `psrs-thir` owns the typed IR that the type checker produces and that Typed Core is elaborated from. It provides `Type`, `TypeId`, `TypeConstructor`, `Expr`, `ExprKind`, `Primitive`, `ConstructorInfo`, `Declaration`, `Binding`, - and `Binder`. + `ExternalType`, and `Binder`. Its `Module.external_types` records one checked, + synonym-expanded scheme per WIT external import. - `psrs-typecheck` checks `Effect` through its imported kind and declarations, using the same type rules as for other abstract type constructors. - `psrs-core` owns Typed Core and the P7 boundary. It provides: - `Module`, `Type`, `Expr`, `ExprKind`, `Primitive`, `ConstructorInfo`, `Declaration`, `Binding`, and `Binder` at the crate root; + - `ExternalType { symbol, ty }`, the checked, synonym-expanded scheme for each + WIT import, remapped with `Module.types`; - `Pattern` and `PatternKind` for the source-oriented pattern form; - `Module::verify(&self) -> Result<(), Vec>`, the P8 input verifier, with `VerifyError` retaining a source span; @@ -363,6 +390,8 @@ consistent before P8 consumes it: - every `TypeId` is inside `Module.types`, and every referenced `TypeId` is valid; +- every WIT external has exactly one `ExternalType`, and its `ty` is a valid + checked scheme in `Module.types`; no compiler intrinsic has an `ExternalType`; - `Local` references are in scope, and `Global` references name a declaration or external; - `Array*` expressions have an array type, `FieldAccess`, `Record*` and record @@ -430,12 +459,15 @@ such a call are specified in [CC IR](../../backend/fp/cc-ir.md). ## Boundaries and interfaces -- **Input.** P6 elaborates checked THIR into Typed Core. The driver links and - prunes declarations and selects the entry `SymbolId` - ([D-01](../../D-01-frontend-and-ir-boundaries.md)). +- **Input.** P6 elaborates checked THIR into Typed Core. The driver links + declarations, selects `Main.main` when present or the unique top-level + `main` otherwise, and prunes from that resolved entry `SymbolId`. The same + identity is used by the lexical `runEffect` check and generated command + wrapper ([D-01](../../D-01-frontend-and-ir-boundaries.md)). - **Output.** A verified Core module for P7 with an explicit checked type on every expression, `quantified` variables at binding sites, source spans, external - `symbols`, and newtype metadata. P7 preserves this contract for P8. + `symbols`, checked WIT `ExternalType` schemes, and newtype metadata. P7 + preserves the checked schemes and remaps their `TypeId`s for P8. - **To P8 (CC IR).** Core fixes evaluation order and carries explicit dictionary evidence. It leaves captures and runtime requirements to [CC IR](../../backend/fp/cc-ir.md). diff --git a/docs/feature/F-02-portable-programs.md b/docs/feature/F-02-portable-programs.md index 84192b5a..1becd537 100644 --- a/docs/feature/F-02-portable-programs.md +++ b/docs/feature/F-02-portable-programs.md @@ -24,10 +24,18 @@ Existing Node.js APIs and JavaScript FFI modules are not supported compatibility targets. Programs that use unsupported syntax, types, or platform services receive source-oriented diagnostics rather than a malformed artifact. -The selected command entry is a zero-argument integer `main`. It may use the -provided `runEffect` operation to execute effect values; other source -declarations cannot invoke the runner. An `Effect` value is opaque to source -code, and constructing it does not execute it. +The compiler selects `Main.main` when that declaration exists; otherwise it +requires exactly one top-level declaration named `main`. The selected entry +takes no arguments and may return `Int` or `Effect Unit`. An integer result +continues to determine the process exit code. For `Effect Unit`, the compiler +runs the returned action once; normal completion exits with code 0, and a guest +trap propagates as a failure. + +A direct reference to the provided `runEffect` operation may appear only in the +selected entry declaration. This is a lexical source restriction: the entry may +pass the runner to a helper, and that helper may call it. An `Effect` value is +opaque to source code, and constructing the value itself does not run its +deferred operation. The compiler emits a WASI 0.2 Component Model artifact. The legacy WASI Preview 1 module ABI is not part of the supported output contract. @@ -69,16 +77,17 @@ The initial slice supports direct top-level functions, integer and boolean values, integer arithmetic and comparisons, scalar `let`, `if`, nullary enum tags, non-parameterized data constructors with scalar or nested aggregate fields, single-field `newtype` values, constructor patterns in `case` and -function parameters, including nested constructor patterns, -a restricted parameterized ADT slice with erased scalar -fields, concrete scalar array literals and indexing, closed concrete records, -field reads, record updates, and closed concrete record patterns with variable, -wildcard, and nested constructor or record field bindings, function values including scalar-capturing closures, -higher-order calls, and the -implemented effect-based WASI console and clock libraries plus random imports. -The selected entry must be a zero-argument integer `main` function. Generic direct -calls and annotated rank-N values are lowered, including quantified parameters, -record and constructor fields, captures, and returned functions. Each use can +function parameters, including nested constructor patterns, a restricted +parameterized ADT slice with erased scalar fields, concrete scalar array +literals and indexing, closed concrete records, field reads, record updates, +and closed concrete record patterns with variable, wildcard, and nested +constructor or record field bindings, function values including +scalar-capturing closures, higher-order calls, and the implemented effect-based +WASI console and clock libraries plus random imports. +The selected source entry must take no arguments and return `Int` or +`Effect Unit`. Generic direct calls and annotated rank-N values are lowered, +including quantified parameters, record and constructor fields, captures, and +returned functions. Each use can instantiate a quantified value independently; nested constraints are supplied through the corresponding class instances. Generic arrays and records cross the supported polymorphic boundaries with their contents @@ -128,10 +137,10 @@ function calls. - A supported source program produces a validated core Wasm module at the requested output path. - The compiler prints WAT or writes it at the requested output path. -- The eventual WASI artifact runs in a compatible WASI runtime and produces - the program's expected observable result. -- The artifact runs in a compatible WASI runtime and produces the program's - expected observable result. +- The WASI artifact runs in a compatible runtime and preserves observable + behavior. An `Int` entry preserves its exit code; an `Effect Unit` entry + executes once, exits with code 0 after normal completion, and propagates a + trap. - Unsupported constructs fail with a source-oriented diagnostic. - Each added platform service has documented behavior and executable tests. diff --git a/docs/implementation/backend/effects.md b/docs/implementation/backend/effects.md index 6dc82cac..12c4283c 100644 --- a/docs/implementation/backend/effects.md +++ b/docs/implementation/backend/effects.md @@ -4,28 +4,28 @@ **Design:** [Effects](../../design/backend/fp/effects.md) -**Progress:** `lower_effects` replaces the opaque `Prelude.Effect` application -with a one-parameter closure after Typed Core and records every closure it -wrote. `EffectLowering::verify` rejects a recorded closure whose parameter list -is not `[Token]` or whose result is not the lowered effect result. The executed -negative fixtures call that check after replacing the node; they stay in Core. -EF-01 through EF-11 are verified on that encoding, including a saturated -`log "message"` and a partial application of an effect-returning function. -`callable_types` remains on the typed module and is always empty. +**Progress:** EF-01 through EF-13 are Verified on the explicit trusted-identity +contract. The 2026-10-04 runtime scoreboard is 124/413 (Wasmtime 49.0.2, `purs` +0.15.16). Those 124 files are the previous non-`Int` entries; each exits 0. +The 63 files with no selected `main` stay blocked. BE-21 stays Partial. A type +table changed after `lower_effects` returns is not checked again. Historical +records below describe the earlier encoding and are not the current evidence. **Roadmap:** [D-04 backend matrix](../../design/D-04-suite-roadmap.md#backend-feature-matrix), primarily BE-21, with BE-02 and BE-26 at closure/library boundaries. ## Scope and dependencies Complete the linked design's `Effect a` representation, `pure`, `bind`, -`runEffect`, hidden execution token, and sequencing through CC/MIR/Wasm. A -computation value is inert until an authorized runner invokes it. The linked -design's present-tense contract is authoritative beyond this matrix. Source -do/ado desugaring and class elaboration are frontend inputs; WASI service -availability belongs to the platform topic. This topic must verify the -ordinary closure interface and the trusted entry boundary. The embedded -library declares `foreign import data Effect` and abstract `psrs:effect` -operations; `lower_effects` supplies their closures. +`runEffect`, hidden execution token, and sequencing through CC/MIR/Wasm. An +Effect value defers its operation until an explicit source runner or the +generated Effect Unit command adapter invokes it; strict source arguments are +still evaluated normally. The linked design's contract is authoritative beyond +this matrix. Source do/ado desugaring and class elaboration are frontend inputs; +WASI service availability belongs to the platform topic. This topic verifies +generic closure conversion and the lexical runEffect reference rule, which is +not a capability or non-escape guarantee. The embedded library declares +`foreign import data Effect` and abstract `psrs:effect` operations; +`lower_effects` supplies their closures. ## Acceptance matrix @@ -34,25 +34,96 @@ Verified row needs behavior-sensitive execution, not only a closure-shaped IR. | ID | Design obligation | Required acceptance evidence | State | | --- | --- | --- | --- | -| EF-01 | `Effect a` is abstract through checking and Typed Core. One representation lowering emits a token closure; later passes do not match `Effect` or consult `callable_types`. | Inspect the lowering and generated CC/MIR; a source fixture cannot pass a function as an effect or name the token. | Verified | -| EF-02 | Constructing, storing, passing, returning, or capturing an Effect value performs no action. | Compile programs that build and discard or store an effect; mandatory execution asserts no import call/output before run. | Verified | +| EF-01 | `Effect a` is abstract through checking and Typed Core. Trusted-library binding resolves the constructor and operation identities once and passes them explicitly to lowering; the runtime form is a generic closure, with no dedicated Effect IR or runtime object. Checked WIT external schemes preserve alias expansion and quantification across THIR, Core, and the backend boundary. | Positive trusted import/re-export cases and same-name untrusted declarations; inspect identity metadata, checked WIT external schemes, and generic closure output. | Verified | +| EF-02 | Effectful WIT imports are classified from trusted identities and checked, synonym-expanded external schemes before type erasure. Only imports with explicit suspension plans receive wrappers; an ordinary WIT import returning a one-parameter closure remains ordinary. The deferred operation is inert, while strict argument expressions keep their source behavior. | Source execution tests check planned-import timing and strict argument behavior. A direct Core/binding fixture proves that an ordinary closure-shaped WIT external is not classified as Effect. | Verified | | EF-03 | `pure` returns the supplied value when run and invokes no external action. | Source and verified Core cases for scalar/reference values; inspect closure call count and value-sensitive result. | Verified | | EF-04 | `bind` runs the first effect before applying the continuation and then runs the returned effect exactly once. | Observable output/call-count order, including a continuation that ignores its argument, nested binds, and expected traps. | Verified | -| EF-05 | `runEffect` is available only to trusted entry/runtime code and invokes the closure once per call. | Unauthorized source call fails with source-associated diagnostic; two authorized runs produce two actions and a single run one action. | Verified | +| EF-05 | A direct source reference to trusted `runEffect` is allowed only inside the selected entry declaration. The entry may pass the function value to a helper, which may invoke it; this is not an authority or non-escape guarantee. | A direct reference outside the selected entry receives a source diagnostic; a runner value passed from the entry to a helper is accepted and invokes the closure once per call. | Verified | | EF-06 | Under-application of a source arrow captures the supplied arguments. The token is a parameter of the effect closure, not a remaining parameter of a function such as `log :: String -> Effect Unit`. | `log "message"` is a saturated call that returns a closure; a genuinely partial source application still captures once and defers the action. | Verified | | EF-07 | Core/P8 preserve strict source order of `let`, effect construction, and effect execution. | Source order cases with distinguishable WASI outputs, failures, and nested/conditional effects; compare Core, CC and runtime sequence. | Verified | | EF-08 | Polymorphic `Effect a` uses the normal erasure, boxing and closure adapters without exposing the token. | Execute effects returning Int, Number, String and a GC aggregate through generic functions; inspect signatures and recovered values. | Verified | -| EF-09 | Linked source modules forward Effect values without running them or granting untrusted modules runner privilege. | Producer/consumer modules with delayed execution, repeated forwarding, and unauthorized `runEffect` attempt. | Verified | -| EF-10 | Wasm/component entry executes only the selected trusted action and preserves WASI call order, results, and failures. | Mandatory Wasmtime component execution with stdout/stderr or another observable import, call counts, exit behavior, and valid binary. | Verified | -| EF-11 | A representation closure whose parameter list is not `[Token]`, or whose result is not the lowered effect result, fails verification before encoding. | Negative fixtures for the closure emitted by representation lowering, including an `Effect (a -> b)` closure that was flattened to arity two. | Verified | +| EF-09 | Linked source modules forward Effect values without running them. The same resolved entry identity governs the lexical `runEffect` check across linked modules. | Producer/consumer modules with delayed execution and repeated forwarding; a direct runner reference in a non-entry declaration is rejected. | Verified | +| EF-10 | The command entry preserves the selected source behavior: `Int` keeps its exit code; `Effect Unit` runs its returned action once, returns zero after normal completion, and propagates a guest trap. | Mandatory Wasmtime execution checks exact output, process status, action count, and an explicit trap marker for both entry forms. | Verified | +| EF-11 | Structural verification checks trusted identities and checked WIT operation signatures, every recorded Effect application closure, each import plan against its host wrapper, and the complete transformed Core including generated wrappers. | Malformed identity, checked WIT scheme, import-plan, closure-shape, wrapper-signature, and post-wrapper Core fixtures fail before CC/encoding; these checks are reported as structural evidence only. | Verified | | EF-12 | `trap` is the `Effect Unit` whose application ends the guest instead of returning, and the effect chain sequenced after it does not run. | A failing library assertion writes its message and traps; a held one lets the program finish; a statement after the trap never writes. | Verified | +| EF-13 | Entry selection resolves one source declaration: prefer `Main.main`, otherwise require a unique top-level `main`. The same `SymbolId` drives the runner check and any generated adapter; accepted result types are `Int` and trusted `Effect Unit`. | Source tests for preferred/fallback/ambiguous selection, aliases of `Effect Unit`, and agreement between selected identity, runner diagnostic, and generated adapter. | Verified | + +## Current evidence (2026-10-04) + +Wasmtime 49.0.2. `purs` 0.15.16. `PSRS_REQUIRE_WASMTIME=1 cargo test --workspace` +passed, as did `cargo clippy --workspace --all-targets -- -D warnings`. The +annotations scoreboard measured L6/M7 at 124/413. The same command, after +the rank-1 wrapper fix below, measured 124/413 again with the same blocker +split, and all 124 files still exited 0. L1–L5 stayed unchanged. Scoreboard +completion is not a golden comparison: a numeric exit with no trap marker +counts as completion. +The focused tests below assert stdout, status, or a trap marker. + +```text +EF-01: + Tests: tests::effects::an_untrusted_prelude_effect_remains_an_ordinary_user_type, + transitive_effect_types_keep_their_closure_representation; + psrs-core and psrs-thir external-signature tests. + Result: pass. Trusted identity is explicit. A same-name untrusted Effect + stays an ordinary user type. Typed Core keeps the application abstract. + Gaps: none for this obligation. +EF-02: + Tests: tests::effects::constructing_an_effect_does_not_execute_it, + effect_import_alias_is_expanded_before_suspension_planning, + a_quantified_effect_import_lowers_to_a_monotype_wrapper, + effect_suspension_conformance_errors_keep_the_imports_source_origin, + class_constrained_wit_imports_are_rejected_with_a_source_diagnostic. + Result: pass. A planned import is suspended from its checked scheme. + A rank-1 scheme keeps its binders on the wrapper declaration and stores + the closure monotype in `ty`. A class-constrained WIT signature is + rejected rather than dropped. + Gaps: none for this obligation. +EF-05: + Tests: tests::effects::run_effect_is_only_available_from_the_selected_entry, + instance_member_references_do_not_bypass_the_run_effect_scope, + the_selected_entry_may_pass_run_effect_to_a_higher_order_helper. + Result: pass. The restriction is lexical. Passing the runner to a helper + is accepted and is not described as capability confinement. + Gaps: none for this obligation. +EF-10: + Tests: tests::effects::an_effect_unit_entry_executes_its_action_once_through_both_source_apis, + effect_unit_entry_propagates_a_trap_from_the_action, + effect_unit_entry_runs_strict_construction_effects_before_its_action, + both_single_source_apis_compile_int_main_with_the_trusted_effect_library. + Result: pass under mandatory Wasmtime. The Effect Unit entry runs once, + returns 0, and a trap keeps the earlier stdout and suppresses later output. + An Int entry still returns its value. + Gaps: the scoreboard does not compare stdout with an upstream golden. +EF-11: + Tests: tests::effects::the_backend_rejects_partial_and_duplicate_trusted_operation_metadata, + the_backend_rejects_operation_identity_and_checked_signature_mismatches, + the_backend_rejects_an_effect_entry_context_for_an_integer_source_entry, + effect_command_metadata_must_name_the_selected_source_entry, + an_effect_source_entry_requires_command_metadata, + checked_import_verification_keeps_the_foreign_source_module. + Result: pass. These failures are returned by lowering before encoding. + Optimization and effect lowering both keep the module recorded on a Core + verification error. + Gaps: a type table rewritten after lower_effects returns is not checked + again. The Core negatives that mutate the table after a successful pass + still fail in EffectLowering::verify, not in the backend mapping. +EF-13: + Tests: tests::effects::a_main_in_the_main_module_takes_precedence_and_unique_main_is_the_fallback, + an_effect_int_entry_remains_invalid, + effect_unit_entry_accepts_a_type_synonym_and_cross_module_value, + typechecking_does_not_require_a_unique_command_entry. + Result: pass. Selection prefers Main.main, otherwise one top-level main. + Effect Int is rejected. Effect Unit synonyms are accepted. + Gaps: files with no selected main stay scoreboard blockers (63). +``` ## Vertical execution order -1. Audit library imports, trusted entry, Core-to-CC lowering, closure layout, - component runner, diagnostics, and tests against each design section. -2. Resolve token and privilege mismatches, then implement `pure`/`bind`/run - semantics and verifier rules with exact negative tests. +1. Audit trusted library identity, import signatures, entry selection, Core + wrapper insertion, external lowering, and the component runner against the + design. +2. Carry trusted Effect identities through the Core boundary; classify imports + before erasure; build wrappers only from plans; verify the transformed Core. 3. Execute inertness, order, repeated-run, polymorphic, and cross-module cases through the normal component path with mandatory Wasmtime. 4. Record evidence and update D-04. Do/ado syntax and unrelated WASI services @@ -62,8 +133,11 @@ Verified row needs behavior-sensitive execution, not only a closure-shaped IR. For each ID record code paths/functions, exact tests/assertions, input boundary, commands, Wasmtime version, actual executions/skips, revision, and -gaps. Distinguish source privacy from a trusted test fixture. Runtime cases -require `PSRS_REQUIRE_WASMTIME=1`; a skip is not verification. After Rust edits +gaps. Distinguish source diagnostics, structural IR checks, and behavior +observed through execution. Runtime cases require `PSRS_REQUIRE_WASMTIME=1`; a +skip is not verification. Scoreboard runtime completion is not a golden output +comparison and cannot identify every host CLI failure; focused tests must +assert exact stdout/status or an explicit trap marker. After Rust edits run `cargo fmt --all --check`, `cargo test --workspace`, and `cargo clippy --workspace --all-targets -- -D warnings`, plus focused runtime cases. Close only when all rows and the complete present-tense design pass. @@ -96,8 +170,10 @@ EF-01: arity test passed in the workspace suite; the partial-application test passed in that same command after it was added. Revision: uncommitted on issue/wit-abi-resolved-type-lowering - Gaps: `callable_types` is still a field and is always empty. Closure - conversion and MIR do not read it. + Gaps: this historical evidence did not check that trusted Effect identity + was passed explicitly; the old lowering recovered it from the qualified + type name and opacity metadata. Same-name untrusted declarations and + trusted re-exports need source-level coverage. EF-02: Implementation: crates/psrs-backend/src/cc/lower/lambda, cc/lower/call, crates/psrs-driver/src/tests/effects.rs @@ -109,7 +185,8 @@ EF-02: Commands: PSRS_REQUIRE_WASMTIME=1 cargo test -p psrs-driver effects:: Result: pass. Each program exits 0 with empty stdout before any run. Revision: 95aebe3 + uncommitted - Gaps: none + Gaps: these cases did not include an ordinary closure-shaped import decoy. + Import classification and wrapper timing require new tests. EF-03: Implementation: crates/psrs-core/src/effect/ (`pure_declaration`), crates/psrs-backend/src/cc/lower/call/partial.rs @@ -147,7 +224,9 @@ EF-05: Result: pass. Unauthorized reference is a P7 entry-selection diagnostic; two authorized runs emit two actions. Revision: 95aebe3 + uncommitted - Gaps: none + Gaps: the direct-reference rule is lexical. This record does not test a + runner value passed from the selected entry to a helper; it must not be + described as whole-program privilege isolation. EF-06: Implementation: crates/psrs-core/src/effect/ (closure parameter list stops at the token), crates/psrs-backend/src/cc/lower/call/partial.rs @@ -207,10 +286,11 @@ EF-09: run_effect_is_only_available_from_the_selected_entry Input boundary: source; executed Wasm component Commands: PSRS_REQUIRE_WASMTIME=1 cargo test -p psrs-driver effects:: - Result: pass. The producer module never references `runEffect`; forwarding - is inert and the selected entry runs the action once. + Result: pass for cross-module Effect forwarding and delayed execution. The + producer does not directly reference `runEffect`. Revision: 95aebe3 + uncommitted - Gaps: none + Gaps: direct lexical reference restriction is not capability isolation; a + runner passed from the selected entry to a helper may be invoked there. EF-10: Implementation: crates/psrs-backend/src/component.rs, crates/psrs-backend/src/wasm/lower/mod.rs (entry wrapper), @@ -221,9 +301,11 @@ EF-10: binary. tests/wasmtime_required.rs gates the runtime baseline. Input boundary: executed Wasm component Commands: PSRS_REQUIRE_WASMTIME=1 cargo test --workspace - Result: pass, 33 suites ok, 0 skipped under PSRS_REQUIRE_WASMTIME=1. + Result: pass for the historical `Int` entry behavior under + `PSRS_REQUIRE_WASMTIME=1`. Revision: 95aebe3 + uncommitted - Gaps: none + Gaps: this does not cover the generated `Effect Unit` adapter, normal zero + exit, exactly-once execution, or trap propagation through that adapter. EF-11: Implementation: crates/psrs-core/src/effect/mod.rs (`lower_effects`, `rewrite_effect_applications`, `EffectLowering::verify`). The pass records @@ -257,11 +339,11 @@ EF-11: node, and fail in `EffectLowering::verify` with a Core `VerifyError`. They do not enter the backend, CC, MIR, or the encoder. Revision: 253809f + uncommitted on issue/wit-abi-resolved-type-lowering - Gaps: the check sees only the closures this pass recorded, which is the only - place that still recognizes `Effect`; a table mutated after the pass ran is - not re-checked. `Type::Closure` stays a general representation: only nodes - the lowering wrote are constrained to `[Token]`. BE-21 remains the broader - landing gate for this topic. + Gaps: these historical negatives stop at the effect-lowering Core check. + They do not exercise semantic identity validation, import-plan consistency, + generated wrapper structure, or verification of the complete transformed + Core. `Type::Closure` remains the generic runtime representation. + BE-21 remains the broader landing gate for this topic. EF-12: Implementation: stdlib/lib/Prelude.purs (`psrs:effect#trap`, `trap :: Effect Unit`), crates/psrs-core/src/effect/operations.rs @@ -284,19 +366,20 @@ EF-12: instruction executed`); the held cases exit 0 and the trap stops the chain, so the statement after it never writes. Revision: uncommitted on feat/ph3-unit-and-test-assert - Gaps: `trap` is `Effect Unit`, not `forall a. Effect a`: a polymorphic form - would need the backend to fill a use-site result type on a path that never - produces one, and no library caller needs it. `assertThrows` needs to - observe a trap from inside the guest, which the target profile does not - provide ([DEC-05](../../decision/DEC-05-wasmtime-feature-set.md)), so the - standard library omits it rather than approximating it. + Gaps: the current public signature is `Effect Unit` because that is the + assertion and platform API the library needs; this is not forced by + non-returning lowering. `assertThrows` needs to observe a trap from inside + the guest, which the target profile does not provide + ([DEC-05](../../decision/DEC-05-wasmtime-feature-set.md)), so the standard + library omits it rather than approximating it. ``` ## Discovered obligations -- The token is the Core `Int` chosen by `lower_effects`. The synthesized - `runEffect` applies the integer `0`. Source programs cannot name that token. - A later stateful token is an open question in the design, not a second +- The token is the Core `Int` chosen by effect lowering. Its current value + `0` is a placeholder: it does not schedule work or establish ordering. + Source programs cannot name the token; order comes from the calls and + optimizer contracts. A later stateful token is an open question, not a second representation. - Partial application of a polymorphic declaration whose result is a type variable previously failed CC verification (the generated function returned diff --git a/docs/implementation/backend/wasi-platform.md b/docs/implementation/backend/wasi-platform.md index c07cb3f4..1fd18a61 100644 --- a/docs/implementation/backend/wasi-platform.md +++ b/docs/implementation/backend/wasi-platform.md @@ -42,7 +42,7 @@ States are **Unverified**, **In progress**, **Blocked**, and **Verified**. | ID | Design obligation | Required acceptance evidence | State | | --- | --- | --- | --- | | WASI-01 | The core module is componentized into a WASI 0.2 command with UTF-8 strings and matching world. | Component emission and world/capability tests. | Verified | -| WASI-02 | The command entry calls `wasi:cli/run` and exits with the program result. | Executed component returns the program exit code. | Verified | +| WASI-02 | The command adapter preserves the selected source entry: `Int` returns its exit code; `Effect Unit` runs once and returns zero after normal completion, while a trap propagates. | Mandatory Wasmtime component execution checks output, status, exactly-once behavior, and an explicit trap marker for both source entry forms. | Verified | | WASI-03 | Console stdout and stderr are wired and observable, linearizing GC strings per call. | Stdout/stderr execution tests and effect ordering. | Verified | | WASI-04 | Monotonic clock is wired. | Clock execution test. | Verified | | WASI-05 | Random bytes are wired, recovering the returned byte list into a GC value. | Random execution test. | Verified | @@ -79,14 +79,23 @@ WASI-01: ```text WASI-02: - Implementation: crates/psrs-backend/src/wasm/lower/mod.rs (entry) and - component.rs. - Tests: component::tests::runs_the_command_when_wasmtime_is_available; - psrs-driver tests::wasi::runs_main_as_a_wasi_component_when_wasmtime_is_available. - Input boundary: source and executed component. + Implementation: crates/psrs-backend/src/effects/entry.rs (Core adapter), + crates/psrs-driver/src/program/mod.rs (entry classification), + component packaging of the resulting zero-argument Int export. + Tests: tests::effects::an_effect_unit_entry_executes_its_action_once_through_both_source_apis, + effect_unit_entry_propagates_a_trap_from_the_action, + effect_unit_entry_runs_strict_construction_effects_before_its_action, + both_single_source_apis_compile_int_main_with_the_trusted_effect_library; + component::tests::runs_the_command_when_wasmtime_is_available. + Input boundary: source and executed component. Assertions cover stdout, + process status, one action, and a trap marker. Commands: PSRS_REQUIRE_WASMTIME=1 cargo test --workspace. - Result: pass. - Gaps: none. + Result: pass on 2026-10-04 under Wasmtime 49.0.2. Effect Unit returns 0 + after one run. A trap keeps `before` and suppresses later output. Int + main still returns its value. The official board moved from 0/413 to + 124/413; every recovered file exits 0. + Gaps: scoreboard completion is not an upstream golden. The 63 files with + no selected main remain blocked and are not given an empty main. ``` ```text