DeepLink-org · reiase · Aug 9, 2026 · Aug 9, 2026
diff --git a/.gitignore b/.gitignore
@@ -1,4 +1,5 @@
 *.pyc
+.DS_Store
 .VSCodeCounter/
 **/.ipynb_checkpoints/*
 build/

diff --git a/README.md b/README.md
@@ -138,7 +138,7 @@ It provides a shared configuration surface for single-point analysis, canonical
 TP/PP/DP strategy exploration. Analysis runs outside the UI event loop, and failed candidates remain visible as
 structured diagnostics.
 
-The existing Calculon and floating-point Streamlit tools remain isolated as an optional legacy interface:
+The existing Calculon Streamlit tools remain isolated as an optional legacy interface. Floating-point analysis is available in the primary NiceGUI workbench:
 
 ```bash
 uv sync --extra legacy-ui

diff --git a/data/validation/baseline_regression_contract.json b/data/validation/baseline_regression_contract.json
@@ -18,14 +18,14 @@
       "paper_mean_absolute_error_percent": 3.654361437637248,
       "paper_max_absolute_error_percent": 8.874452316395821,
       "portable_digests": {
-        "seqsel-tab5/megatron-22B/full": "a702e06f09e0e7ed49b1d06371fdc5f01df40ead",
-        "seqsel-tab5/megatron-22B/seqsel": "d8c1a76517458d5bd92af95c125225a00c1b6a61",
-        "seqsel-tab5/gpt3-175B/full": "b9ed7a9c81a7cbd02066e000478d3488e31c3321",
-        "seqsel-tab5/gpt3-175B/seqsel": "bf7be9b50d482232aaee649c506f4afca5c9dfcb",
-        "seqsel-tab5/turing-530B/full": "3988fe962f1ccecca2cee3a08b98da5e177f8c65",
-        "seqsel-tab5/turing-530B/seqsel": "2e9047b02f855c3527c07cfae116bbc41631eaea",
-        "seqsel-tab5/megatron-1T/full": "d4a11ba89f39f36f002ee9c0179bbc02dc62a542",
-        "seqsel-tab5/megatron-1T/seqsel": "7549a08665566ef4187e9a37ca50d860308c8800"
+        "seqsel-tab5/megatron-22B/full": "00517ca9fb4df346eebe6d4aa63543ca666a7af4",
+        "seqsel-tab5/megatron-22B/seqsel": "8eb389c417a9b33124997c21afd5c18597a39404",
+        "seqsel-tab5/gpt3-175B/full": "2ce66153c5c81ee97c6fa1e2bc14b9e2c0d844ff",
+        "seqsel-tab5/gpt3-175B/seqsel": "5c888d51fd8d5ffb5bb515ff797a9776a12cea6c",
+        "seqsel-tab5/turing-530B/full": "99c4b79b949fa4f58ffbd1cc98661d3b2101f5d6",
+        "seqsel-tab5/turing-530B/seqsel": "4a33b75f901df8c5d4948a8f44d501e8f695674e",
+        "seqsel-tab5/megatron-1T/full": "0e203dc354d91a45d8860c15aee999d57dbb5bbf",
+        "seqsel-tab5/megatron-1T/seqsel": "e7c5e86b0f7e9f9f8f3f47124fc643cf4a4d8e09"
       }
     }
   },

diff --git a/docs/design/ir/model-distributed.en.md b/docs/design/ir/model-distributed.en.md
@@ -6,17 +6,16 @@
 
 ### Semantic domain
 
-`ModelIR` represents tensor and scalar values, typed operations, regions, dataflow, state roles, and effects. It can represent training and inference semantics, symbolic dimensions, parameters, activations, optimizer state, and KV-cache state where known.
+`ModelIR` represents tensor values, typed operations, explicit dataflow, state roles, and effects. It can represent training and inference semantics, symbolic dimensions, parameters, activations, optimizer state, and KV-cache state where known. Semantic regions remain a future contract rather than a current field.
 
 ### Core entities
 
 ```text
 ModelIR
 ├── values: ModelValue[]
 ├── operations: ModelOperation[]
-├── regions: SemanticRegion[]
 ├── inputs / outputs
-├── extensions
+├── attributes
 └── header
 ```
 
@@ -28,7 +27,7 @@ Operations explicitly reference input and output values. Effects such as paramet
 
 ### Well-formedness
 
-The verifier checks unique IDs, definition/use closure, type compatibility, region ownership, input/output reachability, effect ordering, symbolic-domain validity, and deterministic extensions.
+The current structural verifier checks unique IDs, definition/use closure, input/output references, SSA single definition, target-dialect exclusion, and reserved attributes. Cross-operation type/shape compatibility, region ownership, complete effect ordering, and numerical references still require independent checkers or future verifier work.
 
 ### Transformations
 
@@ -44,12 +43,11 @@ Allowed passes include import, shape/type inference, canonicalization, decomposi
 
 ```text
 DistributedTaskIR
-├── meshes: LogicalMesh[]
-├── ranks: LogicalRank[]
+├── mesh: LogicalMesh
 ├── values: DistributedValue[]
-├── tasks: ComputeTask | CollectiveTask | P2PTask | ReshardTask
-├── dependencies
-├── memory_facts
+├── tasks: DistributedTask[]
+├── inputs / outputs
+├── attributes
 └── lineage to ModelIR
 ```
 
@@ -61,7 +59,7 @@ This IR cannot name CUDA, ROCm, LPU, NCCL, physical routes, physical device IDs,
 
 ### Well-formedness
 
-The verifier checks mesh and rank membership, shard reconstruction, ownership, communication matching, message-volume conservation, reshard completeness, cross-rank dependency closure, and effect order.
+The current structural verifier checks mesh and rank membership, sharding rank and axes, ownership, task/value references, DAG order, and local communication-metadata legality. Shard reconstruction, collective matching, message-volume conservation, reshard completeness, and cross-rank semantic closure remain target capabilities for observers and conformance checkers.
 
 ### Transformations
 
@@ -83,8 +81,8 @@ Model linear(x, w)
 
 The current Transformer frontend emits one coarse decoder-training `ModelIR` operation. `DistributeTransformerTrainingPass` expands it into typed primitive invocations and a local TP task DAG with explicit collectives, recomputation phases, and aggregate block memory facts.
 
-The current graph models one local Transformer block conservatively. Full-model PP/DP graphs, cross-stage values, richer topology, inference regions, and KV-cache distribution remain planned.
+The current training graph models one local Transformer block conservatively. Static inference already implements separate prefill/decode phases, KV-cache state and values, and local TP distribution; full-model PP/DP graphs, cross-stage values, richer topology, and inference regions remain planned.
 
 ## Profiler and verification checkpoint
 
-At `ModelIR`, observers can check shapes, types, effects, and optional numerical references. At `DistributedTaskIR`, they can check shard reconstruction, per-rank work, communication matching, and volume conservation. Neither checkpoint may introduce target duration.
+At `ModelIR`, observers can add shape, type, effect, and optional numerical-reference checks. At `DistributedTaskIR`, they can add shard reconstruction, per-rank work, communication matching, and volume-conservation checks; these capabilities must not be inferred from the current structural verifier. Neither checkpoint may introduce target duration.
diff --git a/docs/design/ir/model-distributed.zh.md b/docs/design/ir/model-distributed.zh.md
@@ -6,17 +6,16 @@
 
 ### 语义域
 
-`ModelIR` 表示 tensor/scalar value、typed operation、region、dataflow、state role 和 effect。它可以表示 training/inference semantic、symbolic dimension、parameter、activation、optimizer state，以及已知情况下的 KV-cache state。
+`ModelIR` 表示 tensor value、typed operation、显式 dataflow、state role 和 effect。它可以表示 training/inference semantic、symbolic dimension、parameter、activation、optimizer state，以及已知情况下的 KV-cache state。Semantic region 仍是后续 contract，不是当前字段。
 
 ### 核心 Entity
 
 ```text
 ModelIR
 ├── values: ModelValue[]
 ├── operations: ModelOperation[]
-├── regions: SemanticRegion[]
 ├── inputs / outputs
-├── extensions
+├── attributes
 └── header
 ```
 
@@ -28,7 +27,7 @@ Operation 显式引用 input/output value。Parameter update、random state、mu
 
 ### Well-formedness
 
-Verifier 检查 unique ID、definition/use closure、type compatibility、region ownership、input/output reachability、effect ordering、symbolic-domain validity 和 deterministic extension。
+当前 structural verifier 检查 unique ID、definition/use closure、input/output reference、SSA single definition、target dialect exclusion 与 reserved attributes。Operation 间 type/shape compatibility、region ownership、完整 effect ordering 与 numerical reference 仍需独立 checker 或后续 verifier 实现。
 
 ### Transformation
 
@@ -44,12 +43,11 @@ Verifier 检查 unique ID、definition/use closure、type compatibility、region
 
 ```text
 DistributedTaskIR
-├── meshes: LogicalMesh[]
-├── ranks: LogicalRank[]
+├── mesh: LogicalMesh
 ├── values: DistributedValue[]
-├── tasks: ComputeTask | CollectiveTask | P2PTask | ReshardTask
-├── dependencies
-├── memory_facts
+├── tasks: DistributedTask[]
+├── inputs / outputs
+├── attributes
 └── lineage to ModelIR
 ```
 
@@ -61,7 +59,7 @@ Communication operation 保留 logical semantic：participant、collective kind
 
 ### Well-formedness
 
-Verifier 检查 mesh/rank membership、shard reconstruction、ownership、communication matching、message-volume conservation、reshard completeness、cross-rank dependency closure 和 effect order。
+当前 structural verifier 检查 mesh/rank membership、sharding rank/axis、ownership、task/value reference、DAG 顺序和 communication metadata 的局部合法性。Shard reconstruction、collective matching、message-volume conservation、reshard completeness 与 cross-rank semantic closure 仍是 observer/conformance checker 的目标能力。
 
 ### Transformation
 
@@ -83,8 +81,8 @@ Model linear(x, w)
 
 当前 Transformer frontend 输出一个 coarse decoder-training `ModelIR` operation。`DistributeTransformerTrainingPass` 把它展开为 typed primitive invocation 和 local TP task DAG，并包含显式 collective、recomputation phase 和 aggregate block memory fact。
 
-当前 graph 以保守方式建模一个 local Transformer block。Full-model PP/DP graph、cross-stage value、更丰富 topology、inference region 和 KV-cache distribution 仍在规划中。
+当前 training graph 以保守方式建模一个 local Transformer block。静态 inference 已实现独立 prefill/decode phase、KV-cache state/value 与 local TP distribution；full-model PP/DP graph、cross-stage value、更丰富 topology 和 inference region 仍在规划中。
 
 ## Profiler 与 Verification Checkpoint
 
-在 `ModelIR`，observer 可以检查 shape、type、effect 和可选 numerical reference。在 `DistributedTaskIR`，它可以检查 shard reconstruction、per-rank work、communication matching 和 volume conservation。两个 checkpoint 都不能引入 target duration。
+在 `ModelIR`，observer 可以补充检查 shape、type、effect 和可选 numerical reference。在 `DistributedTaskIR`，observer 可以补充检查 shard reconstruction、per-rank work、communication matching 和 volume conservation；这些能力不能从当前 structural verifier 自动推断。两个 checkpoint 都不能引入 target duration。
diff --git a/docs/design/passes/transformer.en.md b/docs/design/passes/transformer.en.md
@@ -19,15 +19,15 @@ TransformerModelSpec + TransformerTrainingWorkloadSpec + TransformerTrainingMapp
 
 The red boundary in the figure is intentional. `SystemProfile` is consumed only by a derived estimate after `PortablePlanIR`; it is not an implicit target binding and it does not make `ConcretePlanIR` available.
 
-This slice currently models decoder-only training at block scope. Full-model PP/DP task graphs, inference prefill/decode, intermediate-buffer lifetimes, target legalization, and physical scheduling remain subsequent work.
+This page covers decoder-only training at block scope; the repository separately implements a static inference prefill/decode phase slice. Full-model PP/DP task graphs, complete intermediate-buffer lifetimes, target legalization, and physical scheduling remain subsequent work.
 
 ## Typed semantic import
 
 `TransformerModelSpec` owns dimensions and model semantics. `TransformerTrainingWorkloadSpec` owns global/micro batch size and datatype. `TransformerTrainingMappingSpec` owns TP/PP/DP, recomputation, pipeline interleaving, optimizer sharding, and tensor-parallel communication mode. `synthesis_session_for()` converts these independent contracts into explicit workload and strategy bindings.
 
 Physical network-tier selection is deliberately absent. `NetworkTierBinding` is supplied only when a portable plan is evaluated against a `SystemProfile`; changing it cannot change the model, distributed, or portable-plan digest.
 
-The importer rejects invalid dimensions, head divisibility, parallel topology, and inconsistent workload facts before a pass runs. `build_transformer_model_ir()` then creates a coarse, target-neutral `transformer.decoder_training` operation. No target name, peak rate, kernel ID, or latency enters this snapshot.
+The importer rejects invalid dimensions, TP divisibility failures, sequence dimensions that cannot be evenly partitioned under RS+AG, invalid parallel topology, and inconsistent workload or strategy facts before a pass runs. At TP=1, AR and RS+AG have identical local work and memory semantics. `build_transformer_model_ir()` then creates a coarse, target-neutral `transformer.decoder_training` operation. No target name, peak rate, kernel ID, or latency enters this snapshot.
 
 ## Static workload derivation
 
@@ -47,14 +47,14 @@ Recomputation is also structural. Full recomputation clones the required forward
 - distributed boundary values and sharding;
 - stable lineage from every task and value to its model source.
 
-The current dependency chain is conservative and serial within the local block. That is a correctness baseline, not a claim that no target can overlap work. Physical queues, routes, collective algorithms, and overlap are forbidden at this layer because they require target and deployment knowledge.
+The current block has explicit, conservative forward, recompute, backward, and optimizer stage ordering, while remaining serial within each stage. The external block output is produced at the forward terminal; optimizer work cannot masquerade as its activation producer. This is a stage-level correctness baseline, not a claim that no target can overlap work; primitive-level activation/gradient SSA and exact lifetimes are not yet materialized. Physical queues, routes, collective algorithms, and overlap are forbidden at this layer because they require target and deployment knowledge.
 
 The pass must preserve workload semantics and satisfy these checks:
 
 1. the logical mesh size agrees with the strategy;
 2. every rank and dependency resolves;
-3. shard specifications reconstruct the logical boundary tensor;
-4. collective participants, reduction semantics, and message volumes are well formed;
+3. shard rank, mesh axes, ownership, and references are valid;
+4. collective participants, reduction semantics, and non-negative message volumes are structurally well formed;
 5. the output records the source `ModelIR` digest.
 
 ## Portable-plan derivation
@@ -92,7 +92,7 @@ The derivation does not compensate for a discrepancy by reading a reference late
 | Logical mapping contract | `src/blueprinting/mapping/transformer.py` | boundary and validation tests |
 | Workload-to-IR frontend | `src/blueprinting/synthesizer/frontend/transformer.py` | canonical representation and calibration tests |
 | Workload algebra | `src/blueprinting/synthesizer/dialects/transformer/training.py` | `tests/validation/test_calculon.py` |
-| Two derivation passes | `src/blueprinting/synthesizer/lowering/transformer.py` | canonical representation and calibration tests |
+| Two derivation passes | `src/blueprinting/synthesizer/lowering/transformer.py` | `tests/synthesizer/test_transformer_training.py` and calibration tests |
 | Transaction/checkpoints | `src/blueprinting/synthesizer/passes/base.py` | `tests/synthesizer/test_pass_manager.py` |
 | Evidence-derived estimates | `src/blueprinting/analysis/cost_model.py` | validation tests |
 | Calculon/SeqSel oracle gate | `src/blueprinting/validation/calculon.py` | `tests/validation/test_calculon.py` |