From 16f78403b651f30fa5c8e9f1838a4647e95e1041 Mon Sep 17 00:00:00 2001
From: PraneethMerugu <merugufam@gmail.com>
Date: Thu, 3 Sep 2026 08:56:47 -0400
Subject: [PATCH 1/3] Clarify LocalMath authoring and inspection ownership

---
 docs/src/index.md                   |  19 +++
 src/LocalMath.jl                    |   1 +
 src/authoring/syntax.jl             |  26 +++-
 src/bound_law.jl                    |  22 +--
 src/execution.jl                    |   2 +-
 src/execution/program_inspection.jl | 168 ++++++++++++++++++++++
 src/execution/stage_program.jl      | 213 ++++------------------------
 src/inspection.jl                   |  18 +--
 src/model.jl                        |  24 ++--
 test/test_inspection_diagnostics.jl |   2 +-
 10 files changed, 268 insertions(+), 227 deletions(-)
 create mode 100644 src/execution/program_inspection.jl

diff --git a/docs/src/index.md b/docs/src/index.md
index fd5b103..75da715 100644
--- a/docs/src/index.md
+++ b/docs/src/index.md
@@ -6,3 +6,22 @@ computation on CPU and GPU through one KernelAbstractions execution path.
 Start with [Quick start](learn/localmath-quickstart.md), then use
 [Relations and storage](learn/localmath-relations.md) and the
 [Scientific recipes](learn/localmath-recipes.md) for complete models.
+
+## One architecture, from equation to device
+
+LocalMath keeps mathematical meaning and physical execution separate without
+creating parallel representations:
+
+```text
+@localmath
+    → LocalLaw
+    → bind (validated descriptors and scientific storage)
+    → Plan (backend-independent meaning plus a concrete lowering)
+    → PreparedPlan (workspace, provider, and device realization)
+    → KernelAbstractions launches
+    → ExecutionReceipt
+```
+
+`inspect` and `compilation_report` project facts from those existing values;
+execution never consumes a report. CPU and qualified GPU backends use the same
+laws, validation, packed storage, and KernelAbstractions execution path.
diff --git a/src/LocalMath.jl b/src/LocalMath.jl
index 879636b..493af7b 100644
--- a/src/LocalMath.jl
+++ b/src/LocalMath.jl
@@ -89,5 +89,6 @@ include("execution/collect_physical_support.jl")
 include("execution/collect_stage.jl")
 include("execution/stage_program_kernelabstractions.jl")
 include("execution/stage_program.jl")
+include("execution/program_inspection.jl")
 
 end
diff --git a/src/authoring/syntax.jl b/src/authoring/syntax.jl
index d48f21b..daa0c99 100644
--- a/src/authoring/syntax.jl
+++ b/src/authoring/syntax.jl
@@ -199,7 +199,8 @@ end
 _lm_namedtuple(pairs) = Expr(:tuple, Expr(:parameters,
     (Expr(:kw, name, value) for (name, value) in pairs)...))
 
-function _lm_stage(spec, body::Expr, source; label = nothing)
+"""Parse the stage binder and its Cartesian boundary contract at macro time."""
+function _lm_stage_domain(spec, source)
     binder, source_expression, stage_options =
         _lm_binder(spec, source)
     tuple_binder = binder isa Expr && binder.head === :tuple
@@ -230,6 +231,21 @@ function _lm_stage(spec, body::Expr, source; label = nothing)
         source_mode !== :plain &&
             (semantic_source_expression = source_expression.args[2])
     end
+    return (; binder, source_expression, semantic_source_expression,
+        stage_options, cartesian, binder_symbols, source_mode, halo)
+end
+
+"""Lower one authored stage directly to existing typed LocalMath values."""
+function _lm_lower_stage(spec, body::Expr, source; label = nothing)
+    domain_syntax = _lm_stage_domain(spec, source)
+    binder = domain_syntax.binder
+    source_expression = domain_syntax.source_expression
+    semantic_source_expression = domain_syntax.semantic_source_expression
+    stage_options = domain_syntax.stage_options
+    cartesian = domain_syntax.cartesian
+    binder_symbols = domain_syntax.binder_symbols
+    source_mode = domain_syntax.source_mode
+    halo = domain_syntax.halo
     parameter_expression = stage_options.parameters
     declarations = _lm_parameters(parameter_expression, source)
     parameter_names = Tuple(declaration.args[1] for declaration in declarations)
@@ -1096,12 +1112,12 @@ function _lm_stage(spec, body::Expr, source; label = nothing)
         :($(GlobalRef(LocalMath, :LocalLaw))($stage)))
 end
 
-function _lm_expand(args, source)
+function _lm_lower(args, source)
     if length(args) == 2
         spec, body = args
         body isa Expr && body.head === :block ||
             _lm_error("@localmath requires a begin/end body", source; actual = body)
-        return _lm_stage(spec, body, source)
+        return _lm_lower_stage(spec, body, source)
     elseif length(args) == 1
         body = only(args)
         if body isa Expr && body.head === :function
@@ -1129,7 +1145,7 @@ function _lm_expand(args, source)
             label = invocation.args[1]
             stage_spec = length(invocation.args) == 2 ? invocation.args[2] :
                 Expr(:tuple, invocation.args[2:end]...)
-            push!(works, _lm_stage(stage_spec, stage_body, source; label))
+            push!(works, _lm_lower_stage(stage_spec, stage_body, source; label))
         end
         isempty(works) && _lm_error("@localmath requires at least one @stage",
             source)
