@@ -1625,6 +1625,29 @@ pub fn eval_pure_to_bool(source: &str) -> Option<bool> {
16251625 .unwrap_or_default()
16261626}
16271627
1628+/// One step in a path from a `base.compile` result's top-level value down to a
1629+/// value that must satisfy a host refined-type predicate.
1630+#[derive(Clone, Debug, PartialEq, Eq)]
1631+enum RefinePathStep {
1632+ /// Descend into a record field (records carry their named fields;
1633+ /// constructor payloads delegate to `.value` first).
1634+ RecordField(String),
1635+ /// The value is a relation (`[T]`): every element continues along the
1636+ /// remaining path.
1637+ Relation,
1638+ /// The value is a `Maybe`: `Nothing` carries no refined scalar (skip),
1639+ /// `Just` unwraps to its payload and continues.
1640+ Maybe,
1641+}
1642+
1643+/// A leaf of a `base.compile` expected type that is a host-refined type,
1644+/// paired with the path that reaches a value of that type at runtime.
1645+#[derive(Clone, Debug)]
1646+struct RefinePath {
1647+ refined_name: String,
1648+ steps: Vec<RefinePathStep>,
1649+}
1650+
16281651impl<M: cranelift_module::Module> Codegen<M> {
16291652 /// Build a `Codegen` around an already-constructed module. Backend-agnostic:
16301653 /// the ISA/unwind setup is the same for `ObjectModule` (AOT) and `JITModule`.
@@ -7517,18 +7540,15 @@ ast::ExprKind::Atomic(inner) => {
75177540 // subsumption knows refined types only by NAME (their
75187541 // predicates never cross the wire), so a snippet could
75197542 // redeclare `type Port = Int where \_ -> True` and slip a value
7520− // past the name check. When the expected type is a HOST-refined
7521− // type, validate the returned value against the host's own
7522− // predicate chain and swap `Ok` → refinement `Err` on violation.
7523− if let Some(refined_name) = self.refined_expected_type_name(&expected) {
7524− let is_maybe = expected.trim_start().starts_with("Maybe ");
7525− return self.emit_compile_result_refinement_check(
7526− builder,
7527− result,
7528− &refined_name,
7529− is_maybe,
7530− env,
7531− db,
7543+ // past the name check. Validate the returned value against the
7544+ // host's own predicate chain at EVERY host-refined occurrence
7545+ // in the expected type — top-level or nested in a record,
7546+ // relation, or `Maybe` — swapping `Ok` → refinement `Err` on
7547+ // any violation.
7548+ let paths = self.collect_refine_paths(&expected);
7549+ if !paths.is_empty() {
7550+ return self.emit_compile_result_refinement_check_paths(
7551+ builder, result, &paths, env, db,
75327552 );
75337553 }
75347554 return result;
@@ -13635,86 +13655,254 @@ ast::ExprKind::Atomic(inner) => {
1363513655 builder.seal_block(done_block);
1363613656 }
1363713657
13638− /// If `expected` (a compile-expected type source string) denotes a
13639− /// HOST-refined type — `Port` or `Maybe Port` where `Port` is a refined
13640− /// alias the host declared — return its name. This is the trigger for the
13641− /// host-side predicate check on a `base.compile` result: the JIT only
13642− /// knows refined types by NAME (their predicates never cross the wire),
13643− /// so the host must validate the returned value against its own
13644− /// predicate. Only the top-level / top-level-`Maybe` case is handled —
13645− /// refined types nested in records, relations, or function types are not
13646− /// checked here.
13647− fn refined_expected_type_name(&self, expected: &str) -> Option<String> {
13648− let trimmed = expected.trim();
13649− let inner = trimmed
13650− .strip_prefix("Maybe ")
13651− .map(str::trim)
13652− .unwrap_or(trimmed);
13653− // A bare type name (single token) that the host registered as refined.
13654− if !inner.is_empty()
13655− && inner.chars().all(|c| c.is_alphanumeric() || c == '_')
13656− && self.refined_types.contains_key(inner)
13657− {
13658− Some(inner.to_string())
13659− } else {
13660− None
13658+ /// Collect the conjoined predicate chain for a host-refined type
13659+ /// (`type Age = Nat where …` checks `Nat`'s predicates too). Walks the AST
13660+ /// alias map (`alias_ast`): a refined alias's base is the AST type it
13661+ /// wraps, so stepping through `TypeKind::Named` bases visits each stacked
13662+ /// refinement. Empty when `type_name` is not (or does not resolve through)
13663+ /// a host refinement.
13664+ fn refined_predicate_chain(&self, type_name: &str) -> Vec<ast::Expr> {
13665+ let mut preds: Vec<ast::Expr> = Vec::new();
13666+ let mut cur: String = type_name.to_string();
13667+ loop {
13668+ let Some(pred) = self.refined_types.get(&cur) else {
13669+ break;
13670+ };
13671+ preds.push(pred.clone());
13672+ let Some(ast_ty) = self.alias_ast.get(&cur) else {
13673+ break;
13674+ };
13675+ let ast::TypeKind::Refined { base, .. } = &ast_ty.node else {
13676+ break;
13677+ };
13678+ let ast::TypeKind::Named(n) = &base.node else {
13679+ break;
13680+ };
13681+ cur = n.clone();
13682+ }
13683+ preds
13684+ }
13685+
13686+ /// Collect the host-refined occurrences in an expected-type string as
13687+ /// validation paths. The string is rendered by `display_ty_wire` so it
13688+ /// re-parses via `parse_type_str`; the resulting `Type` AST is walked for
13689+ /// `Named` leaves the host registered as refined, recording how to reach
13690+ /// each at runtime. Anything not statically resolvable to a refined scalar
13691+ /// — function types, non-refined ADTs, type variables, opaque structures —
13692+ /// yields no path (the value is accepted unchecked there).
13693+ fn collect_refine_paths(&self, expected: &str) -> Vec<RefinePath> {
13694+ let Some(ast_ty) = knot::parser::parse_type_str(expected) else {
13695+ return Vec::new();
13696+ };
13697+ let mut out = Vec::new();
13698+ let mut steps = Vec::new();
13699+ let mut depth = 0usize;
13700+ self.walk_refine_paths(&ast_ty, &mut steps, &mut out, &mut depth);
13701+ out
13702+ }
13703+
13704+ /// Walk a parsed expected type, accumulating `steps` to each host-refined
13705+ /// leaf. `depth` bounds recursion so a pathological (deeply nested or
13706+ /// cyclic-alias) type cannot overflow the stack; beyond it the walker
13707+ /// conservatively stops (that subtree is unchecked).
13708+ fn walk_refine_paths(
13709+ &self,
13710+ ty: &ast::Type,
13711+ steps: &mut Vec<RefinePathStep>,
13712+ out: &mut Vec<RefinePath>,
13713+ depth: &mut usize,
13714+ ) {
13715+ const MAX_DEPTH: usize = 32;
13716+ if *depth >= MAX_DEPTH {
13717+ return;
13718+ }
13719+ match &ty.node {
13720+ ast::TypeKind::Named(n) => {
13721+ if self.refined_types.contains_key(n) {
13722+ out.push(RefinePath {
13723+ refined_name: n.clone(),
13724+ steps: steps.clone(),
13725+ });
13726+ }
13727+ // A non-refined named type is either a primitive, an alias the
13728+ // wire already resolved, or an ADT/record name — none of which
13729+ // the walker can statically descend into here.
13730+ }
13731+ ast::TypeKind::Record { fields, .. } => {
13732+ for f in fields {
13733+ let name = f.name.clone();
13734+ if name.is_empty() {
13735+ continue;
13736+ }
13737+ steps.push(RefinePathStep::RecordField(name));
13738+ *depth += 1;
13739+ self.walk_refine_paths(&f.value, steps, out, depth);
13740+ *depth -= 1;
13741+ steps.pop();
13742+ }
13743+ }
13744+ ast::TypeKind::Relation(inner) => {
13745+ steps.push(RefinePathStep::Relation);
13746+ *depth += 1;
13747+ self.walk_refine_paths(inner, steps, out, depth);
13748+ *depth -= 1;
13749+ steps.pop();
13750+ }
13751+ // `Maybe x`: the wrapped value is `Nothing {}` (skip) or
13752+ // `Just {value}` (continue). Only the single-argument form is a
13753+ // Maybe; anything else is an opaque application.
13754+ ast::TypeKind::App { func, arg }
13755+ if matches!(&func.node, ast::TypeKind::Named(n) if n == "Maybe") =>
13756+ {
13757+ steps.push(RefinePathStep::Maybe);
13758+ *depth += 1;
13759+ self.walk_refine_paths(arg, steps, out, depth);
13760+ *depth -= 1;
13761+ steps.pop();
13762+ }
13763+ // `IO x` / `Assoc n x`-style single wrappers the wire renders as an
13764+ // application: descend so a refined leaf under them is still found.
13765+ ast::TypeKind::App { func, arg }
13766+ if matches!(&func.node, ast::TypeKind::Named(n) if n == "IO") =>
13767+ {
13768+ *depth += 1;
13769+ self.walk_refine_paths(arg, steps, out, depth);
13770+ *depth -= 1;
13771+ }
13772+ // A refined type used INLINE in an annotation (`Nat \x -> …`) has no
13773+ // host registry entry by name; only named host refinements are
13774+ // gated, so there is nothing to collect from a `Refined` node.
13775+ _ => {}
1366113776 }
1366213777 }
1366313778
13664− /// Wrap a `base.compile` typed result (`Result Text a`) with a host-side
13665− /// refinement check: when the result is `Ok`, run the host's OWN predicate
13666− /// chain for `type_name` against the returned value, swapping to a
13667− /// refinement `Err` on violation. `Err` results pass through untouched.
13779+ /// Walk the runtime value `val` along a refinement path, folding the
13780+ /// all-predicates-passed flag `ok` (an I32 0/1). At each refined leaf the
13781+ /// type's predicate chain runs against the value; intermediate steps
13782+ /// navigate the value: record fields are extracted, `Just` is unwrapped
13783+ /// (`Nothing` skips), and a relation loops over every element. Returns the
13784+ /// AND of `ok` with every predicate verdict reached along the path.
13785+ fn emit_refine_walk(
13786+ &mut self,
13787+ builder: &mut FunctionBuilder,
13788+ val: Value,
13789+ steps: &[RefinePathStep],
13790+ refined_name: &str,
13791+ ok: Value,
13792+ env: &mut Env,
13793+ db: Value,
13794+ ) -> Value {
13795+ match steps.split_first() {
13796+ // Leaf: run the conjoined predicate chain against `val`.
13797+ None => {
13798+ let preds = self.refined_predicate_chain(refined_name);
13799+ let mut acc = ok;
13800+ for pred in &preds {
13801+ let pred_fn = self.compile_expr(builder, pred, env, db);
13802+ let res = self.call_rt(builder, "knot_value_call", &[db, pred_fn, val]);
13803+ let pred_ok =
13804+ self.call_rt_typed(builder, "knot_value_get_bool", &[res], types::I32);
13805+ acc = builder.ins().band(acc, pred_ok);
13806+ }
13807+ acc
13808+ }
13809+ Some((RefinePathStep::RecordField(name), rest)) => {
13810+ let (p, l) = self.string_ptr(builder, name);
13811+ let field = self.call_rt(builder, "knot_record_field", &[val, p, l]);
13812+ self.emit_refine_walk(builder, field, rest, refined_name, ok, env, db)
13813+ }
13814+ Some((RefinePathStep::Maybe, rest)) => {
13815+ // `Nothing {}` carries no refined scalar — skip (pass `ok`
13816+ // through). `Just {value}` unwraps to its payload, which the
13817+ // rest of the path checks. Both arms merge the resulting flag.
13818+ let unwrapped = self.call_rt(builder, "knot_override_unwrap_just", &[val]);
13819+ let present = builder.ins().icmp_imm(IntCC::NotEqual, unwrapped, 0);
13820+ let run_block = builder.create_block();
13821+ let done_block = builder.create_block();
13822+ builder.append_block_param(done_block, types::I32);
13823+ builder.ins().brif(present, run_block, &[], done_block, &[ok.into()]);
13824+ builder.switch_to_block(run_block);
13825+ builder.seal_block(run_block);
13826+ let checked =
13827+ self.emit_refine_walk(builder, unwrapped, rest, refined_name, ok, env, db);
13828+ builder.ins().jump(done_block, &[checked.into()]);
13829+ builder.switch_to_block(done_block);
13830+ builder.seal_block(done_block);
13831+ builder.block_params(done_block)[0]
13832+ }
13833+ Some((RefinePathStep::Relation, rest)) => {
13834+ // Loop over every element; each continues along `rest`. The
13835+ // loop has a back-edge, so the index AND the running flag ride
13836+ // header block parameters (a plain variable can't — its
13837+ // reassignment in the body is read at the header, a cycle).
13838+ let len = self.call_rt_typed(builder, "knot_relation_len", &[val], types::I64);
13839+ let head = builder.create_block();
13840+ let idx_p = builder.append_block_param(head, types::I64);
13841+ let ok_p = builder.append_block_param(head, types::I32);
13842+ let body = builder.create_block();
13843+ let after = builder.create_block();
13844+ builder.append_block_param(after, types::I32);
13845+ let zero = builder.ins().iconst(types::I64, 0);
13846+ builder.ins().jump(head, &[zero.into(), ok.into()]);
13847+ builder.switch_to_block(head);
13848+ // `icmp` yields an i8 boolean; zero-extend to i32 to AND with
13849+ // the running flag (so the loop short-circuits once a
13850+ // predicate fails).
13851+ let in_bounds_i8 = builder.ins().icmp(IntCC::UnsignedLessThan, idx_p, len);
13852+ let in_bounds = builder.ins().uextend(types::I32, in_bounds_i8);
13853+ let keep_going = builder.ins().band(in_bounds, ok_p);
13854+ builder
13855+ .ins()
13856+ .brif(keep_going, body, &[], after, &[ok_p.into()]);
13857+ builder.switch_to_block(body);
13858+ builder.seal_block(body);
13859+ let elem = self.call_rt(builder, "knot_relation_get", &[val, idx_p]);
13860+ let ok_next =
13861+ self.emit_refine_walk(builder, elem, rest, refined_name, ok_p, env, db);
13862+ let i_next = builder.ins().iadd_imm(idx_p, 1);
13863+ builder.ins().jump(head, &[i_next.into(), ok_next.into()]);
13864+ builder.seal_block(head);
13865+ builder.switch_to_block(after);
13866+ builder.seal_block(after);
13867+ builder.block_params(after)[0]
13868+ }
13869+ }
13870+ }
13871+
13872+ /// Gate a `base.compile` result on every host-refined occurrence in the
13873+ /// expected type, reached via `paths`. When the result is `Ok` its `value`
13874+ /// is walked along each path, running the host's predicate chain at every
13875+ /// refined leaf (descending record fields, unwrapping `Just`, iterating
13876+ /// relation elements); any violation swaps `Ok` → a refinement `Err`.
13877+ /// `Err` passes through untouched.
1366813878 ///
13669− /// Why: the JIT enforcing the compile-expected subsumption knows refined
13670− /// types only by NAME — the predicate is not transmitted — so a snippet
13671− /// could redeclare `type Port = Int where \_ -> True` and pass. Running
13672− /// the host's predicate here closes that hole (Option B): the JIT's
13673− /// subsumption still rejects a bare base-typed value, and the host
13674− /// predicate is the authoritative gate on whatever refined value the
13675− /// snippet produced.
13676− fn emit_compile_result_refinement_check(
13879+ /// A bare top-level refined type yields a single `[leaf]` path; the nested
13880+ /// cases (records, relations, `Maybe`) carry non-trivial steps.
13881+ fn emit_compile_result_refinement_check_paths(
1367713882 &mut self,
1367813883 builder: &mut FunctionBuilder,
1367913884 result: Value,
13680− type_name: &str,
13681− is_maybe: bool,
13885+ paths: &[RefinePath],
1368213886 env: &mut Env,
1368313887 db: Value,
1368413888 ) -> Value {
13685− // Collect the conjoined predicate chain (stacked refinements), the
13686− // same walk `emit_refined_override_check` performs.
13687− let mut preds: Vec<ast::Expr> = Vec::new();
13688− let mut cur: String = type_name.to_string();
13689− loop {
13690− let Some(pred) = self.refined_types.get(&cur) else { break };
13691− preds.push(pred.clone());
13692− let Some(ast_ty) = self.alias_ast.get(&cur) else { break };
13693− let ast::TypeKind::Refined { base, .. } = &ast_ty.node else {
13694− break;
13695− };
13696− let ast::TypeKind::Named(n) = &base.node else { break };
13697− cur = n.clone();
13698− }
13699− if preds.is_empty() {
13889+ if paths.is_empty() {
1370013890 return result;
1370113891 }
1370213892
1370313893 // Split on the Result tag: `Err` bypasses the check; `Ok` unwraps its
13704− // `value` and runs the predicates. Merge yields the (possibly swapped)
13705− // result.
13894+ // `value` and walks every path.
1370613895 let merge_block = builder.create_block();
1370713896 builder.append_block_param(merge_block, self.ptr_type);
1370813897 let ok_block = builder.create_block();
13709− let (ok_tag_ptr, ok_tag_len) = self.string_ptr(builder, "Ok");
13710− let is_ok =
13711− self.call_rt_typed(
13712− builder,
13713− "knot_constructor_matches",
13714− &[result, ok_tag_ptr, ok_tag_len],
13715− types::I32,
13716− );
1371713898 let err_block = builder.create_block();
13899+ let (ok_tag_ptr, ok_tag_len) = self.string_ptr(builder, "Ok");
13900+ let is_ok = self.call_rt_typed(
13901+ builder,
13902+ "knot_constructor_matches",
13903+ &[result, ok_tag_ptr, ok_tag_len],
13904+ types::I32,
13905+ );
1371813906 builder.ins().brif(is_ok, ok_block, &[], err_block, &[]);
1371913907
1372013908 // Err path: pass the result straight through.
@@ -13722,68 +13910,40 @@ ast::ExprKind::Atomic(inner) => {
1372213910 builder.seal_block(err_block);
1372313911 builder.ins().jump(merge_block, &[result.into()]);
1372413912
13725− // Ok path: extract `.value` and check the predicate chain.
13913+ // Ok path: extract `.value` and walk each refinement path.
1372613914 builder.switch_to_block(ok_block);
1372713915 builder.seal_block(ok_block);
1372813916 let payload = self.call_rt(builder, "knot_constructor_payload", &[result]);
1372913917 let (v_key_ptr, v_key_len) = self.string_ptr(builder, "value");
13730− let val = self.call_rt(builder, "knot_record_field", &[payload, v_key_ptr, v_key_len]);
13918+ let top = self.call_rt(builder, "knot_record_field", &[payload, v_key_ptr, v_key_len]);
1373113919
13732− // A `Maybe`-wrapped expected type: the value is `Just {value}` /
13733− // `Nothing`. `Nothing` skips the predicate entirely (a None payload
13734− // carries no refined scalar) — branch straight to `pass`. `Just`
13735− // unwraps to the payload, which the predicates check.
13736− //
13737− // `check_block` is where the predicate chain actually runs: the Ok
13738− // path falls into it directly for a non-Maybe type, or conditionally
13739− // (on `Just`) for a Maybe type.
13740− let check_block = builder.create_block();
13741− builder.append_block_param(check_block, self.ptr_type); // the value to check
13920+ // Global all-predicates-passed flag, threaded as a value: each path
13921+ // folds its verdicts in and returns the accumulated flag.
13922+ let mut all_ok = builder.ins().iconst(types::I32, 1);
13923+ for path in paths {
13924+ all_ok = self.emit_refine_walk(
13925+ builder,
13926+ top,
13927+ &path.steps,
13928+ &path.refined_name,
13929+ all_ok,
13930+ env,
13931+ db,
13932+ );
13933+ }
1374213934 let pass_block = builder.create_block();
1374313935 let fail_block = builder.create_block();
13744−
13745− if is_maybe {
13746− // Unwrap `Just {value}` → payload; `Nothing` → null. Jump to the
13747− // check block unconditionally with the (possibly null) value; the
13748− // check block itself skips the predicate on null (Nothing).
13749− let unwrapped = self.call_rt(builder, "knot_override_unwrap_just", &[val]);
13750− builder.ins().jump(check_block, &[unwrapped.into()]);
13751− } else {
13752− builder.ins().jump(check_block, &[val.into()]);
13753− }
13754−
13755− // Check path: run the conjoined predicate chain against the value.
13756− builder.switch_to_block(check_block);
13757− let check_val = builder.block_params(check_block)[0];
13758− if is_maybe {
13759− // A null (Nothing) value skips the predicate: branch to pass.
13760− let present = builder.ins().icmp_imm(IntCC::NotEqual, check_val, 0);
13761− let run_block = builder.create_block();
13762− builder.ins().brif(present, run_block, &[], pass_block, &[]);
13763− builder.switch_to_block(run_block);
13764− builder.seal_block(run_block);
13765− }
13766− builder.seal_block(check_block);
13767− let mut cond = builder.ins().iconst(types::I32, 1);
13768− for pred in &preds {
13769− let pred_fn = self.compile_expr(builder, pred, env, db);
13770− let res = self.call_rt(builder, "knot_value_call", &[db, pred_fn, check_val]);
13771− let pred_ok =
13772− self.call_rt_typed(builder, "knot_value_get_bool", &[res], types::I32);
13773− // And the running condition with this predicate's verdict.
13774− cond = builder.ins().band(cond, pred_ok);
13775− }
13776− builder.ins().brif(cond, pass_block, &[], fail_block, &[]);
13936+ builder.ins().brif(all_ok, pass_block, &[], fail_block, &[]);
1377713937
1377813938 // All predicates held: keep the original Ok.
1377913939 builder.switch_to_block(pass_block);
1378013940 builder.seal_block(pass_block);
1378113941 builder.ins().jump(merge_block, &[result.into()]);
1378213942
13783− // A predicate failed: swap to a refinement Err.
13943+ // A predicate failed: swap to a refinement Err naming that refined type.
1378413944 builder.switch_to_block(fail_block);
1378513945 builder.seal_block(fail_block);
13786− let err_val = self.build_refinement_err(builder, type_name);
13946+ let err_val = self.build_refinement_err(builder, &paths[0].refined_name);
1378713947 builder.ins().jump(merge_block, &[err_val.into()]);
1378813948
1378913949 builder.switch_to_block(merge_block);