Add require clauses and post-monomorph body safety checks

Introduces `require <expr>` clauses on function declarations, checked by
the safety checker at each call site and assumed true inside the body.
Adds a second safety-check pass after monomorphization so that bodies of
`[T; N]` generic functions are verified with concrete sizes.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: wtholliday

cli/src/main.rs

@@ -149,6 +149,23 @@ fn run(args: Args) -> i32 {
         return 1;
     }
 
+    // For `--check`, also run monomorphization so the post-monomorph safety
+    // check (which catches bounds violations in `[T; N]` function bodies)
+    // fires here too. The actual compiled code is discarded. Skip if no
+    // entry point is defined — many test snippets are entry-point-less.
+    if args.check && compiler.has_decls() {
+        let has_entry = compiler
+            .effective_entry_points()
+            .iter()
+            .any(|name| !compiler.decls().find(*name).is_empty());
+        if has_entry {
+            if let Err(e) = compiler.specialize() {
+                eprintln!("{}", e);
+                return 1;
+            }
+        }
+    }
+
     compiler.print_ir = args.ir;
 
     // Select backend via --backend flag, falling back to LYTE_BACKEND env var.

src/checker.rs

@@ -988,6 +988,17 @@ impl Checker {
                 }
             }
 
+            // Type-check require clauses: each must have type bool.
+            for &req in &func_decl.requires {
+                let req_ty = self.check_expr(req, &func_decl.arena, decls);
+                self.eq(
+                    req_ty,
+                    mk_type(Type::Bool),
+                    func_decl.arena.locs[req],
+                    "require clause must be a boolean expression",
+                );
+            }
+
             // Check the body of the function.
             let ty = self.check_expr(body, &func_decl.arena, decls);
 

src/compiler.rs

