git » blacktide.git » commit c4bff21

diff --git a/doc/compiler.md b/doc/compiler.md
index beec5b4..1c7ff77 100644
--- a/doc/compiler.md
+++ b/doc/compiler.md
@@ -18,8 +18,8 @@ For a walkthrough with actual inputs, intermediate data and generated code, see
 | Classification | Preserve analyzed loops without DSL effects and native keyword calls. Make representations explicit for loops that need lowering. |
 | Normalization | Lower sequential and parallel assignments, case and collections. Prepare conversions and save operands in evaluation order. |
 | Graph | Resolve outer labels and check destinations and definite initialization. Compute liveness and allocate slots. |
-| Backend | Fold literal branches and recover structured control with shared joins. Choose safe primitive storage and compact safe intermediates. Use the dispatcher when structured recovery is ineligible. |
-| Emission | Emit Clojure that preserves conversions and construction sites. Seal the result with an Object type boundary. |
+| Backend | Fold literal branches and recover structured control with shared joins. Prove numeric values, choose safe primitive storage, lower numeric operations and compact safe intermediates. Use the dispatcher when structured recovery is ineligible. |
+| Emission | Emit Clojure that preserves conversions and construction sites. Preserve the Object result boundary at exits without taking a tail loop out of tail position. |
 
 `compiler/compile-form` orchestrates source analysis and lowering:
 
@@ -36,9 +36,27 @@ The outer bindings enter as one lexical scope. `Native` contains analyzed subtre
 
 ```text
 Dispatcher:  Machine → Code
-Structured:  Machine → Analysis → Planned → Joined → Stored → Compact → Code
+Structured:  Machine → Numeric → Analysis → Planned → Joined
+                     → Represented → Lexical → Compact → Sealed → Code
 ```
 
+`numeric` recognizes numeric runtime calls and implicit Java numeric conversions, retaining their original signatures. `value-facts` proves scalar values across assignments and backedges; a boxed result can still be known to contain a long. `storage` chooses representations after accounting for consumers, copies and observable identity. `lexical` makes loop arguments explicit. `numeric-lower` implements the proven equivalences using host operations and ordinary control flow. `compact` simplifies safe intermediates, and `results` marks public exits before emission.
+
+Inference and lowering share `numeric-rules`. Knowing the operands' values is insufficient: their original overload determines overflow, conversion and reference-return behavior.
+
+| Numeric surface | Treatment |
+| --- | --- |
+| Checked and unchecked arithmetic; ordered and numeric comparisons | Use primitive overloads when their semantics agree. Preserve generic subtraction's separate negation and addition. |
+| Promoting arithmetic and integral division | Primitive inputs may still produce a `Number`, including BigInt or Ratio. Do not infer a fixed result width. |
+| Floating division, quotient and remainder | Preserve the original NaN handling, zero checks and exception behavior. |
+| `min`/`max` and `=` | Preserve selected references, signed-zero ties and NaN identity. Selected results inherit their possible input origins. |
+| Bit operations | Specialize proven integral values; retain the original rejection of other numeric categories. |
+| Numeric casts and Java parameters | Preserve checked/unchecked conversions, narrowing order and exception behavior. Explicitly widen numeric operands where Clojure would otherwise box them. Java parameter conversion's additional `Number` check remains required for unknown inputs. |
+| `clojure.math`, primitive arrays and explicit JVM arithmetic | Keep source signatures and conversions; primitive results already participate in value inference. |
+| Arbitrary precision, unknown inputs and ordinary Var calls | Keep generic operations and Var semantics. Dynamic decimal precision and rounding remain the runtime's responsibility. |
+
+Specialization is conservative: incompatible value classes, observable boxes and unsupported control-recovery shapes can prevent it. Literal boxes are only re-created when their identity is guaranteed by the small-Long cache. This does not promise allocation-free code or a speedup for every region. The dispatcher retains the original calls.
+
 Backend selection keeps its branching and shared analyses explicit. Compaction returns each simplified subtree with its free-read counts, avoiding repeated analysis of unchanged bodies. Emitters complete their compiler work before returning generated forms; quoted source data remains opaque.
 
 Language derivation describes how grammars relate. It does not set pass order: `Symbolic` extends `CFG`, which extends `Machine`, while lowering visits `Symbolic`, then `CFG`, then `Machine`.
diff --git a/doc/language.md b/doc/language.md
index 1ace9c6..91084a0 100644
--- a/doc/language.md
+++ b/doc/language.md
@@ -133,7 +133,7 @@ Source primitive inference is preserved. This includes int→long and float→do
 
 ### Calls and compilation
 
-Source facts determine overloads and conversion order. Clojure 1.12 qualified method values, functional-interface adaptation and `:param-tags` are supported. Arithmetic respects `*unchecked-math*`. Calls respect `:direct-linking` and direct protocol dispatch.
+Source facts determine overloads and conversion order. Clojure 1.12 qualified method values, functional-interface adaptation and `:param-tags` are supported. Arithmetic respects `*unchecked-math*`. Proven numeric operations may use primitive storage and calls when their value, promotion, overflow, conversion and identity behavior agree with the source. This includes preserving the distinctions between `=` and `==`, and between generic and primitive floating-point operations. Calls respect `:direct-linking` and direct protocol dispatch.
 
 Unreachable code still receives syntax and JVM compilation checks. Very large regions remain subject to JVM method-size limits.
 
diff --git a/doc/tutorial.md b/doc/tutorial.md
index ae4bd54..f0925fb 100644
--- a/doc/tutorial.md
+++ b/doc/tutorial.md
@@ -153,8 +153,7 @@ The remaining examples use `stages` to run the pipeline and retain intermediate
          '[com.tailrecursion.blacktide.compiler.passes.lower :as lower]
          '[com.tailrecursion.blacktide.compiler.passes.transfers :as transfers]
          '[com.tailrecursion.blacktide.compiler.passes.graph :as graph]
