From 881bad59013d6bc78c87cbadb90f9a30dcd114ab Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Sat, 29 Aug 2026 13:12:09 +0100 Subject: [PATCH 1/6] fix(wasm): preserve extern expression stack types --- src/ephapax-wasm/src/lib.rs | 161 +++++++++++++++++++++++++++++++----- 1 file changed, 140 insertions(+), 21 deletions(-) diff --git a/src/ephapax-wasm/src/lib.rs b/src/ephapax-wasm/src/lib.rs index 66a35ec..6f646e8 100644 --- a/src/ephapax-wasm/src/lib.rs +++ b/src/ephapax-wasm/src/lib.rs @@ -232,6 +232,8 @@ struct LocalTracker { next_idx: u32, /// Which locals are linear (must be consumed before scope exit) linear_locals: HashMap, + /// WebAssembly types for non-parameter locals, in index order. + extra_local_types: Vec, } impl LocalTracker { @@ -240,14 +242,21 @@ impl LocalTracker { name_to_idx: HashMap::new(), next_idx: num_params, linear_locals: HashMap::new(), + extra_local_types: Vec::new(), } } /// Bind a named variable to the next available local slot. fn bind(&mut self, name: &str, is_linear: bool) -> u32 { + self.bind_typed(name, is_linear, ValType::I32) + } + + /// Bind a named variable with its concrete WebAssembly local type. + fn bind_typed(&mut self, name: &str, is_linear: bool, ty: ValType) -> u32 { let idx = self.next_idx; self.next_idx += 1; self.name_to_idx.insert(name.to_string(), idx); + self.extra_local_types.push(ty); if is_linear { self.linear_locals.insert(idx, false); // false = not yet consumed } @@ -258,6 +267,7 @@ impl LocalTracker { fn temp(&mut self) -> u32 { let idx = self.next_idx; self.next_idx += 1; + self.extra_local_types.push(ValType::I32); idx } @@ -286,6 +296,16 @@ impl LocalTracker { fn num_extra_locals(&self, num_params: u32) -> u32 { self.next_idx.saturating_sub(num_params) } + + /// Declarations for `wasm_encoder::Function::new`, preserving local + /// index order across mixed-width Ephapax bindings. + fn wasm_local_declarations(&self) -> Vec<(u32, ValType)> { + self.extra_local_types + .iter() + .copied() + .map(|ty| (1, ty)) + .collect() + } } // --------------------------------------------------------------------------- @@ -344,11 +364,11 @@ pub struct Codegen { /// Order = emission order in the import section. extern_imports: Vec, - /// Lookup: extern fn name -> wasm function index. + /// Lookup: extern fn name -> (wasm function index, returns language Unit). /// `compile_expr` consults this to resolve `Var(name)` references /// that come from extern blocks; calls become `Call(idx)` into the /// import. - extern_fn_indices: HashMap, + extern_fn_indices: HashMap, /// Names of extern types declared in the AST. Used only as a /// presence check during typecheck-style queries; the wasm layer @@ -934,7 +954,8 @@ impl Codegen { } => { let wasm_params: Vec = params.iter().map(|(_, ty)| ty_to_valtype(ty)).collect(); - let wasm_results = if matches!(ret_ty, Ty::Base(BaseTy::Unit)) { + let returns_unit = matches!(ret_ty, Ty::Base(BaseTy::Unit)); + let wasm_results = if returns_unit { vec![] } else { vec![ty_to_valtype(ret_ty)] @@ -952,7 +973,8 @@ impl Codegen { name: name.to_string(), wasm_type_idx: type_idx, }); - self.extern_fn_indices.insert(name.to_string(), import_idx); + self.extern_fn_indices + .insert(name.to_string(), (import_idx, returns_unit)); } } } @@ -1122,6 +1144,7 @@ impl Codegen { let mut dummy_func = Function::new(vec![(64, ValType::I32)]); // generous self.compile_expr(&mut dummy_func, body); let extra = self.locals.num_extra_locals(num_params); + let local_declarations = self.locals.wasm_local_declarations(); // Restore data state self.data_entries.truncate(data_snapshot.0); @@ -1136,11 +1159,8 @@ impl Codegen { } } - let mut func = Function::new(if extra > 0 { - vec![(extra, ValType::I32)] - } else { - vec![] - }); + debug_assert_eq!(extra as usize, local_declarations.len()); + let mut func = Function::new(local_declarations); self.compile_expr(&mut func, body); func.instruction(&Instruction::End); @@ -1212,6 +1232,7 @@ impl Codegen { self.compile_expr(&mut dummy_func, &lambda_info.body); let extra = self.locals.num_extra_locals(num_params); + let local_declarations = self.locals.wasm_local_declarations(); // Restore data state self.data_entries.truncate(data_snapshot.0); @@ -1230,11 +1251,8 @@ impl Codegen { self.locals.bind(captured_name, false); } - let mut func = Function::new(if extra > 0 { - vec![(extra, ValType::I32)] - } else { - vec![] - }); + debug_assert_eq!(extra as usize, local_declarations.len()); + let mut func = Function::new(local_declarations); // Load captured variables from env_ptr into local slots for (i, _) in lambda_info.captured_vars.iter().enumerate() { @@ -1821,11 +1839,17 @@ impl Codegen { ExprKind::StringConcat { left, right } => self.compile_string_concat(func, left, right), ExprKind::StringLen(inner) => self.compile_string_len(func, inner), ExprKind::Let { - name, value, body, .. - } => self.compile_let(func, name, value, body, false), + name, + ty, + value, + body, + } => self.compile_let(func, name, ty.as_ref(), value, body, false), ExprKind::LetLin { - name, value, body, .. - } => self.compile_let(func, name, value, body, true), + name, + ty, + value, + body, + } => self.compile_let(func, name, ty.as_ref(), value, body, true), ExprKind::Lambda { param, param_ty, @@ -1970,6 +1994,7 @@ impl Codegen { &mut self, func: &mut Function, name: &str, + ty: Option<&Ty>, value: &Expr, body: &Expr, is_linear: bool, @@ -1978,7 +2003,8 @@ impl Codegen { self.compile_expr(func, value); // Bind it to a local - let local_idx = self.locals.bind(name, is_linear); + let local_ty = ty.map(ty_to_valtype).unwrap_or(ValType::I32); + let local_idx = self.locals.bind_typed(name, is_linear, local_ty); func.instruction(&Instruction::LocalSet(local_idx)); // Compile the body @@ -2278,7 +2304,7 @@ impl Codegen { // Direct call to an extern import (phase 2B-ii of #43). // Extern fns are wasm imports — their index lives in // `extern_fn_indices` after `collect_extern_imports` runs. - if let Some(&import_idx) = self.extern_fn_indices.get(head) { + if let Some(&(import_idx, returns_unit)) = self.extern_fn_indices.get(head) { // A lone synthetic `()` is the nullary-call placeholder // (`f()` → `App(f, ())`); push no args for it. Otherwise // push every real arg in order. @@ -2291,6 +2317,14 @@ impl Codegen { self.compile_expr(func, a); } func.instruction(&Instruction::Call(import_idx)); + // Language-level Unit is represented as i32 zero inside + // compiled expressions, but a host Unit-returning import has + // no WebAssembly result. Reconstitute the language value so + // the enclosing expression has the stack shape its caller + // expects. + if returns_unit { + func.instruction(&Instruction::I32Const(0)); + } return; } } @@ -4471,11 +4505,96 @@ mod tests { codegen.collect_extern_imports(&module); assert_eq!( codegen.extern_fn_indices.get("do_thing").copied(), - Some(NUM_BUILTIN_IMPORTS), + Some((NUM_BUILTIN_IMPORTS, false)), "first extern fn must occupy import slot 2 (right after the 2 builtin imports)" ); } + /// A Unit-returning extern has no WebAssembly result, while Ephapax + /// expressions represent Unit as `i32 0`. Direct-call lowering must + /// restore that value or the enclosing function is structurally invalid. + #[test] + fn unit_returning_extern_call_reconstitutes_language_unit() { + let module = AstModule { + name: "test".into(), + imports: vec![], + decls: vec![ + Decl::Extern { + abi: "host".to_string(), + items: vec![ExternItem::Fn { + name: "notify".into(), + params: vec![("value".into(), Ty::Base(BaseTy::I32))], + ret_ty: Ty::Base(BaseTy::Unit), + }], + }, + Decl::Fn { + name: "entry".into(), + visibility: Visibility::Private, + type_params: vec![], + params: vec![], + ret_ty: Ty::Base(BaseTy::Unit), + body: e(ExprKind::App { + func: Box::new(e(ExprKind::Var("notify".into()))), + arg: Box::new(e(ExprKind::Lit(Literal::I32(7)))), + }), + }, + ], + }; + + let wasm = compile_module(&module).expect("module must compile"); + validate_wasm(&wasm); + } + + /// Declared non-i32 let bindings must retain their WebAssembly local + /// type. This models Gossamer's capability-token path, where an i64 host + /// result is stored and passed to another host import. + #[test] + fn annotated_i64_let_uses_i64_wasm_local() { + let module = AstModule { + name: "test".into(), + imports: vec![], + decls: vec![ + Decl::Extern { + abi: "host".to_string(), + items: vec![ + ExternItem::Fn { + name: "cap_token".into(), + params: vec![("kind".into(), Ty::Base(BaseTy::I32))], + ret_ty: Ty::Base(BaseTy::I64), + }, + ExternItem::Fn { + name: "i64_is_zero".into(), + params: vec![("value".into(), Ty::Base(BaseTy::I64))], + ret_ty: Ty::Base(BaseTy::I32), + }, + ], + }, + Decl::Fn { + name: "entry".into(), + visibility: Visibility::Private, + type_params: vec![], + params: vec![], + ret_ty: Ty::Base(BaseTy::I32), + body: e(ExprKind::Let { + name: "token".into(), + ty: Some(Ty::Base(BaseTy::I64)), + value: Box::new(e(ExprKind::App { + func: Box::new(e(ExprKind::Var("cap_token".into()))), + arg: Box::new(e(ExprKind::Lit(Literal::I32(0)))), + })), + body: Box::new(e(ExprKind::App { + func: Box::new(e(ExprKind::Var("i64_is_zero".into()))), + arg: Box::new(e(ExprKind::Var("token".into()))), + })), + }), + }, + ], + }; + + let wasm = compile_module(&module).expect("module must compile"); + validate_wasm(&wasm); + } + // ----------------------------------------------------------------------- // ExprKind::Match — br_table dispatch // ----------------------------------------------------------------------- From cc483a634b71b66d98338a325328b147a4723538 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Sat, 29 Aug 2026 13:34:17 +0100 Subject: [PATCH 2/6] fix(wasm): retain inferred and captured value types --- src/ephapax-wasm/src/lib.rs | 302 ++++++++++++++++++++++++++++++++---- 1 file changed, 268 insertions(+), 34 deletions(-) diff --git a/src/ephapax-wasm/src/lib.rs b/src/ephapax-wasm/src/lib.rs index 6f646e8..086c168 100644 --- a/src/ephapax-wasm/src/lib.rs +++ b/src/ephapax-wasm/src/lib.rs @@ -208,6 +208,8 @@ struct UserFnInfo { wasm_fn_idx: u32, /// Index of its type in the type section wasm_type_idx: u32, + /// Concrete WebAssembly result type used for direct-call inference. + result_type: ValType, /// Parameter names (in order) for local binding #[allow(dead_code)] param_names: Vec, @@ -228,6 +230,8 @@ struct UserFnInfo { struct LocalTracker { /// Map from variable name to its local index name_to_idx: HashMap, + /// Concrete WebAssembly type for each named local and parameter. + name_to_type: HashMap, /// Number of locals allocated so far (parameters first, then compiler temps) next_idx: u32, /// Which locals are linear (must be consumed before scope exit) @@ -240,6 +244,7 @@ impl LocalTracker { fn new(num_params: u32) -> Self { Self { name_to_idx: HashMap::new(), + name_to_type: HashMap::new(), next_idx: num_params, linear_locals: HashMap::new(), extra_local_types: Vec::new(), @@ -256,6 +261,7 @@ impl LocalTracker { let idx = self.next_idx; self.next_idx += 1; self.name_to_idx.insert(name.to_string(), idx); + self.name_to_type.insert(name.to_string(), ty); self.extra_local_types.push(ty); if is_linear { self.linear_locals.insert(idx, false); // false = not yet consumed @@ -276,6 +282,11 @@ impl LocalTracker { self.name_to_idx.get(name).copied() } + /// Look up a named local's concrete WebAssembly type. + fn get_type(&self, name: &str) -> Option { + self.name_to_type.get(name).copied() + } + /// Mark a linear local as consumed. fn mark_consumed(&mut self, idx: u32) { if let Some(v) = self.linear_locals.get_mut(&idx) { @@ -364,11 +375,11 @@ pub struct Codegen { /// Order = emission order in the import section. extern_imports: Vec, - /// Lookup: extern fn name -> (wasm function index, returns language Unit). + /// Lookup: extern fn name -> (wasm function index, optional wasm result). /// `compile_expr` consults this to resolve `Var(name)` references /// that come from extern blocks; calls become `Call(idx)` into the /// import. - extern_fn_indices: HashMap, + extern_fn_indices: HashMap)>, /// Names of extern types declared in the AST. Used only as a /// presence check during typecheck-style queries; the wasm layer @@ -430,6 +441,8 @@ struct LambdaInfo { wasm_type_idx: u32, /// Variables captured from the enclosing scope captured_vars: Vec, + /// Concrete type and byte offset for each captured variable. + captured_layout: Vec<(ValType, u64)>, /// Lambda parameter name param: String, /// Lambda parameter type @@ -636,6 +649,7 @@ impl Codegen { UserFnInfo { wasm_fn_idx: self.first_user_fn(), wasm_type_idx: TYPE_VOID_VOID, + result_type: ValType::I32, param_names: Vec::new(), param_kinds: Vec::new(), }, @@ -810,6 +824,7 @@ impl Codegen { UserFnInfo { wasm_fn_idx: idx, wasm_type_idx: type_idx, + result_type: ty_to_valtype(ret_ty), param_names, param_kinds, }, @@ -954,11 +969,15 @@ impl Codegen { } => { let wasm_params: Vec = params.iter().map(|(_, ty)| ty_to_valtype(ty)).collect(); - let returns_unit = matches!(ret_ty, Ty::Base(BaseTy::Unit)); - let wasm_results = if returns_unit { - vec![] + let wasm_result = if matches!(ret_ty, Ty::Base(BaseTy::Unit)) { + None } else { - vec![ty_to_valtype(ret_ty)] + Some(ty_to_valtype(ret_ty)) + }; + let wasm_results = if let Some(result) = wasm_result { + vec![result] + } else { + vec![] }; let type_idx = self.register_type(wasm_params, wasm_results); @@ -974,7 +993,7 @@ impl Codegen { wasm_type_idx: type_idx, }); self.extern_fn_indices - .insert(name.to_string(), (import_idx, returns_unit)); + .insert(name.to_string(), (import_idx, wasm_result)); } } } @@ -1133,6 +1152,9 @@ impl Codegen { self.locals = LocalTracker::new(num_params); for (i, (pname, pty)) in params.iter().enumerate() { self.locals.name_to_idx.insert(pname.to_string(), i as u32); + self.locals + .name_to_type + .insert(pname.to_string(), ty_to_valtype(pty)); if pty.is_linear() { self.locals.linear_locals.insert(i as u32, false); } @@ -1154,6 +1176,9 @@ impl Codegen { self.locals = LocalTracker::new(num_params); for (i, (pname, pty)) in params.iter().enumerate() { self.locals.name_to_idx.insert(pname.to_string(), i as u32); + self.locals + .name_to_type + .insert(pname.to_string(), ty_to_valtype(pty)); if pty.is_linear() { self.locals.linear_locals.insert(i as u32, false); } @@ -1206,15 +1231,26 @@ impl Codegen { self.locals = LocalTracker::new(num_params); // param 0 = env_ptr (anonymous, used internally) self.locals.name_to_idx.insert("__env_ptr".to_string(), 0); + self.locals + .name_to_type + .insert("__env_ptr".to_string(), ValType::I32); // param 1 = lambda parameter self.locals.name_to_idx.insert(lambda_info.param.clone(), 1); + self.locals.name_to_type.insert( + lambda_info.param.clone(), + ty_to_valtype(&lambda_info.param_ty), + ); if lambda_info.param_ty.is_linear() { self.locals.linear_locals.insert(1, false); } // Bind captured variables as locals (loaded from env_ptr) - for captured_name in &lambda_info.captured_vars { - self.locals.bind(captured_name, false); + for (captured_name, (captured_type, _)) in lambda_info + .captured_vars + .iter() + .zip(&lambda_info.captured_layout) + { + self.locals.bind_typed(captured_name, false, *captured_type); } // Save data state so pass 1 string literals don't duplicate @@ -1223,9 +1259,14 @@ impl Codegen { let mut dummy_func = Function::new(vec![(64, ValType::I32)]); // generous // Emit captured var loads in dry run - for (i, _) in lambda_info.captured_vars.iter().enumerate() { + for (i, (_, (captured_type, offset))) in lambda_info + .captured_vars + .iter() + .zip(&lambda_info.captured_layout) + .enumerate() + { dummy_func.instruction(&Instruction::LocalGet(0)); // env_ptr - dummy_func.instruction(&Instruction::I32Load(mem_arg((i * 4) as u64))); + emit_typed_load(&mut dummy_func, *captured_type, *offset); let local_idx = num_params + i as u32; dummy_func.instruction(&Instruction::LocalSet(local_idx)); } @@ -1241,23 +1282,39 @@ impl Codegen { // --- Pass 2: compile for real with correct local count -- self.locals = LocalTracker::new(num_params); self.locals.name_to_idx.insert("__env_ptr".to_string(), 0); + self.locals + .name_to_type + .insert("__env_ptr".to_string(), ValType::I32); self.locals.name_to_idx.insert(lambda_info.param.clone(), 1); + self.locals.name_to_type.insert( + lambda_info.param.clone(), + ty_to_valtype(&lambda_info.param_ty), + ); if lambda_info.param_ty.is_linear() { self.locals.linear_locals.insert(1, false); } // Re-bind captured variables as locals - for captured_name in &lambda_info.captured_vars { - self.locals.bind(captured_name, false); + for (captured_name, (captured_type, _)) in lambda_info + .captured_vars + .iter() + .zip(&lambda_info.captured_layout) + { + self.locals.bind_typed(captured_name, false, *captured_type); } debug_assert_eq!(extra as usize, local_declarations.len()); let mut func = Function::new(local_declarations); // Load captured variables from env_ptr into local slots - for (i, _) in lambda_info.captured_vars.iter().enumerate() { + for (i, (_, (captured_type, offset))) in lambda_info + .captured_vars + .iter() + .zip(&lambda_info.captured_layout) + .enumerate() + { func.instruction(&Instruction::LocalGet(0)); // env_ptr (param 0) - func.instruction(&Instruction::I32Load(mem_arg((i * 4) as u64))); + emit_typed_load(&mut func, *captured_type, *offset); let local_idx = num_params + i as u32; func.instruction(&Instruction::LocalSet(local_idx)); } @@ -1990,6 +2047,55 @@ impl Codegen { func.instruction(&Instruction::Call(self.fn_string_len())); } + /// Recover the concrete WebAssembly value type needed by local lowering. + /// The typechecker has already accepted the AST, but inferred let types + /// are not written back into `ExprKind::Let`, so codegen reconstructs the + /// small amount of representation information it needs here. + fn infer_expr_valtype(&self, expr: &Expr) -> ValType { + match &expr.kind { + ExprKind::Lit(Literal::I64(_)) => ValType::I64, + ExprKind::Lit(Literal::F32(_)) => ValType::F32, + ExprKind::Lit(Literal::F64(_)) => ValType::F64, + ExprKind::Lit(_) => ValType::I32, + ExprKind::Var(name) => self.locals.get_type(name).unwrap_or(ValType::I32), + ExprKind::Let { body, .. } | ExprKind::LetLin { body, .. } => { + self.infer_expr_valtype(body) + } + ExprKind::App { func, arg } => { + if let Some((head, _)) = flatten_app_chain(func, arg) { + if let Some(info) = self.user_fns.get(head) { + return info.result_type; + } + if let Some((_, result)) = self.extern_fn_indices.get(head) { + return result.unwrap_or(ValType::I32); + } + } + ValType::I32 + } + ExprKind::If { then_branch, .. } => self.infer_expr_valtype(then_branch), + ExprKind::Region { body, .. } | ExprKind::Copy(body) | ExprKind::Deref(body) => { + self.infer_expr_valtype(body) + } + ExprKind::Block(exprs) => exprs + .last() + .map(|last| self.infer_expr_valtype(last)) + .unwrap_or(ValType::I32), + ExprKind::UnaryOp { + op: UnaryOp::Neg, + operand, + } => self.infer_expr_valtype(operand), + ExprKind::BinOp { + op: BinOp::Add | BinOp::Sub | BinOp::Mul | BinOp::Div | BinOp::Mod, + left, + .. + } => self.infer_expr_valtype(left), + // The legacy `__ffi` surface is defined as i64-in/i64-out. + ExprKind::FFI { .. } => ValType::I64, + ExprKind::TupleLit(elements) if elements.len() > 2 => ValType::I64, + _ => ValType::I32, + } + } + fn compile_let( &mut self, func: &mut Function, @@ -1999,11 +2105,14 @@ impl Codegen { body: &Expr, is_linear: bool, ) { + let local_ty = ty + .map(ty_to_valtype) + .unwrap_or_else(|| self.infer_expr_valtype(value)); + // Compile the value expression self.compile_expr(func, value); // Bind it to a local - let local_ty = ty.map(ty_to_valtype).unwrap_or(ValType::I32); let local_idx = self.locals.bind_typed(name, is_linear, local_ty); func.instruction(&Instruction::LocalSet(local_idx)); @@ -2189,6 +2298,18 @@ impl Codegen { let mut bound_vars = std::collections::HashSet::new(); bound_vars.insert(param.to_string()); let captured_vars = self.find_free_vars(body, &bound_vars); + let mut next_capture_offset = 0_u64; + let captured_layout: Vec<(ValType, u64)> = captured_vars + .iter() + .map(|name| { + let ty = self.locals.get_type(name).unwrap_or(ValType::I32); + let (size, alignment, _) = valtype_storage(ty); + next_capture_offset = align_up(next_capture_offset, alignment); + let offset = next_capture_offset; + next_capture_offset += size; + (ty, offset) + }) + .collect(); // 2. Lambda functions take (env_ptr, param) -> result let lambda_type_idx = TYPE_CLOSURE_CALL; @@ -2207,19 +2328,15 @@ impl Codegen { wasm_fn_idx: lambda_fn_idx, wasm_type_idx: lambda_type_idx, captured_vars: captured_vars.clone(), + captured_layout: captured_layout.clone(), param: param.to_string(), param_ty: param_ty.clone(), body: body.clone(), }); // 6. Allocate environment block for captured variables - // Layout: [captured_0: i32, captured_1: i32, ...] - let num_captured = captured_vars.len() as u32; - let env_size = if num_captured > 0 { - num_captured * 4 - } else { - 4 - }; // min 4 bytes + // Layout preserves each captured value's width and alignment. + let env_size = next_capture_offset.max(4); // Allocate env block via bump allocator func.instruction(&Instruction::I32Const(env_size as i32)); @@ -2230,16 +2347,16 @@ impl Codegen { func.instruction(&Instruction::LocalSet(env_local)); // Store each captured variable's current value into the env block - for (i, var_name) in captured_vars.iter().enumerate() { + for (var_name, (captured_type, offset)) in captured_vars.iter().zip(&captured_layout) { func.instruction(&Instruction::LocalGet(env_local)); // env_ptr (address) if let Some(var_idx) = self.locals.get(var_name) { func.instruction(&Instruction::LocalGet(var_idx)); // captured value } else { // Variable not in locals — could be a top-level function reference. // Default to 0 (will be resolved by name during lambda body compilation). - func.instruction(&Instruction::I32Const(0)); + emit_typed_zero(func, *captured_type); } - func.instruction(&Instruction::I32Store(mem_arg((i * 4) as u64))); + emit_typed_store(func, *captured_type, *offset); } // 7. Allocate closure cell: (table_idx: i32, env_ptr: i32) @@ -2304,7 +2421,7 @@ impl Codegen { // Direct call to an extern import (phase 2B-ii of #43). // Extern fns are wasm imports — their index lives in // `extern_fn_indices` after `collect_extern_imports` runs. - if let Some(&(import_idx, returns_unit)) = self.extern_fn_indices.get(head) { + if let Some(&(import_idx, wasm_result)) = self.extern_fn_indices.get(head) { // A lone synthetic `()` is the nullary-call placeholder // (`f()` → `App(f, ())`); push no args for it. Otherwise // push every real arg in order. @@ -2322,7 +2439,7 @@ impl Codegen { // no WebAssembly result. Reconstitute the language value so // the enclosing expression has the stack shape its caller // expects. - if returns_unit { + if wasm_result.is_none() { func.instruction(&Instruction::I32Const(0)); } return; @@ -3093,6 +3210,58 @@ fn mem_arg(offset: u64) -> wasm_encoder::MemArg { } } +/// Size, byte alignment, and WebAssembly alignment exponent for a captured +/// scalar value. Ephapax's current runtime representation reaches this helper +/// only with numeric scalar types and i32 handles. +fn valtype_storage(ty: ValType) -> (u64, u64, u32) { + match ty { + ValType::I64 | ValType::F64 => (8, 8, 3), + _ => (4, 4, 2), + } +} + +fn align_up(offset: u64, alignment: u64) -> u64 { + (offset + alignment - 1) & !(alignment - 1) +} + +fn typed_mem_arg(ty: ValType, offset: u64) -> wasm_encoder::MemArg { + let (_, _, align) = valtype_storage(ty); + wasm_encoder::MemArg { + offset, + align, + memory_index: 0, + } +} + +fn emit_typed_zero(func: &mut Function, ty: ValType) { + match ty { + ValType::I64 => func.instruction(&Instruction::I64Const(0)), + ValType::F32 => func.instruction(&Instruction::F32Const(0.0)), + ValType::F64 => func.instruction(&Instruction::F64Const(0.0)), + _ => func.instruction(&Instruction::I32Const(0)), + }; +} + +fn emit_typed_store(func: &mut Function, ty: ValType, offset: u64) { + let arg = typed_mem_arg(ty, offset); + match ty { + ValType::I64 => func.instruction(&Instruction::I64Store(arg)), + ValType::F32 => func.instruction(&Instruction::F32Store(arg)), + ValType::F64 => func.instruction(&Instruction::F64Store(arg)), + _ => func.instruction(&Instruction::I32Store(arg)), + }; +} + +fn emit_typed_load(func: &mut Function, ty: ValType, offset: u64) { + let arg = typed_mem_arg(ty, offset); + match ty { + ValType::I64 => func.instruction(&Instruction::I64Load(arg)), + ValType::F32 => func.instruction(&Instruction::F32Load(arg)), + ValType::F64 => func.instruction(&Instruction::F64Load(arg)), + _ => func.instruction(&Instruction::I32Load(arg)), + }; +} + // --------------------------------------------------------------------------- // Type mapping: Ephapax Ty -> WASM ValType // --------------------------------------------------------------------------- @@ -4505,7 +4674,7 @@ mod tests { codegen.collect_extern_imports(&module); assert_eq!( codegen.extern_fn_indices.get("do_thing").copied(), - Some((NUM_BUILTIN_IMPORTS, false)), + Some((NUM_BUILTIN_IMPORTS, Some(ValType::I32))), "first extern fn must occupy import slot 2 (right after the 2 builtin imports)" ); } @@ -4550,7 +4719,75 @@ mod tests { /// result is stored and passed to another host import. #[test] fn annotated_i64_let_uses_i64_wasm_local() { + let module = i64_extern_let_module(Some(Ty::Base(BaseTy::I64))); + let wasm = compile_module(&module).expect("module must compile"); + validate_wasm(&wasm); + } + + /// Inferred let types are not written back into the AST, so codegen must + /// recover an extern call's result representation rather than defaulting + /// every unannotated binding to i32. + #[test] + fn unannotated_i64_extern_result_infers_i64_wasm_local() { + let module = i64_extern_let_module(None); + let wasm = compile_module(&module).expect("module must compile"); + validate_wasm(&wasm); + } + + /// Closure environments must preserve captured scalar widths. An i64 + /// captured into an i32-only slot produces invalid loads/local sets in the + /// generated lambda body. + #[test] + fn lambda_capture_preserves_i64_type_and_layout() { let module = AstModule { + name: "test".into(), + imports: vec![], + decls: vec![ + Decl::Extern { + abi: "host".to_string(), + items: vec![ExternItem::Fn { + name: "i64_is_zero".into(), + params: vec![("value".into(), Ty::Base(BaseTy::I64))], + ret_ty: Ty::Base(BaseTy::I32), + }], + }, + Decl::Fn { + name: "entry".into(), + visibility: Visibility::Private, + type_params: vec![], + params: vec![], + ret_ty: Ty::Base(BaseTy::I32), + body: e(ExprKind::Let { + name: "token".into(), + ty: None, + value: Box::new(e(ExprKind::Lit(Literal::I64(5)))), + body: Box::new(e(ExprKind::Let { + name: "check".into(), + ty: None, + value: Box::new(e(ExprKind::Lambda { + param: "unused".into(), + param_ty: Ty::Base(BaseTy::I32), + body: Box::new(e(ExprKind::App { + func: Box::new(e(ExprKind::Var("i64_is_zero".into()))), + arg: Box::new(e(ExprKind::Var("token".into()))), + })), + })), + body: Box::new(e(ExprKind::App { + func: Box::new(e(ExprKind::Var("check".into()))), + arg: Box::new(e(ExprKind::Lit(Literal::I32(0)))), + })), + })), + }), + }, + ], + }; + + let wasm = compile_module(&module).expect("module must compile"); + validate_wasm(&wasm); + } + + fn i64_extern_let_module(annotation: Option) -> AstModule { + AstModule { name: "test".into(), imports: vec![], decls: vec![ @@ -4577,7 +4814,7 @@ mod tests { ret_ty: Ty::Base(BaseTy::I32), body: e(ExprKind::Let { name: "token".into(), - ty: Some(Ty::Base(BaseTy::I64)), + ty: annotation, value: Box::new(e(ExprKind::App { func: Box::new(e(ExprKind::Var("cap_token".into()))), arg: Box::new(e(ExprKind::Lit(Literal::I32(0)))), @@ -4589,10 +4826,7 @@ mod tests { }), }, ], - }; - - let wasm = compile_module(&module).expect("module must compile"); - validate_wasm(&wasm); + } } // ----------------------------------------------------------------------- From a05fe71261c8767c5021515c43f21ad777eec9a0 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Sat, 29 Aug 2026 13:35:57 +0100 Subject: [PATCH 3/6] perf(wasm): group adjacent local declarations --- src/ephapax-wasm/src/lib.rs | 39 ++++++++++++++++++++++++++----------- 1 file changed, 28 insertions(+), 11 deletions(-) diff --git a/src/ephapax-wasm/src/lib.rs b/src/ephapax-wasm/src/lib.rs index 086c168..8ad8e9a 100644 --- a/src/ephapax-wasm/src/lib.rs +++ b/src/ephapax-wasm/src/lib.rs @@ -304,18 +304,21 @@ impl LocalTracker { } /// Total number of extra (non-parameter) locals needed. - fn num_extra_locals(&self, num_params: u32) -> u32 { - self.next_idx.saturating_sub(num_params) + fn num_extra_locals(&self) -> u32 { + self.extra_local_types.len() as u32 } /// Declarations for `wasm_encoder::Function::new`, preserving local /// index order across mixed-width Ephapax bindings. fn wasm_local_declarations(&self) -> Vec<(u32, ValType)> { - self.extra_local_types - .iter() - .copied() - .map(|ty| (1, ty)) - .collect() + let mut declarations: Vec<(u32, ValType)> = Vec::new(); + for ty in &self.extra_local_types { + match declarations.last_mut() { + Some((count, previous_ty)) if previous_ty == ty => *count += 1, + _ => declarations.push((1, *ty)), + } + } + declarations } } @@ -1165,7 +1168,7 @@ impl Codegen { let mut dummy_func = Function::new(vec![(64, ValType::I32)]); // generous self.compile_expr(&mut dummy_func, body); - let extra = self.locals.num_extra_locals(num_params); + let extra = self.locals.num_extra_locals(); let local_declarations = self.locals.wasm_local_declarations(); // Restore data state @@ -1184,7 +1187,14 @@ impl Codegen { } } - debug_assert_eq!(extra as usize, local_declarations.len()); + debug_assert_eq!( + extra, + local_declarations + .iter() + .map(|(count, _)| count) + .copied() + .sum::() + ); let mut func = Function::new(local_declarations); self.compile_expr(&mut func, body); @@ -1272,7 +1282,7 @@ impl Codegen { } self.compile_expr(&mut dummy_func, &lambda_info.body); - let extra = self.locals.num_extra_locals(num_params); + let extra = self.locals.num_extra_locals(); let local_declarations = self.locals.wasm_local_declarations(); // Restore data state @@ -1303,7 +1313,14 @@ impl Codegen { self.locals.bind_typed(captured_name, false, *captured_type); } - debug_assert_eq!(extra as usize, local_declarations.len()); + debug_assert_eq!( + extra, + local_declarations + .iter() + .map(|(count, _)| count) + .copied() + .sum::() + ); let mut func = Function::new(local_declarations); // Load captured variables from env_ptr into local slots From 90381a811ddfe5ff7e35be1802ba8516bf56cc88 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Sat, 29 Aug 2026 13:57:47 +0100 Subject: [PATCH 4/6] docs(proofs): publish current trust boundaries --- docs/proof-debt.adoc | 78 +++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 77 insertions(+), 1 deletion(-) diff --git a/docs/proof-debt.adoc b/docs/proof-debt.adoc index 6ee342f..d942813 100644 --- a/docs/proof-debt.adoc +++ b/docs/proof-debt.adoc @@ -1,7 +1,83 @@ Copyright (c) Jonathan D.A. Jewell j.d.a.jewell@open.ac.uk SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) –> -== Proof Debt — ephapax (SUPERSEDED — archaeology only) +== Proof Debt — ephapax + +=== Current enforced inventory (2026-08-29) + +This section is the current inventory consumed by the trusted-base gate. The +older closure plan below is retained only as labelled archaeology. A path being +listed here means that its trust boundary is documented; it does *not* mean the +obligation has been discharged. + +==== `+formal/Semantics.v:9258+` — legacy `+preservation+` + +* *Status*: one real outer `+Admitted.+`; not proved. +* *Classification*: durable legacy counterexample boundary. The theorem as + originally stated is false, as demonstrated by the five `+Qed+` witnesses in + `+formal/Counterexample.v+`. It must not be presented as closable proof debt + without first replacing the false statement. +* *Owner*: @hyperpolymath. +* *Acceptance*: retain the counterexample regression and publish any replacement + theorem with its exact restricted boundary and zero hidden escape hatches. + +==== `+formal/Semantics_L1.v:3318+` — `+step_pop_disjoint_from_type_l1+` + +* *Status*: one internal `+admit.+` followed by one outer `+Admitted.+`; not + proved. +* *Obligation*: establish region-count coherence when a congruence step exits a + region still required by a sibling's type. Ten former sub-cases are closed; + this is the one residual case. +* *Obstacle*: the snapshot region environment and result type do not encode the + temporal distinction needed to show that the sibling's occurrence survives + the exit. The choreographic experiment in + `+formal/L1-ELIMINATOR-FORK.adoc+` showed that the first proposed formulation + relocates this obligation rather than discharging it. +* *Owner*: @hyperpolymath. +* *Plan and tracking*: continue the staged calculus work in issues #240, #241, + and #242; first require a coherent minimal counterexample/positive control, + then prove the supporting lemma without circularly assuming preservation. +* *Acceptance*: `+Qed.+`, a clean `+Print Assumptions + step_pop_disjoint_from_type_l1.+`, and a regression showing that an invalid + region exit is rejected. + +==== `+formal/Semantics_L1.v:3337+` — `+preservation_l1+` + +* *Status*: one internal `+admit.+` followed by one outer `+Admitted.+`; not + proved. +* *Dependency*: blocked by `+step_pop_disjoint_from_type_l1+` and the staged L2 + restrictions tracked in issues #240, #241, and #242. +* *Owner*: @hyperpolymath. +* *Acceptance*: the theorem ends in `+Qed.+`, `+Print Assumptions + preservation_l1.+` reports no project escape hatch, and the complete Coq + build plus counterexample suite passes. + +==== `+idris2/src/Main.idr:22+` — global `+%default partial+` + +* *Status*: real module-wide Idris2 totality waiver; configured and compiled, + but neither totality-audited nor proved. +* *Scope*: the affine front-end executable, including argument parsing, file + I/O orchestration, parser invocation, type checking, and emission. +* *Owner*: @hyperpolymath. +* *Plan and tracking*: issue #380. Audit each definition under + `+%default total+`; keep any unavoidable partiality narrowly attached to the + smallest I/O boundary with a stated precondition and failure result. This is + part of the Idris2 ABI trust boundary, so a global waiver is not an acceptable + final state. +* *Acceptance*: a negative control demonstrates that Idris2 rejects a deliberately + non-total pure definition; the module builds under total-by-default checking; + every remaining local `+partial+` is individually documented and gated. + +=== Rust/Creusot verification boundary + +Ephapax contains proof-critical Rust but currently has no Creusot integration, +contracts, reproducible solver setup, or hard verification gate. Issue #378 is +the canonical closure record. Rust tests, Coq bridge tests, and typed-Wasm checks +are valuable evidence, but they do not imply that Creusot obligations were +generated or discharged. Until #378 is completed with its required failing +positive control, the Rust implementation is *tested, not Creusot-proved*. + +=== Archived 2026-05-26 inventory (superseded) ____ === 🛑 SUPERSEDED From 4f471ab9b9302c426c4de4e6e9bb05e3f051579e Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Sat, 29 Aug 2026 14:00:39 +0100 Subject: [PATCH 5/6] ci: pin repaired Standards governance --- .github/workflows/governance.yml | 2 +- .github/workflows/hypatia-scan.yml | 2 +- .github/workflows/mirror.yml | 2 +- .github/workflows/rust-ci.yml | 2 +- .github/workflows/scorecard.yml | 2 +- .github/workflows/secret-scanner.yml | 2 +- 6 files changed, 6 insertions(+), 6 deletions(-) diff --git a/.github/workflows/governance.yml b/.github/workflows/governance.yml index f33964f..6455f45 100644 --- a/.github/workflows/governance.yml +++ b/.github/workflows/governance.yml @@ -15,4 +15,4 @@ permissions: jobs: governance: - uses: hyperpolymath/standards/.github/workflows/governance-reusable.yml@84355587cb2a1f86e6882de83514a32db2646e7a + uses: hyperpolymath/standards/.github/workflows/governance-reusable.yml@6b38eb50104901e2fec80f9455a972bc3eced813 diff --git a/.github/workflows/hypatia-scan.yml b/.github/workflows/hypatia-scan.yml index f684ec7..52662fa 100644 --- a/.github/workflows/hypatia-scan.yml +++ b/.github/workflows/hypatia-scan.yml @@ -18,4 +18,4 @@ permissions: jobs: scan: - uses: hyperpolymath/standards/.github/workflows/hypatia-scan-reusable.yml@84355587cb2a1f86e6882de83514a32db2646e7a + uses: hyperpolymath/standards/.github/workflows/hypatia-scan-reusable.yml@6b38eb50104901e2fec80f9455a972bc3eced813 diff --git a/.github/workflows/mirror.yml b/.github/workflows/mirror.yml index d4ac835..3fe9bb8 100644 --- a/.github/workflows/mirror.yml +++ b/.github/workflows/mirror.yml @@ -13,5 +13,5 @@ permissions: jobs: mirror: - uses: hyperpolymath/standards/.github/workflows/mirror-reusable.yml@84355587cb2a1f86e6882de83514a32db2646e7a + uses: hyperpolymath/standards/.github/workflows/mirror-reusable.yml@6b38eb50104901e2fec80f9455a972bc3eced813 secrets: inherit diff --git a/.github/workflows/rust-ci.yml b/.github/workflows/rust-ci.yml index 28e60bb..3a8d198 100644 --- a/.github/workflows/rust-ci.yml +++ b/.github/workflows/rust-ci.yml @@ -31,7 +31,7 @@ concurrency: jobs: rust-ci: - uses: hyperpolymath/standards/.github/workflows/rust-ci-reusable.yml@84355587cb2a1f86e6882de83514a32db2646e7a + uses: hyperpolymath/standards/.github/workflows/rust-ci-reusable.yml@6b38eb50104901e2fec80f9455a972bc3eced813 no-default-features: name: Cargo build + test (ephapax-cli, --no-default-features) diff --git a/.github/workflows/scorecard.yml b/.github/workflows/scorecard.yml index b1b1fd8..9fd37c8 100644 --- a/.github/workflows/scorecard.yml +++ b/.github/workflows/scorecard.yml @@ -17,4 +17,4 @@ jobs: contents: read security-events: write id-token: write - uses: hyperpolymath/standards/.github/workflows/scorecard-reusable.yml@84355587cb2a1f86e6882de83514a32db2646e7a + uses: hyperpolymath/standards/.github/workflows/scorecard-reusable.yml@6b38eb50104901e2fec80f9455a972bc3eced813 diff --git a/.github/workflows/secret-scanner.yml b/.github/workflows/secret-scanner.yml index f129fbd..29c25f1 100644 --- a/.github/workflows/secret-scanner.yml +++ b/.github/workflows/secret-scanner.yml @@ -21,5 +21,5 @@ jobs: contents: read pull-requests: write actions: read - uses: hyperpolymath/standards/.github/workflows/secret-scanner-reusable.yml@84355587cb2a1f86e6882de83514a32db2646e7a + uses: hyperpolymath/standards/.github/workflows/secret-scanner-reusable.yml@6b38eb50104901e2fec80f9455a972bc3eced813 secrets: inherit From 318e28e7b58e5a5993d7ea27eb86542535e27572 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Sat, 29 Aug 2026 14:14:30 +0100 Subject: [PATCH 6/6] fix(governance): reconcile policy and action locks --- .github/workflows/actions.lock | 22 +++++++++++----------- .github/workflows/instant-sync.yml | 8 ++++++-- CLAUDE.md | 4 +--- 3 files changed, 18 insertions(+), 16 deletions(-) diff --git a/.github/workflows/actions.lock b/.github/workflows/actions.lock index 4e32038..841130e 100644 --- a/.github/workflows/actions.lock +++ b/.github/workflows/actions.lock @@ -3,13 +3,6 @@ # Docs: https://gh.io/actions-lockfile version: 'v0.0.2' workflows: - '.github/workflows/governance.yml': [] - '.github/workflows/hypatia-scan.yml': [] - '.github/workflows/label-triage.yml': [] - '.github/workflows/labels.yml': [] - '.github/workflows/mirror.yml': [] - '.github/workflows/scorecard.yml': [] - '.github/workflows/secret-scanner.yml': [] '.github/workflows/abi-verify.yml': - 'actions/checkout@v7.0.1' '.github/workflows/codeql.yml': @@ -20,14 +13,21 @@ workflows: '.github/workflows/ffi-seams.yml': - 'actions/checkout@v7.0.1' - 'mlugg/setup-zig@v2.2.1' + '.github/workflows/governance.yml': [] + '.github/workflows/hypatia-scan.yml': [] '.github/workflows/instant-sync.yml': - 'peter-evans/repository-dispatch@v4.0.1' + '.github/workflows/label-triage.yml': [] + '.github/workflows/labels.yml': [] + '.github/workflows/mirror.yml': [] '.github/workflows/push-email-notify.yml': - - 'dawidd6/action-send-mail@v3.12.0' + - 'dawidd6/action-send-mail@v18' '.github/workflows/rust-ci.yml': - 'actions/checkout@v7.0.1' - 'dtolnay/rust-toolchain@v1' - 'swatinem/rust-cache@v2.9.2' + '.github/workflows/scorecard.yml': [] + '.github/workflows/secret-scanner.yml': [] '.github/workflows/status-gate.yml': - 'actions/checkout@v7.0.1' - 'dtolnay/rust-toolchain@v1' @@ -38,9 +38,9 @@ dependencies: commit: 'sha1-3d3c42e5aac5ba805825da76410c181273ba90b1' owner_id: 44036562 repo_id: 197814629 - 'dawidd6/action-send-mail@v3.12.0': - ref: 'v3.12.0' - commit: 'sha1-0bbdab096651ee93f37ec02383e088183d41ff0b' + 'dawidd6/action-send-mail@v18': + ref: 'v18' + commit: 'sha1-94de994a9f6fffee200243214e17002e2920bb59' owner_id: 9713907 repo_id: 222439721 'dtolnay/rust-toolchain@v1': diff --git a/.github/workflows/instant-sync.yml b/.github/workflows/instant-sync.yml index c7ba288..244e239 100644 --- a/.github/workflows/instant-sync.yml +++ b/.github/workflows/instant-sync.yml @@ -22,10 +22,13 @@ jobs: timeout-minutes: 5 steps: - name: Trigger Propagation - if: ${{ secrets.FARM_DISPATCH_TOKEN != '' }} + id: propagate + if: ${{ env.FARM_DISPATCH_TOKEN != '' }} uses: peter-evans/repository-dispatch@v4.0.1 + env: + FARM_DISPATCH_TOKEN: ${{ secrets.FARM_DISPATCH_TOKEN }} with: - token: ${{ secrets.FARM_DISPATCH_TOKEN }} + token: ${{ env.FARM_DISPATCH_TOKEN }} repository: hyperpolymath/.git-private-farm event-type: propagate client-payload: |- @@ -37,6 +40,7 @@ jobs: } - name: Confirm + if: ${{ steps.propagate.outcome == 'success' }} run: echo "::notice::Propagation triggered for ${{ github.event.repository.name }}" - name: K9-SVC Validation diff --git a/CLAUDE.md b/CLAUDE.md index b202515..cf6a7a4 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -1,7 +1,5 @@ - - @@ -11,7 +9,7 @@ **This repo is `hyperpolymath/ephapax`.** It is **NOT** `hyperpolymath/affinescript`. -| | This repo | NOT this repo | +| Criterion | This repo | NOT this repo | |---|---|---| | Name | **Ephapax** | AffineScript | | Path | `hyperpolymath/ephapax` | `hyperpolymath/affinescript` |