@@ -65,6 +65,7 @@ fn builtin_decls() -> Vec<Decl> {
             body: None,
             ret: mk_type(Type::Void),
             constraints: vec![],
+            requires: vec![],
             loc: test_loc(),
             arena: ExprArena::new(),
             types: vec![],
@@ -83,6 +84,7 @@ fn builtin_decls() -> Vec<Decl> {
             body: None,
             ret: mk_type(Type::Void),
             constraints: vec![],
+            requires: vec![],
             loc: test_loc(),
             arena: ExprArena::new(),
             types: vec![],
@@ -101,6 +103,7 @@ fn builtin_decls() -> Vec<Decl> {
             body: None,
             ret: mk_type(Type::Void),
             constraints: vec![],
+            requires: vec![],
             loc: test_loc(),
             arena: ExprArena::new(),
             types: vec![],
@@ -130,6 +133,7 @@ fn builtin_decls() -> Vec<Decl> {
                 body: None,
                 ret: ret_ty,
                 constraints: vec![],
+                requires: vec![],
                 loc: test_loc(),
                 arena: ExprArena::new(),
                 types: vec![],
@@ -155,6 +159,7 @@ fn builtin_decls() -> Vec<Decl> {
                 body: None,
                 ret: bool_ty,
                 constraints: vec![],
+                requires: vec![],
                 loc: test_loc(),
                 arena: ExprArena::new(),
                 types: vec![],
@@ -188,6 +193,7 @@ fn builtin_decls() -> Vec<Decl> {
                 body: None,
                 ret: ret_ty,
                 constraints: vec![],
+                requires: vec![],
                 loc: test_loc(),
                 arena: ExprArena::new(),
                 types: vec![],
@@ -225,6 +231,7 @@ fn builtin_decls() -> Vec<Decl> {
         body: None,
         ret: f32x4_ty,
         constraints: vec![],
+        requires: vec![],
         loc: test_loc(),
         arena: ExprArena::new(),
         types: vec![],
@@ -244,6 +251,7 @@ fn builtin_decls() -> Vec<Decl> {
         body: None,
         ret: f32x4_ty,
         constraints: vec![],
+        requires: vec![],
         loc: test_loc(),
         arena: ExprArena::new(),
         types: vec![],
@@ -627,7 +635,11 @@ impl Compiler {
         let mut pass = MonomorphPass::new();
         let entry_points = self.effective_entry_points();
         let all_decls = pass.monomorphize_multi(&self.decls, &entry_points)?;
-        // monomorphize now returns all decls (original + specialized)
+        // Capture the names of newly-generated specialized decls so we can
+        // run a focused safety-check pass on them (their bodies were skipped
+        // pre-monomorph because they contained size variables).
+        let specialized_names: std::collections::HashSet<Name> =
+            pass.instantiated_names().collect();
         self.decls = DeclTable::new(all_decls);
 
         // Rename non-generic overloaded functions to unique symbols.
@@ -636,6 +648,32 @@ impl Compiler {
         rename_overloaded_functions(&mut self.decls);
         self.decls = DeclTable::new(self.decls.decls.clone());
 
+        // Re-run the safety checker on specialized declarations only.
+        // Their bodies were skipped pre-monomorph because they had non-empty
+        // size_vars; now sizes are concrete (`[T; Known(K)]`) so bounds and
+        // require clauses can be verified properly.
+        if !specialized_names.is_empty() {
+            let mut sc = SafetyChecker::new();
+            for decl in &self.decls.decls {
+                if let Decl::Func(f) = decl {
+                    if specialized_names.contains(&f.name) {
+                        sc.check_decl(decl, &self.decls);
+                    }
+                }
+            }
+            if !self.quiet {
+                sc.print_errors();
+            }
+            for err in &sc.errors {
+                self.last_errors
+                    .push(format_error(err.location, &err.message));
+            }
+            self.last_safety_errors.extend(sc.errors.iter().cloned());
+            if !sc.errors.is_empty() {
+                return Err(format!("safety check failed for {} call(s)", sc.errors.len()));
+            }
+        }
+
         // Hoist loop-invariant struct field reads (after monomorphization
         // so we operate on concrete types, and after safety checking).
         {

src/decl.rs

@@ -56,6 +56,11 @@ pub struct FuncDecl {
     /// The interfaces that must be available for this function.
     pub constraints: Vec<InterfaceConstraint>,
 
+    /// Precondition expressions checked by the safety checker:
+    /// assumed true inside the body, must be provable at every call site.
+    /// Each ExprID indexes into `arena`.
+    pub requires: Vec<ExprID>,
+
     /// Location of the declaration in source code.
     pub loc: Loc,
 
@@ -312,6 +317,12 @@ fn format_func_decl(func: &FuncDecl, is_macro: bool) -> String {
         format!(" → {}", func.ret.pretty_print())
     };
     let constraints = format_constraints(&func.constraints);
+    let requires = func
+        .requires
+        .iter()
+        .map(|&r| format!(" require {}", func.arena.exprs[r].pretty_print(&func.arena, 0)))
+        .collect::<Vec<_>>()
+        .join("");
 
     let signature = if is_macro {
         format!("macro {}{}", func.name, typevars)
@@ -324,11 +335,14 @@ fn format_func_decl(func: &FuncDecl, is_macro: bool) -> String {
     if let Some(body_id) = func.body {
         let body_str = func.arena.exprs[body_id].pretty_print(&func.arena, 0);
         format!(
-            "{}({}){}{} {}",
-            signature, params, ret_type, constraints, body_str
+            "{}({}){}{}{} {}",
+            signature, params, ret_type, constraints, requires, body_str
         )
     } else {
-        format!("{}({}){}{}", signature, params, ret_type, constraints)
+        format!(
+            "{}({}){}{}{}",
+            signature, params, ret_type, constraints, requires
+        )
     }
 }
 
@@ -400,6 +414,7 @@ mod tests {
             body: None,
             ret: mk_type(Type::Int32),
             constraints: vec![],
+            requires: vec![],
             loc: test_loc(),
             arena: ExprArena::new(),
             types: vec![],
@@ -428,6 +443,7 @@ mod tests {
             body: Some(body_id),
             ret: mk_type(Type::Var(Name::str("T"))),
             constraints: vec![],
+            requires: vec![],
             loc: test_loc(),
             arena,
             types: vec![],
@@ -486,6 +502,7 @@ mod tests {
                 body: None,
                 ret: mk_type(Type::Int32),
                 constraints: vec![],
+                requires: vec![],
                 loc: test_loc(),
                 arena: ExprArena::new(),
                 types: vec![],
@@ -546,6 +563,7 @@ mod tests {
             body: Some(body_id),
             ret: mk_type(Type::Int32),
             constraints: vec![],
+            requires: vec![],
             loc: test_loc(),
             arena,
             types: vec![],

src/jit.rs

@@ -1761,6 +1761,7 @@ impl<'a> FunctionTranslator<'a> {
                             body: Some(*body),
                             ret: rng,
                             constraints: vec![],
+                            requires: vec![],
                             loc: decl.loc,
                             arena: decl.arena.clone(),
                             types: decl.types.clone(),

src/lexer.rs

@@ -83,6 +83,7 @@ pub enum Token {
     Assume,
     Const,
     Extern,
+    Require,
     End,
     Error,
 }
@@ -211,6 +212,7 @@ impl Lexer {
                 "assume" => Token::Assume,
                 "const" => Token::Const,
                 "extern" => Token::Extern,
+                "require" => Token::Require,
                 _ => Token::Id(Name::str(&id)),
             };
         }

src/llvm_jit.rs

@@ -3400,6 +3400,7 @@ impl<'a, 'ctx> FunctionTranslator<'a, 'ctx> {
                     body: Some(body),
                     ret: rng,
                     constraints: vec![],
+                    requires: vec![],
                     loc: decl.loc,
                     arena: decl.arena.clone(),
                     types: decl.types.clone(),

src/monomorph_pass.rs

@@ -618,6 +618,13 @@ impl MonomorphPass {
         &self.out_decls
     }
 
+    /// The mangled names of all functions newly created by monomorphization
+    /// (i.e., specialized versions of generic functions). Excludes entry
+    /// points and any pre-existing non-generic functions.
+    pub fn instantiated_names(&self) -> impl Iterator<Item = Name> + '_ {
+        self.instantiations.values().copied()
+    }
+
     /// Get the mangled name for a specific instantiation, if it exists
     pub fn get_instantiation(&self, key: &MonomorphKey) -> Option<Name> {
         self.instantiations.get(key).copied()
@@ -721,6 +728,7 @@ mod tests {
             size_vars: vec![],
             params: Vec::new(),
             constraints: Vec::new(),
+            requires: vec![],
             ret: mk_type(Type::Void),
             body: Some(body_expr),
             arena,
@@ -834,6 +842,7 @@ mod tests {
             size_vars: Vec::new(),
             params: Vec::new(),
             constraints: Vec::new(),
+            requires: vec![],
             ret: mk_type(Type::Void),
             body: Some(block),
             arena,
@@ -863,6 +872,7 @@ mod tests {
             size_vars: Vec::new(),
             params: Vec::new(),
             constraints: Vec::new(),
+            requires: vec![],
             ret: mk_type(Type::Void),
             body: Some(binop),
             arena,
@@ -892,6 +902,7 @@ mod tests {
             size_vars: Vec::new(),
             params: Vec::new(),
             constraints: Vec::new(),
+            requires: vec![],
             ret: mk_type(Type::Void),
             body: Some(array),
             arena,
@@ -1127,6 +1138,7 @@ mod tests {
             size_vars: Vec::new(),
             params: Vec::new(),
             constraints: Vec::new(),
+            requires: vec![],
             ret: mk_type(Type::Void),
             body: Some(if_expr),
             arena,
@@ -1160,6 +1172,7 @@ mod tests {
             size_vars: Vec::new(),
             params: Vec::new(),
             constraints: Vec::new(),
+            requires: vec![],
             ret: mk_type(Type::Int32),
             body: Some(body_expr),
             arena,
@@ -1199,6 +1212,7 @@ mod tests {
                 ty: Some(t_var),
             }],
             constraints: Vec::new(),
+            requires: vec![],
             ret: t_var,
             body: Some(id_param_expr),
             arena: id_arena,
@@ -1224,6 +1238,7 @@ mod tests {
             size_vars: Vec::new(),
             params: Vec::new(),
             constraints: Vec::new(),
+            requires: vec![],
             ret: i32_type,
             body: Some(call_expr),
             arena: main_arena,

src/parser.rs

@@ -945,6 +945,7 @@ fn parse_func_decl(name: Name, cx: &mut ParseContext) -> FuncDecl {
     let mut params = vec![];
     let mut all_vars = vec![];
     let mut constraints = vec![];
+    let mut requires = vec![];
     let loc = cx.lex.loc;
     let mut arena = ExprArena::new();
 
@@ -984,6 +985,16 @@ fn parse_func_decl(name: Name, cx: &mut ParseContext) -> FuncDecl {
         }
     }
 
+    skip_newlines(cx.lex);
+
+    // Parse zero or more `require <expr>` clauses.
+    while cx.lex.tok == Token::Require {
+        cx.next();
+        let cond = parse_expr(&mut arena, &all_vars, cx);
+        requires.push(cond);
+        skip_newlines(cx.lex);
+    }
+
     // Separate size vars (used as array sizes) from type vars.
     let mut size_vars: Vec<Name> = vec![];
     for param in &params {
@@ -1013,6 +1024,7 @@ fn parse_func_decl(name: Name, cx: &mut ParseContext) -> FuncDecl {
         body,
         ret,
         constraints,
+        requires,
         loc,
         arena,
         types: vec![],