@@ -1625,29 +1625,6 @@ 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−
16511628impl<M: cranelift_module::Module> Codegen<M> {
16521629 /// Build a `Codegen` around an already-constructed module. Backend-agnostic:
16531630 /// the ISA/unwind setup is the same for `ObjectModule` (AOT) and `JITModule`.
@@ -7534,24 +7511,7 @@ ast::ExprKind::Atomic(inner) => {
75347511 {
75357512 let src = self.compile_arg_expr(builder, args[0], env, db);
75367513 let (eptr, elen) = self.string_ptr(builder, &expected);
7537− let result =
7538− self.call_rt(builder, "knot_builtin_compile_typed", &[src, eptr, elen]);
7539− // Option B — host-side refinement gate. The JIT's expected-type
7540− // subsumption knows refined types only by NAME (their
7541− // predicates never cross the wire), so a snippet could
7542− // redeclare `type Port = Int where \_ -> True` and slip a value
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,
7552− );
7553− }
7554− return result;
7514+ return self.call_rt(builder, "knot_builtin_compile_typed", &[src, eptr, elen]);
75557515 }
75567516 }
75577517
@@ -13655,302 +13615,6 @@ ast::ExprKind::Atomic(inner) => {
1365513615 builder.seal_block(done_block);
1365613616 }
1365713617
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− _ => {}
13776− }
13777− }
13778−
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.
13878− ///
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(
13882− &mut self,
13883− builder: &mut FunctionBuilder,
13884− result: Value,
13885− paths: &[RefinePath],
13886− env: &mut Env,
13887− db: Value,
13888− ) -> Value {
13889− if paths.is_empty() {
13890− return result;
13891− }
13892−
13893− // Split on the Result tag: `Err` bypasses the check; `Ok` unwraps its
13894− // `value` and walks every path.
13895− let merge_block = builder.create_block();
13896− builder.append_block_param(merge_block, self.ptr_type);
13897− let ok_block = builder.create_block();
13898− 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− );
13906− builder.ins().brif(is_ok, ok_block, &[], err_block, &[]);
13907−
13908− // Err path: pass the result straight through.
13909− builder.switch_to_block(err_block);
13910− builder.seal_block(err_block);
13911− builder.ins().jump(merge_block, &[result.into()]);
13912−
13913− // Ok path: extract `.value` and walk each refinement path.
13914− builder.switch_to_block(ok_block);
13915− builder.seal_block(ok_block);
13916− let payload = self.call_rt(builder, "knot_constructor_payload", &[result]);
13917− let (v_key_ptr, v_key_len) = self.string_ptr(builder, "value");
13918− let top = self.call_rt(builder, "knot_record_field", &[payload, v_key_ptr, v_key_len]);
13919−
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− }
13934− let pass_block = builder.create_block();
13935− let fail_block = builder.create_block();
13936− builder.ins().brif(all_ok, pass_block, &[], fail_block, &[]);
13937−
13938− // All predicates held: keep the original Ok.
13939− builder.switch_to_block(pass_block);
13940− builder.seal_block(pass_block);
13941− builder.ins().jump(merge_block, &[result.into()]);
13942−
13943− // A predicate failed: swap to a refinement Err naming that refined type.
13944− builder.switch_to_block(fail_block);
13945− builder.seal_block(fail_block);
13946− let err_val = self.build_refinement_err(builder, &paths[0].refined_name);
13947− builder.ins().jump(merge_block, &[err_val.into()]);
13948−
13949− builder.switch_to_block(merge_block);
13950− builder.seal_block(merge_block);
13951− builder.block_params(merge_block)[0]
13952− }
13953−
1395413618 fn emit_override_literal(
1395513619 &mut self,
1395613620 builder: &mut FunctionBuilder,