@@ -1176,5 +1192,5 @@ interpretation. The macro creates no alternate executor or runtime syntax
 tree.
 """
 macro localmath(args...)
-    return esc(_lm_expand(args, __source__))
+    return esc(_lm_lower(args, __source__))
 end
diff --git a/src/bound_law.jl b/src/bound_law.jl
index a98fe40..792c1d9 100644
--- a/src/bound_law.jl
+++ b/src/bound_law.jl
@@ -236,9 +236,9 @@ function _field_publication_requires_initialization(
     return !_publication_initializes_field(stage, publication, field)
 end
 
-function _require_definite_field_initialization(work::LocalLaw, field::Field)
+function _require_definite_field_initialization(law::LocalLaw, field::Field)
     initialized = false
-    for (index, stage) in enumerate(work.stages)
+    for (index, stage) in enumerate(law.stages)
         if !initialized && _field_used_at_stage_entry(stage, field)
             throw(LocalMathValidationError(
                 "an uninitialized allocated Field is read before a proven total assignment";
@@ -269,9 +269,9 @@ function _require_definite_field_initialization(work::LocalLaw, field::Field)
     return nothing
 end
 
-function _collect_allocation_schema(work::LocalLaw, collection::Collection)
+function _collect_allocation_schema(law::LocalLaw, collection::Collection)
     schemas = Any[]
-    for stage in work.stages, publication in stage.publications
+    for stage in law.stages, publication in stage.publications
         publication.law isa Collect || continue
         any(publication.components) do component
             component isa CollectionPublication &&
@@ -316,14 +316,14 @@ _zeroed_int32_storage(backend, length::Int) =
     _filled_int32_storage(backend, length, Int32(0))
 
 function _collection_allocation(
-        work::LocalLaw, collection::Collection, request::Allocate, backend,
+        law::LocalLaw, collection::Collection, request::Allocate, backend,
     )
     request.initial isa _EmptyAllocation || throw(LocalMathValidationError(
         "Collection allocation uses the zero-argument Allocate() form";
         stage = :bind, contract = :collection_allocation_initialization,
         expected = :empty_collection, actual = request.initial,
     ))
-    schema = _collect_allocation_schema(work, collection)
+    schema = _collect_allocation_schema(law, collection)
     capacity = Int(collection.capacity)
     records = _allocate_compacted_records(backend, eltype(collection), capacity)
     count = _zeroed_int32_storage(backend, 1)
@@ -454,15 +454,15 @@ function _declared_collection_binding(entry::Pair)
     return _collection_storage_binding(collection, storage)
 end
 
-function _materialized_field_declaration(work, entry::Pair, backend)
+function _materialized_field_declaration(law, entry::Pair, backend)
     field, declaration = entry
     if declaration isa Temporary
-        _require_definite_field_initialization(work, field)
+        _require_definite_field_initialization(law, field)
         return field => _TemporaryStorageRequest(backend)
     end
     declaration isa Allocate || return entry
     declaration.initial isa UndefInitializer &&
-        _require_definite_field_initialization(work, field)
+        _require_definite_field_initialization(law, field)
     return field => _field_allocation(field, declaration, backend)
 end
 
@@ -494,11 +494,11 @@ function _materialized_relation_declaration(entry::Pair, backend)
     return relation => materialized
 end
 
-function _materialized_collection_declaration(work, entry::Pair, backend)
+function _materialized_collection_declaration(law, entry::Pair, backend)
     collection, declaration = entry
     declaration isa Allocate || return entry
     return collection => _collection_allocation(
-        work, collection, declaration, backend)
+        law, collection, declaration, backend)
 end
 
 function _contains_allocation(declaration::Allocate)
diff --git a/src/execution.jl b/src/execution.jl
index f2a83e3..46df982 100644
--- a/src/execution.jl
+++ b/src/execution.jl
@@ -395,7 +395,7 @@ function _observe_receipt_failure(receipt::ExecutionReceipt)
     error = _prepared_validation_error_at(
         receipt.prepared, receipt.lease_index)
     error === nothing && return nothing
-    return _with_work_source_origin(error,
+    return _with_law_source_origin(error,
         _plan_law(receipt.prepared.plan), :wait, error.contract)
 end
 
diff --git a/src/execution/program_inspection.jl b/src/execution/program_inspection.jl
new file mode 100644
index 0000000..8d129a6
--- /dev/null
+++ b/src/execution/program_inspection.jl
@@ -0,0 +1,168 @@
+"""Cold inspection of planned and prepared LocalMath programs.
+
+This file projects facts from the semantic law, validated binding, physical
+lowering, and prepared runtime. Execution never consumes these projections.
+"""
+
+"""
+    LocalMath.inspect(plan::Plan)
+
+Return the semantic projection together with validated relation proofs,
+producer dependencies, workspace requirements, specialization signatures, and
+the currently planned physical phases. Physical planning fields describe the
+current implementation and are not additional scientific semantics.
+"""
+inspect(plan::Plan{<:_BoundLaw}; level = nothing) =
+    _inspection_projection(_plan_inspection(plan, :Plan), level)
+
+_structural_leaf_inspection(fact::_StructuralLeafFact) = (
+    name = fact.name,
+    storage_type = fact.storage_type,
+    logical = fact.logical,
+    prepared = fact.prepared,
+)
+
+function _binding_realization(binding::_ValidatedStructuralBinding)
+    fields = map(binding.fields, binding.field_facts) do value, facts
+        (identity = semantic_identity(value.field),
+            binding_identity = value.binding_id,
+            ownership = _ownership_inspection(value.ownership),
+            leaves = map(_structural_leaf_inspection, facts))
+    end
+    relations = map(binding.relations, binding.proofs) do value, proof
+        (identity = semantic_identity(value.relation),
+            binding_identity = value.binding_id,
+            ownership = _ownership_inspection(value.ownership),
+            dynamic_generation = value.generation !== nothing,
+            dynamic_status = value.status !== nothing,
+            leaves = map(_structural_leaf_inspection,
+                proof.binding_schema.physical_leaves))
+    end
+    collections = map(binding.collections,
+            binding.collection_facts) do value, facts
+        (identity = semantic_identity(value.collection),
+            binding_identity = value.binding_id,
+            leaves = map(_structural_leaf_inspection, facts))
+    end
+    return (; fields, relations, collections)
+end
+
+"""
+    LocalMath.inspect(prepared::PreparedPlan)
+
+Return the plan projection plus concrete storage, callable admission, provider,
+workspace, submission-layout, and mutable receipt-counter observations. The
+operation is cold and does not submit or synchronize work.
+"""
+function inspect(prepared::PreparedPlan; level = nothing)
+    report = _plan_inspection(prepared.plan, :PreparedPlan; prepared)
+    callbacks = map(prepared.plan.lowering.callable_admissions) do entry
+        (purpose = entry.purpose, signature = entry.signature,
+            return_type = entry.return_type,
+            admission = entry.admission,
+            method = entry.method)
+    end
+    realized = (
+        prepared_launch_types = Tuple(map(launch -> typeof(launch.stage),
+            prepared.runtime.launches)),
+        callback_methods = callbacks,
+        provider = _lane_provider(prepared.lane),
+        device = _lane_device(prepared.lane),
+        bindings = _binding_realization(prepared.plan.bound.binding),
+        parameter_layout = _stage_parameter_layout_inspection(
+            prepared.submission_schema),
+        dependency_arity = prepared.dependency_arity,
+        lease_capacity = length(prepared.leases),
+        workspace_ownership = prepared.workspace_ownership,
+        state = (
+            submitted = prepared.submitted,
+            drained = prepared.drained,
+            outstanding = prepared.outstanding,
+            poisoned = prepared.poisoned,
+            provider_completions = _lane_wait_count(prepared.lane),
+            provider_scope_completions =
+                _lane_scope_wait_count(prepared.lane),
+            validation_transfers = _lane_transfer_count(prepared.lane),
+        ),
+    )
+    return _inspection_projection(merge(report, (; realized)), level)
+end
+
+function _distinct_specialization_count(stages)
+    signatures = map(stage -> stage.planning.specialization_signature, stages)
+    return length(unique(signatures))
+end
+
+_callable_admission_inspection(entry::_CallableAdmissionFact) = (
+    purpose = entry.purpose,
+    callable_type = typeof(entry.callback),
+    selected_method = entry.method,
+    analyzed_signature = entry.signature,
+    inferred_return_type = entry.return_type,
+    admission_contract = entry.admission,
+)
+
+"""
+    LocalMath.compilation_report(plan::Plan)
+
+Return cold structural compiler facts: specialization families, callable
+signatures, physical phases, relationship validation, and workspace shape.
+The report contains no predicted wall time and is never consumed by planning.
+"""
+function compilation_report(plan::Plan{<:_BoundLaw})
+    report = _plan_inspection(plan, :Plan)
+    return (
+        lifecycle = :PlanCompilationReport,
+        compiler = report.planning.compiler,
+        stage_count = length(report.stages),
+        specialization_family_count = _distinct_specialization_count(
+            report.stages),
+        specialization_signatures = map(
+            stage -> stage.planning.specialization_signature, report.stages),
+        callable_signatures = map(
+            stage -> stage.planning.evaluator_signature, report.stages),
+        callable_admissions = map(_callable_admission_inspection,
+            plan.lowering.callable_admissions),
+        relationship_receipts = map(
+            stage -> stage.planning.relationship_receipts, report.stages),
+        stage_phases = report.planning.stage_phases,
+        provider_launch_count = report.planning.base_provider_launch_count,
+        workspace = report.planning.workspace,
+        workspace_bytes = report.planning.workspace_bytes,
+    )
+end
+
+"""
+    LocalMath.compilation_report(prepared::PreparedPlan)
+
+Return the plan report together with realized launch types, selected callback
+methods, parameter layout, dependency arity, and provider facts. This operation
+does not submit work or synchronize the provider.
+"""
+function compilation_report(prepared::PreparedPlan)
+    planned = compilation_report(prepared.plan)
+    report = inspect(prepared)
+    return merge(planned, (
+        lifecycle = :PreparedCompilationReport,
+        prepared_launch_types = report.realized.prepared_launch_types,
+        callback_methods = report.realized.callback_methods,
+        parameter_layout = report.realized.parameter_layout,
+        dependency_arity = report.realized.dependency_arity,
+        provider = report.realized.provider,
+        device = report.realized.device,
+    ))
+end
+
+"""`execution_contract(prepared)` reports provider-scope receipt behavior without submitting work."""
+function execution_contract(prepared::PreparedPlan)
+    lane = prepared.lane
+    return (
+        provider = _lane_provider(lane),
+        receipt_scope = _lane_wait_scope(lane),
+        receipt_cumulative = _lane_cumulative(lane),
+        receipt_selective = _lane_selective(lane),
+        observed_provider_completions = _lane_wait_count(lane),
+        observed_scope_completions = _lane_scope_wait_count(lane),
+        observed_validation_transfers = _lane_transfer_count(lane),
+    )
+end
diff --git a/src/execution/stage_program.jl b/src/execution/stage_program.jl
index db801e6..34295f7 100644
--- a/src/execution/stage_program.jl
+++ b/src/execution/stage_program.jl
@@ -719,8 +719,8 @@ Base.@nospecializeinfer Base.@noinline function plan(
     return Plan(planned_bound, backend, lowering)
 end
 
-plan(work::LocalLaw, binding::_StructuralBinding;
-    backend::KernelAbstractions.Backend) = plan(_bind_law(work, binding); backend)
+plan(law::LocalLaw, binding::_StructuralBinding;
+    backend::KernelAbstractions.Backend) = plan(_bind_law(law, binding); backend)
 
 function _validate_stage_program_leaf_facts(storage, prefix::Symbol, facts)
     leaves = storage === nothing ? () : _structural_physical_leaves(prefix, storage)
@@ -1745,9 +1745,9 @@ function _semantic_stage_inspection(stage::Stage, index::Int;
     )
 end
 
-function _semantic_equivalence(work::LocalLaw)
-    _, relations, _ = _law_descriptor_requirements(work)
-    stages = Tuple(map(enumerate(work.stages)) do (index, stage)
+function _semantic_equivalence(law::LocalLaw)
+    _, relations, _ = _law_descriptor_requirements(law)
+    stages = Tuple(map(enumerate(law.stages)) do (index, stage)
         report = _semantic_stage_inspection(stage, index)
         publications = map(report.publications) do publication
             merge(publication, (origin = nothing,))
@@ -1757,7 +1757,7 @@ function _semantic_equivalence(work::LocalLaw)
     end)
     return (
         parameters = map(_parameter_inspection,
-            work.parameters.declarations),
+            law.parameters.declarations),
         relations = map(relation -> _relation_inspection(relation, nothing),
             relations),
         stages,
@@ -1766,23 +1766,23 @@ function _semantic_equivalence(work::LocalLaw)
                 type = typeof(stage.evaluator.evaluator),
                 parameters = map(_parameter_inspection,
                     stage.evaluator.parameters),
-            ), work.stages),
+            ), law.stages),
     )
 end
 
-function _inspect_local_law(work::LocalLaw)
-    _, relations, _ = _law_descriptor_requirements(work)
+function _inspect_local_law(law::LocalLaw)
+    _, relations, _ = _law_descriptor_requirements(law)
     return (
         lifecycle = :LocalLaw,
         parameters = map(_parameter_inspection,
-            work.parameters.declarations),
+            law.parameters.declarations),
         relations = map(relation -> _relation_inspection(relation, nothing),
             relations),
-        stages = Tuple(map(enumerate(work.stages)) do (index, stage)
+        stages = Tuple(map(enumerate(law.stages)) do (index, stage)
             _semantic_stage_inspection(stage, index)
         end),
         planning = nothing,
-        equivalence = _semantic_equivalence(work),
+        equivalence = _semantic_equivalence(law),
     )
 end
 
@@ -1892,18 +1892,18 @@ _stage_layout_name(::_CandidateStageExecutor{<:_DirectIdentityUniqueLayout}) =
 _stage_layout_name(::_CollectStageExecutor) = :compacted_sequence
 _stage_layout_name(::_OrderedFoldStageExecutor) = :ordered_recurrence
 
-function _segment_materializations(work::LocalLaw, indices)
+function _segment_materializations(law::LocalLaw, indices)
     return Tuple(semantic_identity(component.field)
         for index in indices
-        for publication in work.stages[index].publications
+        for publication in law.stages[index].publications
         for component in publication.components
         if component isa FieldPublication)
 end
 
 function _physical_segment_inspection(
-        launch::_PointwiseSegmentEntry, work::LocalLaw)
+        launch::_PointwiseSegmentEntry, law::LocalLaw)
     indices = map(member -> member.logical_index, launch.members)
-    source = work.stages[first(indices)].source
+    source = law.stages[first(indices)].source
     return (
         logical_stages = indices,
         family = :direct_pointwise,
@@ -1916,15 +1916,15 @@ function _physical_segment_inspection(
 end
 
 function _physical_segment_inspection(
-        entry::_StageLoweringEntry, work::LocalLaw)
+        entry::_StageLoweringEntry, law::LocalLaw)
     index = entry.logical_index
     phases = _planned_stage_phases(entry)
     return (
         logical_stages = (index,),
         family = _stage_layout_name(entry.executor),
         launch_count = _phase_count(phases),
-        traversal = semantic_identity(work.stages[index].source),
-        retained_materializations = _segment_materializations(work, (index,)),
+        traversal = semantic_identity(law.stages[index].source),
+        retained_materializations = _segment_materializations(law, (index,)),
         forwarded_values = (),
         boundary_reason = :semantic_barrier,
     )
@@ -1976,8 +1976,8 @@ end
 
 function _plan_inspection(plan::Plan, lifecycle::Symbol;
         prepared = nothing)
-    work = plan.bound.law
-    _, relations, _ = _law_descriptor_requirements(work)
+    law = plan.bound.law
+    _, relations, _ = _law_descriptor_requirements(law)
     binding = plan.bound.binding
     proofs = map(relations) do relation
         identity = semantic_identity(relation)
@@ -1999,7 +1999,7 @@ function _plan_inspection(plan::Plan, lifecycle::Symbol;
     phase_values = Any[]
     logical_entries = _logical_lowering_entries(plan.lowering)
     for (index, entry) in enumerate(logical_entries)
-        semantic = work.stages[index]
+        semantic = law.stages[index]
         phases = _planned_stage_phases(entry)
         push!(phase_values, phases)
         stage_planning = _stage_planning_inspection(entry, semantic, phases)
@@ -2014,7 +2014,7 @@ function _plan_inspection(plan::Plan, lifecycle::Symbol;
         _workspace_requirement_facts(plan.lowering,
             length(prepared.leases))
     physical_segments = map(plan.lowering.launches) do launch
-        _physical_segment_inspection(launch, work)
+        _physical_segment_inspection(launch, law)
     end
     stage_local = sum(segment -> segment.launch_count,
         physical_segments; init = 0)
@@ -2035,173 +2035,10 @@ function _plan_inspection(plan::Plan, lifecycle::Symbol;
     return (
         lifecycle,
         parameters = map(_parameter_inspection,
-            work.parameters.declarations),
+            law.parameters.declarations),
         relations = map(_relation_inspection, relations, proofs),
         stages = Tuple(stages),
         planning,
-        equivalence = _semantic_equivalence(work),
-    )
-end
-
-"""
-    LocalMath.inspect(plan::Plan)
-
-Return the semantic projection together with validated relation proofs,
-producer dependencies, workspace requirements, specialization signatures, and
-the currently planned physical phases. Physical planning fields describe the
-current implementation and are not additional scientific semantics.
-"""
-inspect(plan::Plan{<:_BoundLaw}; level = nothing) =
-    _inspection_projection(_plan_inspection(plan, :Plan), level)
-
-_structural_leaf_inspection(fact::_StructuralLeafFact) = (
-    name = fact.name,
-    storage_type = fact.storage_type,
-    logical = fact.logical,
-    prepared = fact.prepared,
-)
-
-function _binding_realization(binding::_ValidatedStructuralBinding)
-    fields = map(binding.fields, binding.field_facts) do value, facts
-        (identity = semantic_identity(value.field),
-            binding_identity = value.binding_id,
-            ownership = _ownership_inspection(value.ownership),
-            leaves = map(_structural_leaf_inspection, facts))
-    end
-    relations = map(binding.relations, binding.proofs) do value, proof
-        (identity = semantic_identity(value.relation),
-            binding_identity = value.binding_id,
-            ownership = _ownership_inspection(value.ownership),
-            dynamic_generation = value.generation !== nothing,
-            dynamic_status = value.status !== nothing,
-            leaves = map(_structural_leaf_inspection,
-                proof.binding_schema.physical_leaves))
-    end
-    collections = map(binding.collections,
-            binding.collection_facts) do value, facts
-        (identity = semantic_identity(value.collection),
-            binding_identity = value.binding_id,
-            leaves = map(_structural_leaf_inspection, facts))
-    end
-    return (; fields, relations, collections)
-end
-
-"""
-    LocalMath.inspect(prepared::PreparedPlan)
-
-Return the plan projection plus concrete storage, callable admission, provider,
-workspace, submission-layout, and mutable receipt-counter observations. The
-operation is cold and does not submit or synchronize work.
-"""
-function inspect(prepared::PreparedPlan; level = nothing)
-    report = _plan_inspection(prepared.plan, :PreparedPlan; prepared)
-    callbacks = map(prepared.plan.lowering.callable_admissions) do entry
-        (purpose = entry.purpose, signature = entry.signature,
-            return_type = entry.return_type,
-            admission = entry.admission,
-            method = entry.method)
-    end
-    realized = (
-        prepared_launch_types = Tuple(map(launch -> typeof(launch.stage),
-            prepared.runtime.launches)),
-        callback_methods = callbacks,
-        provider = _lane_provider(prepared.lane),
-        device = _lane_device(prepared.lane),
-        bindings = _binding_realization(prepared.plan.bound.binding),
-        parameter_layout = _stage_parameter_layout_inspection(
-            prepared.submission_schema),
-        dependency_arity = prepared.dependency_arity,
-        lease_capacity = length(prepared.leases),
-        workspace_ownership = prepared.workspace_ownership,
-        state = (
-            submitted = prepared.submitted,
-            drained = prepared.drained,
-            outstanding = prepared.outstanding,
-            poisoned = prepared.poisoned,
-            provider_completions = _lane_wait_count(prepared.lane),
-            provider_scope_completions =
-                _lane_scope_wait_count(prepared.lane),
-            validation_transfers = _lane_transfer_count(prepared.lane),
-        ),
-    )
-    return _inspection_projection(merge(report, (; realized)), level)
-end
-
-function _distinct_specialization_count(stages)
-    signatures = map(stage -> stage.planning.specialization_signature, stages)
-    return length(unique(signatures))
-end
-
-_callable_admission_inspection(entry::_CallableAdmissionFact) = (
-    purpose = entry.purpose,
-    callable_type = typeof(entry.callback),
-    selected_method = entry.method,
-    analyzed_signature = entry.signature,
-    inferred_return_type = entry.return_type,
-    admission_contract = entry.admission,
-)
-
-"""
-    LocalMath.compilation_report(plan::Plan)
-
-Return cold structural compiler facts: specialization families, callable
-signatures, physical phases, relationship validation, and workspace shape.
-The report contains no predicted wall time and is never consumed by planning.
-"""
-function compilation_report(plan::Plan{<:_BoundLaw})
-    report = _plan_inspection(plan, :Plan)
-    return (
-        lifecycle = :PlanCompilationReport,
-        compiler = report.planning.compiler,
-        stage_count = length(report.stages),
-        specialization_family_count = _distinct_specialization_count(
-            report.stages),
-        specialization_signatures = map(
-            stage -> stage.planning.specialization_signature, report.stages),
-        callable_signatures = map(
-            stage -> stage.planning.evaluator_signature, report.stages),
-        callable_admissions = map(_callable_admission_inspection,
-            plan.lowering.callable_admissions),
-        relationship_receipts = map(
-            stage -> stage.planning.relationship_receipts, report.stages),
-        stage_phases = report.planning.stage_phases,
-        provider_launch_count = report.planning.base_provider_launch_count,
-        workspace = report.planning.workspace,
-        workspace_bytes = report.planning.workspace_bytes,
-    )
-end
-
-"""
-    LocalMath.compilation_report(prepared::PreparedPlan)
-
-Return the plan report together with realized launch types, selected callback
-methods, parameter layout, dependency arity, and provider facts. This operation
-does not submit work or synchronize the provider.
-"""
-function compilation_report(prepared::PreparedPlan)
-    planned = compilation_report(prepared.plan)
-    report = inspect(prepared)
-    return merge(planned, (
-        lifecycle = :PreparedCompilationReport,
-        prepared_launch_types = report.realized.prepared_launch_types,
-        callback_methods = report.realized.callback_methods,
-        parameter_layout = report.realized.parameter_layout,
-        dependency_arity = report.realized.dependency_arity,
-        provider = report.realized.provider,
-        device = report.realized.device,
-    ))
-end
-
-"""`execution_contract(prepared)` reports provider-scope receipt behavior without submitting work."""
-function execution_contract(prepared::PreparedPlan)
-    lane = prepared.lane
-    return (
-        provider = _lane_provider(lane),
-        receipt_scope = _lane_wait_scope(lane),
-        receipt_cumulative = _lane_cumulative(lane),
-        receipt_selective = _lane_selective(lane),
-        observed_provider_completions = _lane_wait_count(lane),
-        observed_scope_completions = _lane_scope_wait_count(lane),
-        observed_validation_transfers = _lane_transfer_count(lane),
+        equivalence = _semantic_equivalence(law),
     )
 end
diff --git a/src/inspection.jl b/src/inspection.jl
index 11579e1..960a930 100644
--- a/src/inspection.jl
+++ b/src/inspection.jl
@@ -286,11 +286,11 @@ function _show_publication_summary(io::IO, publication::Publication)
     show(IOContext(io, :compact => true), destinations)
 end
 
-function _show_law_summary(io::IO, work::LocalLaw)
-    fields, relations, collections = _law_descriptor_requirements(work)
+function _show_law_summary(io::IO, law::LocalLaw)
+    fields, relations, collections = _law_descriptor_requirements(law)
     println(io, "LocalLaw")
     print(io, "  parameters: ")
-    _show_parameter_summary(io, work.parameters)
+    _show_parameter_summary(io, law.parameters)
     println(io, "\n  descriptors:")
     for field in fields
         print(io, "    field: ")
@@ -308,7 +308,7 @@ function _show_law_summary(io::IO, work::LocalLaw)
         println(io)
     end
     println(io, "  stages:")
-    for (index, stage) in enumerate(work.stages)
+    for (index, stage) in enumerate(law.stages)
         print(io, "    stage ", index, "\n      domain: ")
         _show_space_summary(io, stage.source; identity = false)
         print(io, "\n      reads:")
@@ -341,14 +341,14 @@ function _show_law_summary(io::IO, work::LocalLaw)
             print(io, "\n      origin: ")
             _show_validation_origin(io, stage.origin)
         end
-        index == length(work.stages) || println(io)
+        index == length(law.stages) || println(io)
     end
 end
 
-Base.show(io::IO, work::LocalLaw) =
-    print(io, "LocalLaw(stages=", length(work.stages), ")")
-Base.show(io::IO, ::MIME"text/plain", work::LocalLaw) =
-    _show_law_summary(io, work)
+Base.show(io::IO, law::LocalLaw) =
+    print(io, "LocalLaw(stages=", length(law.stages), ")")
+Base.show(io::IO, ::MIME"text/plain", law::LocalLaw) =
+    _show_law_summary(io, law)
 Base.show(io::IO, plan::Plan) =
     print(io, "Plan(family=stage_program",
         ", backend=", typeof(plan.backend), ")")
diff --git a/src/model.jl b/src/model.jl
index 717c0de..602d815 100644
--- a/src/model.jl
+++ b/src/model.jl
@@ -147,36 +147,36 @@ function LocalLaw(stage; parameters = nothing)
 end
 
 """