-         '[com.tailrecursion.blacktide.compiler.passes.emit :as emit]
-         '[com.tailrecursion.blacktide.compiler.passes.host-emit :as host])
+         '[com.tailrecursion.blacktide.compiler.passes.emit :as emit])
 
 (defn stages [form]
   (let [ctx {:locals {} :macro-env {}
@@ -174,8 +173,8 @@ The remaining examples use `stages` to run the pipeline and retain intermediate
         cfg (transfers/resolve-program symbolic)
         machine (graph/analyze cfg)]
     {:bound bound :ordered ordered :cfg cfg :machine machine
-     :dispatcher (host/box-form (emit/program-form machine))
-     :code (host/box-form (compiler/compile-program machine))}))
+     :dispatcher (emit/program-form machine)
+     :code (compiler/compile-program machine)}))
 
 (defn readable [value]
   (walk/postwalk
@@ -482,39 +481,31 @@ Having carefully dismantled the loop, we would now like a loop. Here's the norma
 ```
 
 ```text
-(^{:param-tags [java.lang.Object]} clojure.lang.RT/box
- (let*
-  [v0
-   (^{:param-tags [java.lang.Object]} clojure.lang.RT/box '0)
-   v25
-   (clojure.lang.RT/longCast '10)]
-  (loop*
-   [v0
-    (^{:param-tags [java.lang.Object]} clojure.lang.RT/box v0)
-    v3
-    '0]
-   (if
-    (clojure.lang.Numbers/lt v3 v25)
-    (let*
-     [v41
-      (^{:param-tags [java.lang.Object]} clojure.lang.RT/box
-       (clojure.lang.Numbers/add ^java.lang.Object v0 v3))]
-     (recur v41 (clojure.lang.Numbers/unchecked_inc v3)))
-    v0))))
+(loop*
+ [v0 '0 v3 '0]
+ (if
+  (^{:param-tags [long long]} clojure.lang.Numbers/lt v3 '10)
+  (let*
+   [v41 (^{:param-tags [long long]} clojure.lang.Numbers/add v0 v3)]
+   (recur
+    v41
+    (^{:param-tags [long]} clojure.lang.Numbers/unchecked_inc v3)))
+  (^{:param-tags [java.lang.Object]} clojure.lang.RT/box v0)))
 ```
 
-There is no program counter or dispatch. The limit lives outside the loop; the loop carries the accumulator and index. All `recur` arguments are evaluated before either loop binding is rebound.
+There is no program counter or dispatch. The constant limit is used directly; the loop carries the accumulator and index. All `recur` arguments are evaluated before either loop binding is rebound.
 
-The casts and `Object` hints are still there. In particular, [`RT.box(Object)`](https://github.com/clojure/clojure/blob/clojure-1.12.6/src/jvm/clojure/lang/RT.java#L1037-L1039) returns its argument unchanged. Its `Object` return type keeps Clojure from treating that result as a primitive; the call itself doesn't allocate a box. The accumulator preserves object identity, while the index can use primitive storage.
+The accumulator and index now use primitive longs. Numeric analysis proves that every update to `x` produces a long or throws on overflow; storage analysis establishes that no use needs the intermediate boxes' identities. The `:param-tags` select the primitive overloads explicitly. The exit's [`RT.box(Object)`](https://github.com/clojure/clojure/blob/clojure-1.12.6/src/jvm/clojure/lang/RT.java#L1037-L1039) keeps the macro's result typed as an Object. Returning the result may box it; the recurrence uses primitive arithmetic. Placing this boundary at the exit also keeps the loop in tail position: wrapping the whole loop in a call would make Clojure generate an extra function for it.
 
 Two terms help here: a _join_ is a point where control-flow paths meet, and a _loop invariant_ is a value or computation that stays the same across iterations. The backend's main jobs are:
 
 | Pass group | Purpose |
 | --- | --- |
-| Feasibility and value facts | Select branches with known tests; determine which values can safely use primitive storage. |
+| Feasibility, numeric recognition and value facts | Select known branches, recognize audited numeric operations and prove scalar values. |
 | Join planning and structured recovery | Arrange shared paths and recover conditionals and loops. |
-| Invariants and storage | Move safe computations whose results don't depend on the iteration out of loops; choose storage types. |
-| Compaction and emission | Remove unnecessary intermediate bindings and emit Clojure. |
+| Invariants and storage | Remove loop parameters that only forward unchanged outer values; choose storage without changing object identity. |
+| Numeric lowering | Select proven primitive overloads; preserve other calls unchanged. |
+| Compaction, result boundaries and emission | Remove safe intermediates, mark public exits and emit Clojure. |
 
 The [architecture guide](compiler.md) covers these passes in detail. Graphs outside the structured backend's supported shapes use the dispatcher. A graph with nested cycles does not automatically get reconstructed as nested Clojure loops.
 
diff --git a/src/com/tailrecursion/blacktide/compiler.clj b/src/com/tailrecursion/blacktide/compiler.clj
index 62d8a1e..137204a 100644
--- a/src/com/tailrecursion/blacktide/compiler.clj
+++ b/src/com/tailrecursion/blacktide/compiler.clj
@@ -18,14 +18,17 @@
             [com.tailrecursion.blacktide.compiler.passes.graph :as graph]
             [com.tailrecursion.blacktide.compiler.passes.feasible :as feasible]
             [com.tailrecursion.blacktide.compiler.passes.value-facts :as value-facts]
+            [com.tailrecursion.blacktide.compiler.passes.numeric :as numeric]
+            [com.tailrecursion.blacktide.compiler.passes.numeric-lower :as numeric-lower]
+            [com.tailrecursion.blacktide.compiler.passes.lexical :as lexical]
             [com.tailrecursion.blacktide.compiler.passes.joins :as joins]
             [com.tailrecursion.blacktide.compiler.passes.structure :as structure]
             [com.tailrecursion.blacktide.compiler.passes.invariants :as invariants]
             [com.tailrecursion.blacktide.compiler.passes.storage :as storage]
             [com.tailrecursion.blacktide.compiler.passes.compact :as compact]
+            [com.tailrecursion.blacktide.compiler.passes.results :as results]
             [com.tailrecursion.blacktide.compiler.passes.structured-emit :as structured]
             [com.tailrecursion.blacktide.compiler.passes.emit :as emit]
-            [com.tailrecursion.blacktide.compiler.passes.host-emit :as host]
             [typed.clojure :as-alias t]))
 
 (np/defpass compile-program
@@ -34,14 +37,18 @@
   (let [analysis (-> {:entry (:entry machine) :blocks (:blocks machine)}
                      feasible/program
                      graph/analyze
+                     numeric/program
                      value-facts/analyze)
         decision (-> analysis joins/plan structure/recover)]
     (if (= :structured (:op decision))
-      (let [compact (->> (:body decision)
+      (let [program (->> (:body decision)
                          (invariants/expression #{})
                          (storage/select-storage analysis)
-                         compact/program)]
-        (structured/expression (:types compact) (:body compact)))
+                         lexical/program
+                         numeric-lower/program
+                         compact/program
+                         results/program)]
+        (structured/expression (:types program) (:body program)))
       (emit/program-form machine))))
 
 (np/defpass compile-tree
@@ -59,8 +66,7 @@
       lower/stage
       transfers/resolve-program
       graph/analyze
-      compile-program
-      host/box-form))
+      compile-program))
 
 (np/defpass caller-locals
   {:from [l/Bound Context] :to [l/Bound Context] :body true}
diff --git a/src/com/tailrecursion/blacktide/compiler/languages.clj b/src/com/tailrecursion/blacktide/compiler/languages.clj
index e8eb822..f2ee98a 100644
--- a/src/com/tailrecursion/blacktide/compiler/languages.clj
+++ b/src/com/tailrecursion/blacktide/compiler/languages.clj
@@ -177,12 +177,28 @@
                                 :blocks (t/Map Label Block) :labels LabelTable
                                 :loops (t/Map t/Sym Label)} :complete? true)}})
 
+;; Recognized numeric calls retain the original host operation and operands.
+;; Value facts precede representation selection; neither changes source JVM facts.
+(np/derive-language Numeric Machine
+  {:add {Rhs [(t/HMap :mandatory {:op ':numeric :args (t/Vec Operand)
+                                 :parameters (t/Vec java.lang.Class) :return java.lang.Class
+                                 :operation (t/HMap :mandatory {:op ':static :class java.lang.Class
+                                                                :member t/Sym :tags l/JVM-Tags} :complete? true)}
+                      :optional {:conversion l/JVM-Conversion} :complete? true)]}
+   :replace {ValueType (t/U ':bottom ':boxed java.lang.Class)
+             ArgumentTypes (t/Vec ValueType)
+             Plan (t/HMap :mandatory {:recipe (t/U ':call ':negate-add ':promoting-negate-add ':divide
+                                                   ':zero-guard ':select ':compare ':narrow-int ':narrow-char ':narrow-checked ':widen-char)
+                                      :parameters (t/Vec java.lang.Class) :result java.lang.Class :fresh? t/Bool} :complete? true)
+             Graph (t/HMap :mandatory {:entry Label :blocks (t/Map Label Block)}
+                           :optional {:slots (t/Vec t/Sym) :live (t/Map Label (t/Set t/Sym))} :complete? true)}})
+
 ;; Facts and plans used by structured control recovery.
 (np/deflanguage Analysis
   {Type (t/U ':bottom ':boxed java.lang.Class)
    Types (t/Map t/Sym Type)
-   Definitions (t/Map t/Sym (t/Vec l/Machine-Rhs))
-   Program (t/HMap :mandatory {:machine l/Machine-Program :types Types
+   Definitions (t/Map t/Sym (t/Vec l/Numeric-Rhs))
+   Program (t/HMap :mandatory {:machine l/Numeric-Program :types Types
                                :reachable (t/Set l/Machine-Label)} :complete? true)})
 
 (np/derive-language Planned Analysis
@@ -192,12 +208,13 @@
     Regions (t/Map l/Machine-Label Region)
     Join (t/HMap :mandatory {:target l/Machine-Label :result t/Sym} :complete? true)
     Joins (t/Map l/Machine-Label Join)
-    Program (t/HMap :mandatory {:machine l/Machine-Program :types Types
+    Program (t/HMap :mandatory {:machine l/Numeric-Program :types Types
                                 :reachable (t/Set l/Machine-Label) :joins Joins} :complete? true)}})
 
-;; Structured recovery produces Joined expressions, then Stored programs.
+;; Structured recovery produces Joined expressions. Representation selection
+;; produces Represented; lexical and numeric lowering follow it.
 (np/deflanguage Structured
-  {Expr (t/U (t/HMap :mandatory {:op ':bind :binding l/Machine-Operation :body Expr} :complete? true)
+  {Expr (t/U (t/HMap :mandatory {:op ':bind :binding l/Numeric-Operation :body Expr} :complete? true)
              (t/HMap :mandatory {:op ':branch :test l/Machine-Atom :yes Expr :no Expr} :complete? true)
              (t/HMap :mandatory {:op ':switch :test l/Machine-Atom :arms (t/Vec Expr)} :complete? true)
              (t/HMap :mandatory {:op ':loop :slots (t/Vec t/Sym) :body Expr} :complete? true)
@@ -215,21 +232,20 @@
 
 (np/derive-language Joined Structured
   {:add {Expr [(t/HMap :mandatory {:op ':join :target t/Sym :value Expr :body Expr} :complete? true)]}
-   :replace {Context (t/HMap :mandatory {:machine l/Machine-Program :header (t/Option l/Machine-Label)
+   :replace {Context (t/HMap :mandatory {:machine l/Numeric-Program :header (t/Option l/Machine-Label)
                                         :slots (t/Vec t/Sym) :joins l/Planned-Joins
                                         :stop (t/Option (t/HVec [l/Machine-Label t/Sym]))} :complete? true)}})
 
-(np/derive-language Stored Joined
+(np/derive-language Represented Joined
   {:replace {Types (t/Map t/Sym java.lang.Class)
              Program (t/HMap :mandatory {:body Expr :types Types} :complete? true)}})
 
-;; Compact extends machine operands for lexical emission after storage.
-(np/derive-language Compact Machine
-  {:add {Atom [(t/HMap :mandatory {:op ':inline :value Rhs :type (t/Option java.lang.Class)} :complete? true)]}
-   :replace
+;; Lexical makes loop arguments and nested operands explicit before numeric
+;; lowering. Compact removes numeric operations; simplification follows lowering.
+(np/derive-language Lexical Numeric
+  {:replace
    {Binding (t/HMap :mandatory {:target t/Sym :value Atom} :complete? true)
     Expr (t/U (t/HMap :mandatory {:op ':bind :binding Operation :body Expr} :complete? true)
-              (t/HMap :mandatory {:op ':effect :binding Operation :body Expr} :complete? true)
               (t/HMap :mandatory {:op ':join :target t/Sym :value Expr :body Expr} :complete? true)
               (t/HMap :mandatory {:op ':branch :test Atom :yes Expr :no Expr} :complete? true)
               (t/HMap :mandatory {:op ':switch :test Atom :arms (t/Vec Expr)} :complete? true)
@@ -239,3 +255,13 @@
               (t/HMap :mandatory {:op ':throw :value Atom} :complete? true))
     Types (t/Map t/Sym java.lang.Class)
     Program (t/HMap :mandatory {:body Expr :types Types} :complete? true)}})
+
+(np/derive-language Compact Lexical
+  {:remove {Rhs #{:numeric}}
+   :add {Atom [(t/HMap :mandatory {:op ':inline :value Rhs :type (t/Option java.lang.Class)} :complete? true)]
+         Expr [(t/HMap :mandatory {:op ':effect :binding Operation :body Expr} :complete? true)]}})
+
+;; Public exits carry an Object boundary; join results remain internal values.
+(np/derive-language Sealed Compact
+  {:add {Expr [(t/HMap :mandatory {:op ':result :value Atom} :complete? true)
+               (t/HMap :mandatory {:op ':raise :value Atom} :complete? true)]}})
diff --git a/src/com/tailrecursion/blacktide/compiler/passes/box_origins.clj b/src/com/tailrecursion/blacktide/compiler/passes/box_origins.clj
index 3d8cbbf..88ebc44 100644
--- a/src/com/tailrecursion/blacktide/compiler/passes/box_origins.clj
+++ b/src/com/tailrecursion/blacktide/compiler/passes/box_origins.clj
@@ -6,32 +6,50 @@
             [com.tailrecursion.nanopass :as np]
             [com.tailrecursion.blacktide.compiler.languages :as l]
             [com.tailrecursion.blacktide.compiler.passes.value-facts :as facts]
+            [com.tailrecursion.blacktide.compiler.passes.numeric :as numeric]
             [typed.clojure :as-alias t]))
 
-(np/defpass copy-source {:from [l/Machine Rhs] :to (t/Option t/Sym) :body true}
+(np/defpass copy-source {:from [l/Numeric Rhs] :to (t/Option t/Sym) :body true}
   [rhs]
   (when (and (= :value (:op rhs)) (= :local (:op (:value rhs)))) (:id (:value rhs))))
 
-(np/defpass reboxable? {:from [l/Machine Rhs] :to t/Bool :body true}
-  [rhs]
+(np/defpass origin-values
+  {:from [l/Numeric Rhs] :to (t/Vec l/Machine-Atom) :args [l/Analysis-Types] :body true}
+  [types rhs]
   (case (:op rhs)
-    :value (let [value (:value rhs)]
-             (boolean (and (= :literal (:op value)) (instance? Long (:value value))
-                           (<= -128 (:value value) 127))))
-    (:host :convert) (class? (facts/rhs-type {} rhs))
-    false))
+    :value [(:value rhs)]
+    :numeric (if-let [plan (numeric/plan types rhs)]
+               (if (:fresh? plan) [] (mapv :value (:args rhs))) [])
+    []))
+
+(np/defpass reboxable? {:from [l/Numeric Rhs] :to t/Bool :args [l/Analysis-Types] :body true}
+  [types rhs]
+  (let [origins (origin-values types rhs)]
+    (if (seq origins)
+      ;; Selected references (min/max and NaN division) inherit all possible
+      ;; origins, just like copies. The fixed point checks local dependencies.
+      (every? (fn [^{::t/- l/Machine-Atom} value]
+                (or (= :local (:op value))
+                    (and (= :literal (:op value)) (instance? Long (:value value))
+                         (<= -128 (:value value) 127)))) origins)
+      (case (:op rhs)
+        :numeric (or (boolean (:fresh? (numeric/plan types rhs))) (class? (facts/rhs-type {} (numeric/source-call rhs))))
+        (:host :convert) (class? (facts/rhs-type {} rhs))
+        false))))
 
 (np/defpass reboxable-values {:from [l/Analysis Program] :to (t/Set t/Sym) :body true}
   [analysis]
   (let [definitions (facts/definitions (:reachable analysis) (:machine analysis))
         initial (reduce-kv
-                  (fn [^{::t/- (t/Set t/Sym)} out ^{::t/- t/Sym} id ^{::t/- (t/Vec l/Machine-Rhs)} values]
-                    (if (some #(and (nil? (copy-source %)) (not (reboxable? %))) values) (conj out id) out))
+                  (fn [^{::t/- (t/Set t/Sym)} out ^{::t/- t/Sym} id ^{::t/- (t/Vec l/Numeric-Rhs)} values]
+                    (if (some #(not (reboxable? (:types analysis) %)) values) (conj out id) out))
                   #{} definitions)
         denied ((fn ^{::t/- [(t/Set t/Sym) :-> (t/Set t/Sym)]} solve [denied]
                   (let [next (reduce-kv
-                               (fn [^{::t/- (t/Set t/Sym)} out ^{::t/- t/Sym} id ^{::t/- (t/Vec l/Machine-Rhs)} values]
-                                 (if (some #(contains? denied (copy-source %)) values) (conj out id) out))
+                               (fn [^{::t/- (t/Set t/Sym)} out ^{::t/- t/Sym} id ^{::t/- (t/Vec l/Numeric-Rhs)} values]
+                                 (if (some (fn [rhs]
+                                             (some #(and (= :local (:op %)) (contains? denied (:id %)))
+                                                   (origin-values (:types analysis) rhs))) values) (conj out id) out))
                                denied definitions)]
                     (if (= next denied) denied (recur next)))) initial)]
     (set/difference (set (keys definitions)) denied)))
diff --git a/src/com/tailrecursion/blacktide/compiler/passes/compact.clj b/src/com/tailrecursion/blacktide/compiler/passes/compact.clj
index 65824fd..a542ba5 100644
--- a/src/com/tailrecursion/blacktide/compiler/passes/compact.clj
+++ b/src/com/tailrecursion/blacktide/compiler/passes/compact.clj
@@ -9,16 +9,6 @@
             [com.tailrecursion.blacktide.compiler.jvm :as jvm]
             [typed.clojure :as-alias t]))
 
-(np/defpass introduce {:from [l/Stored Expr] :to [l/Compact Expr]}
-  [node]
-  :bind (assoc node :body (introduce (:body node)))
-  :join (assoc node :value (introduce (:value node)) :body (introduce (:body node)))
-  :branch (assoc node :yes (introduce (:yes node)) :no (introduce (:no node)))
-  :switch (assoc node :arms (mapv introduce (:arms node)))
-  :loop {:op :loop :bindings (mapv (fn [id] {:target id :value {:op :local :id id}}) (:slots node))
-         :body (introduce (:body node))}
-  :recur {:op :recur :args (mapv (fn [id] {:op :local :id id}) (:slots node))}
-  :return node :throw node)
 
 (np/defpasses
   (atom-reads {:from [l/Compact Atom] :to (t/Vec t/Sym)}
@@ -81,12 +71,18 @@
   [types rhs]
   (and (= :host (:op rhs))
        (let [operation (:operation rhs)]
-         (and (= :static (:op operation)) (= clojure.lang.Numbers (:class operation))
-              (contains? '#{lt lte gt gte equiv unchecked_add unchecked_minus unchecked_multiply
-                            unchecked_inc unchecked_dec unchecked_negate} (:member operation))
+         (and (= :static (:op operation))
+              (or (and (identical? clojure.lang.Numbers (:class operation))
+                       (contains? '#{lt lte gt gte equiv unchecked_add unchecked_minus unchecked_multiply
+                                     unchecked_inc unchecked_dec unchecked_negate} (:member operation)))
+                  (and (identical? clojure.lang.Util (:class operation)) (= 'equiv (:member operation))))
               (every? (fn [^{::t/- l/Compact-Operand} operand]
                         (let [type (atom-type types (:value operand))]
-                          (and (contains? #{Long/TYPE Double/TYPE} type) (= type (:type (:jvm operand))))))
+                          (and (contains? #{Long/TYPE Double/TYPE} type) (= type (:type (:jvm operand)))
+                               ;; An inlined operand can still throw. Moving a pure
+                               ;; comparison must not move its checked conversion.
+                               (or (not= :inline (:op (:value operand)))
+                                   (movable? types (:value (:value operand)))))))
                       (:args rhs))
               (let [type (jvm/host-type (mapv #(:type (:jvm %)) (:args rhs)) operation)]
                 (and (class? type) (.isPrimitive ^Class type) (not= Void/TYPE type)))))))
@@ -100,6 +96,10 @@
                ;; A bound reference must not become several independently boxed reads.
                (when (and (= type (atom-type types value))
                           (or type (= :local (:op value)))
+                          ;; Reading a primitive local boxes afresh; emitting its
+                          ;; literal at an Object use instead loads a pooled box.
+                          (or (not= :literal (:op value))
+                              (and (instance? Long (:value value)) (<= -128 (:value value) 127)))
                           (or (not= :inline (:op value)) (= uses 1))) value))
       :convert (let [conversion (:conversion rhs) operand (:value rhs)]
                  (when (and type (:parameter? conversion) (= type (:type conversion))
@@ -233,6 +233,6 @@
                      refs (rseq (:bindings node)))])
     :recur [node (reads node)] :return [node (reads node)] :throw [node (reads node)]))
 
-(np/defpass program {:from [l/Stored Program] :to [l/Compact Program] :body true}
+(np/defpass program {:from [l/Compact Program] :to [l/Compact Program] :body true}
   [program]
-  {:types (:types program) :body (first (simplify (:types program) (introduce (:body program))))})
+  {:types (:types program) :body (first (simplify (:types program) (:body program)))})
diff --git a/src/com/tailrecursion/blacktide/compiler/passes/emit.clj b/src/com/tailrecursion/blacktide/compiler/passes/emit.clj
index f9bb232..7960dac 100644
--- a/src/com/tailrecursion/blacktide/compiler/passes/emit.clj
+++ b/src/com/tailrecursion/blacktide/compiler/passes/emit.clj
@@ -52,8 +52,8 @@
   :branch (list 'if (atom-form (:test term))
                 (edge-form slots live (:yes term)) (edge-form slots live (:no term)))
   :switch (cases/arms-form (mapv #(edge-form slots live %) (:targets term)) (atom-form (:test term)))
-  :return (atom-form (:value term))
-  :throw (list 'throw (atom-form (:value term))))
+  :return (host/box-form (atom-form (:value term)))
+  :throw (host/box-form (list 'throw (atom-form (:value term)))))
 
 (np/defpass block-form
   {:from [l/Machine Block] :to [l/Machine Code]
@@ -74,4 +74,4 @@
                    (sort-by key (:blocks program)))]
     (list 'loop* bindings
           (list* 'clojure.core/case pc
-                 (conj arms (list 'throw (list 'clojure.core/ex-info "Invalid machine PC" {:pc pc})))))))
+                 (conj arms (host/box-form (list 'throw (list 'clojure.core/ex-info "Invalid machine PC" {:pc pc}))))))))
diff --git a/src/com/tailrecursion/blacktide/compiler/passes/graph.clj b/src/com/tailrecursion/blacktide/compiler/passes/graph.clj
index 381e5e3..a9fe93b 100644
--- a/src/com/tailrecursion/blacktide/compiler/passes/graph.clj
+++ b/src/com/tailrecursion/blacktide/compiler/passes/graph.clj
@@ -12,7 +12,7 @@
   :literal #{}
   :local #{(:id node)})
 
-(np/defpass rhs-reads {:from [l/CFG Rhs] :to (t/Set t/Sym)}
+(np/defpass rhs-reads {:from [l/Numeric Rhs] :to (t/Set t/Sym)}
   [node]
   :value (atom-reads (:value node))
   :global #{}
@@ -23,6 +23,7 @@
   :construct (into #{} (mapcat atom-reads) (:items node))
   :metadata (set/union (atom-reads (:value node)) (atom-reads (:metadata node)))
   :convert (atom-reads (:value (:value node)))
+  :numeric (into #{} (mapcat #(atom-reads (:value %))) (:args node))
   :host (into #{} (mapcat #(atom-reads (:value %))) (:args node))
   :invoke (into (atom-reads (:function node)) (mapcat atom-reads) (:args node)))
 
@@ -43,18 +44,18 @@
   :return []
   :throw [])
 
-(np/defpass block-facts {:from [l/CFG Block] :to [l/CFG BlockFacts] :body true}
+(np/defpass block-facts {:from [l/Numeric Block] :to [l/CFG BlockFacts] :body true}
   [block]
   (let [[reads defs]
         (reduce (fn [^{::t/- (t/HVec [(t/Set t/Sym) (t/Set t/Sym)])} acc
-                     ^{::t/- l/CFG-Operation} op]
+                     ^{::t/- l/Numeric-Operation} op]
                   (let [[reads defs] acc]
                     [(set/union reads (set/difference (rhs-reads (:value op)) defs))
                      (conj defs (:target op))])) [#{} #{}] (:ops block))]
     {:reads (set/union reads (set/difference (term-reads (:term block)) defs))
      :defs defs :successors (successors (:term block))}))
 
-(np/defpass collect-facts {:from [l/CFG Program] :to [l/CFG Facts] :body true}
+(np/defpass collect-facts {:from [l/Numeric Graph] :to [l/CFG Facts] :body true}
   [program]
   (update-vals (:blocks program) block-facts))
 
diff --git a/src/com/tailrecursion/blacktide/compiler/passes/joins.clj b/src/com/tailrecursion/blacktide/compiler/passes/joins.clj
index fd70633..673a392 100644
--- a/src/com/tailrecursion/blacktide/compiler/passes/joins.clj
+++ b/src/com/tailrecursion/blacktide/compiler/passes/joins.clj
@@ -8,13 +8,13 @@
             [com.tailrecursion.blacktide.compiler.passes.graph :as graph]
             [typed.clojure :as-alias t]))
 
-(np/defpass postdominators {:from [l/Machine Program] :to [l/Planned Postdominators] :body true}
+(np/defpass postdominators {:from [l/Numeric Program] :to [l/Planned Postdominators] :body true}
   [machine]
   (let [labels (set (keys (:blocks machine)))]
     ((fn ^{::t/- [l/Planned-Postdominators :-> l/Planned-Postdominators]} solve [known]
        (let [next (reduce-kv
                     (fn [^{::t/- l/Planned-Postdominators} out ^{::t/- l/Machine-Label} id
-                         ^{::t/- l/Machine-Block} block]
+                         ^{::t/- l/Numeric-Block} block]
                       (let [successors (graph/successors (:term block))
                             common (if (seq successors)
                                      (reduce set/intersection labels (map #(get known % #{}) successors)) #{})]
@@ -23,14 +23,14 @@
 
 (np/defpass region
   {:from [l/Machine Label] :to (t/Option l/Planned-Region)
-   :args [l/Machine-Program l/Machine-Label] :body true}
+   :args [l/Numeric-Program l/Machine-Label] :body true}
   [machine stop id]
   ;; Prove blocks only after every successor is proved. Each block contributes
   ;; once; shared paths do not exhaust a traversal budget. Cycles never qualify.
   ((fn ^{::t/- [l/Planned-Regions :-> (t/Option l/Planned-Region)]} solve [known]
      (let [next (reduce-kv
                   (fn [^{::t/- l/Planned-Regions} out ^{::t/- l/Machine-Label} label
-                       ^{::t/- l/Machine-Block} block]
+                       ^{::t/- l/Numeric-Block} block]
                     (let [successors (graph/successors (:term block))]
                       (if (and (not (contains? out label)) (seq successors)
                                (every? #(contains? out %) successors))
@@ -44,7 +44,7 @@
 
 (np/defpass candidate
   {:from [l/Machine Label] :to (t/Option l/Planned-Join)
-   :args [l/Machine-Program l/Planned-Postdominators] :body true}
+   :args [l/Numeric-Program l/Planned-Postdominators] :body true}
   [machine known id]
   (when-let [block (get (:blocks machine) id)]
     (let [term (:term block)
diff --git a/src/com/tailrecursion/blacktide/compiler/passes/lexical.clj b/src/com/tailrecursion/blacktide/compiler/passes/lexical.clj
new file mode 100644
index 0000000..50f8f8b
--- /dev/null
+++ b/src/com/tailrecursion/blacktide/compiler/passes/lexical.clj
@@ -0,0 +1,19 @@
+(ns ^:typed.clojure com.tailrecursion.blacktide.compiler.passes.lexical
+  "Expose loop bindings and simultaneous recur arguments for expression lowering."
+  (:require [com.tailrecursion.nanopass :as np]
+            [com.tailrecursion.blacktide.compiler.languages :as l]))
+
+(np/defpass introduce {:from [l/Represented Expr] :to [l/Lexical Expr]}
+  [node]
+  :bind (assoc node :body (introduce (:body node)))
+  :join (assoc node :value (introduce (:value node)) :body (introduce (:body node)))
+  :branch (assoc node :yes (introduce (:yes node)) :no (introduce (:no node)))
+  :switch (assoc node :arms (mapv introduce (:arms node)))
+  :loop {:op :loop :bindings (mapv (fn [id] {:target id :value {:op :local :id id}}) (:slots node))
+         :body (introduce (:body node))}
+  :recur {:op :recur :args (mapv (fn [id] {:op :local :id id}) (:slots node))}
+  :return node :throw node)
+
+
+(np/defpass program {:from [l/Represented Program] :to [l/Lexical Program] :body true}
+  [program] (assoc program :body (introduce (:body program))))
diff --git a/src/com/tailrecursion/blacktide/compiler/passes/numeric.clj b/src/com/tailrecursion/blacktide/compiler/passes/numeric.clj
new file mode 100644
index 0000000..c04abbe
--- /dev/null
+++ b/src/com/tailrecursion/blacktide/compiler/passes/numeric.clj
@@ -0,0 +1,59 @@
+(ns ^:typed.clojure com.tailrecursion.blacktide.compiler.passes.numeric
+  "Recognize numeric runtime calls and freeze their original signatures.
+  Value inference and representation selection consult the same semantic rules;
+  calls without a proof retain their original overload and operand facts."
+  (:require [com.tailrecursion.nanopass :as np]
+            [com.tailrecursion.blacktide.compiler.languages :as l]
+            [com.tailrecursion.blacktide.compiler.jvm :as jvm]
+            [com.tailrecursion.blacktide.compiler.passes.value-facts :as facts]
+            [com.tailrecursion.blacktide.compiler.passes.numeric-rules :as rules]
+            [typed.clojure :as-alias t]))
+
+(np/defpass conversion-call {:from [l/Machine Rhs] :to [l/Numeric Rhs] :body true}
+  [rhs]
+  (if (and (= :convert (:op rhs)) (:parameter? (:conversion rhs))
+           (not (:primitive? (:jvm (:value rhs)))))
+    (let [type (:type (:conversion rhs))
+          names (get {Byte/TYPE '[byteCast uncheckedByteCast] Short/TYPE '[shortCast uncheckedShortCast]
+                      Integer/TYPE '[intCast uncheckedIntCast] Long/TYPE '[longCast uncheckedLongCast]
+                      Float/TYPE '[floatCast uncheckedFloatCast] Double/TYPE '[doubleCast uncheckedDoubleCast]} type)]
+      (if names
+        {:op :numeric :args [(:value rhs)] :parameters [Object] :return type :conversion (:conversion rhs)
+         :operation {:op :static :class clojure.lang.RT :member (nth names (if *unchecked-math* 1 0)) :tags [Object]}}
+        rhs)) rhs))
+
+(np/defpass rhs {:from [l/Machine Rhs] :to [l/Numeric Rhs] :body true}
+  [rhs]
+  (if (and (= :host (:op rhs)) (= :static (:op (:operation rhs)))
+           (rules/family (:operation rhs)))
+    (let [operation (:operation rhs)
+          method (jvm/select-method (mapv #(:type (:jvm %)) (:args rhs)) (:tags operation)
+                                    (jvm/methods (:class operation) (count (:args rhs)) true (:member operation)))]
+      (if method (assoc rhs :op :numeric :parameters (jvm/parameters method) :return (jvm/return-type method)) rhs))
+    (conversion-call rhs)))
+
+(np/defpass operation {:from [l/Machine Operation] :to [l/Numeric Operation] :body true}
+  [operation] (assoc operation :value (rhs (:value operation))))
+
+(np/defpass block {:from [l/Machine Block] :to [l/Numeric Block] :body true}
+  [block] (update block :ops #(mapv operation %)))
+
+(np/defpass program {:from [l/Machine Program] :to [l/Numeric Program] :body true}
+  [program] (update program :blocks update-vals block))
+
+(np/defpass source-call {:from [l/Numeric Rhs] :to [l/Machine Rhs] :body true}
+  [rhs]
+  (if (= :numeric (:op rhs))
+    (if-let [conversion (:conversion rhs)]
+      {:op :convert :conversion conversion :value (nth (:args rhs) 0)}
+      (assoc (dissoc rhs :parameters :return) :op :host)) rhs))
+
+(np/defpass plan
+  {:from [l/Numeric Rhs] :to (t/Option l/Numeric-Plan) :args [l/Analysis-Types] :body true}
+  [types rhs]
+  (when (= :numeric (:op rhs))
+    (let [arguments (mapv #(facts/atom-type types (:value %)) (:args rhs))]
+      ;; JVM numeric parameter conversion casts to Number before calling RT.
+      ;; An unknown input (including Character) must retain that check.
+      (when (or (nil? (:conversion rhs)) (every? rules/number-type arguments))
+        (rules/plan arguments (:parameters rhs) (:return rhs) (:operation rhs))))))
diff --git a/src/com/tailrecursion/blacktide/compiler/passes/numeric_lower.clj b/src/com/tailrecursion/blacktide/compiler/passes/numeric_lower.clj
new file mode 100644
index 0000000..7c0a202
--- /dev/null
+++ b/src/com/tailrecursion/blacktide/compiler/passes/numeric_lower.clj
@@ -0,0 +1,142 @@
+(ns ^:typed.clojure com.tailrecursion.blacktide.compiler.passes.numeric-lower
+  "Realize numeric plans as primitive calls and explicit control. Saved operands
+  are already evaluated. Checks remain at the original operation; generic exits
+  retain their original overload, boxed identity and exception behavior."
+  (:require [com.tailrecursion.nanopass :as np]
+            [com.tailrecursion.blacktide.compiler.languages :as l]
+            [com.tailrecursion.blacktide.compiler.passes.numeric :as numeric]
+            [com.tailrecursion.blacktide.compiler.passes.value-facts :as facts]
+            [typed.clojure :as-alias t]))
+
+(np/defpass operand
+  {:from [l/Compact Atom] :to [l/Compact Operand] :args [l/JVM-Type] :body true}
+  [type value]
+  {:value value :jvm {:type type :primitive? (and (class? type) (.isPrimitive ^Class type))
+                      :hint nil :var-meta {} :hint-error nil}})
+
+(np/defpass call
+  {:from [l/JVM Operation] :to [l/Compact Operand]
+   :args [(t/Vec l/Compact-Operand) java.lang.Class] :body true}
+  [args result operation]
+  ;; Clojure only emits a few primitive widening conversions directly. Make
+  ;; numeric promotions explicit instead of boxing a long to pass it as double.
+  (let [args (if-let [parameters (:tags operation)]
+               (mapv (fn [^{::t/- l/Compact-Operand} arg ^{::t/- t/Any} parameter]
+                       (let [type (:type (:jvm arg))]
+                         (if (and (not= type parameter)
+                                  (or (and (= Long/TYPE parameter) (contains? #{Byte/TYPE Short/TYPE Integer/TYPE} type))
+                                      (and (= Double/TYPE parameter) (contains? #{Byte/TYPE Short/TYPE Integer/TYPE Long/TYPE Float/TYPE} type))))
+                           (call [arg] (if (= Long/TYPE parameter) (or Long/TYPE Long) (or Double/TYPE Double))
+                                 {:op :static :class clojure.lang.RT :member (if (= Long/TYPE parameter) 'longCast 'doubleCast)
+                                  :tags [(if (class? type) type Object)]}) arg))) args parameters) args)]
+    (operand result {:op :inline :type (when (.isPrimitive ^Class result) result)
+                     :value {:op :host :operation operation :args args}})))
+
+(np/defpass primitive
+  {:from [l/Numeric Plan] :to [l/Compact Operand]
+   :args [java.lang.Class t/Sym (t/Vec l/Compact-Operand)] :body true}
+  [owner member args plan]
+  (call args (:result plan) {:op :static :class owner :member member :tags (:parameters plan)}))
+
+(np/defpass returned {:from [l/Compact Operand] :to [l/Compact Expr] :body true}
+  [value] {:op :return :value (:value value)})
+
+(np/defpass branch
+  {:from [l/Compact Expr] :to [l/Compact Expr] :args [l/Compact-Operand l/Compact-Expr] :body true}
+  [test yes no] {:op :branch :test (:value test) :yes yes :no no})
+
+(np/defpass nonzero
+  {:from [l/Compact Expr] :to [l/Compact Expr] :args [l/Compact-Operand java.lang.Class] :body true}
+  [divisor type body]
+  (let [test (call [divisor] (or Boolean/TYPE Boolean)
+                   {:op :static :class clojure.lang.Numbers :member 'isZero :tags [type]})
+        error (call [(operand String {:op :literal :value "Divide by zero"})] ArithmeticException
+                    {:op :constructor :class ArithmeticException :tags [String]})]
+    (branch test {:op :throw :value (:value error)} body)))
+
+(np/defpass nan-returns
+  {:from [l/Compact Expr] :to [l/Compact Expr]
+   :args [(t/Vec l/Compact-Operand) (t/Vec java.lang.Class)] :body true}
+  [args parameters body]
+  (reduce (fn [^{::t/- l/Compact-Expr} out ^{::t/- t/Int} index]
+            (if (= Double/TYPE (nth parameters index))
+              (branch (call [(nth args index)] (or Boolean/TYPE Boolean)
+                            {:op :static :class Double :member 'isNaN :tags [Double/TYPE]})
+                      (returned (nth args index)) out) out))
+          body (reverse (range (count args)))))
+
+(np/defpass recipe
+  {:from [l/Numeric Rhs] :to [l/Compact Expr]
+   :args [l/Numeric-Plan l/Represented-Types] :body true}
+  [plan types rhs]
+  (if (= :numeric (:op rhs))
+    (let [args (mapv (fn [^{::t/- l/Numeric-Operand} arg]
+                      (let [type (facts/atom-type types (:value arg))]
+                        (operand (if (class? type) type :unknown) (:value arg)))) (:args rhs))
+          owner (:class (:operation rhs)) member (:member (:operation rhs))
+          parameters (:parameters plan) result (:result plan)
+          direct (fn [] (primitive owner member args plan))]
+      (case (:recipe plan)
+        :call (returned (direct))
+        :compare (let [test (fn [relation]
+                             (call args (or Boolean/TYPE Boolean)
+                                   {:op :static :class clojure.lang.Numbers :member relation :tags parameters}))
+                       value (fn [n] {:op :return :value {:op :literal :value n}})]
+                   (branch (test 'lt) (value -1) (branch (test 'gt) (value 1) (value 0))))
+        :widen-char (returned (call [(call args (or Integer/TYPE Integer)
+                                          {:op :static :class clojure.lang.RT :member 'intCast :tags [Character/TYPE]})]
+                                    result {:op :static :class clojure.lang.RT :member 'longCast :tags [Integer/TYPE]}))
+        (:negate-add :promoting-negate-add)
+        (let [promoting? (= :promoting-negate-add (:recipe plan))
+              unchecked? (= 'unchecked_minus member)
+              negative-type (if (and promoting? (= Long/TYPE (second parameters))) Number (or (second parameters) result))
+              negative (call [(nth args 1)] negative-type
+                             {:op :static :class owner :member member :tags [(second parameters)]})]
+          (returned (call [(nth args 0) negative] result
+                          {:op :static :class owner
+                           :member (cond promoting? 'addP unchecked? 'unchecked_add :else 'add)
+                           :tags [(first parameters) (if (= Number negative-type) Object negative-type)]})))
+        :zero-guard (nonzero (nth args 1) (or (second parameters) result) (returned (direct)))
+        :divide (nan-returns args parameters
+                            (nonzero (nth args 1) (or (second parameters) result) (returned (direct))))
+        :select (nan-returns args parameters
+                            (branch (call args (or Boolean/TYPE Boolean)
+                                          {:op :static :class owner :member (if (= 'max member) 'gt 'lt) :tags parameters})
+                                    (returned (nth args 0)) (returned (nth args 1))))
+        (:narrow-int :narrow-char :narrow-checked)
+        (let [char? (contains? '#{charCast uncheckedCharCast} member)
+              n (call args (or Long/TYPE Long)
+                      {:op :static :class clojure.lang.RT :member (if char? 'uncheckedLongCast 'longCast) :tags [Double/TYPE]})
+              narrowed (call [n] result {:op :static :class clojure.lang.RT
+                                         :member (case member byteCast 'uncheckedByteCast shortCast 'uncheckedShortCast
+                                                               charCast 'uncheckedCharCast member)
+                                         :tags [Long/TYPE]})]
+          (if (not= :narrow-checked (:recipe plan)) (returned narrowed)
+            (let [[lo hi] (case member byteCast [-128 127] shortCast [-32768 32767] charCast [0 65535])
+                  original (call (:args rhs) (:return rhs) (assoc (:operation rhs) :tags (:parameters rhs)))
+                  compare-bound (fn [relation bound]
+                                  (call [n (operand Long/TYPE {:op :literal :value bound})] (or Boolean/TYPE Boolean)
+                                        {:op :static :class clojure.lang.Numbers :member relation :tags [Long/TYPE Long/TYPE]}))]
+              (branch (compare-bound 'lt lo) (returned original)
+                      (branch (compare-bound 'gt hi) (returned original) (returned narrowed))))))))
+    (throw (IllegalStateException. "Numeric recipe requires a recognized call"))))
+
+(np/defpass expression {:from [l/Lexical Expr] :to [l/Compact Expr] :args [l/Represented-Types]}
+  [types node]
+  :bind (let [binding (:binding node) rhs (:value binding) target (:target binding)
+              body (expression types (:body node))
+              plan (numeric/plan types rhs)]
+          (if (and plan (or (:fresh? plan) (contains? types target)))
+            (let [value (recipe plan types rhs)]
+              (if (and (= :return (:op value)) (= :inline (:op (:value value))))
+                {:op :bind :binding {:target target :value (:value (:value value))} :body body}
+                {:op :join :target target :value value :body body}))
+            {:op :bind :binding {:target target :value (numeric/source-call rhs)} :body body}))
+  :join (assoc node :value (expression types (:value node)) :body (expression types (:body node)))
+  :branch (assoc node :yes (expression types (:yes node)) :no (expression types (:no node)))
+  :switch (assoc node :arms (mapv #(expression types %) (:arms node)))
+  :loop (assoc node :body (expression types (:body node)))
+  :recur node :return node :throw node)
+
+(np/defpass program {:from [l/Lexical Program] :to [l/Compact Program] :body true}
+  [program] (assoc program :body (expression (:types program) (:body program))))
diff --git a/src/com/tailrecursion/blacktide/compiler/passes/numeric_rules.clj b/src/com/tailrecursion/blacktide/compiler/passes/numeric_rules.clj
new file mode 100644
index 0000000..55c3303
--- /dev/null
+++ b/src/com/tailrecursion/blacktide/compiler/passes/numeric_rules.clj
@@ -0,0 +1,100 @@
+(ns ^:typed.clojure com.tailrecursion.blacktide.compiler.passes.numeric-rules
+  "Numeric equivalences depend on the original overload as well as value types.
+  Plans preserve checked arithmetic, promotion, zero checks and reference returns.
+  JVM primitive widths remain distinct; only arithmetic promotes their values."
+  (:require [com.tailrecursion.nanopass :as np]
+            [com.tailrecursion.blacktide.compiler.languages :as l]
+            [typed.clojure :as-alias t]))
+
+(np/defpass family {:from [l/JVM Operation] :to (t/Option t/Kw) :body true}
+  [operation]
+  (when (= :static (:op operation))
+    (let [owner (:class operation) member (:member operation)]
+      (cond
+        (identical? owner clojure.lang.Numbers)
+        (case member
+          (add multiply inc dec abs unchecked_add unchecked_multiply unchecked_inc unchecked_dec) :arithmetic
+          (minus unchecked_minus) :subtract
+          (addP multiplyP incP decP minusP) :promoting
+          divide :divide
+          (quotient remainder) :quotient
+          (min max) :select
+          (lt lte gt gte equiv isZero isPos isNeg) :predicate
+          compare :compare
+          (not and or xor andNot clearBit setBit flipBit testBit shiftLeft shiftRight unsignedShiftRight) :bit
+          nil)
+        (identical? owner clojure.lang.Util) (case member equiv :equality compare :compare nil)
+        (identical? owner clojure.lang.RT)
+        (case member
+          (byteCast shortCast intCast longCast floatCast doubleCast charCast
+           uncheckedByteCast uncheckedShortCast uncheckedIntCast uncheckedLongCast
+           uncheckedFloatCast uncheckedDoubleCast uncheckedCharCast) :cast
+          nil)))))
+
+(np/defpass number-type {:from [l/Numeric ValueType] :to (t/Option java.lang.Class) :body true}
+  [type]
+  (cond (contains? #{Byte/TYPE Short/TYPE Integer/TYPE Long/TYPE} type) Long/TYPE
+        (contains? #{Float/TYPE Double/TYPE} type) Double/TYPE))
+
+(np/defpass plan
+  {:from [l/JVM Operation] :to (t/Option l/Numeric-Plan)
+   :args [l/Numeric-ArgumentTypes (t/Vec java.lang.Class) java.lang.Class] :body true}
+  [types parameters result operation]
+  (when (= :static (:op operation))
+    (let [family (family operation) member (:member operation)
+          numbers (mapv number-type types)
+          numeric? (every? some? numbers)
+          tags (into [] (keep identity) numbers)
+          ints? (and numeric? (every? #{Long/TYPE} tags))
+          objects? (boolean (some #(not (.isPrimitive ^Class %)) parameters))
+          generic? (and objects? (not (some #(= Double/TYPE %) parameters)))
+          arithmetic-result (if (some #(= Double/TYPE %) tags) (or Double/TYPE result) (or (first tags) result))
+          direct {:recipe :call :parameters tags :result arithmetic-result :fresh? true}]
+      (case family
+        :arithmetic (when numeric? direct)
+        :subtract (when numeric?
+                    (if (and generic? (= 2 (count tags))) (assoc direct :recipe :negate-add) direct))
+        :promoting (when numeric?
+                     (cond-> (assoc direct :result (if ints? Number arithmetic-result))
+                       (and generic? (= 'minusP member) (= 2 (count tags)))
+                       (assoc :recipe :promoting-negate-add)))
+        :predicate (when numeric? (assoc direct :result result))
+        :compare (when numeric? (assoc direct :recipe :compare :result result))
+        :bit (when ints? (assoc direct :result result))
+        :quotient (when numeric?
+                    (cond-> direct (and objects? ints?) (assoc :recipe :zero-guard)))
+        :divide (when numeric?
+                  (cond ints? (assoc direct :result Number)
+                        generic? (assoc direct :recipe :divide :fresh? false
+                                        ;; A Float NaN is returned unchanged, while
+                                        ;; ordinary floating division yields Double.
+                                        :result (if (some #(= Float/TYPE %) types) Number arithmetic-result))
+                        :else direct))
+        :select (when (and numeric? (apply = types))
+                  (if objects?
+                    (assoc direct :recipe :select :result (or (first (filter class? types)) result) :fresh? false)
+                    direct))
+        :equality (when (or ints? (and numeric? (some #(= Double/TYPE %) parameters)))
+                    ;; Object/Object equality observes NaN aliasing. Mixed integer/
+                    ;; floating equality also differs from numeric equivalence.
+                    (when (apply = tags) (assoc direct :result result)))
+        :cast (when (and (= 1 (count types)) (or numeric? (= Character/TYPE (first types))))
+                (let [type (first types)
+                      actual (vec (filter class? types))
+                      direct (assoc direct :parameters actual :result result)]
+                  (if-not objects? (assoc direct :parameters parameters)
+                    (cond
+                      (and (not numeric?) (not (contains? '#{charCast intCast longCast uncheckedCharCast uncheckedIntCast} member))) nil
+                      (and (= Character/TYPE type) (= 'longCast member))
+                      (assoc direct :recipe :widen-char)
+                      (and (not ints?) numeric? (= 'intCast member)) (assoc direct :recipe :narrow-int)
+                      (and (not ints?) numeric? (= 'uncheckedCharCast member)) (assoc direct :recipe :narrow-char)
+                      (and (not ints?) numeric? (contains? '#{byteCast shortCast charCast} member))
+                      (assoc direct :recipe :narrow-checked)
+                      ;; Object floatCast first converts to double (except Float).
+                      ;; Object longCast converts floating inputs through double.
+                      (or (and (= 'floatCast member) (not= Float/TYPE type))
+                          (and (= 'longCast member) (not ints?) numeric?))
+                      (assoc direct :parameters (if-let [double-type Double/TYPE] [double-type] []))
+                      :else direct))))
+        nil))))
diff --git a/src/com/tailrecursion/blacktide/compiler/passes/results.clj b/src/com/tailrecursion/blacktide/compiler/passes/results.clj
new file mode 100644
index 0000000..87ae959
--- /dev/null
+++ b/src/com/tailrecursion/blacktide/compiler/passes/results.clj
@@ -0,0 +1,22 @@
+(ns ^:typed.clojure com.tailrecursion.blacktide.compiler.passes.results
+  "Place the public Object boundary at exits, not around the whole region.
+  This leaves tail loops in tail position; Clojure otherwise wraps an expression
+  loop in a function. A join's result belongs to its enclosing computation."
+  (:require [com.tailrecursion.nanopass :as np]
+            [com.tailrecursion.blacktide.compiler.languages :as l]
+            [typed.clojure :as-alias t]))
+
+(np/defpass expression {:from [l/Compact Expr] :to [l/Sealed Expr] :args [t/Bool]}
+  [public? node]
+  :bind (assoc node :body (expression public? (:body node)))
+  :effect (assoc node :body (expression public? (:body node)))
+  :join (assoc node :value (expression false (:value node)) :body (expression public? (:body node)))
+  :branch (assoc node :yes (expression public? (:yes node)) :no (expression public? (:no node)))
+  :switch (assoc node :arms (mapv #(expression public? %) (:arms node)))
+  :loop (assoc node :body (expression public? (:body node)))
+  :recur node
+  :return (if public? (assoc node :op :result) node)
+  :throw (if public? (assoc node :op :raise) node))
+
+(np/defpass program {:from [l/Compact Program] :to [l/Sealed Program] :body true}
+  [program] (assoc program :body (expression true (:body program))))
diff --git a/src/com/tailrecursion/blacktide/compiler/passes/storage.clj b/src/com/tailrecursion/blacktide/compiler/passes/storage.clj
index 887ad3e..9f12626 100644
--- a/src/com/tailrecursion/blacktide/compiler/passes/storage.clj
+++ b/src/com/tailrecursion/blacktide/compiler/passes/storage.clj
@@ -8,6 +8,7 @@
             [com.tailrecursion.blacktide.compiler.languages :as l]
             [com.tailrecursion.blacktide.compiler.passes.graph :as graph]
             [com.tailrecursion.blacktide.compiler.passes.native :as native]
+            [com.tailrecursion.blacktide.compiler.passes.numeric :as numeric]
             [com.tailrecursion.blacktide.compiler.passes.value-facts :as facts]
             [com.tailrecursion.blacktide.compiler.passes.box-origins :as origins]
             [typed.clojure :as-alias t]))
@@ -21,22 +22,14 @@
   :loop (into (loop-slots (:body node)) (:slots node))
   :recur #{} :return #{} :throw #{})
 
-(np/defpass cyclic? {:from [l/Joined Expr] :to t/Bool}
-  [node]
-  :bind (cyclic? (:body node))
-  :join (or (cyclic? (:value node)) (cyclic? (:body node)))
-  :branch (or (cyclic? (:yes node)) (cyclic? (:no node)))
-  :switch (boolean (some cyclic? (:arms node)))
-  :loop true :recur true :return false :throw false)
-
 (np/defpass operand-boxes
-  {:from [l/Machine Operand] :to (t/Set t/Sym) :args [l/Stored-Types] :body true}
+  {:from [l/Machine Operand] :to (t/Set t/Sym) :args [l/Represented-Types] :body true}
   [types operand]
   (let [type (facts/atom-type types (:value operand))]
     (if (and (class? type) (= type (:type (:jvm operand)))) #{} (graph/atom-reads (:value operand)))))
 
 (np/defpass operation-boxes
-  {:from [l/Machine Operation] :to (t/Set t/Sym) :args [l/Stored-Types (t/Set t/Sym)] :body true}
+  {:from [l/Numeric Operation] :to (t/Set t/Sym) :args [l/Represented-Types (t/Set t/Sym)] :body true}
   [types observed operation]
   (let [rhs (:value operation)]
     (case (:op rhs)
@@ -45,6 +38,12 @@
                  (if-let [source (origins/copy-source rhs)]
                    (if (contains? types source) #{} #{(:target operation)}) #{})
                  (graph/atom-reads (:value rhs))))
+      :numeric (let [plan (numeric/plan types rhs)]
+                 (if (and plan (or (:fresh? plan) (contains? types (:target operation)))) #{}
+                   (let [source (numeric/source-call rhs)]
+                     (cond-> (into (if plan (graph/rhs-reads rhs) #{}) (mapcat #(operand-boxes types %)) (:args rhs))
+                       (not= (get types (:target operation)) (facts/rhs-type {} source))
+                       (conj (:target operation))))))
       :host (if (#{:adapt} (:op (:operation rhs))) (graph/rhs-reads rhs)
                 (into #{} (mapcat #(operand-boxes types %)) (:args rhs)))
       :convert (let [conversion (:conversion rhs)]
@@ -55,18 +54,18 @@
       (graph/rhs-reads rhs))))
 
 (np/defpass observed-values
-  {:from [l/Machine Program] :to (t/Set t/Sym) :body true}
+  {:from [l/Numeric Program] :to (t/Set t/Sym) :body true}
   [machine]
   (let [ops (mapcat :ops (vals (:blocks machine)))
         initial (into (into #{} (mapcat #(graph/term-reads (:term %))) (vals (:blocks machine)))
                       (mapcat #(if (= :value (:op (:value %))) #{} (graph/rhs-reads (:value %)))) ops)]
     ((fn ^{::t/- [(t/Set t/Sym) :-> (t/Set t/Sym)]} solve [observed]
-       (let [next (reduce (fn [^{::t/- (t/Set t/Sym)} out ^{::t/- l/Machine-Operation} op]
+       (let [next (reduce (fn [^{::t/- (t/Set t/Sym)} out ^{::t/- l/Numeric-Operation} op]
                             (if (contains? observed (:target op)) (into out (graph/rhs-reads (:value op))) out)) observed ops)]
          (if (= observed next) observed (recur next)))) initial)))
 
 (np/defpass term-boxes
-  {:from [l/Machine Term] :to (t/Set t/Sym) :args [l/Stored-Types (t/Set t/Sym)] :body true}
+  {:from [l/Machine Term] :to (t/Set t/Sym) :args [l/Represented-Types (t/Set t/Sym)] :body true}
   [types reboxable term]
   (case (:op term)
     :return (if (and (= :local (:op (:value term))) (contains? reboxable (:id (:value term))))
@@ -76,21 +75,19 @@
     (graph/term-reads term)))
 
 (np/defpass select-storage
-  {:from [l/Joined Expr] :to [l/Stored Program] :args [l/Analysis-Program] :body true}
+  {:from [l/Joined Expr] :to [l/Represented Program] :args [l/Analysis-Program] :body true}
   [analysis expr]
-  ;; Clojure wraps an expression-position loop in an Object-returning call.
-  ;; Acyclic code has no such boundary: keep its return boxed so outer numeric
-  ;; overloads and native loop promotions cannot change after storage selection.
-  (let [reboxable (if (cyclic? expr) (origins/reboxable-values analysis) #{})
+  ;; The results pass preserves the public Object boundary at every exit.
+  (let [reboxable (origins/reboxable-values analysis)
         slots (loop-slots expr)
         initial (reduce-kv
-                  (fn [^{::t/- l/Stored-Types} out ^{::t/- t/Sym} id ^{::t/- l/Analysis-Type} type]
+                  (fn [^{::t/- l/Represented-Types} out ^{::t/- t/Sym} id ^{::t/- l/Analysis-Type} type]
                     (if (and (class? type) (or (not (contains? slots id)) (#{Long/TYPE Double/TYPE} type)))
                       (assoc out id type) out)) {} (:types analysis))
         machine (update (:machine analysis) :blocks #(select-keys % (:reachable analysis)))
         observed (observed-values machine)
         blocks (vals (:blocks machine))
-        types ((fn ^{::t/- [l/Stored-Types :-> l/Stored-Types]} solve [types]
+        types ((fn ^{::t/- [l/Represented-Types :-> l/Represented-Types]} solve [types]
                  (let [boxed (into (into #{} (mapcat #(operation-boxes types observed %)) (mapcat :ops blocks))
                                    (mapcat #(term-boxes types reboxable (:term %))) blocks)
                        next (apply dissoc types boxed)]
diff --git a/src/com/tailrecursion/blacktide/compiler/passes/structure.clj b/src/com/tailrecursion/blacktide/compiler/passes/structure.clj
index 46216ef..284249d 100644
--- a/src/com/tailrecursion/blacktide/compiler/passes/structure.clj
+++ b/src/com/tailrecursion/blacktide/compiler/passes/structure.clj
@@ -8,13 +8,13 @@
             [typed.clojure :as-alias t]))
 
 (np/defpass block
-  {:from [l/Machine Label] :to [l/Machine Block] :args [l/Machine-Program] :body true}
+  {:from [l/Machine Label] :to [l/Numeric Block] :args [l/Numeric-Program] :body true}
   [machine id]
   (or (get (:blocks machine) id) (throw (IllegalStateException. "Missing checked block"))))
 
 (np/defpass scan
   {:from [l/Machine Label] :to [l/Joined Scan]
-   :args [l/Machine-Program (t/Set l/Machine-Label) l/Joined-Scan] :body true}
+   :args [l/Numeric-Program (t/Set l/Machine-Label) l/Joined-Scan] :body true}
   [machine path state id]
   (let [[seen headers] state]
     (cond (contains? path id) [seen (conj headers id)]
@@ -29,7 +29,7 @@
   :local true
   :literal (nil? (:value atom)))
 
-(np/defpass harmless-block? {:from [l/Machine Block] :to t/Bool :body true}
+(np/defpass harmless-block? {:from [l/Numeric Block] :to t/Bool :body true}
   [block]
   ;; Lowering leaves nil result copies after transfers. No host/native form or
   ;; arbitrary quoted constant may disappear before Clojure validates it.
@@ -42,9 +42,9 @@
            (:branch :switch) (harmless-atom? (:test term))))))
 
 (np/defpass wrap
-  {:from [l/Machine Block] :to [l/Joined Expr] :args [l/Joined-Expr] :body true}
+  {:from [l/Numeric Block] :to [l/Joined Expr] :args [l/Joined-Expr] :body true}
   [end block]
-  (reduce (fn [^{::t/- l/Joined-Expr} body ^{::t/- l/Machine-Operation} op]
+  (reduce (fn [^{::t/- l/Joined-Expr} body ^{::t/- l/Numeric-Operation} op]
             {:op :bind :binding op :body body}) end (reverse (:ops block))))
 
 (np/defpasses
@@ -113,7 +113,7 @@
         :else (body ctx inside? budget id)))))
 
 (np/defpass construction-site?
-  {:from [l/Machine Rhs] :to t/Bool :body true}
+  {:from [l/Numeric Rhs] :to t/Bool :body true}
   [rhs]
   (case (:op rhs)
     :native true
@@ -130,7 +130,7 @@
     false))
 
 (np/defpass site-failure
-  {:from [l/Machine Program] :to (t/Option ':native-sites)
+  {:from [l/Numeric Program] :to (t/Option ':native-sites)
    :args [(t/Vec l/Machine-Label)] :body true}
   [blocks machine]
   (let [copies (frequencies blocks)
diff --git a/src/com/tailrecursion/blacktide/compiler/passes/structured_emit.clj b/src/com/tailrecursion/blacktide/compiler/passes/structured_emit.clj
index 6b9ed9d..a403479 100644
--- a/src/com/tailrecursion/blacktide/compiler/passes/structured_emit.clj
+++ b/src/com/tailrecursion/blacktide/compiler/passes/structured_emit.clj
@@ -19,7 +19,7 @@
   (list (with-meta (symbol "clojure.lang.RT" (str (.getName type) "Cast")) {:param-tags [type]}) form))
 
 (np/defpass binding-form
-  {:from [l/Machine Code] :to [l/Machine Code] :args [l/Stored-Types t/Sym (t/Option java.lang.Class)] :body true}
+  {:from [l/Machine Code] :to [l/Machine Code] :args [l/Represented-Types t/Sym (t/Option java.lang.Class)] :body true}
   [types id actual form]
   (if-let [type (get types id)] (if (= type actual) form (primitive-form type form)) (host/box-form form)))
 
@@ -75,9 +75,9 @@
   (binding-form types (:target op) (rhs-type types (:value op)) (rhs-form types (:value op))))
 
 (np/defpasses
-  (let-form {:from [l/Compact Expr] :to [l/Machine Code] :args [l/Compact-Types] :body true}
+  (let-form {:from [l/Sealed Expr] :to [l/Machine Code] :args [l/Compact-Types] :body true}
     [types node]
-    ((fn ^{::t/- [(t/Vec t/Any) l/Compact-Expr :-> l/Machine-Code]} bindings [pairs node]
+    ((fn ^{::t/- [(t/Vec t/Any) l/Sealed-Expr :-> l/Machine-Code]} bindings [pairs node]
        (case (:op node)
          :bind (let [op (:binding node)]
                  (recur (conj pairs (:target op) (operation-form types op)) (:body node)))
@@ -85,7 +85,7 @@
                             (binding-form types (:target node) nil (expression types (:value node)))) (:body node))
          (list 'let* pairs (expression types node)))) [] node))
 
-  (expression {:from [l/Compact Expr] :to [l/Machine Code] :args [l/Compact-Types]}
+  (expression {:from [l/Sealed Expr] :to [l/Machine Code] :args [l/Compact-Types]}
     [types node]
     :bind (let-form types node)
     :effect (let [binding (:binding node) rhs (:value binding) type (get types (:target binding))
@@ -105,4 +105,6 @@
               ;; Tail compaction must retain the region's opaque result type.
               (if (and (= :inline (:op value)) (= :native (:op (:value value))))
                 (host/box-form form) form))
+    :result (host/box-form (atom-form types (:value node)))
+    :raise (host/box-form (list 'throw (atom-form types (:value node))))
     :throw (list 'throw (atom-form types (:value node)))))
diff --git a/src/com/tailrecursion/blacktide/compiler/passes/value_facts.clj b/src/com/tailrecursion/blacktide/compiler/passes/value_facts.clj
index dd45f4d..297acfa 100644
--- a/src/com/tailrecursion/blacktide/compiler/passes/value_facts.clj
+++ b/src/com/tailrecursion/blacktide/compiler/passes/value_facts.clj
@@ -1,9 +1,11 @@
 (ns ^:typed.clojure com.tailrecursion.blacktide.compiler.passes.value-facts
-  "Prove primitive results across all reachable definitions, including copy
-  cycles. Hints describe consumers; only actual primitive producers prove values."
+  "Prove scalar values across reachable definitions and copy cycles. Numeric
+  calls may carry long values in boxes; storage selection decides whether those
+  boxes can disappear. Source JVM facts remain unchanged."
   (:require [com.tailrecursion.nanopass :as np]
             [com.tailrecursion.blacktide.compiler.languages :as l]
             [com.tailrecursion.blacktide.compiler.jvm :as jvm]
+            [com.tailrecursion.blacktide.compiler.passes.numeric-rules :as rules]
             [com.tailrecursion.blacktide.compiler.passes.graph :as graph]
             [typed.clojure :as-alias t]))
 
@@ -23,7 +25,7 @@
                  (instance? Double (:value node)) (primitive Double/TYPE)
                  :else :boxed))
 
-(np/defpass rhs-type {:from [l/Machine Rhs] :to [l/Analysis Type] :args [l/Analysis-Types]}
+(np/defpass rhs-type {:from [l/Numeric Rhs] :to [l/Analysis Type] :args [l/Analysis-Types]}
   [types rhs]
   :value (atom-type types (:value rhs))
   :external (if (:primitive? (:jvm rhs)) (primitive (:type (:jvm rhs))) :boxed)
@@ -31,6 +33,12 @@
   :dispatch (primitive Long/TYPE)
   :host (if (#{:adapt} (:op (:operation rhs))) :boxed
             (primitive (jvm/host-type (mapv #(:type (:jvm %)) (:args rhs)) (:operation rhs))))
+  :numeric (let [actual (primitive (:return rhs))
+                 args (mapv #(atom-type types (:value %)) (:args rhs))]
+             (if (class? actual) actual
+               (if-let [plan (rules/plan args (:parameters rhs) (:return rhs) (:operation rhs))]
+                 (primitive (:result plan))
+                 (if (and (some #{:bottom} args) (not (some #{:boxed} args))) :bottom :boxed))))
   :native :boxed
   :global :boxed
   :var :boxed
@@ -39,9 +47,9 @@
   :invoke :boxed)
 
 (np/defpass definitions
-  {:from [l/Machine Program] :to [l/Analysis Definitions] :args [(t/Set l/Machine-Label)] :body true}
+  {:from [l/Numeric Program] :to [l/Analysis Definitions] :args [(t/Set l/Machine-Label)] :body true}
   [reachable machine]
-  (reduce (fn [^{::t/- l/Analysis-Definitions} out ^{::t/- l/Machine-Operation} op]
+  (reduce (fn [^{::t/- l/Analysis-Definitions} out ^{::t/- l/Numeric-Operation} op]
             (assoc out (:target op) (conj (get out (:target op) []) (:value op))))
           {} (mapcat :ops (vals (select-keys (:blocks machine) reachable)))))
 
@@ -49,7 +57,7 @@
   [definitions]
   ((fn ^{::t/- [l/Analysis-Types :-> l/Analysis-Types]} fixed-point [types]
      (let [next (reduce-kv
-                  (fn [^{::t/- l/Analysis-Types} out ^{::t/- t/Sym} id ^{::t/- (t/Vec l/Machine-Rhs)} values]
+                  (fn [^{::t/- l/Analysis-Types} out ^{::t/- t/Sym} id ^{::t/- (t/Vec l/Numeric-Rhs)} values]
                     (assoc out id
                       ((fn ^{::t/- [t/Int l/Analysis-Type :-> l/Analysis-Type]} common [index type]
                          (if (< index (count values))
@@ -57,7 +65,7 @@
                        0 :bottom))) {} definitions)]
        (if (= types next) next (recur next)))) {}))
 
-(np/defpass analyze {:from [l/Machine Program] :to [l/Analysis Program] :body true}
+(np/defpass analyze {:from [l/Numeric Program] :to [l/Analysis Program] :body true}
   [machine]
   (let [reachable (graph/reachable (graph/collect-facts {:entry (:entry machine) :blocks (:blocks machine)}) (:entry machine))]
     {:machine machine :reachable reachable :types (solve (definitions reachable machine))}))
diff --git a/test/com/tailrecursion/blacktide/backend_test.clj b/test/com/tailrecursion/blacktide/backend_test.clj
index 6b1cd5b..99b12a5 100644
--- a/test/com/tailrecursion/blacktide/backend_test.clj
+++ b/test/com/tailrecursion/blacktide/backend_test.clj
@@ -11,6 +11,7 @@
             [com.tailrecursion.blacktide.compiler.passes.storage :as storage]
             [com.tailrecursion.blacktide.compiler.passes.compact :as compact]
             [com.tailrecursion.blacktide.compiler.passes.value-facts :as facts]
+            [com.tailrecursion.blacktide.compiler.passes.numeric :as numeric]
             [com.tailrecursion.blacktide.compiler.passes.box-origins :as origins]
             [com.tailrecursion.blacktide.compiler.passes.graph :as graph]
             [com.tailrecursion.blacktide.compiler.jvm :as jvm]
@@ -20,7 +21,8 @@
 
 (defn compile-program [form mode]
   (binding [*ns* (the-ns 'com.tailrecursion.blacktide.backend-test)]
-    (with-redefs [compiler/compile-program (if (= mode :dispatcher)
+    (with-redefs [numeric/program (if (= mode :generic) identity numeric/program)
+                  compiler/compile-program (if (= mode :dispatcher)
                                                   emit/program-form
                                                   compiler/compile-program)]
       (eval (list 'fn '[events] form)))))
@@ -50,7 +52,8 @@
     @selected))
 
 (defmacro local-class [name]
-  (list 'quote (.getJavaClass ^clojure.lang.Compiler$LocalBinding (get &env name))))
+  (let [^clojure.lang.Compiler$LocalBinding binding (get &env name)]
+    (list 'quote (if (.hasJavaClass binding) (.getJavaClass binding) Object))))
 
 (deftest compaction-carries-free-read-counts
   (let [x (m/local 'x) y (m/local 'y) result {:op :return :value x}
@@ -144,7 +147,7 @@
     (let [literal (Long. (long n)) cached? (<= -128 n 127)
           form (list 'loophole ['i 0 'x literal]
                      '(while (< i 2) (setq i (inc i))) 'x)]
-      (is (= cached? (origins/reboxable? {:op :value :value (m/literal literal)})))
+      (is (= cached? (origins/reboxable? {} {:op :value :value (m/literal literal)})))
       (doseq [mode [:default :dispatcher]]
         (let [f (compile-program form mode) first-value (f nil)]
           (is (= n first-value))
diff --git a/test/com/tailrecursion/blacktide/check.clj b/test/com/tailrecursion/blacktide/check.clj
index a850174..d343df1 100644
--- a/test/com/tailrecursion/blacktide/check.clj
+++ b/test/com/tailrecursion/blacktide/check.clj
@@ -69,3 +69,12 @@
     (probes/accepts? 'com.tailrecursion.blacktide.compiler.languages/Cases-Node (assoc node :op :select) true)
     (probes/accepts? 'com.tailrecursion.blacktide.compiler.languages/CFG-Term
                     {:op :switch :test {:op :literal :value 0} :targets [1 2]} true)))
+
+(deftest numeric-representation-boundary
+  (let [call {:op :numeric :operation {:op :static :class clojure.lang.Numbers :member 'add :tags nil} :args [] :parameters [] :return Number}
+        expr {:op :bind :binding {:target 'x :value call}
+              :body {:op :return :value {:op :local :id 'x}}}]
+    (probes/accepts? 'com.tailrecursion.blacktide.compiler.languages/Numeric-Rhs call true)
+    (probes/accepts? 'com.tailrecursion.blacktide.compiler.languages/Machine-Rhs call false)
+    (probes/accepts? 'com.tailrecursion.blacktide.compiler.languages/Represented-Expr expr true)
+    (probes/accepts? 'com.tailrecursion.blacktide.compiler.languages/Compact-Expr expr false)))
diff --git a/test/com/tailrecursion/blacktide/generated_test.clj b/test/com/tailrecursion/blacktide/generated_test.clj
index 823bad3..39a0125 100644
--- a/test/com/tailrecursion/blacktide/generated_test.clj
+++ b/test/com/tailrecursion/blacktide/generated_test.clj
@@ -9,7 +9,9 @@
             [com.tailrecursion.blacktide :refer [loophole label goto setq psetq]]
             [com.tailrecursion.blacktide.backend-test :as backend]
             [com.tailrecursion.blacktide.compiler.passes.structure :as structure]
-            [com.tailrecursion.blacktide.compiler.passes.storage :as storage]))
+            [com.tailrecursion.blacktide.compiler.passes.storage :as storage]
+            [com.tailrecursion.blacktide.compiler.passes.numeric :as numeric]
+            [com.tailrecursion.blacktide.compiler.passes.numeric-lower :as numeric-lower]))
 
 (defn three-steps [x k] (+ x (* 3 k)))
 
@@ -94,18 +96,27 @@
 
 (def configuration
   (gen/let [representation (gen/elements [:boxed :primitive :hinted :literal])
-            scalar? gen/boolean native-result? gen/boolean
+            scalar? gen/boolean native-result? gen/boolean numeric-only? gen/boolean
             limit (gen/choose 0 6) cut (gen/choose 0 8)
             x (gen/choose -15 15) y (gen/choose -15 15)
-            steps (gen/vector (gen/tuple (gen/elements operations) (gen/choose -4 4)) 0 5)]
+            steps (gen/vector (gen/tuple (gen/elements (if numeric-only? [:case :snapshot :shadow :cast] operations)) (gen/choose -4 4)) 0 5)]
     {:numeric? (not= :boxed representation) :hinted? (= :hinted representation)
      :literal-init? (= :literal representation) :scalar? scalar? :native-result? native-result?
      :limit limit :cut cut :x x :y y :steps steps}))
 
 (deftest generated-backend-equivalence
   (let [seed 618033 coverage (atom {}) recover structure/recover
-        choose storage/select-storage]
-    (with-redefs [structure/recover (fn [analysis]
+        choose storage/select-storage lower numeric-lower/program]
+    (with-redefs [numeric-lower/program
+                  (fn [program]
+                    (when (some #(and (map? %) (= :numeric (:op %))
+                                      (= 'add (:member (:operation %)))
+                                      (numeric/plan (:types program) %)
+                                      (some (fn [operand] (not= Long/TYPE (:type (:jvm operand)))) (:args %)))
+                                (tree-seq coll? seq (:body program)))
+                      (swap! coverage update :specialized-add (fnil inc 0)))
+                    (lower program))
+                  structure/recover (fn [analysis]
                                     (let [out (recover analysis)]
                                       (when (and (= :structured (:op out))
                                                  (empty? (second (structure/scan (:machine analysis) #{} [#{} #{}]
@@ -126,10 +137,11 @@
                        (let [expected (model config)]
                          (every? true?
                            (for [control [:linear :goto :recur :nested]
-                                 renamed? [false true] mode [:default :dispatcher]]
+                                 renamed? [false true] mode [:default :generic :dispatcher]]
                              (= expected (outcome config control renamed? mode))))))
                      :seed seed)]
         (is (:pass? result) (pr-str result))))
+    (is (pos? (get @coverage :specialized-add 0)) (str @coverage))
     (is (pos? (get @coverage :structured 0)) (str @coverage))
     (is (pos? (get @coverage :acyclic 0)) (str @coverage))
     (is (pos? (get @coverage :cycles 0)) (str @coverage))
diff --git a/test/com/tailrecursion/blacktide/numeric_test.clj b/test/com/tailrecursion/blacktide/numeric_test.clj
new file mode 100644
index 0000000..c95756a
--- /dev/null
+++ b/test/com/tailrecursion/blacktide/numeric_test.clj
@@ -0,0 +1,221 @@
+(ns com.tailrecursion.blacktide.numeric-test
+  "Numeric value proofs, primitive lowering, and the observations that forbid it."
+  (:require [clojure.test :refer [deftest is]]
+            [clojure.math]
+            [clojure.test.check :as tc]
+            [clojure.test.check.generators :as gen]
+            [clojure.test.check.properties :as prop]
+            [com.tailrecursion.blacktide.backend-test :as backend]
+            [com.tailrecursion.blacktide.compiler.passes.storage :as storage]))
+
+(def modes [:default :generic :dispatcher])
+
+(deftest accumulator-recurrence-is-primitive
+  (let [form '(loophole [sum 0]
+                (dotimes [i 10] (when (= i 5) (goto done)) (setq sum (+ sum i)))
+                (label done) sum)
+        program (backend/stored form)
+        slots (storage/loop-slots (:body program))
+        code (backend/compacted form)
+        adds (filter #(and (map? %) (= :host (:op %)) (= 'add (:member (:operation %))))
+                     (tree-seq coll? seq (:body code)))]
+    (is (= 2 (count slots)))
+    (is (= (zipmap slots (repeat Long/TYPE)) (select-keys (:types program) slots)))
+    (is (= 1 (count adds)))
+    (is (= [Long/TYPE Long/TYPE] (:tags (:operation (first adds)))))
+    (is (every? #(= Long/TYPE (:type (:jvm %))) (:args (first adds))))
+    (doseq [mode modes] (is (= {:value 10 :trace []} (backend/execution form mode))))))
+
+(def unary
+  '[+ * - / -' inc dec inc' dec' abs zero? pos? neg? bit-not
+    unchecked-negate unchecked-inc unchecked-dec unchecked-negate-int unchecked-inc-int unchecked-dec-int
+    byte short int long float double char unchecked-byte unchecked-short
+    unchecked-int unchecked-long unchecked-float unchecked-double unchecked-char
+    bigint biginteger bigdec rationalize numerator denominator
+    rational? integer? float? double? int? pos-int? neg-int? nat-int? decimal? ratio? number? even? odd?])
+
+(def binary
+  '[+ - * / +' -' *' quot rem mod min max = == < <= > >=
+    unchecked-add unchecked-subtract unchecked-multiply unchecked-add-int unchecked-subtract-int
+    unchecked-multiply-int unchecked-divide-int unchecked-remainder-int compare
+    bit-and bit-or bit-xor bit-and-not bit-clear bit-set bit-flip bit-test
+    bit-shift-left bit-shift-right unsigned-bit-shift-right])
+
+(def boundaries
+  {'long [Long/MIN_VALUE (inc Long/MIN_VALUE) -129 -1 0 1 63 127 128 65536
+          9007199254740993 4611686293305294849 Long/MAX_VALUE]
+   'byte [-128 -1 0 1 127]
+   'short [-32768 -129 -1 0 1 127 32767]
+   'int [Integer/MIN_VALUE -129 -1 0 1 127 128 Integer/MAX_VALUE]
+   'double [Double/NEGATIVE_INFINITY (- (double Long/MAX_VALUE)) -32768.9 -128.9 -1.0 -0.0 0.0 1.0
+            127.9 32767.9 65535.9 2147483647.9 4294967296.0 (double Long/MAX_VALUE)
+            Double/MAX_VALUE Double/POSITIVE_INFINITY Double/NaN]
+   'float [Float/NEGATIVE_INFINITY (- Float/MAX_VALUE) -128.9 -1 -0.0 0.0 1.0 127.9
+           2147483648.0 Float/MAX_VALUE Float/POSITIVE_INFINITY Float/NaN]
+   'char [0 1 127 255 65535]
+   'identity [nil true \a 1/2 1N 1M 1.00M 9223372036854775808N (biginteger 1)]})
+
+(defn outcome [f input]
+  (try (let [value (f input)]
+         [(class value) (cond (instance? Double value) (Double/doubleToLongBits value)
+                              (instance? Float value) (Float/floatToIntBits value)
+                              (instance? BigDecimal value) (.toString ^BigDecimal value)
+                              :else value)])
+       (catch Throwable error
+         ;; Helpful NPE text includes generated local names, which differ by backend.
+         [(class error) (when-not (instance? NullPointerException error) (ex-message error))])))
+
+(defn boxed [form]
+  (list (with-meta 'clojure.lang.RT/box {:param-tags [Object]}) form))
+
+(deftest numeric-surface
+  ;; Compile each shape once, then exercise boundaries. The ordinary Clojure
+  ;; oracle explicitly boxes its locals, matching mutable source-local reads.
+  ;; Canonical NaN bits ignore payloads while still distinguishing signed zero.
+  (doseq [[left right] '[[long long] [double double] [long double] [double long]
+                         [float float] [int int] [long int] [byte byte] [short short] [char char] [identity identity]]
+          expression (concat (map #(list % 'x) unary) (map #(list % 'x 'y) binary)
+                             (map #(list % 'x 'y 'x) '[+ - * / +' -' *' min max < <= > >= = ==]))
+          :let [bindings ['x (list left '(nth events 0)) 'y (list right '(nth events 1))]
+                form (list 'loophole bindings expression)
+                reference (backend/compile-program
+                            (list 'let (vec (mapcat (fn [[id value]] [id (boxed value)]) (partition 2 bindings)))
+                                  expression) :default)
+                functions (mapv #(backend/compile-program form %) modes)
+                inputs (for [x (boundaries left)
+                             y (if (= 2 (count expression)) [(first (boundaries right))] (boundaries right))] [x y])
+                mismatch (some (fn [input]
+                                 (let [expected (outcome reference input) actual (mapv #(outcome % input) functions)]
+                                   (when-not (every? #{expected} actual) [input expected actual]))) inputs)]]
+    (is (nil? mismatch) (pr-str [form mismatch]))))
+
+(def expression-gen
+  (gen/recursive-gen
+    (fn [inner]
+      (gen/one-of [(gen/let [op (gen/elements '[+ - * / +' -' *' quot rem min max unchecked-add bit-xor])
+                            a inner b inner] (list op a b))
+                   (gen/let [a inner b inner] (list 'if '(even? i) a b))
+                   (gen/let [a inner b inner] (list 'case '(mod i 3) 0 a b))]))
+    (gen/elements '[x i -1 0 1 2 0.5])))
+
+(deftest generated-numeric-recurrences
+  (let [result (tc/quick-check
+                 160
+                 (prop/for-all [expression (gen/resize 8 expression-gen)
+                                kind (gen/elements '[long double])
+                                initial (gen/elements [-1 0 1 Long/MIN_VALUE Long/MAX_VALUE])
+                                n (gen/choose 0 8)
+                                unchecked gen/boolean]
+                   (binding [*unchecked-math* unchecked]
+                    (let [init (list kind initial)
+                         form (list 'loophole ['x init]
+                                    (list 'dotimes ['i n] (list 'setq 'x expression)) 'x)
+                         reference (list 'loop ['x (boxed init) 'i 0]
+                                         (list 'if (list '< 'i n)
+                                               (list 'recur (boxed expression) '(inc i)) 'x))
+                         expected (outcome (backend/compile-program reference :default) nil)]
+                     (every? #(= expected (outcome (backend/compile-program form %) nil)) modes))))
+                 :seed 271828)]
+    (is (:pass? result) (pr-str result))))
+
+(deftest unchecked-math-keeps-wrapping
+  (doseq [mode modes]
+    (binding [*unchecked-math* true]
+      (is (= {:value Long/MIN_VALUE :trace []}
+             (backend/execution '(loophole [x Long/MAX_VALUE] (setq x (+ x 1)) x) mode))))))
+
+(deftest references-survive-numeric-computation
+  (doseq [mode modes
+          form '[(loophole [x 0 y nil]
+                   (dotimes [i 2] (setq x (+ x 1000)))
+                   (setq y x) [(identical? x y) (identical? x x)])
+                 (loophole [x 0 y nil]
+                   (dotimes [i 2] (psetq y x x (+ x 1000)))
+                   [(identical? y y) (not (identical? x y))])
+                 (loophole [x 0]
+                   (dotimes [i 2] (setq x (+ x 1000)))
+                   (let [saved x] (setq x (+ x 1)) [(identical? saved saved) (not (identical? saved x))]))]]
+    (is (= {:value [true true] :trace []} (backend/execution form mode)) (pr-str form)))
+  (doseq [mode modes]
+    (let [value (Long. 1000)
+          f (backend/compile-program '(loophole [x events]
+                                        (dotimes [i 0] (setq x (+ x i))) x) mode)]
+      (is (identical? value (f value)))))
+  (doseq [init '[nil 1.5 1/2 1N 1M] mode modes
+          :let [form (list 'loophole '[x 0]
+                           (list 'dotimes '[i 2] (list 'setq 'x (list 'if '(zero? i) init '(+ x 1)))) 'x)]]
+    (is (= (backend/execution form :dispatcher) (backend/execution form mode)) (pr-str form))))
+
+(deftest exceptions-stay-between-the-same-effects
+  (doseq [mode modes
+          form '[(loophole [x Long/MAX_VALUE]
+                   [(do (swap! events conj :before) (setq x (+ x 1)))
+                    (swap! events conj :after)])
+                 (loophole [x Long/MAX_VALUE y 0]
+                   (psetq y (do (swap! events conj :before) 7)
+                          x (+ x 1) y (do (swap! events conj :after) 8)))]]
+    (is (= {:throw ArithmeticException :trace [:before]} (backend/execution form mode))))
+  (doseq [mode modes]
+    (is (= {:value 10 :trace [:first :second]}
+           (backend/execution '(loophole [x 0]
+                                 (+ (do (swap! events conj :first) (setq x (+ x 3)))
+                                    (do (swap! events conj :second) (setq x (+ x 4))))) mode)))))
+
+(deftest selection-and-nan-identity
+  (doseq [mode modes
+          expression '[(= x x) (= (/ x 1) x) (identical? (/ x 1) x)
+                        (identical? (min x y) x) (identical? (max x y) x)]
+          cast '[float double]
+          :let [form (list 'loophole ['x (list cast 'Double/NaN) 'y (list cast 1)] expression)]]
+    (is (= {:value true :trace []} (backend/execution form mode)) (pr-str [mode form])))
+  ;; A numerical consumer permits selection lowering, including the tie rule.
+  (doseq [expression '[(double (min x y)) (double (max x y)) (double (/ x y))]
+          :let [form (list 'loophole '[x (double (first events)) y (double (second events))] expression)
+                functions (mapv #(backend/compile-program form %) modes)]
+          x [-0.0 0.0 Double/NaN] y [-0.0 0.0 Double/NaN]]
+    (is (apply = (map #(outcome % [x y]) functions)) (pr-str [expression x y]))))
+
+(deftest math-and-java-conversions
+  (doseq [expression
+          (concat (map #(list (symbol "clojure.math" (name %)) 'x)
+                       '[sin cos tan asin acos atan to-radians to-degrees exp log log10 sqrt cbrt ceil floor rint
+                         round ulp signum sinh cosh tanh expm1 log1p get-exponent next-up next-down])
+                  (map #(list (symbol "clojure.math" (name %)) 'x 'y)
+                       '[IEEE-remainder atan2 pow hypot copy-sign next-after scalb
+                         add-exact subtract-exact multiply-exact floor-div floor-mod])
+                  '[(Math/abs x) (Math/getExponent x) (Math/round x)
+                    (String/valueOf x) (Character/isDigit x) (Boolean/logicalAnd x y)])
+          kind '[long double identity]
+          unchecked [false true]
+          :let [bindings ['x (list kind '(first events)) 'y (list kind '(second events))]
+                form (list 'loophole bindings expression)
+                functions (binding [*unchecked-math* unchecked]
+                            (mapv #(backend/compile-program form %) modes))]]
+    (doseq [input [[-0.0 0.0] [1 2] [Long/MAX_VALUE -1] [Double/MAX_VALUE 2]
+                   [Double/NaN 0] [nil nil] [\a \b] [false true]]]
+      (is (apply = (map #(outcome % input) functions)) (pr-str [form unchecked input])))))
+
+(deftest numeric-array-loop
+  (let [form '(let [^doubles xs events]
+                (loophole [sum 0.0 i 0]
+                  (while (< i (alength xs))
+                    (setq sum (+ sum (aget xs i)) i (inc i)))
+                  (double sum)))
+        program (backend/stored form)
+        slots (storage/loop-slots (:body program))]
+    (is (= #{Long/TYPE Double/TYPE} (set (vals (select-keys (:types program) slots)))))
+    (doseq [mode modes xs [[] [1.0] [1.0 2.0 3.0] [Double/NaN] [-0.0]]]
+      (let [reference #(reduce + 0.0 %)]
+        (is (= (outcome reference xs) (outcome (backend/compile-program form mode) (double-array xs))))))))
+
+(deftest selected-origins-and-primitive-emission
+  (doseq [form '[(loophole [x 0] (dotimes [i 10] (setq x (max x i))) x)
+                 (loophole [x (double 0)] (dotimes [i 10] (setq x (max x (double i)))) x)]]
+    (let [program (backend/stored form)
+          slots (storage/loop-slots (:body program))]
+      (is (every? (:types program) slots) (pr-str form))
+      (doseq [mode modes] (is (= 9.0 (double (:value (backend/execution form mode))))))))
+  (let [warnings (java.io.StringWriter.)]
+    (binding [*err* warnings *unchecked-math* :warn-on-boxed]
+      (backend/compile-program '(loophole [sum 0] (dotimes [i 10] (setq sum (+ sum i))) sum) :default))
+    (is (not (.contains (str warnings) "Boxed math warning")) (str warnings))))
diff --git a/test/com/tailrecursion/test_runner.clj b/test/com/tailrecursion/test_runner.clj
index 879c48d..9ffa39f 100644
--- a/test/com/tailrecursion/test_runner.clj
+++ b/test/com/tailrecursion/test_runner.clj
@@ -9,6 +9,7 @@
     com.tailrecursion.nanopass.flow-test
     com.tailrecursion.blacktide.machine-test
     com.tailrecursion.blacktide.backend-test
+    com.tailrecursion.blacktide.numeric-test
     com.tailrecursion.blacktide.generated-test
     com.tailrecursion.blacktide.aot-test
     com.tailrecursion.blacktide.package-test