iter embedding-abi-m1.1 (DONE 7/7): Embedding-ABI M1 — scalar AILang fn callable from C/Rust

Tasks 4-7 on the Boss-Repaired plan, completing the M1 iteration:

- Task 4: check-side export-signature gate — CheckError variants
  ExportNonScalarSignature / ExportHasEffects (codes
  export-non-scalar-signature / export-has-effects), code() arms,
  check_fn gate (params->ret->effects, first-violation-wins,
  unconditional on f.export.is_some()). The clause-3 discriminator
  in code: effectful/non-scalar exports fail to typecheck. 6/6.
- Task 5: codegen Target::StaticLib — Target enum, threaded param,
  @main/MissingEntryMain gated behind Target::Executable, one
  external @<sym> forwarder per export to @ail_<module>_<fn>
  (fn_scalar_sig/llvm_scalar). In-source missing_entry_main_is_error
  byte-unchanged. Lowering pin 2/2.
- Task 6: CLI ail build --emit=staticlib — clap field, Cmd::Build
  branch, build_staticlib (verbatim build_to prefix + has_export
  guard + two-archive clang -c/ar rcs tail) + run_cmd. CLI pin 2/2.
- Task 7: C-host E2E coherent-stop proof (cc links
  libembed_backtest_step.a + libailang_rt.a, backtest_step(0,3)=9 /
  (9,4)=25, s==25, exit 0) + DESIGN.md §"Embedding ABI (M1)"
  (scalar C ABI, provisional until M3). E2E pin 1/1.

Independent Boss verification: E2E 1/1, gate 6/6, full workspace
0 failures, roundtrip_cli + design_schema_drift + spec_drift green,
Invariant 1 holds (no new dep in core/codegen/runtime). 3 behaviour-
neutral plan pseudo-vs-reality concerns in the journal. Default-exe
codegen/runtime path byte-unchanged (check.py firing = tracked-P2
known-noise, audit-adjudicated). INDEX line added.

Completes the M1 iteration (impl). Milestone-close audit + fieldtest
(surface-touching) are the next pipeline steps.

crates/ailang-check/src/lib.rs

@@ -444,6 +444,20 @@ pub enum CheckError {
     #[error("const `{0}` may not have effects (got !{1:?})")]
     ConstHasEffects(String, Vec<String>),
 
+    /// An `(export …)` fn has a parameter or return type that is not
+    /// a C-scalar (`Int`/`Float`). M1's embedding ABI is scalar-only;
+    /// `Bool`/`Str`/every ADT is rejected at typecheck (the
+    /// feature-acceptance clause-3 discriminator, in code).
+    /// Code: `export-non-scalar-signature`.
+    #[error("export `{0}`: M1 embedding ABI is scalar-only — {1} type `{2}` is not `Int`/`Float`")]
+    ExportNonScalarSignature(String, &'static str, String),
+
+    /// An `(export …)` fn has a non-empty effect set. An embedding
+    /// kernel must be pure (a `(State,Chunk)->State` fold has no
+    /// effects). Code: `export-has-effects`.
+    #[error("export `{0}` must be pure — declared effects !{1:?} are not allowed on an embedding boundary")]
+    ExportHasEffects(String, Vec<String>),
+
     /// A `Type::Con` named a type not in [`Env::types`] or with a wrong
     /// arity for a parameterised ADT. Code: `unknown-type`.
     #[error("unknown type: `{0}`")]
@@ -695,6 +709,8 @@ impl CheckError {
             CheckError::ParamCountMismatch { .. } => "param-count-mismatch",
             CheckError::PolymorphicNotSupported(_) => "polymorphic-not-supported",
             CheckError::ConstHasEffects(..) => "const-has-effects",
+            CheckError::ExportNonScalarSignature(..) => "export-non-scalar-signature",
+            CheckError::ExportHasEffects(..) => "export-has-effects",
             CheckError::UnknownType(_) => "unknown-type",
             CheckError::UnknownCtor { .. } => "unknown-ctor",
             CheckError::UnknownCtorInPattern(_) => "unknown-ctor-in-pattern",
@@ -1895,6 +1911,41 @@ fn check_fn(f: &FnDef, env: &Env, out_warnings: &mut Vec<Diagnostic>) -> Result<
     }
     check_type_well_formed(&ret_ty, &env)?;
 
+    // Embedding-ABI M1: an `(export …)` fn is the C call boundary.
+    // Its signature must be scalar-only (`Int`/`Float`) and pure.
+    // Gate order: params → ret → effects, first violation wins
+    // (so a combined Str+IO export deterministically fails on the
+    // signature). Unconditional at check-time — independent of the
+    // codegen emit mode — this IS the clause-3 discriminator.
+    if f.export.is_some() {
+        fn is_c_scalar(t: &Type) -> bool {
+            matches!(t, Type::Con { name, args, .. }
+                if args.is_empty() && (name == "Int" || name == "Float"))
+        }
+        for p in &param_tys {
+            if !is_c_scalar(p) {
+                return Err(CheckError::ExportNonScalarSignature(
+                    f.name.clone(),
+                    "parameter",
+                    ailang_core::pretty::type_to_string(p),
+                ));
+            }
+        }
+        if !is_c_scalar(&ret_ty) {
+            return Err(CheckError::ExportNonScalarSignature(
+                f.name.clone(),
+                "return",
+                ailang_core::pretty::type_to_string(&ret_ty),
+            ));
+        }
+        if !declared_effs.is_empty() {
+            return Err(CheckError::ExportHasEffects(
+                f.name.clone(),
+                declared_effs.clone(),
+            ));
+        }
+    }
+
     // mq.3: build the post-superclass-expansion declared-constraint
     // set ONCE here and stash on env, so synth's Var-arm class-method
     // branch can hand it to `resolve_method_dispatch`'s constraint-