-    sequence(works::LocalLaw...)
+    sequence(laws::LocalLaw...)
 
 Concatenate scientific stages and merge their one cold schemas in first
 declaration order.  This is value composition only: it adds no scheduler,
 topology bundle, compatibility operation, or execution route.
 """
-function sequence(works::LocalLaw...)
-    isempty(works) && throw(LocalMathValidationError(
+function sequence(laws::LocalLaw...)
+    isempty(laws) && throw(LocalMathValidationError(
         "a LocalLaw sequence requires at least one program";
         stage = :construct, contract = :program_sequence,
     ))
-    stages = Tuple(stage for work in works for stage in work.stages)
+    stages = Tuple(stage for law in laws for stage in law.stages)
     parameters = _merge_parameter_schemas(Tuple(
-        work.parameters for work in works
+        law.parameters for law in laws
     ))
     return LocalLaw(stages, parameters)
 end
 
-sequence(works::Tuple{Vararg{LocalLaw}}) = sequence(works...)
+sequence(laws::Tuple{Vararg{LocalLaw}}) = sequence(laws...)
 
-function _work_source_origin(work::LocalLaw, stage::Union{Nothing, Int})
+function _law_source_origin(law::LocalLaw, stage::Union{Nothing, Int})
     stage === nothing && return _NO_SOURCE_ORIGIN
     index = stage
-    1 <= index <= length(work.stages) || return _NO_SOURCE_ORIGIN
-    return work.stages[index].origin
+    1 <= index <= length(law.stages) || return _NO_SOURCE_ORIGIN
+    return law.stages[index].origin
 end
 
-function _with_work_source_origin(
+function _with_law_source_origin(
         error,
-        work::LocalLaw,
+        law::LocalLaw,
         lifecycle::Symbol,
         contract::Symbol;
         stage::Union{Nothing, Int} = nothing,
@@ -184,7 +184,7 @@ function _with_work_source_origin(
     stage_index = stage === nothing ? _validation_stage_index(error) : stage
     return _with_source_origin(
         error,
-        _work_source_origin(work, stage_index),
+        _law_source_origin(law, stage_index),
         lifecycle,
         contract,
     )
diff --git a/test/test_inspection_diagnostics.jl b/test/test_inspection_diagnostics.jl
index 0179800..fd80502 100644
--- a/test/test_inspection_diagnostics.jl
+++ b/test/test_inspection_diagnostics.jl
@@ -47,7 +47,7 @@ end
         stage = :execute,
         contract = :provider_execution,
     )
-    @test LMID._with_work_source_origin(global_error, law,
+    @test LMID._with_law_source_origin(global_error, law,
         :execute, :provider_execution) === global_error
 
     authored = LMID._with_source_origin(

From a38495d42a0b4499bdb4f9185b20e85869451720 Mon Sep 17 00:00:00 2001
From: PraneethMerugu <merugufam@gmail.com>
Date: Thu, 3 Sep 2026 09:23:21 -0400
Subject: [PATCH 2/3] Complete LocalLaw terminology cutover

---
 src/authoring/syntax.jl |  8 ++++----
 src/execution.jl        | 24 ++++++++++++------------
 2 files changed, 16 insertions(+), 16 deletions(-)

diff --git a/src/authoring/syntax.jl b/src/authoring/syntax.jl
index daa0c99..939d6c4 100644
--- a/src/authoring/syntax.jl
+++ b/src/authoring/syntax.jl
@@ -1130,7 +1130,7 @@ function _lm_lower(args, source)
         body isa Expr && body.head === :block ||
             _lm_error("@localmath requires a binder or @stage block", source;
                 actual = body)
-        works = Any[]
+        laws = Any[]
         for statement in body.args
             statement isa LineNumberNode && continue
             statement isa Expr && statement.head === :macrocall &&
@@ -1145,11 +1145,11 @@ function _lm_lower(args, source)
             label = invocation.args[1]
             stage_spec = length(invocation.args) == 2 ? invocation.args[2] :
                 Expr(:tuple, invocation.args[2:end]...)
-            push!(works, _lm_lower_stage(stage_spec, stage_body, source; label))
+            push!(laws, _lm_lower_stage(stage_spec, stage_body, source; label))
         end
-        isempty(works) && _lm_error("@localmath requires at least one @stage",
+        isempty(laws) && _lm_error("@localmath requires at least one @stage",
             source)
-        return :($(GlobalRef(LocalMath, :sequence))($(works...)))
+        return :($(GlobalRef(LocalMath, :sequence))($(laws...)))
     end
     _lm_error("@localmath accepts a function definition, one binder and body, or a stage block",
         source; actual = args)
diff --git a/src/execution.jl b/src/execution.jl
index 46df982..b519ba2 100644
--- a/src/execution.jl
+++ b/src/execution.jl
@@ -55,19 +55,19 @@ end
     return :(($(values...),))
 end
 
-struct _SuccessfulWorkGate{G,S} <: AbstractVector{Bool}
+struct _SuccessfulLawGate{G,S} <: AbstractVector{Bool}
     parent::G
     statuses::S
     lease_index::Int32
 end
 
-Base.size(::_SuccessfulWorkGate) = (1,)
-Base.length(::_SuccessfulWorkGate) = 1
-Base.strides(::_SuccessfulWorkGate) = (1,)
-Base.IndexStyle(::Type{<:_SuccessfulWorkGate}) = IndexLinear()
+Base.size(::_SuccessfulLawGate) = (1,)
+Base.length(::_SuccessfulLawGate) = 1
+Base.strides(::_SuccessfulLawGate) = (1,)
+Base.IndexStyle(::Type{<:_SuccessfulLawGate}) = IndexLinear()
 
-function Adapt.adapt_structure(to, gate::_SuccessfulWorkGate)
-    return _SuccessfulWorkGate(
+function Adapt.adapt_structure(to, gate::_SuccessfulLawGate)
+    return _SuccessfulLawGate(
         Adapt.adapt(to, gate.parent),
         Adapt.adapt(to, gate.statuses),
         gate.lease_index,
@@ -86,14 +86,14 @@ end
     )
 end
 
-@inline function Base.getindex(gate::_SuccessfulWorkGate, index::Integer)
+@inline function Base.getindex(gate::_SuccessfulLawGate, index::Integer)
     @boundscheck index == 1 || throw(BoundsError(gate, index))
     return @inbounds(gate.parent[1]) && _validation_prefix_succeeded(
         gate.statuses, gate.lease_index
     )
 end
 
-function KernelAbstractions.get_backend(gate::_SuccessfulWorkGate)
+function KernelAbstractions.get_backend(gate::_SuccessfulLawGate)
     backend = KernelAbstractions.get_backend(gate.parent)
     all(status -> KernelAbstractions.get_backend(status) == backend,
         gate.statuses) || throw(LocalMathValidationError(
@@ -108,7 +108,7 @@ end
 
 function _success_gate(prepared::PreparedPlan, lease_index::Int32, parent)
     current_task() === prepared.owner || throw(LocalMathValidationError(
-        "a success gate belongs to the task that prepared its source work";
+        "a success gate belongs to the task that prepared its source law";
         stage = :execute,
         contract = :receipt_owner,
         expected = prepared.owner,
@@ -118,13 +118,13 @@ function _success_gate(prepared::PreparedPlan, lease_index::Int32, parent)
         status -> status.device, _prepared_validation_statuses(prepared)
     )
     isempty(statuses) && throw(LocalMathValidationError(
-        "success_gate requires a source work with device validation status";
+        "success_gate requires a source law with device validation status";
         stage = :prepare,
         contract = :validation_status,
         expected = :device_validation_status,
         actual = :none,
     ))
-    return _SuccessfulWorkGate(
+    return _SuccessfulLawGate(
         parent, statuses, lease_index
     )
 end

From ba65753b95578ab43993963a0c5c0130ed727a06 Mon Sep 17 00:00:00 2001
From: PraneethMerugu <merugufam@gmail.com>
Date: Thu, 3 Sep 2026 09:34:51 -0400
Subject: [PATCH 3/3] Separate LocalMath authoring lowering passes

---
 src/authoring/syntax.jl | 612 +++++++++++++++++++++-------------------
 1 file changed, 329 insertions(+), 283 deletions(-)

diff --git a/src/authoring/syntax.jl b/src/authoring/syntax.jl
index 939d6c4..291e491 100644
--- a/src/authoring/syntax.jl
+++ b/src/authoring/syntax.jl
@@ -235,20 +235,9 @@ function _lm_stage_domain(spec, source)
         stage_options, cartesian, binder_symbols, source_mode, halo)
 end
 
-"""Lower one authored stage directly to existing typed LocalMath values."""
-function _lm_lower_stage(spec, body::Expr, source; label = nothing)
-    domain_syntax = _lm_stage_domain(spec, source)
-    binder = domain_syntax.binder
-    source_expression = domain_syntax.source_expression
-    semantic_source_expression = domain_syntax.semantic_source_expression
-    stage_options = domain_syntax.stage_options
-    cartesian = domain_syntax.cartesian
-    binder_symbols = domain_syntax.binder_symbols
-    source_mode = domain_syntax.source_mode
-    halo = domain_syntax.halo
-    parameter_expression = stage_options.parameters
-    declarations = _lm_parameters(parameter_expression, source)
-    parameter_names = Tuple(declaration.args[1] for declaration in declarations)
+"""Discover and lower bounded reads while preserving first-use order."""
+function _lm_discover_stage_accesses(domain_syntax, source)
+    (; binder, cartesian, binder_symbols, source_mode, halo) = domain_syntax
     reads = Union{_LocalMathReadSyntax,_LocalMathCollectionReadSyntax}[]
     read_roles = Dict{Tuple{Symbol,Union{Nothing,Symbol},Symbol},Symbol}()
     used_read_roles = Dict{Symbol,Int}()
@@ -449,6 +438,302 @@ function _lm_lower_stage(spec, body::Expr, source; label = nothing)
             (transform(argument; requested_mode) for argument in expression.args)...)
     end
 
+    return (; reads, transform, relation_index,
+        synthetic_relation_expressions, reads_symbol, parameters_symbol,
+        item_symbol)
+end
+
+"""Parse one ordered-state block into the existing OrderedFold syntax fact."""
+function _lm_parse_ordered_state!(
+        statement, line, domain_syntax, access, parse_state, source)
+    (; binder) = domain_syntax
+    (; transform, reads_symbol, item_symbol) = access
+    (; publications, publication_port, evaluator_aliases) = parse_state
+    length(statement.args) == 4 || _lm_error(
+        "@ordered requires `(by=..., state=...)` and a body", source;
+        actual = statement)
+    specification, ordered_body = statement.args[3], statement.args[4]
+    specification isa Expr && specification.head === :tuple || _lm_error(
+        "@ordered requires `(by=..., state=...)`", source;
+        actual = specification)
+    options = Dict{Symbol,Any}()
+    for option in specification.args
+        option isa Expr && option.head === :(=) &&
+            option.args[1] in (:by, :state) || _lm_error(
+                "@ordered accepts only by and state", source; actual=option)
+        options[option.args[1]] = option.args[2]
+    end
+    all(haskey(options, name) for name in (:by, :state)) || _lm_error(
+        "@ordered requires by and state", source; actual=keys(options))
+    by = options[:by]
+    source_ordered = _lm_literal_symbol(by) === :source
+    source_ordered || by isa Expr && by.head === :tuple && length(by.args) == 2 ||
+        _lm_error("@ordered by must be `(key, identity)`", source;
+            actual=by)
+    state_expression = options[:state]
+    state_expression isa Expr && state_expression.head === :tuple ||
+        _lm_error("@ordered state must be target => initial pairs", source;
+            actual=state_expression)
+    state_pairs = Pair{Symbol,Symbol}[]
+    for pair in state_expression.args
+        _lm_call(pair, :(=>)) && length(pair.args) == 3 &&
+            pair.args[2] isa Symbol && pair.args[3] isa Symbol ||
+            _lm_error("ordered state entries must be `target => initial`",
+                source; actual=pair)
+        push!(state_pairs, pair.args[2] => pair.args[3])
+    end
+    targets = first.(state_pairs)
+    state_symbol = gensym(:state)
+    transition_reads = reads_symbol
+    transition_item = item_symbol
+    function ordered_transform(value)
+        value isa Symbol && haskey(evaluator_aliases, value) &&
+            return ordered_transform(evaluator_aliases[value])
+        value === binder && return transition_item
+        value isa Expr || return value
+        if value.head === :ref && value.args[1] isa Symbol &&
+                value.args[1] in targets
+            length(value.args) == 2 || _lm_error(
+                "ordered state reads require one linear index", source;
+                actual=value)
+            return :(getproperty($state_symbol,
+                $(QuoteNode(value.args[1])))[$(ordered_transform(value.args[2]))])
+        elseif value.head === :ref
+            # A descriptor-rooted reference is a new bounded read and
+            # must pass through the ordinary access lowering. References
+            # rooted in an authored alias (including record projections
+            # such as `event.sites[1]`) must instead expand that alias
+            # recursively inside the ordered transition. Sending the
+            # latter back through `transform` would leave the alias as an
+            # accidental global and destroy inference.
+            root = value.args[1]
+            if root isa Symbol && !haskey(evaluator_aliases, root)
+                return transform(value)
+            end
+            return Expr(:ref,
+                (ordered_transform(arg) for arg in value.args)...)
+        end
+        return Expr(value.head, (ordered_transform(arg) for arg in value.args)...)
+    end
+    local_statements = Any[]
+    writes = Dict{Symbol,Any}()
+    halt = false
+    function parse_ordered_block(block, condition=true)
+        block isa Expr && block.head === :block ||
+            _lm_error("@ordered requires a begin/end body", source;
+                actual=block)
+        for value in block.args
+            value isa LineNumberNode && continue
+            if _lm_call(value, :halt_when) && length(value.args) == 2
+                halt === false || _lm_error(
+                    "@ordered admits one halt_when condition", source;
+                    actual=value)
+                halt = ordered_transform(value.args[2])
+            elseif value isa Expr && value.head === :if
+                length(value.args) in (2,3) || _lm_error(
+                    "ordered condition has invalid shape", source; actual=value)
+                length(value.args) == 3 && !(value.args[3] === nothing) &&
+                    _lm_error("ordered state conditions do not admit else",
+                        source; actual=value)
+                combined = condition === true ? ordered_transform(value.args[1]) :
+                    :($condition && $(ordered_transform(value.args[1])))
+                parse_ordered_block(value.args[2], combined)
+            elseif value isa Expr && value.head === :(=) &&
+                    value.args[1] isa Expr && value.args[1].head === :ref &&
+                    value.args[1].args[1] in targets
+                lhs, rhs = value.args
+                name = lhs.args[1]
+                haskey(writes, name) && _lm_error(
+                    "each ordered state component may be assigned once",
+                    source; actual=name)
+                length(lhs.args) == 2 || _lm_error(
+                    "ordered state writes require one bounded index or tuple",
+                    source; actual=lhs)
+                destinations = lhs.args[2] isa Expr &&
+                    lhs.args[2].head === :tuple ? Tuple(lhs.args[2].args) :
+                    (lhs.args[2],)
+                replacements = rhs isa Expr && rhs.head === :tuple ?
+                    Tuple(rhs.args) : (rhs,)
+                length(destinations) == length(replacements) || _lm_error(
+                    "ordered state destination and value widths must match",
+                    source; actual=value)
+                keys = Expr(:tuple, (:(Int32($(ordered_transform(key))))
+                    for key in destinations)...)
+                vals = Expr(:tuple,
+                    (ordered_transform(replacement) for replacement in replacements)...)
+                count = condition === true ? Int32(length(destinations)) :
+                    :(ifelse($condition, Int32($(length(destinations))), Int32(0)))
+                writes[name] = :($(GlobalRef(LocalMath, :_authoring_bounded_writes))(
+                    $keys, $vals, $count))
+            elseif value isa Expr && value.head === :(=) &&
+                    value.args[1] isa Symbol
+                push!(local_statements, Expr(:(=), value.args[1],
+                    ordered_transform(value.args[2])))
+            else
+                _lm_error("ordered bodies admit local values, conditions, and bounded state assignments",
+                    source; actual=value)
+            end
+        end
+    end
+    parse_ordered_block(ordered_body)
+    isempty(writes) && _lm_error("@ordered requires a state assignment", source)
+    missing_targets = filter(target -> !haskey(writes, target), targets)
+    isempty(missing_targets) || _lm_error(
+        "@ordered must define every declared state component in one FoldStep",
+        source; actual=Tuple(missing_targets))
+    update_pairs = Pair{Symbol,Any}[]
+    for pair in state_pairs
+        target = first(pair)
+        expression = writes[target]
+        push!(update_pairs, target => expression)
+    end
+    transition = Expr(:->,
+        Expr(:tuple, state_symbol, gensym(:event), transition_item,
+            transition_reads),
+        Expr(:block, local_statements...,
+            :(return $(GlobalRef(LocalMath, :_authoring_fold_step))(
+                $(_lm_namedtuple(update_pairs)), $(ordered_transform(halt))))))
+    key, identity = source_ordered ? (item_symbol, nothing) :
+        (transform(by.args[1]), transform(by.args[2]))
+    port = publication_port(nothing, :ordered_state)
+    push!(publications, _LocalMathPublicationSyntax(nothing, nothing,
+        port, :ordered_state,
+        source_ordered ? key : Expr(:tuple, key, identity),
+        (; state_pairs=Tuple(state_pairs), transition, by,
+            source_ordered), line))
+    return nothing
+end
+
+"""Parse one field/collection publication equation when the statement is one."""
+function _lm_parse_publication!(
+        statement, current_line, domain_syntax, access, parse_state, source)
+    is_publication = _lm_call(statement, :publish) ||
+        statement.head in (:(=), :(+=)) && statement.args[1] isa Expr &&
+        statement.args[1].head === :ref
+    is_publication || return false
+    (; binder) = domain_syntax
+    (; relation_index, transform) = access
+    (; publications, publication_port, evaluator_type_aliases) = parse_state
+    if _lm_call(statement, :publish)
+        positional, keywords = _lm_call_options(statement, source)
+        length(positional) == 2 || _lm_error(
+            "publish requires a destination Field and one value", source;
+            actual = statement)
+        field, value = positional
+        field isa Symbol || _lm_error(
+            "publish destination must be a simple Field binding", source;
+            actual = field)
+        all(haskey(keywords, key) for key in (:route, :key)) || _lm_error(
+            "runtime publish requires explicit route and key keywords",
+            source; actual = statement)
+        relation = keywords[:route]
+        relation isa Symbol || _lm_error(
+            "publish route must be a simple RuntimeRelation binding",
+            source; actual = relation)
+        law_value = get(keywords, :law, QuoteNode(:unique))
+        law = law_value isa QuoteNode ? law_value.value : law_value
+        law in (:unique, :reduce, :resolve) || _lm_error(
+            "runtime publish law must be :unique, :reduce, or :resolve",
+            source; actual = law)
+        allowed = law === :unique ?
+            (:route, :key, :law, :when, :maximum) :
+            law === :reduce ?
+            (:route, :key, :law, :when, :maximum, :op, :seed,
+                :onempty, :order) :
+                (:route, :key, :law, :when, :maximum, :score, :lower,
+                :upper, :sense, :tie, :onempty)
+        _lm_require_keywords(keywords, allowed, :publish, source)
+        delete!(keywords, :route)
+        delete!(keywords, :law)
+        if law === :resolve
+            all(haskey(keywords, key) for key in (:score, :lower, :upper)) ||
+                _lm_error("runtime Resolve requires score, lower, and upper",
+                    source; actual = statement)
+            keywords[:payload] = value
+            haskey(keywords, :tie) &&
+                (keywords[:_tie_fields] = _lm_explicit_tie_fields(
+                    keywords[:tie], binder, source,
+                    evaluator_type_aliases))
+        end
+        port = publication_port(field, law)
+        transformed_options = (; (key => transform(val)
+            for (key, val) in keywords)...)
+        push!(publications, _LocalMathPublicationSyntax(field, relation,
+            port, law, transform(value), transformed_options, current_line))
+    elseif statement.head in (:(=), :(+=)) && statement.args[1] isa Expr &&
+            statement.args[1].head === :ref
+        lhs, rhs = statement.args
+        length(lhs.args) >= 2 || _lm_error(
+            "publication targets require a bounded index", source; actual = lhs)
+        field, indices = lhs.args[1], Tuple(lhs.args[2:end])
+        field isa Symbol || _lm_error(
+            "publication descriptors must be simple bindings", source;
+            actual = field)
+        relation = relation_index(indices, field)
+        relation === missing && _lm_error(
+            "a publication index must be the item or `relation(item)`",
+            source; actual = indices)
+        law, value, options = statement.head === :(+=) ?
+            (:reduce, rhs, NamedTuple()) : (:unique, rhs, NamedTuple())
+        if _lm_call(rhs, :reduce_to)
+            positional, keywords = _lm_call_options(rhs, source)
+            _lm_require_keywords(keywords,
+                (:op, :seed, :order, :onempty, :when, :maximum),
+                :reduce_to, source)
+            length(positional) == 1 || _lm_error(
+                "reduce_to requires one contribution", source; actual = rhs)
+            law, value = :reduce, only(positional)
+            options = (; (key => val for (key, val) in keywords)...)
+        elseif _lm_call(rhs, :resolve_to)
+            positional, keywords = _lm_call_options(rhs, source)
+            _lm_require_keywords(keywords,
+                (:score, :payload, :lower, :upper, :sense, :when,
+                    :maximum, :tie, :onempty), :resolve_to, source)
+            isempty(positional) || _lm_error(
+                "resolve_to uses score and payload keywords", source; actual = rhs)
+            all(haskey(keywords, key) for key in (:score, :payload, :lower, :upper)) ||
+                _lm_error("resolve_to requires score, payload, lower, and upper",
+                    source; actual = rhs)
+            haskey(keywords, :tie) &&
+                (keywords[:_tie_fields] = _lm_explicit_tie_fields(
+                    keywords[:tie], binder, source,
+                    evaluator_type_aliases))
+            law, value = :resolve, nothing
+            options = (; (key => val for (key, val) in keywords)...)
+        elseif _lm_call(rhs, :bounded_collect)
+            positional, keywords = _lm_call_options(rhs, source)
+            _lm_require_keywords(keywords,
+                (:maximum, :group, :groups, :overflow, :when,
+                    :order, :projection),
+                :bounded_collect, source)
+            length(positional) == 1 || _lm_error(
+                "bounded_collect requires one record", source; actual = rhs)
+            haskey(keywords, :maximum) || _lm_error(
+                "bounded_collect requires a static maximum", source; actual = rhs)
+            overflow = _lm_literal_symbol(get(keywords, :overflow,
+                QuoteNode(:reject)))
+            overflow === :reject || _lm_error(
+                "bounded_collect currently supports only overflow=:reject",
+                source; actual = overflow)
+            haskey(keywords, :group) == haskey(keywords, :groups) ||
+                _lm_error("routed Collect requires both group and groups",
+                    source; actual = keys(keywords))
+            law, value = :collect, only(positional)
+            options = (; (key => val for (key, val) in keywords)...)
+        end
+        port = publication_port(field, law)
+        transformed_value = value === nothing ? nothing : transform(value)
+        transformed_options = (; (key => transform(val)
+            for (key, val) in pairs(options))...)
+        push!(publications, _LocalMathPublicationSyntax(field, relation,
+            port, law, transformed_value, transformed_options, current_line))
+    end
+    return true
+end
+
+"""Parse stage statements in authored order using the dedicated law parsers."""
+function _lm_parse_stage_body(body, domain_syntax, access, source)
+    (; transform) = access
     publications = _LocalMathPublicationSyntax[]
     used_publication_ports = Dict{Symbol,Int}()
     function publication_port(field, law::Symbol)
@@ -460,281 +745,18 @@ function _lm_lower_stage(spec, body::Expr, source; label = nothing)
     evaluator_statements = Any[]
     evaluator_aliases = Dict{Symbol,Any}()
     evaluator_type_aliases = Dict{Symbol,Any}()
-    function ordered_syntax(statement, line)
-        length(statement.args) == 4 || _lm_error(
-            "@ordered requires `(by=..., state=...)` and a body", source;
-            actual = statement)
-        specification, ordered_body = statement.args[3], statement.args[4]
-        specification isa Expr && specification.head === :tuple || _lm_error(
-            "@ordered requires `(by=..., state=...)`", source;
-            actual = specification)
-        options = Dict{Symbol,Any}()
-        for option in specification.args
-            option isa Expr && option.head === :(=) &&
-                option.args[1] in (:by, :state) || _lm_error(
-                    "@ordered accepts only by and state", source; actual=option)
-            options[option.args[1]] = option.args[2]
-        end
-        all(haskey(options, name) for name in (:by, :state)) || _lm_error(
-            "@ordered requires by and state", source; actual=keys(options))
-        by = options[:by]
-        source_ordered = _lm_literal_symbol(by) === :source
-        source_ordered || by isa Expr && by.head === :tuple && length(by.args) == 2 ||
-            _lm_error("@ordered by must be `(key, identity)`", source;
-                actual=by)
-        state_expression = options[:state]
-        state_expression isa Expr && state_expression.head === :tuple ||
-            _lm_error("@ordered state must be target => initial pairs", source;
-                actual=state_expression)
-        state_pairs = Pair{Symbol,Symbol}[]
-        for pair in state_expression.args
-            _lm_call(pair, :(=>)) && length(pair.args) == 3 &&
-                pair.args[2] isa Symbol && pair.args[3] isa Symbol ||
-                _lm_error("ordered state entries must be `target => initial`",
-                    source; actual=pair)
-            push!(state_pairs, pair.args[2] => pair.args[3])
-        end
-        targets = first.(state_pairs)
-        state_symbol = gensym(:state)
-        transition_reads = reads_symbol
-        transition_item = item_symbol
-        function ordered_transform(value)
-            value isa Symbol && haskey(evaluator_aliases, value) &&
-                return ordered_transform(evaluator_aliases[value])
-            value === binder && return transition_item
-            value isa Expr || return value
-            if value.head === :ref && value.args[1] isa Symbol &&
-                    value.args[1] in targets
-                length(value.args) == 2 || _lm_error(
-                    "ordered state reads require one linear index", source;
-                    actual=value)
-                return :(getproperty($state_symbol,
-                    $(QuoteNode(value.args[1])))[$(ordered_transform(value.args[2]))])
-            elseif value.head === :ref
-                # A descriptor-rooted reference is a new bounded read and
-                # must pass through the ordinary access lowering. References
-                # rooted in an authored alias (including record projections
-                # such as `event.sites[1]`) must instead expand that alias
-                # recursively inside the ordered transition. Sending the
-                # latter back through `transform` would leave the alias as an
-                # accidental global and destroy inference.
-                root = value.args[1]
-                if root isa Symbol && !haskey(evaluator_aliases, root)
-                    return transform(value)
-                end
-                return Expr(:ref,
-                    (ordered_transform(arg) for arg in value.args)...)
-            end
-            return Expr(value.head, (ordered_transform(arg) for arg in value.args)...)
-        end
-        local_statements = Any[]
-        writes = Dict{Symbol,Any}()
-        halt = false
-        function parse_ordered_block(block, condition=true)
-            block isa Expr && block.head === :block ||
-                _lm_error("@ordered requires a begin/end body", source;
-                    actual=block)
-            for value in block.args
-                value isa LineNumberNode && continue
-                if _lm_call(value, :halt_when) && length(value.args) == 2
-                    halt === false || _lm_error(
-                        "@ordered admits one halt_when condition", source;
-                        actual=value)
-                    halt = ordered_transform(value.args[2])
-                elseif value isa Expr && value.head === :if
-                    length(value.args) in (2,3) || _lm_error(
-                        "ordered condition has invalid shape", source; actual=value)
-                    length(value.args) == 3 && !(value.args[3] === nothing) &&
-                        _lm_error("ordered state conditions do not admit else",
-                            source; actual=value)
-                    combined = condition === true ? ordered_transform(value.args[1]) :
-                        :($condition && $(ordered_transform(value.args[1])))
-                    parse_ordered_block(value.args[2], combined)
-                elseif value isa Expr && value.head === :(=) &&
-                        value.args[1] isa Expr && value.args[1].head === :ref &&
-                        value.args[1].args[1] in targets
-                    lhs, rhs = value.args
-                    name = lhs.args[1]
-                    haskey(writes, name) && _lm_error(
-                        "each ordered state component may be assigned once",
-                        source; actual=name)
-                    length(lhs.args) == 2 || _lm_error(
-                        "ordered state writes require one bounded index or tuple",
-                        source; actual=lhs)
-                    destinations = lhs.args[2] isa Expr &&
-                        lhs.args[2].head === :tuple ? Tuple(lhs.args[2].args) :
-                        (lhs.args[2],)
-                    replacements = rhs isa Expr && rhs.head === :tuple ?
-                        Tuple(rhs.args) : (rhs,)
-                    length(destinations) == length(replacements) || _lm_error(
-                        "ordered state destination and value widths must match",
-                        source; actual=value)
-                    keys = Expr(:tuple, (:(Int32($(ordered_transform(key))))
-                        for key in destinations)...)
-                    vals = Expr(:tuple,
-                        (ordered_transform(replacement) for replacement in replacements)...)
-                    count = condition === true ? Int32(length(destinations)) :
-                        :(ifelse($condition, Int32($(length(destinations))), Int32(0)))
-                    writes[name] = :($(GlobalRef(LocalMath, :_authoring_bounded_writes))(
-                        $keys, $vals, $count))
-                elseif value isa Expr && value.head === :(=) &&
-                        value.args[1] isa Symbol
-                    push!(local_statements, Expr(:(=), value.args[1],
-                        ordered_transform(value.args[2])))
-                else
-                    _lm_error("ordered bodies admit local values, conditions, and bounded state assignments",
-                        source; actual=value)
-                end
-            end
-        end
-        parse_ordered_block(ordered_body)
-        isempty(writes) && _lm_error("@ordered requires a state assignment", source)
-        missing_targets = filter(target -> !haskey(writes, target), targets)
-        isempty(missing_targets) || _lm_error(
-            "@ordered must define every declared state component in one FoldStep",
-            source; actual=Tuple(missing_targets))
-        update_pairs = Pair{Symbol,Any}[]
-        for pair in state_pairs
-            target = first(pair)
-            expression = writes[target]
-            push!(update_pairs, target => expression)
-        end
-        transition = Expr(:->,
-            Expr(:tuple, state_symbol, gensym(:event), transition_item,
-                transition_reads),
-            Expr(:block, local_statements...,
-                :(return $(GlobalRef(LocalMath, :_authoring_fold_step))(
-                    $(_lm_namedtuple(update_pairs)), $(ordered_transform(halt))))))
-        key, identity = source_ordered ? (item_symbol, nothing) :
-            (transform(by.args[1]), transform(by.args[2]))
-        port = publication_port(nothing, :ordered_state)
-        push!(publications, _LocalMathPublicationSyntax(nothing, nothing,
-            port, :ordered_state,
-            source_ordered ? key : Expr(:tuple, key, identity),
-            (; state_pairs=Tuple(state_pairs), transition, by,
-                source_ordered), line))
-        return nothing
-    end
+    parse_state = (; publications, publication_port, evaluator_aliases,
+        evaluator_type_aliases)
     current_line = source.line
     for statement in body.args
         statement isa LineNumberNode && (current_line = statement.line; continue)
         statement isa Expr || (push!(evaluator_statements, statement); continue)
         if statement.head === :macrocall &&
                 statement.args[1] === Symbol("@ordered")
-            ordered_syntax(statement, current_line)
-        elseif _lm_call(statement, :publish)
-            positional, keywords = _lm_call_options(statement, source)
-            length(positional) == 2 || _lm_error(
-                "publish requires a destination Field and one value", source;
-                actual = statement)
-            field, value = positional
-            field isa Symbol || _lm_error(
-                "publish destination must be a simple Field binding", source;
-                actual = field)
-            all(haskey(keywords, key) for key in (:route, :key)) || _lm_error(
-                "runtime publish requires explicit route and key keywords",
-                source; actual = statement)
-            relation = keywords[:route]
-            relation isa Symbol || _lm_error(
-                "publish route must be a simple RuntimeRelation binding",
-                source; actual = relation)
-            law_value = get(keywords, :law, QuoteNode(:unique))
-            law = law_value isa QuoteNode ? law_value.value : law_value
-            law in (:unique, :reduce, :resolve) || _lm_error(
-                "runtime publish law must be :unique, :reduce, or :resolve",
-                source; actual = law)
-            allowed = law === :unique ?
-                (:route, :key, :law, :when, :maximum) :
-                law === :reduce ?
-                (:route, :key, :law, :when, :maximum, :op, :seed,
-                    :onempty, :order) :
-                    (:route, :key, :law, :when, :maximum, :score, :lower,
-                    :upper, :sense, :tie, :onempty)
-            _lm_require_keywords(keywords, allowed, :publish, source)
-            delete!(keywords, :route)
-            delete!(keywords, :law)
-            if law === :resolve
-                all(haskey(keywords, key) for key in (:score, :lower, :upper)) ||
-                    _lm_error("runtime Resolve requires score, lower, and upper",
-                        source; actual = statement)
-                keywords[:payload] = value
-                haskey(keywords, :tie) &&
-                    (keywords[:_tie_fields] = _lm_explicit_tie_fields(
-                        keywords[:tie], binder, source,
-                        evaluator_type_aliases))
-            end
-            port = publication_port(field, law)
-            transformed_options = (; (key => transform(val)
-                for (key, val) in keywords)...)
-            push!(publications, _LocalMathPublicationSyntax(field, relation,
-                port, law, transform(value), transformed_options, current_line))
-        elseif statement.head in (:(=), :(+=)) && statement.args[1] isa Expr &&
-                statement.args[1].head === :ref
-            lhs, rhs = statement.args
-            length(lhs.args) >= 2 || _lm_error(
-                "publication targets require a bounded index", source; actual = lhs)
-            field, indices = lhs.args[1], Tuple(lhs.args[2:end])
-            field isa Symbol || _lm_error(
-                "publication descriptors must be simple bindings", source;
-                actual = field)
-            relation = relation_index(indices, field)
-            relation === missing && _lm_error(
-                "a publication index must be the item or `relation(item)`",
-                source; actual = indices)
-            law, value, options = statement.head === :(+=) ?
-                (:reduce, rhs, NamedTuple()) : (:unique, rhs, NamedTuple())
-            if _lm_call(rhs, :reduce_to)
-                positional, keywords = _lm_call_options(rhs, source)
-                _lm_require_keywords(keywords,
-                    (:op, :seed, :order, :onempty, :when, :maximum),
-                    :reduce_to, source)
-                length(positional) == 1 || _lm_error(
-                    "reduce_to requires one contribution", source; actual = rhs)
-                law, value = :reduce, only(positional)
-                options = (; (key => val for (key, val) in keywords)...)
-            elseif _lm_call(rhs, :resolve_to)
-                positional, keywords = _lm_call_options(rhs, source)
-                _lm_require_keywords(keywords,
-                    (:score, :payload, :lower, :upper, :sense, :when,
-                        :maximum, :tie, :onempty), :resolve_to, source)
-                isempty(positional) || _lm_error(
-                    "resolve_to uses score and payload keywords", source; actual = rhs)
-                all(haskey(keywords, key) for key in (:score, :payload, :lower, :upper)) ||
-                    _lm_error("resolve_to requires score, payload, lower, and upper",
-                        source; actual = rhs)
-                haskey(keywords, :tie) &&
-                    (keywords[:_tie_fields] = _lm_explicit_tie_fields(
-                        keywords[:tie], binder, source,
-                        evaluator_type_aliases))
-                law, value = :resolve, nothing
-                options = (; (key => val for (key, val) in keywords)...)
-            elseif _lm_call(rhs, :bounded_collect)
-                positional, keywords = _lm_call_options(rhs, source)
-                _lm_require_keywords(keywords,
-                    (:maximum, :group, :groups, :overflow, :when,
-                        :order, :projection),
-                    :bounded_collect, source)
-                length(positional) == 1 || _lm_error(
-                    "bounded_collect requires one record", source; actual = rhs)
-                haskey(keywords, :maximum) || _lm_error(
-                    "bounded_collect requires a static maximum", source; actual = rhs)
-                overflow = _lm_literal_symbol(get(keywords, :overflow,
-                    QuoteNode(:reject)))
-                overflow === :reject || _lm_error(
-                    "bounded_collect currently supports only overflow=:reject",
-                    source; actual = overflow)
-                haskey(keywords, :group) == haskey(keywords, :groups) ||
-                    _lm_error("routed Collect requires both group and groups",
-                        source; actual = keys(keywords))
-                law, value = :collect, only(positional)
-                options = (; (key => val for (key, val) in keywords)...)
-            end
-            port = publication_port(field, law)
-            transformed_value = value === nothing ? nothing : transform(value)
-            transformed_options = (; (key => transform(val)
-                for (key, val) in pairs(options))...)
-            push!(publications, _LocalMathPublicationSyntax(field, relation,
-                port, law, transformed_value, transformed_options, current_line))
+            _lm_parse_ordered_state!(
+                statement, current_line, domain_syntax, access, parse_state, source)
+        elseif _lm_parse_publication!(
+                statement, current_line, domain_syntax, access, parse_state, source)
         elseif statement.head === :while
             _lm_error("@localmath does not admit unbounded while loops", source;
                 actual = statement)
@@ -750,6 +772,19 @@ function _lm_lower_stage(spec, body::Expr, source; label = nothing)
     isempty(publications) && _lm_error(
         "an @localmath stage requires at least one publication equation", source)
 
+    return (; publications, evaluator_statements,
+        evaluator_type_aliases)
+end
+
+"""Emit hygienic typed LocalMath constructors from parsed authoring facts."""
+function _lm_emit_stage(
+        domain_syntax, declarations, access, parsed, source, label)
+    (; binder, source_expression, semantic_source_expression, stage_options,
+        cartesian, binder_symbols, source_mode, halo) = domain_syntax
+    (; reads, synthetic_relation_expressions, reads_symbol,
+        parameters_symbol, item_symbol) = access
+    (; publications, evaluator_statements, evaluator_type_aliases) = parsed
+    parameter_names = Tuple(declaration.args[1] for declaration in declarations)
     source_local, full_source_local, identity_local =
         gensym(:source), gensym(:full_source), gensym(:identity)
     field_reads = filter(read -> read isa _LocalMathReadSyntax, reads)
@@ -1112,6 +1147,17 @@ function _lm_lower_stage(spec, body::Expr, source; label = nothing)
         :($(GlobalRef(LocalMath, :LocalLaw))($stage)))
 end
 
+"""Lower one authored stage directly to existing typed LocalMath values."""
+function _lm_lower_stage(spec, body::Expr, source; label = nothing)
+    domain_syntax = _lm_stage_domain(spec, source)
+    declarations = _lm_parameters(
+        domain_syntax.stage_options.parameters, source)
+    access = _lm_discover_stage_accesses(domain_syntax, source)
+    parsed = _lm_parse_stage_body(body, domain_syntax, access, source)
+    return _lm_emit_stage(
+        domain_syntax, declarations, access, parsed, source, label)
+end
+
 function _lm_lower(args, source)
     if length(args) == 2
         spec, body = args