Clarify LocalMath architecture and authoring ownership

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.

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

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)

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
@@ -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
 

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