title

SMPDC Paper 06｜擴散程式語言與可驗證編譯器：持續工作流、相位效果、線性資源、PDAIS-IR 與異質降階

english_title

Diffusive Programming Language and Verifiable Compiler: Persistent Workflows, Phase Effects, Linear Resources, PDAIS-IR, and Heterogeneous Lowering

series

SMPDC — Stellar Multi-Primary Persistent Diffusive Computing

paper

06 / 11

version

0.1

status

Full Research Manuscript — Candidate Language/Compiler Contract; Implementation and Performance Validation Pending

date

2026-10-16

language

zh-TW

primary_concept_originator

Neo.K

research_collaboration

Aletheia / GPT-6

institution

EveMissLab / 一言諾科技有限公司

canonical_source

UTF-8 Markdown; inline math $...$ ; display math $$...$$

predecessors

SMPDC Paper 00 v0.1 (2026-10-16) · SMPDC Paper 01 v0.1 (2026-10-16) · SMPDC Paper 02 v0.1 (2026-10-16) · SMPDC Paper 03 v0.1 (2026-10-16) · SMPDC Paper 04 v0.1 (2026-10-16) · SMPDC Paper 05 v0.1 (2026-10-16)

artifact_scope

Language design, typed effect calculus, operational constraints, compiler intermediate representations, conformance rules, conditional correctness propositions, reference implementation plan, and falsifiable evaluation

SMPDC Paper 06｜擴散程式語言與可驗證編譯器

——持續工作流、相位效果、線性資源、PDAIS-IR 與 CPU／GPU 異質降階

英文： Diffusive Programming Language and Verifiable Compiler: Persistent Workflows, Phase Effects, Linear Resources, PDAIS-IR, and Heterogeneous Lowering
系列： 群星多主節點持續擴散計算論（SMPDC）
主構想提出： Neo.K
研究協作： Aletheia / GPT-6
機構： EveMissLab／一言諾科技有限公司
版本／日期： v0.1／2026-10-16
成熟度： L1，具有候選語法、語義與驗證規格；本文中的語言範例及編譯流程是待實作的研究規格，不是已產生可執行二進位檔的產品聲明。
直接前置： SMPDC Paper 00–05 [I0–I5]。

作者： Neo.K
日期： 2026-10-16
版本： 0.1

摘要

SMPDC 第一系列 Paper 00–05 已提出多主工作流的邏輯自治、具型別相位耦合、有界持續擴散、R0–R3 冗餘資訊流、推測計算與權威提交分離，以及持續擴散抽象指令集 PDAIS。若這些約束只能由程式員手工透過普通函式呼叫排列，實際系統將缺乏一個可以同時理解邏輯工作流身分、跨節點事件世代、一次性傳播權、證據血緣、暫態／正式結果、外部效果與 CPU／GPU 可見性的共同語義邊界。另一方面，現代語言、型別系統與 MLIR/LLVM 已有非同步、線性／仿射所有權、效果註記、SSA、記憶體順序及 GPU 降階等成熟能力；不應僅因構想具有「擴散」「群星」「類神經」等詞彙便宣稱必須從零發明整套語言技術。

本文提出候選語言 SMPDC-Lang（暫用名稱） 與其編譯器 SMPDC-C。語言不將每個 CPU 核心硬編碼成不可移動的執行緒，而以 flow 定義可持續、可喚醒、可安全重綁的邏輯主工作流；以具型別 phase 及 couple 約束交互資格；以不可複製的 SendCredit、DeliveryPermit 與 EventEpoch 限制擴散；以不同建構子與來源證明區分 R1 競速、R2 佐證和 R3 編碼復原；以 Tentative<T,B>、SealedLocalOutcome<K>、ValidatedProposal<K> 與 Committed<T,K> 排除無授權的正式結果轉換；以具備 Pending / Rejected / Failed / Unknown 的非丟失式結果代數阻止危險重試。編譯器必須將這些語義以型別保留的方式翻譯至 PDAIS-IR，並在優化和 CPU／GPU 降階時維持資源、權威、因果順序及可觀察 trace 契約。

本研究交付：一份可收斂至 V0 的 EBNF 語法子集、一套分離非線性與仿射資源上下文的型別／效果系統、編譯期與執行期責任矩陣、九個指令家族的語言映射、七項有前提的語義安全命題、三十條編譯器最低拒絕規則、反例及合法性保持的優化矩陣、概念性 SSA 降階追蹤、確定性參考解釋器設計與 V0–V1 可證偽實驗規範。本文不宣稱已完成新 CPU ISA、GPU 互連、完整編譯器或實際 AI 訓練加速。候選研究增量在於跨協議義務能否成為一級語言規格、被不同後端保守實現並創造淨效益，而非新語法名稱本身。

關鍵詞： 擴散程式語言、多主工作流、持續性計算、相位型別、效果系統、線性資源、仿射所有權、型別化冗餘、PDAIS-IR、SSA、編譯器驗證、語義保持、GPU 非同步、分層權威、可證偽系統研究。

1. 本篇的研究位置與成功條件

1.1 研究鏈的位置

第一系列的研究方向依序為：

• Paper 00：中宏觀計算系統與可反證總綱。
• Paper 01：PrimaryFlowNode Contract v0.1，穩定的邏輯主要工作流與承載映射。
• Paper 02：相位激活、有界 credit、背壓、靜止偵測與事件世代。
• Paper 03：R0–R3 的訊息血緣、候選證據、主節點局部聚合。
• Paper 04：推測分支、正式提交鍵、版本化驗證、權威與外部效果。
• Paper 05：PDAIS Abstract ISA Specification v0.1，具型別操作和小步抽象機器。
• Paper 06（本篇）： 程式員如何編寫、分析、型別檢查、編譯、移植並驗證遵守上述規範的程式。

這個次序的重點是：語言不得重新定義前篇已明確建立的安全契約；語言只是將該契約變成可被作者、編譯器、Runtime 與後端共同檢查的形式。

1.2 核心研究問題

1. 如何讓每個工作流都可成為局部主要計算責任者，同時不製造全域寫入權衝突？
2. 如何把相位作為對交互資格有實際影響的具型別變量，而不是所有事件的別名？
3. 如何讓有界擴散和冗餘傳送在語言層可見，但不依賴無限制廣播？
4. 如何阻止程式把「收到一份資料」「GPU kernel 完成」「局部驗證通過」誤當正式提交？
5. 如何在多種 CPU、GPU、OS 及虛擬機器上維持同一套可觀察安全邊界？
6. 哪些約束可由編譯器證明，哪些必須在 Runtime／權威服務重新檢查？
7. 現有 MLIR 與其他編譯器是否已能直接承載全部需求？若能，新 dialect 的實際收益是什麼？
8. 是否能以更少的程式缺陷、更低協議成本或更好的工作負載效能證明研究增量？

1.3 本篇不宣稱的事項

本篇不宣稱多主工作流在所有 CPU 上都有速度優勢；不宣稱 GPU 可以取代 cache coherence fabric、總線、NoC 或 PCIe；不預先規定中宏觀圖在電晶體級必須是星狀或圓形；不把編譯成功當作 formal proof；不把某種語言的線性型別當作端到端 exactly-once 的證據；不強迫所有 AI 訓練都轉為事件驅動；不假定新語言本身能消除記憶體容量、傳輸頻寬或編碼複雜度。

1.4 四層完成度

本篇的正文屬 L1。任何未來提交 L2／L3 成果者，須另外交付實際可執行檔、版本化原始碼與測試證據，不得以本文的計畫項目冒充 PASS。

2. 語言設計哲學：多主、持續、分層、可驗證

2.1 主要工作流不是單一領導者

SMPDC 的 flow 是一個擁有本地工作責任、局部狀態及可被喚醒的邏輯主節點（Primary Workflow Node, PWN）。許多 flow 可同時處於 Ready、Waiting 或 Executing；個別 flow 能在授權的作用域內決定如何處理事件，但無權藉自己的「主」身分接管他人狀態。全域配置與局部自治可以並存，且後端可以採固定綁核、動態重綁、協程、actor 或事件迴圈實現。

語言保證的是明確的工作流責任，並不保證一個 flow 永遠佔據一顆實體核心。 某 flow 可以休眠、遷移、因資源不足暫停；多個 flow 也可能在一顆核心上分時承載。P/E core、CCD、NUMA、SMT 等硬體差異是編譯和 Runtime 的 placement 資訊，而不是 flow 身分本體。

2.2 持續不等於無限 busy-loop

persist 在語言中表示邏輯生命週期與狀態受持續契約管理。對沒有事件可處理的 flow，合法的實作可以停止 CPU 時間使用；系統仍保留其識別、狀態、待處理義務及可恢復證據。

若一個語言設計把「持續性」寫成 while(true) { poll(); }，並認為 CPU 使用率達到 100% 就表示架構成功，便違反 SMPDC 的測量目標。低延遲可以透過事件喚醒、有限短輪詢、自適應休眠與明確的截止時間取得；其選擇需要依工作負載測量。

2.3 擴散是一種有權限與預算的效果

語言中的 diffuse 不能只是 send_to_all(neighbors) 的新名稱。真正的擴散至少具有事件世代、合法拓撲邊、相位守衛、受控 data credit、byte／attempt 預算、背壓及取消語義。最初的資料傳送與後續每個新增受准許的資料擴散都必須納入資源帳本，不能藉「分裂」「融合」「複製」繞過計數。

2.4 計算與正式提交是兩種權限

數值運算可在 CPU、GPU、其他 kernel 或多個局部主節點執行；合法的正式狀態更新由權威提交域決定。語言必須禁止 Tentative、LocalOutcome、GPUEvent、MessageAck 直接轉型為 Committed。對外部效果則須再有可觀察的 outbox／effect 路徑。

2.5 可選 AI 與無 AI 核心

AI 可以建議 placement、batch size、fanout、證據策略或衝突解決候選；不能因此簽發真正的 SendCredit、竄改 AuthorityGeneration 或跳過提交驗證。可用純確定性 OS／Runtime 執行所有核心語義，否則研究結果會被 AI 的不穩定行為與模型版本混淆。

2.6 語言的必要增量，不是語法華麗

若傳統 Rust／C++／MLIR 及現成 actor／transaction library 已能完整表示某案例，新語言未必有正當的替代價值。SMPDC-Lang 必須在跨協議靜態拒絕、編譯最佳化合法性、資源審計、移植成本、實際開發缺陷率或效能中至少證明一項可重現優勢。否則可以選擇把本篇型別與 effect 契約做成 Rust DSL 與 MLIR dialect，而不建造額外的完整語言生態 [E1–E4]。

3. 分層架構與跨篇契約對接

3.1 語言—IR—Runtime—權威鏈

SMPDC-Lang source / restricted embedded DSL
    │  Lexer / Parser / Named Resolution
    ▼
Typed AST and High-Level Flow IR
    │  effect inference + resource checker + lineage rules
    ▼
PDAIS-IR v0.1 (typed SSA and explicit protocol edges)
    │  verifier + preservation-aware optimization + legality check
    ├──► Deterministic Reference VM (V0)
    │
    ├──► Host CPU lowering / LLVM and Runtime ABI (V1)
    │
    └──► GPU subgraph / MLIR GPU dialect / device adapter (V1-G)
                      │
                      ▼
             OS + Runtime + Authority
                      │
                      ▼
            Trace + state / result evidence

圖上每個箭頭均是帶有必須維持的語義義務的轉換，不只是檔案格式轉換。安全屬性跨後端失真時，不能只說「生成成功」；必須拒絕並產生可檢查的原因。

3.2 系統角色與權限分離

3.3 契約延續表

3.4 三種等價不能混同

1. 值等價： 兩個運算產出相同的值。
2. 協議等價： 兩個程序對授權、credit、證據來源、提交、失敗與可見性有等價或明確細化的 trace。
3. 成本等價： 兩個程序的延遲、吞吐、能源與資源消耗是否落在相同契約之內。

一般常數折疊可能保持值等價但破壞審計；非同步 GPU 合批可能保持協議等價但改變截止時間；重複傳送可能改變成本但不增加證據。語言必須明確標示欲維護的等價等級。

4. 語言表面設計：最小標準子集與語法

4.1 暫定名稱與檔案

候選語言名稱為 SMPDC-Lang，正式系列識別仍是 SMPDC；候選副檔名為 .smpdc。名稱、標準庫、關鍵字與實際外部識別名稱都屬可修改的 v0.1 設計，應在正式發表前檢查命名衝突。與既有 C／Rust／LLVM 程式共存是最低相容目標。第一版只要求一個可解析、可型別檢查、可映射 PDAIS-IR 的嚴格子集。

4.2 文字形式與詞法

• 原始文字為 UTF-8，識別符第一階段可限定 ASCII，避免混用字形攻擊；字串可使用 Unicode。
• 保留 flow、owns、requires、let、move、call、match、case、return、bounded 與 effect 等字。
• 註解可採 // 單行及 /* ... */ 有界區塊。詞法器必須在讀取後維持原始位元／位元組位置映射，錯誤回報應包含可靠的 UTF-8 原始碼範圍。
• ResultId、FlowId 等識別與實際 runtime 不可偽造證書分離：原始碼的字串常量不能直接構成權威 Cap。
• 下列語法是候選規範子集，不是宣稱已存在的 compiler 或現行 MLIR 語法。

4.3 EBNF 候選文法（V0 核心）

module       = "module", identifier, "version", string, "{", { declaration }, "}" ;
declaration  = feature_decl | type_decl | function_decl | flow_decl ;
feature_decl = "feature", identifier, ":", "required" | "optional", ";" ;
type_decl    = "type", identifier, "=", type_expr, ";" ;
function_decl= "fn", identifier, "(", [ parameters ], ")", "->", type_expr,
               "effects", "[", [ identifiers ], "]", block ;
flow_decl    = "flow", identifier, "(", [ parameters ], ")",
               "owns", identifier, ":", type_expr,
               "requires", "[", [ identifiers ], "]", block ;
parameters   = parameter, { ",", parameter } ;
parameter    = identifier, ":", type_expr ;
type_expr    = identifier, [ "<", type_expr, { ",", type_expr }, ">" ]
             | "(", type_expr, { ",", type_expr }, ")" ;
block        = "{", { statement }, "}" ;
statement    = let_stmt | call_stmt | match_stmt | bounded_loop | return_stmt
             | defer_stmt | assert_stmt ;
let_stmt     = [ "linear" ], "let", identifier, [ ":", type_expr ], "=", expression, ";" ;
call_stmt    = "call", operation_name, "(", [ arguments ], ")", ";" ;
match_stmt   = "match", expression, "{", case_branch, { case_branch }, "}" ;
case_branch  = "case", pattern, "=>", block ;
bounded_loop = "bounded", "loop", "(", expression, ")", block ;
return_stmt  = "return", [ expression ], ";" ;
defer_stmt   = "defer", block ;
assert_stmt  = "assert", expression, ";" ;
expression   = literal | identifier | "move", identifier | operation_call
             | "(", expression, ")" ;
operation_call = "call", operation_name, "(", [ arguments ], ")" ;
arguments    = expression, { ",", expression } ;
operation_name= identifier, ".", identifier ;
pattern      = identifier, [ "(", [ identifiers ], ")" ] ;
identifier   = letter, { letter | digit | "_" } ;
string       = '"', { string_char }, '"' ;

此文法刻意只涵蓋安全語義的骨架，並非可完整表達算術、泛型約束、任意 lambda、模組導入和巨集的通用語法；literal、string_char 等詞法元件須由後續 lexer 規範補足。語言的核心操作以 call Namespace.OP(...) 形式呈現，讓讀者與編譯器不必猜測一個語法糖會展開成幾個帶權限效果的狀態轉移。後續可逐步加入相位、擴散的簡寫形式，但必須保持精確的 SSA 展開。

4.4 靜態規格與執行配置的分離

語言模組可對某工作流宣告 placement_hint = preferred_p_core，但 hint 是可被 OS／Runtime 拒絕或改寫的最佳化輸入。它不能成為 AuthorityGeneration、StateVersion 或合法的 GPUHostVisible 證書。對無法保證 P/E core 的平台，編譯器應維持所有安全效果，採明確 CPU-only 或泛用執行回退。

4.5 禁止的隱式語法糖

即使未來提供 diffuse x to peers、verify evidence 或 commit result 的便利語法，展開時仍必須明列來源證據、credit、scope、epoch 與授權。以下寫法在 v0.1 不應被接受為合法單步運算：

// NON-CONFORMING: 沒有指定 epoch / credit / topology permission
diffuse payload to all;

// NON-CONFORMING: 把本地選擇等同權威提交
let official = cast<Committed<Result>>(local_outcome);

// NON-CONFORMING: 把 kernel launch 當 GPU 與 CPU 之間的共享記憶體屏障
let host_value = cast<HostVisible<Buffer>>(gpu_launch_token);

禁令的目的是防止不誠實的語義簡化；不表示這些字串是已開發的 compiler 診斷。

5. 型別系統：一般值、仿射權利、能力與證據

5.1 最小型別分群

將型別分為五個語義群，而不把所有 handle 都變成可以任意 clone() 的一般物件：

其中線性與仿射不應模糊：仿射值至多使用一次，允許不使用；線性責任則要求資源在終止路徑上被消耗或以明確規範動作清償。實際網路 token 的 crash、drop、消耗失敗與 unknown status 不能靠一般語言的 RAII destructor 自動當作「已安全清償」，因為解構時可能無法聯繫權威、磁碟或遠端接收者。

5.2 宣告的抽象資料型別

FlowHandle<F>                    FlowLease<F,G>
FlowState<F,S,V>                 PhaseEvidence<E,Kind,Scope>
EventEpoch<E,Mode>              AdmittedEdge<From,To,TopoGen>
SendCredit<E,CreditId>          DeliveryPermit<E,MessageId>
Message<MsgId,T>                DeliveryAttempt<MsgId,AttemptId>
Candidate<ResultId,Origin,T>    SourceLineage<Origin>
IndependentWitness<Origin,Rule> EncodedShard<Group,Index,Scheme>
ReconcileComparison<ResultId>   SealedLocalOutcome<ResultId,T>
SpecBranch<BranchId,Domain>     Tentative<T,BranchId>
Snapshot<T,Version>             CommitProposal<Domain,CommitKey>
ValidatedProposal<Domain,Key>   CommitDecision<Domain,Key>
Committed<T,Key>                EffectIntent<EffectKey>
GPUBufferLease<Device,Buffer>   GPUEvent<Device,Work>
HostVisible<T,Buffer>           AuthorityCap<Scope,Generation,Effect>
TraceEvidence<EventId>

這一組型別沿用 Paper 05 的 PDAIS 候選型別，不是經標準化後的各語言泛型 API。型別參數中的 Epoch、Scope 或 Generation 若僅在執行時確定，必須以動態 seal 與受控 guard 表示，而非讓語言的泛型參數暗中等於現實世界驗證成功。

5.3 型別上下文與效果上下文

候選型別判斷為：

其中：

• $\Gamma$：一般值、唯讀資料與可重用但非權威的型別環境；
• $\Delta$：具有唯一消費、轉移及清償責任的 affine/linear 資源環境；
• $\Sigma$：模組、相位／權威 scope、effect policy、可用設備特性與靜態證書；
• $\tau$：運算產生的型別；
• $\varepsilon$：操作可能產生的具名效果集合；
• $\Delta'$：運算結束後仍有效的資源集合。

核心不是推導出一個看似複雜的符號，而是使 compiler 能回答：「某個 SendCredit 是在哪一條 control-flow path 被真正使用，使用後是否能在另一條路徑被再次消耗？」

5.4 消費規則與 alias 拒絕

對唯一的 credit $c$，合法的消費型別規則可描述為：

$\Delta_r$ 不含可再次使用的 $c$。如果結果為 Rejected，Runtime 是否保有原 credit 及如何返還給同一合法 owner，需要由明確的返回 variant／transactional rollback表示；不能由 compiler 把失敗後的舊 alias 神奇地恢復成可使用 token。Paper 05 對成功預留後取消採取不退款、轉入 Burned/Retired 帳本的基線，本篇維持該規則。

對下列形態，靜態 checker 必須拒絕：

linear let c: SendCredit<E0,C0> = source_credit;
linear let p1 = call DIFFUSE.RESERVE(edge1, move c, desc1);
linear let p2 = call DIFFUSE.RESERVE(edge2, move c, desc2); // ERROR: reused

即使 p1 在 Runtime 遇到 Pending，也不能因此默認原始 $c$ 同時可用。應由 Pending 返回唯一 cancel_handle 或受控的 reservation ownership 物件，對生命週期進行追蹤。

5.5 clone()、borrow()、move() 的不同保證

• clone(value)：只適用普通可複製資料；SendCredit、可生效的 AuthorityCap、DeliveryPermit 不提供複製實作。
• borrow(token)：唯讀觀測可參照身分和非機密 meta，但不能取得「使用該權利」的另一個有效 owner。
• move(token)：轉移所有權並使舊變量無法再被消耗；跨執行緒／FFI 邊界也須落實此義務。
• split(token)：只有標準庫提供具有守恆證明的合法拆分 op 時才可使用；v0.1 不提供 data credit 任意 split，避免單一 token 擴張成無界傳播。
• drop(token)：對持久化的外部義務不得自動標記成功回收；必須輸出 RetireRequired 或交予持有該義務的 Runtime 管理。

5.6 能力（capability）不等於身分與字串

AuthorityCap<Domain,Generation,Commit> 並非把 domain_id 拼成合法 UUID 就能建立的值，而應由受信任的 capability resolver 提供不可偽造或可重新驗證的受控 handle。編譯器能拒絕不帶 AuthorityCap 的 COMMIT_DECIDE；但當時的權威世代是否已被 fencing、外部服務是否撤銷權限，只能由適當 Runtime／仲裁域進行最新檢查。

5.7 證據型別不是證據真實性的神諭

IndependentWitness<Origin,Rule> 可以表示已通過指定來源獨立性政策的證書，卻不等於「獲得另一個永遠正確的答案」。它必須具有來源血緣、方法、版本及 failure-domain 的驗證證據，並附明確的 rule ID。當多個結果共享模型權重、錯誤前處理或同一資料汙染時，兩條獨立傳輸路徑也不應被判定為獨立研究結果。

6. 效果系統與跨協議權限

6.1 候選效果字母表

FlowCreate, FlowPersist, FlowWake, FlowRebind, FlowClose
PhaseObserve, PhaseSignal, PhaseWait, PhaseValidate
CouplePropose, CoupleAdmit, CoupleRevoke, CoupleQuiesce
EpochAdmit, EpochSeal, EpochQuiesce, CreditReserve
DiffuseSend, DiffuseAck, DiffuseCancel, Backpressure
RedundancyPlan, EvidenceCompare, EvidenceSeal, CodedRecover
SpecBegin, SpecRead, SpecDerive, SpecAbort
CommitPropose, CommitValidate, CommitDecide, CommitPublish
EffectEnqueue, EffectDeliver, EffectObserve
GPUAlloc, GPUDispatch, GPUWait, GPUCopy, GPURelease
AuditEmit, ExternalIO, AuthorityResolve

對普通純計算可以推導空效果集合 $\varnothing$ ；但不能因底層呼叫看似只輸出一個常數，便將它宣告為純函數。若 MESSAGE_REGISTER 更動防重資料庫，或 EPOCH_SEAL 更動可入場狀態，它們即使返回 true／false，仍然是有狀態效果。

6.2 效果子型別與授權

令模組規格允許的效果集合為 $\varepsilon_{allow}$，每個語句需要的效果集合為 $\varepsilon_s$，至少要求：

這個必要條件不充分。CommitDecide 雖可能出現在程式宣告的 effect 集合中，仍必須同時持有有效 scoped capability、通過 runtime guard 與提交域決策。效果註記表示可能發生何種狀態變化，不是取得變化權利的許可證。

6.3 效果界限與跨模組組合

假設函數 $f$ 的效果是 $\varepsilon_f$，呼叫函數 $g$ 的效果是 $\varepsilon_g$，則保守組合應包含：

若呼叫之間的 guard 能嚴格排除某條效果路徑，compiler 可以標記效果條件，但必須附明確 path predicate；不能為了優化消除 UnknownCommit、AuditEmit 或 Backpressure 等對外可觀察的分支。

6.4 外部 FFI 是信任邊界

FFI 對接 C／C++、Rust、LLVM 或 Python 時，普通指標與不透明 handle 不能靠型別宣告立即轉變成安全權限。任何可修改 CreditLedger、CommitLedger、StateVersion 或 EffectLedger 的 FFI 必須進入 trusted_adapter 名冊，配置 runtime guards、版本、入出參 ABI 和失效測試。對不可審核的 FFI，保守效果型別應視為 UnsafeExternal 並禁止在受保護提交路徑中直接使用。

6.5 動態角色與靜態保證的邊界

部分權限可在編譯時知道作用域，部分可能在執行時根據租約、權限政策或資源回收發生改變。當 AuthorityGeneration 只有執行時才確定時，不可要求 compiler 通靈；應輸出具明確 failure path 的 AUTHORITY_VALIDATE guard。錯誤模型需保留 StaleGeneration、RevokedCapability、UnknownDecision 等不同狀態。

7. 持續工作流與局部主節點程式模型

7.1 flow 的語義

flow F 宣告的是長期邏輯實體的程式模板，不是在編譯時為所有 CPU 核心分配固定 thread。啟動一個 flow 需要 runtime registration，產生穩定 FlowId、FlowGeneration、局部 state owner 和有效 lease。flow 對外提供事件入口、局部 transition、persistence policy 與 capability requirements。

7.2 工作流與 process、thread、coroutine、actor 的關係

7.3 工作流的持續狀態與安全暫停

在暫停點之前，flow 必須交出必要的可重放狀態快照及尚在途義務；在恢復點之後，必須重新確認其 lease、epoch、拓撲及授權。這不是要求每次事件都完整序列化整個記憶體，而是根據變更日誌、狀態版本及持續策略合理地完成必要保存。

若編譯器生成的 coroutine frame 持有尚未清償的 DeliveryPermit，不能任意將 frame 丟棄，並認為 credit 已回到池內。可採「禁止 drop」「交接至 Runtime 持有者」或「進行受控退休」三種策略，但不可靜默遺失責任。

7.4 重新承載與 fencing

FLOW_REBIND 可被語言呼叫，但成功不是把 thread_id 欄位修改一下。必須依 Paper 01 撤銷、遞增 generation、fence 舊 owner、處理未清資源，並確認新 owner 的合法承載。編譯器應把 FlowLease<F,G> 視為世代敏感資源，禁止舊 generation 在受保護效果點重新生效。

7.5 終止與長期存在分離

FLOW_CLOSE 的合法性依賴未清訊息、epoch、暫態分支、外部效果與狀態保存的政策。EPOCH_QUIESCE 則是對一批擴散事件判定是否靜止，不等於 flow 實體結束。長期 flow 可以跨多個已靜止 epoch 維持存在，而某 epoch 即使沒有正在執行的 thread，也可能仍有在途訊息或待確認義務。

8. 相位型別與耦合資格

8.1 相位是交互條件，不只是時間戳

延續 PCMT 及 GCCFT 相位論 [I7–I8]：相位可以是 readiness、causal、synchronization、verification 等具體且 task-relevant 的狀態座標，不必是振盪器角度，也不能把所有狀態更新都稱為相位。相位必須能改變互動資格、事件依賴或合法的轉移，才能構成本篇可觀測的 phase effect。

8.2 PHASE_SIGNAL 不等於就緒證書

某工作流聲稱 ready 只能形成具有來源與版本的 PhaseEvidence。若實際依賴尚未完成、尚未取得資料或另有版本衝突，PHASE_VALIDATE 必須拒絕該 interaction。這也防止程式透過將 phase = ready 寫為常數來「加速」所有同步。

8.3 耦合的型別守衛

對來源 flow $a$ 、目標 flow $b$ 和耦合邊 $k$，合法的互動入場可抽象為：

此式是候選交互資格的必要條件彙整，不意味上述條件在所有應用中可以純編譯期確定。它們可能需要 Runtime guard 或外部授權查核。

8.4 不強迫全部節點全域同步

相位安全不代表每次傳播前都呼叫一個全域 barrier。可採局部版本與因果依賴；無共享約束的獨立 flow 可在不同相位進度下運作。若某協議真的需要全域屏障，則其時間、參與者數、失效與可用性成本必須明列，不得偷換為免費「耦合」。

9. 有界擴散與背壓：在語言中保存計量

9.1 credit 帳本與取消的完整方程

延續 Paper 05 的不退款基線，對 event epoch $e$ 設定初始 credit 額度 $B_0(e)$，其可用、已預留、已消耗、已退休量分別為 $U_e,Q_e,S_e,D_e$，要求：

每一項不得為負。此式只計算受准許的邏輯資料傳送權；額外 transport 嘗試、位元組、GPU kernel、控制訊息、下一個 epoch 的入場均另行計量。DIFFUSE_SEND 不可在 R1 或「快速傳輸」名義下無償產生額外的新 logical send。

9.2 reserve、send 的返回協議

DIFFUSE_RESERVE 成功產生一次性 DeliveryPermit；DIFFUSE_SEND 消耗一次性 permit 並產生受控 dispatch obligation。若網路回應遺失，Unknown 不代表發送一定失敗，須先依穩定 MessageId 和 durable dispatch record 查詢、才可依規範重試；而重試並不自動增加新的 logic credit。對物理封包嘗試仍須遵守獨立的 attempt／byte budget。

9.3 Pending 不等於 spin

如果接收端佇列滿，函數應返回 Pending(wait_condition, cancel_handle) 或明確容量拒絕，而不是在語言層默默 busy-loop 直到成功。Runtime 可用背壓、令牌桶、配額或調整批次化策略處理，但需維持既有 EPOCH_QUIESCE 所必需的控制流量，不得讓 ACK／撤銷因與資料共用完全耗盡的 credit 而永久等待。

9.4 credit 語義穿過編譯器邊界

若編譯器將多條相鄰小訊息合批，可以在同一物理 transport 呼叫中承載它們；但每個受控 logical message 仍需可追蹤的 credit 花費、來源、必要版本及其個別失敗狀態。不能以合批後只呼叫一次 OS send() 就宣稱可只消耗一個信用額度。

9.5 控制流的有界性不是終止性

有限 data credit 僅保證某種被允許的新增發送數量上界，並不推出所有 local CPU compute 必然終止，也不保證控制通道一定無損、流程永遠沒有 deadlock 或下一個 epoch 不會被不斷建立。必須另外限制 loop、控制成本、epoch admission 和 fairness。從 Dijkstra–Scholten 的擴散計算終止偵測到現代背壓設計，這類問題已有成熟先例 [E12]；本篇的增量是將之與多主相位、冗餘證據及編譯器效果檢查接在同一語義契約中。

10. R0–R3 冗餘資訊流：型別化建構與去重

10.1 四種模式不是程度由弱到強的一條直線

上述型別只是需要經受控建構與證據規則認定的分類；R1 路徑也可能因共享資源競爭而更慢，R2 也可能遇到共通原因造成一致錯誤。資訊的多路交換不能直接推導出更高精準度。

10.2 四層身分不可壓縮成一個 digest

ResultId
  └─ CandidateId
       └─ MessageId
            └─ DeliveryAttemptId

這是說明身分粒度的示意樹，不表示所有實體皆一對一。Runtime 必須正確保存跨層關聯，compiler 不得把同一候選的兩個 attempt 當兩個源自獨立模型或演算法的結果，也不能因 payload hash 相同便認定兩個候選具有相同的權威權限。

10.3 型別化 R1 建構

對單一 candidate，可預先建立合法的多路傳輸計畫，接著分別預留各路受控 credit。合格的 RacingCopy 應保留原始 CandidateId 與 OriginId，並在 winner 選定後保留 loser 的 cancellation／in-flight 義務。假設有效候選完成時刻為 $T_1,T_2$，競速可用時刻近似：

其中 $V$ 為必要驗證， $H$ 為提交、複製、資源競爭及取消開銷。若 $H$ 過大，雙路傳送可能反而更慢 [E11]。

10.4 型別化 R2 來源審核

IndependentWitness<Origin,Rule> 不能由 DeliveryAttempt、Receipt 或 ResultId 直接鑄造。受信任的 EvidenceVerifier 應審查模型／演算法、共同資料與 seed、來源血緣、共同失效域、獨立政策及驗證時間。通過指定 Rule 只表示該規則所要求的依賴分離成立，不表示答案必然正確。

10.5 型別化 R3 解碼

在擦除碼 $(n,k)$ 且 schema、索引、checksum／完整性與 shards 的有效性滿足協議條件時，至少需要 $k$ 個具合法解碼關係的有效 shard：

若面對拜占庭錯誤或互相矛盾 shard，單靠此下界並不能建立容錯正確性。必須使用相符的錯誤模型與碼距條件；compiler 不應接受未宣告碼參數、重複 shard index 或可疑 provenance 的直接 CodedRecover -> TrustedPayload 轉換。

10.6 主節點局部聚合的上限

RECONCILE_SEAL 產生 SealedLocalOutcome，其語義是本地聚合策略在某輪完成；與 Paper 04 的 CommitDecision 不同。局部聚合在以下情況必須產生 ConflictHold 而非編造結果：非交換性的合併被重排；版本衝突未解；R2 來源不符合政策；R3 重建條件不足；品質門檻尚未到達。

11. 推測運算、提交與外部效果的語言邊界

11.1 三階值型別

至少區分：

Tentative 表示屬於可撤銷分支 $B$ 的暫態結果；SealedLocal 表示局部比較、品質與血緣檢查依宣告規則完成；Committed 才代表某正式提交域對相應鍵 $K$ 作出有效權威決策。這三者不是 enum 值「調整一下狀態」即可互換的抽象。其間須經過權限、版本驗證與受控仲裁。

11.2 推測讀取的依賴必須被追蹤

執行 SPEC_READ 時應記錄快照版本與依賴集合。任何暫態分支 $b$ 若依賴已被撤銷、過期或衝突的狀態，就應標記為 Invalidated，並向未提交的後代傳播撤銷。compiler 可以重排不相關的純計算，但不得將某個未經再次驗證的暫態結果跨過正式提交屏障。

11.3 快照一致性不等於可序列化

兩個各自讀到相同快照的提交分支，可能各自只寫入不同 key，卻共同破壞跨鍵業務不變量。Paper 04 的 write skew 反例因此必須出現在語言的 isolation_policy，不能默認單 key CAS 或 Snapshot Isolation 已足以維護所有 invariant。要求強一致性的作用域可使用更強的序列化驗證、predicate tracking 或仲裁規則 [E13]。

11.4 UnknownCommit 的模式比對義務

如果提交決策在持久化後、回應送到 caller 前發生通訊故障，caller 可能看到 Unknown(query_handle, scope)。此時重新生成一個新 CommitKey 並執行第二次提交通常不安全。語言應強制 Unknown 分支顯式處理，下一步必須進行 COMMIT_QUERY 或其他經規範的恢復操作；不能將 Unknown 當作 Rejected 或 false。

11.5 模式比對的不可丟失性

核心結果和錯誤族採封閉代數資料型別：

StepResult<T> =
    Applied(T, ObservableEventRef)
  | Pending(WaitCondition, CancelHandle)
  | Rejected(ErrorCode, EvidenceRef)
  | Failed(ErrorCode, RecoveryHint)
  | Unknown(QueryHandle, Scope)

match 對這五種 variant 必須窮舉，或有經 effect policy 核准的明確 fail-closed catch-all。對權威操作，禁止一個只有 if result 的布林捷徑。Applied 只代表該 op 的已聲明成功，不等於所有外部效果已完成。

11.6 外部效果與正式狀態的牆

EFFECT_ENQUEUE 必須取得合法已提交的狀態決策或規範允許的 effect intent，並生成穩定 EffectKey。EFFECT_DELIVER 需要遵守 outbox 與接收端的冪等政策；本地 durable decision 與外部世界「只發生一次」仍是不同的保證。對無 idempotency key 的第三方 API，既不能聲稱任意 crash-retry 都 exactly-once，也不能把補償交易說成真正回滾已發生的不可逆行動。

11.7 推測區域禁止未隔離效果

若允許 spec { body } 這類語法糖，compiler 必須確認其 body effect 不含非隔離、不可撤銷外部操作。純計算、暫態局部狀態、受控 GPU kernel 可在恰當資源隔離下屬於合法推測；寄信、付款、實體機械動作等無法真正撤銷的效果不可預先在 Tentative 階段直接發布。

12. GPU 與異質記憶體的型別邊界

12.1 三層分開

GPUEvent 代表某個 GPU 提交／執行流程的非同步依賴；GPUBufferLease 表示在特定設備、buffer 與生命週期下的資源控制；HostVisible<T,Buffer> 表示依對應 memory/transfer protocol 證明 CPU 使用者能合法存取的值。這三者互不等價。

12.2 發送 GPU 工作不表示 GPU 已完成

Kernel launch 可能非同步返回；CUDA/MLIR GPU dialect 已提供 async dependency token 的相關先例 [E3, E5]。語言必須讓後續 CPU 的讀取等待真實完成和必要同步，而非直接對 device buffer 做不受保護的 host dereference。

12.3 Buffer 生命週期

GPU batch 的輸入與輸出應有可檢查的 allocation、read/write lease、事件依賴、可見性與釋放規則。若某 GPU 工作尚在執行，Runtime 不得提前回收其讀取中的 host-pinned buffer；若同一 buffer 被不同 kernel 同時寫入，必須在指定 memory ordering 和 data-race policy 下維持一致性。

12.4 資料移動必須是顯式成本

GPU 加速是否划算，必須納入提交排隊、host→device／device→host 資料搬移、同步、kernel 啟動、batch formation 及 CPU 等待時間：

此式為方便初步帳目展開的階段加總上界式示意，實際 pipeline 可能部分重疊、共享關鍵路徑且具有重疊或資源爭奪，不能把它當成普遍的精確延遲恆等式。測量應同時提供端到端 wall-clock 與各階段事件 trace。

12.5 對 CPU／GPU 的功能定位

CPU 實體核心可在某些工作負載上提供優良的低延遲序列、分支與控制計算；GPU 提供高吞吐、大批次並行的運算通道。但 GPU 執行「節點之間的關係運算」不表示它能讓 CPU cache coherence、PCIe 或物理 NoC 傳輸零延遲。微觀互連是 Paper 09 的硬體研究問題，不能在語言降階中被虛構。

12.6 GPU 不可用時的保守 fallback

對純計算而且數值精度與品質契約可保持的 kernel，compiler 可以明確選擇 HostCPU fallback。若 GPU 計算結果的浮點順序或近似誤差對品質有影響，則不能僅憑「程式跑得通」就宣稱等價。某些 op 必須回傳 UnsupportedTarget，而不是自動改用具有不同一致性或錯誤模型的後端。

13. 從 AST 到具型別 PDAIS-IR

13.1 五層中介表示

Typed AST 和 Flow-HIR 是研究建議，不是 Paper 05 已有的正式指令額外家族。IR 分層的目的，是把適合高階優化的資訊保留足夠久，再交由較低層處理實體記憶體與設備細節。

13.2 PDAISOperationV0_1 必備資料

沿用 Paper 05 的九個核心欄位：

PDAISOperationV0_1 {
    op_name: NamespacedOperationId
    signature: InputOutputTypeSignature
    effect_set: EffectSet
    authority_requirements: CapabilityRequirements
    consumes: List[AffineOrLinearTokenType]
    produces: List[TypedResult]
    phase_guard: OptionalTypedPredicate
    event_epoch_binding: OptionalEventEpoch
    resource_estimate: ResourceUpperBound
    failure_variants: ClosedTaggedUnion
    replay_class: Pure | Idempotent | QueryFirst | NonReplayable
    trace_contract: RequiredTraceFields
    lowering_contract: TargetSpecificProofObligation
}

若未取得任何 lowering_contract 的證據，compile 可產生 VM-only artifact，但不能標記為 target-native conformant。op_name、effect 和 failure set 受到版本協商拘束；無法辨識的 required op 需 fail closed。

13.3 九個家族的規範映射

13.4 SSA 中的能力資源流

PDAIS-IR 宜採 SSA 表示每次成功的資源狀態：原始 %credit 作為一次性消費 operand；成功分支產生 %permit，失敗分支產生被政策允許的 RetiredCredit 或受控返回 handle。對一條 control-flow edge，可攜帶 block argument 傳遞 resource ownership；多分支 phi 合流應遵守唯一實際分支的值，不能在動態執行中同時產生兩個有效 owner。

13.5 失敗路徑是 IR 的一等控制流

例如：

%step = smpdc.commit.decide %validated, %cap
switch %step {
  Applied(%decision, %ev) => smpdc.commit.publish %decision
  Pending(%wait,%cancel)   => suspend_with_owned_cancel %cancel
  Rejected(%code,%evid)   => terminate_branch %code,%evid
  Failed(%code,%repair)   => recover_under_policy %repair
  Unknown(%q,%scope)      => smpdc.commit.query %q,%scope
}

這是 IR 語義的簡化示意，不是保證目前 MLIR 可以直接解析的語法。不可將其偷換成單一 bool success，也不得讓 default catch-all 對 Unknown 自動重試新 key。

14. 一個具體、可逐步審查的跨層編譯案例

14.1 案例設定

令有兩個邏輯主要工作流 Ingress、Compute，一個資料結果 R12，一個事件世代 E7。Ingress 在已獲授權的邊與 credit 下，傳送可檢查的候選資訊到 Compute。接收端用已登記的 MessageId 完成去重，形成 SealedLocalOutcome，再依權威協議建立提案、版本驗證及提交決策。整個案例完全可以不呼叫 GPU；GPU 分支只是在計算密集且符合成本條件時可選的替代後端。

14.2 原始語言核心子集示例

下列範例使用第 4 章的候選語法形態；call Namespace.OP 對應第 13 章的具型別 op。省略的能力解析、Message 初始化與裝置配置以輸入參數表示，不假裝由文字常量取得權限。

module Example06 version "0.1" {
  feature gpu_batch: optional;

  flow Ingress(
      m: Message<Msg9,Payload>,
      c: SendCredit<E7,C4>,
      edge: AdmittedEdge<Ingress,Compute,T3>,
      epoch: EventEpoch<E7,Open>)
    owns local: IngressState
    requires [CreditReserve, DiffuseSend, AuditEmit] {

    linear let outcome = call DIFFUSE.RESERVE(edge, move c, m, epoch);
    match outcome {
      case Applied(permit, ev) => {
        let sent = call DIFFUSE.SEND(move permit, m);
        match sent {
          case Applied(receipt, e1) => { return; }
          case Pending(wait, cancel) => { call FLOW.YIELD(wait); return; }
          case Rejected(code, evidence) => { return; }
          case Failed(code, repair) => { return; }
          case Unknown(query, scope) => { call DIFFUSE.QUERY(query, scope); return; }
        }
      }
      case Pending(wait, cancel) => { call FLOW.YIELD(wait); return; }
      case Rejected(code, evidence) => { return; }
      case Failed(code, repair) => { return; }
      case Unknown(query, scope) => { call DIFFUSE.QUERY(query, scope); return; }
    }
  }
}

規格判讀： 這仍是語義示例，不是 V0 conformance PASS 的可執行程式：例中 DIFFUSE.QUERY、FLOW.YIELD 的實際作用域、返回結果、cancel handle 的資源移轉及 EventEpoch<E7,Open> 的真正權限來源，須由完整 ABI 與 owner 架構驗證。若 Pending 分支只是丟棄帶清償責任的 cancel，真正的靜態 verifier 必須拒絕或要求轉交至受控 Runtime。此處刻意保留該檢查點，以說明「語法合理」絕不等於「合規」。

14.3 合法資源交接版本的抽象追蹤

一條合規 trace 不會讓分支意外消失：

T0  Runtime grants FlowHandle(Ingress), epoch E7 and unique credit C4.
T1  COUPLE_ADMIT produced edge (Ingress,Compute,T3) under valid policy.
T2  DIFFUSE_RESERVE atomically consumes C4 and creates permit P9.
T3  DIFFUSE_SEND consumes P9 and records message Msg9 as DispatchUnknown-or-Pending.
T4  If receipt is Unknown, stable Msg9 is queried; no new credit is minted.
T5  Receiver performs MESSAGE_REGISTER(Msg9, hash, E7).
T6  Receiver classifies payload CandidateId / OriginId, not attempt count.
T7  RECONCILE_COMPARE / SELECT / SEAL produces local outcome L12.
T8  COMMIT_PROPOSE with stable key K31 and snapshot dependencies.
T9  COMMIT_VALIDATE checks version, policy, authority and isolation.
T10 COMMIT_DECIDE resolves one authoritative decision in domain D2.
T11 COMMIT_PUBLISH exposes committed state under correct ordering.
T12 EFFECT_ENQUEUE is optional and requires the committed decision.

其中 T3 的發送結果不必立刻成功；T9–T11 也不能因源碼書寫為相鄰行，就在物理系統假定具有單步原子性。這是跨協議路徑而不是一顆 CPU 的單一 opcode。

14.4 語言到 SSA 的核心節點

// Conceptual PDAIS-IR only; not claimed to compile under existing MLIR.
%permit_step = smpdc.diffuse.reserve %edge, %credit, %message_desc, %epoch
    {consume_credit=true, event_epoch="E7"}
    : (!smpdc.edge, !smpdc.credit, !smpdc.message_desc,
       !smpdc.epoch) -> !smpdc.step_result<!smpdc.permit>

// The verifier generates explicit branches and ownership transfers.
smpdc.step.match %permit_step {
  ^applied(%permit,!smpdc.observable_event):
      %sent = smpdc.diffuse.send %permit, %message
      smpdc.step.match %sent { /* Applied/Pending/Rejected/Failed/Unknown */ }
  ^pending(%wait,%cancel):
      smpdc.runtime.own_cancel %cancel
  ^rejected(%error,%evidence):
      smpdc.trace.reject %error,%evidence
  ^failed(%error,%recovery):
      smpdc.runtime.recover_or_halt %error,%recovery
  ^unknown(%query,%scope):
      smpdc.diffuse.query %query,%scope
}

這個例子明確區分 compiler 合成的 runtime.own_cancel 與使用者原始程式。若 Runtime 沒有合規 cancel-handle ownership adapter，該降階路線便不合法。

14.5 CPU-only 降階

DIFFUSE_RESERVE 可由受控 registry + 原子 token 狀態變更實作；DIFFUSE_SEND 可由共享記憶體 queue、原子 release/acquire、epoch/lease guard 及 durable dispatch record 構成；RECONCILE_SEAL 可由純 CPU 比較器與證據登錄實作。此路線的優點是先測出 PDAIS 語義本身的開銷，不需要假設 GPU 能加速任何一次消息傳遞。

14.6 可選的 GPU 子圖

若 RECONCILE_COMPARE 面對大量規律資料，可以在正確的 GPUBufferLease 與批次大小下改走 GPU kernel；其結果只是供 CPU／權威層消費的受控候選。等候 GPU event 和資料合法可見的必要同步應保留在 DAG 上，而不由 LLVM 的普通 load 取代。

14.7 本例的反證目標

如果傳統 actor + typed transaction library 在相同測試下，已經同樣能阻止所有非法轉換，而且其 CPU/GPU 延遲、記憶體和開發複雜度明顯更低，SMPDC-Lang 需要重新解釋必要性。更嚴格的效果檢查可能仍有價值，但不能藉「理論新」掩飾負面測量。

15. SMPDC-C 編譯器驗證器：三十條最低拒絕規則

15.1 驗證不是單一 verify() 呼叫

一個編譯模組需經過：語法及名稱解析、型別等價檢查、resource ownership、effect inference、phase／epoch scope、data lineage、authority-sensitive operation、target legality、ABI feature agreement 及 trace-obligation completeness。各層可以回傳 StaticallyProven、GuardRequired、Rejected，但不能把「編譯器不知道」回傳為 True。對純 Runtime 狀態條件可安排動態 guard；對缺少權限來源、線性消費規則或非法跨安全型別的情況，必須編譯失敗。

15.2 三十條核心規則

與 Paper 05 的關係： C06 規則不覆蓋或取消 V05-01 至 V05-20，而是對 source-to-IR 轉譯增加針對語言與 compiler pipeline 的拒絕規格。最終 compiler 若輸出 PDAIS-IR，仍需執行 Paper 05 所定義的最低 IR verifier。每一個錯誤碼應附 rule_id、source span、IR op ID、責任 scope 與可解釋修正方向。

15.3 編譯器可證明與必須 guard 的差異

下列三例說明何時必須 fail closed：

1. CreditDuplicated 是明確的靜態 alias／ownership 違反，不能以「Runtime 會檢查」縱容兩份同時有效的 token。
2. 對編譯時未知的 FlowLease 世代，compiler 可以將 AuthorityGeneration 當動態參數並在使用前安排 runtime fencing guard；但若完全沒有 lease／capability provenance，則不是可推遲的數值檢查，而是非法的權限建構。
3. GPUEvent 可在編譯時被保留成等待依賴，實際完成需由 device runtime 判定；compiler 必須保證所有 host read 之前都有相符的 completion／visibility path，而不能假定該事件已發生。

15.4 診斷必須具可反駁性

每條拒絕規則應包含至少一份 negative example、一份合法修正版、一份轉譯前後 IR 追蹤。不能只在文件中列出「有 verifier」，卻沒有測試或根本無法觀察它拒絕什麼。某些檢查需要 SMT／有限模型，而不是單純 Rust-style move checker；V0 應先對有限子集明確實作，再依確實的驗證結果擴張規格。

16. 編譯最佳化：在合法範圍內改善效能

16.1 四種最佳化義務

任何 pass 對一段程式 $P$ 產生 $P'$ 時，至少需檢查：

• 型別保持： 轉換後所有值、權限及 affine obligations 仍合法。
• 可觀察安全性保持： 不會新增合法源碼不容許的提交、效果、信用花費或來源偽裝。
• 因果／失敗保持： 不會移除關鍵依賴與 Unknown 等不可丟失的結果分支。
• 資源策略保持： 不會突破所宣告 credit、bytes、attempt、deadline、memory 及 device lease 範圍。

某最佳化若不保證精確 trace 相等，而只滿足 trace refinement，必須在模組 policy 中說明允許的可觀察差異；不允許偷偷刪除拒絕事件以讓 benchmark 看似沒有失敗。

16.2 候選優化與合法性護欄

其中有些優化只是成熟編譯器／Runtime 做法的候選映射，並非 SMPDC 的獨立發明。研究重點是它們能否在同一跨協議驗證器之下安全組合。

16.3 從值保持到 trace refinement

令 $\mathcal{T}_{obs}(P)$ 表示程式 $P$ 在相同輸入、環境、故障與 policy 下所有可能觀察 trace 的集合。當編譯後的實作更受限時，可以使用候選細化條件：

這項包含關係以相同的可觀測事件投影為前提；若兩個程序的 trace 格式不同，需先定義事件與非觀察步的投影映射。此條件若成立，且原始 $P$ 的所有觀察 trace 均滿足安全性 $S$，則 $P'$ 的所有觀察 trace 亦滿足 $S$。但它不自動保持活性、fairness、latency SLA、能源上界或所有需要的非確定性能力；研究必須另立 progress/budget/quality obligations。

16.4 不可見的內部步與不能消去的證據

只有在不影響任何觀察者／權威／恢復系統的前提下，才可將 local memory layout 改寫或某些純計算步隱藏為 $\tau$。對 AuthorityGeneration、SendCredit、CommitDecision、EffectIntent 或 GPUHostVisible 相關的狀態變化，compiler 必須保守處理。可觀察事件不只是使用者看見的畫面，也是事故後能否追查責任、重播因果和維持合法性所需的證據。

16.5 MLIR 利用方式與自訂 dialect 的範圍

MLIR 已支援 dialect op、type、attribute、side-effect interface、async 與 GPU dialect、conversion target／type converter 和 legality checks [E1–E5]。因此 SMPDC-C 應先嘗試：

1. 在 SMPDC dialect 中定義高層 op 與效果／capability attributes；
2. 使用既有 async、gpu、func、cf／scf 與 LLVM lowering 工具處理成熟部分；
3. 對提交、credit、evidence lineage、Unknown、fencing 保留受控 Runtime op，直到可證明它們的較低層展開；
4. 在最終 backend 採 applyFullConversion 等方法嚴格拒絕不合法 required op；
5. 不將尚未 lower 的權威操作以 dummy no-op 忽略。

如果使用 applyPartialConversion 作為中間步驟，不得把 partial success 當作產生合規原生執行檔。某 op 對 GPU backend 無相符降階時，應保持 VM fallback 或回報 UnsupportedTarget。

17. CPU、GPU、OS 與 Runtime 的降階正確性

17.1 最小可實作的 CPU 後端

第一版可採 Rust／C++ Runtime 配合 LLVM 或靜態函式呼叫生成，使用 FlowRegistry、EpochLedger、CouplingRegistry、CreditLedger、MessageRegistry、ReconcileService、CommitAuthority、TraceStore。CPU task execution 可以透過 OS thread、coroutine 或 work-stealing executor，但跨服務記憶體語義必須明列正確的 atomic ordering、鎖、mutex 及局部 ownership。

17.2 記憶體順序不是語言形容詞

LLVM 的 happens-before、atomic load/store、acquire-release 和 seq_cst 均有正式語義 [E6]。例如在 message queue 中，producer 對 payload 的寫入必須經過相符 publish synchronization，consumer 才能合法觀察完整 payload。若使用普通 data race 的共享 bool ready，即使某 Intel CPU 實測常常正確，也不能作為跨平台語義證明。

17.3 P/E core、CCD、SMT 及非均一快取

新型 Intel 的 P/E 核、AMD 的多 CCD、SMT 共用執行資源與不同 cache domain 是不同的異質性維度；語言 front-end 不應以 PWN=physical core 作為永不變的靜態定理。Placement planner 可收集核數、可用容量、核心群組與親和性資料，實作時需區分 requested_placement、eligible_placement 與 observed_placement。

17.4 不能把 CPU 核間傳送當作 GPU kernel 自動完成

兩顆 CPU 核之間的資料流，仍須透過實體 cache coherence、共享記憶體或其他互連。GPU kernel 可以計算下一段關係圖、批量合併證據或做向量比對，但這不等於 GPU 變成物理 CPU interconnect。模型既允許 GPU 加速，也要求在不適合的路徑上採 CPU-only。

17.5 目標專屬型別轉換

!smpdc.credit<e,c> 在 CPU 端可能降低成受控 token handle + ledger 索引；在 VM 端可能是線性值表項；若某 FPGA 未來提供硬體 credit tracking，仍需要等價的 authority、fencing、replay 與 failure semantics。不能因 target 不支援某個高層型別，就默默轉為無限制 uint64_t 並允許呼叫者複製。

17.6 GPU adapter 的最低欄位

GPUExecutionRequestV0_1 {
    work_id: WorkId
    device_id: DeviceId
    device_generation: Generation
    dependency_events: List[GPUEvent]
    input_leases: List[GPUBufferLease]
    output_leases: List[GPUBufferLease]
    precision_policy: PrecisionPolicy
    required_result_quality: QualityContract
    callback_scope: AuthorityScope
    deadline: OptionalDeadline
    trace_obligations: TraceSchemaRef
}

這個請求是運算請求，不是一份可直接產生正式提交的權威證書。GPU kernel 完成後，其結果還必須依 HostVisible guard、必要的品質驗證與 Paper 04 的提交流程處理。

17.7 資料局部性與算子實際性能

在小型訊息、頻繁跨設備搬移、分散控制流程、多次同步的場景中，GPU offload 可能大幅劣於 CPU-only。反過來，若大量可合批的比較、稀疏邊運算或解碼處理能降低 kernel launch 次數、提高算術強度，GPU 值得測試。這些是待測的工作負載條件，非已成立的普遍加速結論。

18. 形式化命題、證明概要與不可越界的結論

本節給出七個有前提的候選命題。它們尚未經 Lean、Coq、TLA+、Verus、SMT 形式證書或真實的完整 compiler refinement proof 驗證。每個結論必須視其假設成立而定，不得擴張為對任意程式、任意故障模型或任意硬體成立。

18.1 命題 A：合法資源型別檢查排除直接 credit alias

假設： A1：所有 SendCredit 均由唯一受控來源生成；A2：型別檢查器採用實際控制流敏感的所有權分析；A3：通往 DIFFUSE_RESERVE 的使用路徑必須消費唯一的 credit owner；A4：沒有繞過型別的未受信任 FFI；A5：每個轉移的動態守衛不會重新鑄造同一 credit。

結論： 通過 V0 型別檢查的單一 execution path，不能對同一 SendCredit 建立兩次互相獨立、同時有效的合法預留。

證明概要： 對程式語法／控制流歸納；唯一的 credit 保存在線性／仿射上下文，第一次合法消費將其移除；任何後續重用須有新的合法生成規則，與 A1–A5 矛盾。若存在 raw pointer、未知 FFI 或 Runtime ledger 的非原子 race，結論不適用。此命題不推出所有實體物理傳輸數必然有界，因為同一 logical send 的 transport retry 仍須另有預算。

18.2 命題 B：型別保持且正確降階下的非法權威提升排除

假設： B1：只有 COMMIT_DECIDE 的權威仲裁能引入受控 CommitDecision；B2：lowering 保留能力與 runtime check；B3：外部 bypass 通道被禁止；B4：作用域與世代有效性由真正權威服務裁定。

結論： 僅持有 Tentative、SealedLocalOutcome、MessageAck 或 GPUEvent 的受控程式，不能合法創造新的已授權提交決策。

證明概要： 在型別引入規則中，只有具有 ValidatedProposal 與有效 authority 的規範轉移可得 CommitDecision；對所有其他轉移的 effect 分析可確定無相應寫入效果。若 IR cast／FFI／Runtime bypass 存在則無法推出結論。

18.3 命題 C：R1 傳送不會自動提升 R2 獨立來源數

假設： C1：每個 candidate 的 origin lineage 不可隨 message attempt 而更改；C2：見證者型別由受信任 verifier 發出；C3：reconciliation 按來源政策而非 attempt 個數累計。

結論： 對同一 candidate 的多個 R1 delivery attempts，單純增加 attempt 次數不會產生新的 IndependentWitness。

證明概要： attempt 被映射回不變的 candidate/origin，驗證器不會因 multiplicity 改變其來源分割。若 provenance 不可信或模型共通錯誤被隱藏，不能推導統計獨立或結果真實。

18.4 命題 D：提交回應未知不能合法轉為新鍵無條件重送

假設： D1：StepResult 的 Unknown variant 必須被處理；D2：CommitKey 的唯一性與語義受校驗；D3：compiler verifier 禁止 Unknown -> create new key -> commit 的未授權路徑；D4：runtime 提供可靠 query-first 或 fail-closed policy。

結論： 符合此語言和 Runtime 契約的 caller 不會因把 Unknown 誤當 Rejected，自動發起一項全新鍵的相同效果提交。

限制： 不推出外部 receiver exactly-once；亦不保證 query 總會立即成功。

18.5 命題 E：GPU 完成與 CPU 可見性保持分離

假設： E1：每個 host read 的合法型別是 HostVisible<T,B>；E2：此型別只能由符合 target memory model 的實際同步與可見性確認取得；E3：GPU buffer lease 在該路徑上有效；E4：不存在繞過型別的 raw-pointer host read。

結論： 在受控路徑中，不能僅憑 GPUEvent 直接合法讀取受保護的 GPU output。

限制： 仍須在實際 GPU API、driver 與設備上正確實作同步；一個錯誤的 adapter 可破壞全部假設。

18.6 命題 F：trace refinement 對安全性之條件保持

假設： F1：原始語義所有可觀察 trace 滿足安全性 $S$ ；F2：編譯器與 Runtime 降階後的 trace 在相同事件投影與故障假設下是原始 trace 集合的子集；F3： $S$ 只依該觀察投影決定。

結論： 目標實作的所有可觀察 trace 滿足 $S$。

證明概要： 集合包含關係的直接推論。若優化變動觀察方式、漏掉提交／失效事件、或讓故障模型與來源不同，F2/F3 不成立。此命題不給出低延遲或高吞吐保證。

18.7 命題 G：有限 credit 不等於編譯器證明 termination

假設： G1：某 epoch 初始 data credit $B_0(e)$ 有限；G2：每次新受准許的資料擴散都消耗唯一 credit；G3：credit 不複製、不退款；G4：新 epoch 入場獨立限額。

結論： 該 epoch 的受准許 logical data emission 次數有界於 $B_0(e)$，但不能從此推出所有本地計算、控制訊息、重送、接收、驗證或正式提交必然停止。

反例： 兩個 flow 在沒有再送任何資料的情況下，仍可因等待彼此不可達的 phase predicate 而永久停滯。此反例反映了安全、活性與終止性的邏輯差異。

18.8 尚待形式檢查與機器可讀證據

L2 階段建議利用有限狀態模型檢查 CreditLedger、lease fencing、Unknown recovery；利用型別／資料流 checker 驗證一次性資源；對可靠的局部 Rust 實作可評估 Verus、TLA+、property-based testing 等工具。但這些工具本身不代表研究已完成；必須提供實際 property、假設、solver 結果、反例 trace 與版本固定的原始碼 [E9]。

19. 確定性參考解釋器與微型可執行語義

19.1 V0 的實作目標

在開始寫 LLVM 或 GPU backend 前，先建立一個單進程、可重演、可檢查轉移的參考執行器。其目的不是模擬 CPU cache 或 GPU 實體效能，而是在有限的流程與故障空間內清楚回答：某指令是否可執行？若可執行，它如何改變資源、版本與證據？若不能，會出現哪一種 Rejected／Failed／Unknown？

一個可接受的 V0 Reference VM 應具有：

1. 固定且可查驗的 module_header 與 feature agreement；
2. 工作流、phase、topology、epoch、message、credit、reconciliation、speculation、commit 的 typed registries；
3. 單步 deterministic transition（給定同一 state、同一 event queue、同一 scheduler choice）；
4. 明確的 scheduler event order，必要時以固定 seed 重播非確定性候選；
5. 帶 source op span、IR op ID、flow_id、event_epoch、authority_scope 的 trace；
6. 分別呈現 Applied、Pending、Rejected、Failed、Unknown；
7. 每步可執行不變量檢查；
8. 有限模型探索／狀態 hash／重複偵測；
9. 可輸出 JSONL trace 與 machine-readable rejected witness；
10. 允許與 hand-coded baseline 比較，而不把「參考解釋器速度」當成 SMPDC 的硬體成績。

19.2 抽象 VM 狀態

延續 Paper 05 的十項解釋器分解（不是新增第十個中觀計算本體軸）：

對 VM 定義小步轉移 $\mathbb M\xrightarrow{i,\ell}\mathbb M'$。$i$ 為一項具型別 PDAIS 操作；$\ell$ 是可觀察事件標籤。對有權限的外部效果，即使轉移尚未成功，亦可記錄拒絕／未知結果；但不能悄悄修改被保護的 CreditLedger、CommitLedger 或權威登錄而只輸出錯誤字串。

19.3 最小轉移表

19.4 必須刻意區分模型簡化與物理實作

模型中的 DIFFUSE_RESERVE 可以是一個抽象原子轉移；實際 CPU Runtime 可能以 CAS、鎖和日誌組合實作。VM 中的線性化點是候選規格需求，而不是 x86／ARM 某條指令天然就是整個跨作用域 protocol 的 atomic transaction。若參考 VM 的合法模型無法被實際後端細化，工程應被判定為未完成，而不是修改 VM trace 以掩飾違反。

19.5 確定性不等於固定唯一排程

V0 可以在某一次 trace 使用 deterministic scheduler；同時必須允許有限模型遍歷多種不同但合法的事件順序。若只測一個 seed，就可能無法發現 credit 重複、ACK 遲到與 rebind 同時發生的競速。必要時應使用 bounded interleaving exploration，並對不同 trace 映射到相同安全性規則。

19.6 一個能檢查的微型 Python 參考子集

以下程式只示範信用與提交鍵的受控狀態轉移。它不是完整的 SMPDC-Lang parser，不處理持久化、GPU、R2、分散式故障或外部服務權威；不可將它當作 L2 級完整 compiler。程式可在 Python 3 標準環境執行，目的在檢查資源與拒絕行為的最低邏輯。

from dataclasses import dataclass, field
from typing import Dict

@dataclass
class MiniState:
    budget: int
    tokens: Dict[str, str] = field(default_factory=dict)
    permits: Dict[str, str] = field(default_factory=dict)
    committed: Dict[str, str] = field(default_factory=dict)
    trace: list[str] = field(default_factory=list)

    def __post_init__(self):
        if self.budget < 0:
            raise ValueError("negative budget")
        if not self.tokens:
            self.tokens = {f"c{i}": "Available" for i in range(self.budget)}

    def reserve(self, credit: str, permit: str) -> str:
        if self.tokens.get(credit) != "Available":
            self.trace.append("Rejected:CreditUnavailable:" + credit)
            return "Rejected"
        if permit in self.permits:
            self.trace.append("Rejected:PermitDuplicate:" + permit)
            return "Rejected"
        self.tokens[credit] = "Reserved"
        self.permits[permit] = credit
        self.trace.append("Applied:Reserve:" + credit)
        self.check()
        return "Applied"

    def send(self, permit: str) -> str:
        credit = self.permits.pop(permit, None)
        if credit is None:
            self.trace.append("Rejected:PermitMissing:" + permit)
            return "Rejected"
        assert self.tokens[credit] == "Reserved"
        self.tokens[credit] = "Spent"
        self.trace.append("Applied:Send:" + credit)
        self.check()
        return "Applied"

    def retire(self, permit: str) -> str:
        credit = self.permits.pop(permit, None)
        if credit is None:
            return "Rejected"
        assert self.tokens[credit] == "Reserved"
        self.tokens[credit] = "Retired"
        self.trace.append("Applied:Retire:" + credit)
        self.check()
        return "Applied"

    def decide(self, key: str, digest: str, authorized: bool) -> str:
        if not authorized:
            return "Rejected"
        prior = self.committed.get(key)
        if prior is not None and prior != digest:
            return "Conflict"
        if prior is None:
            self.committed[key] = digest
            self.trace.append("Applied:Commit:" + key)
        return "Existing" if prior is not None else "Applied"

    def check(self) -> None:
        counters = {name: list(self.tokens.values()).count(name)
                    for name in ("Available", "Reserved", "Spent", "Retired")}
        assert sum(counters.values()) == self.budget
        assert all(self.tokens[c] == "Reserved" for c in self.permits.values())
        assert len(set(self.permits.values())) == len(self.permits)

if __name__ == "__main__":
    s = MiniState(budget=2)
    assert s.reserve("c0", "p0") == "Applied"
    assert s.reserve("c0", "p1") == "Rejected"
    assert s.send("p0") == "Applied"
    assert s.send("p0") == "Rejected"
    assert s.reserve("c1", "p2") == "Applied"
    assert s.retire("p2") == "Applied"
    assert s.decide("k1", "digest-A", True) == "Applied"
    assert s.decide("k1", "digest-A", True) == "Existing"
    assert s.decide("k1", "digest-B", True) == "Conflict"
    assert s.decide("k2", "digest-C", False) == "Rejected"
    s.check()
    print("mini semantic checks passed")

研究限制： MiniState.decide 的 authorized: bool 僅適合離線玩具測試；真正權威必須具有 scope／generation／version／durability 檢查，不能把布林值直接當 capability。此子集沒有運用語言的編譯期仿射 checker，僅驗證 VM 的局部 runtime 防重邏輯；不能用它宣稱已形式證明或實作完整 PDAIS。

20. 故障注入、負面測試與屬性導向驗證

20.1 最低 V0 負面工作負載

每一類至少要產生可重播 trace，並指定預期 rejection：

20.2 Finite-state／property-based 模型

以小型配置（例如 2–3 flows、有限 credit、2 epochs、2 versions、少量 messages）完整列舉排程與故障。必查性質包括：

• 任一 token 在任何有效狀態最多一個 owner；
• 任一 active permit 的 credit 必為 Reserved；
• Spent／Retired token 不會再次恢復 Available，除非規範升級明確另訂安全回收；
• 相同 (domain,commit_key) 不得有兩個彼此衝突的合法決策；
• 舊 owner 無法越過有效 fencing；
• Tentative／GPUEvent 不得透過未授權路徑成為正式結果；
• 已 seal epoch 的 quiescence 判定必須包含在途 control/data obligations；
• 當實體接收者不可達時，不得宣告必然活性。

20.3 差異測試與 oracle

把同一組 typed PDAIS-IR 交給 V0 VM 和 V1 CPU backend，對相同輸入和故障腳本比較合法可觀察 trace，而不只比較最後的數值。建立至少三種 oracle：source semantics oracle、protocol invariant oracle、task-result quality oracle，避免一個 faulty system 同時「產生錯誤結果」和「自行認定錯誤結果合法」。

20.4 Property generator 的分層

建議產生三種不同輸入族：

1. Well-typed, policy-compliant programs： 探索真正合法操作的排程競速；
2. Ill-typed or forged programs： 確認 30 條 compiler rejection 規則能阻止；
3. Well-typed but stale-at-runtime inputs： 確認不同設備／租約／版本的動態失效被正確拒絕。

只測第 2 類會高估靜態 verifier 的效果；只測第 1 類則容易漏掉真實系統的權限和版本競速。

20.5 必須公開的失敗證據

對所有失敗案例保留：source digest、AST/IR hash、compiler version、target、policy digest、seed、觀察到的錯誤碼、預期規則、事件偏序、最短可重放 trace、實際結果。不要讓「失敗數量多」被直接解讀為安全性更差；更多負面測試也可能只是更早揭露錯誤。比較必須對齊測試集合、工作負載與主張的安全契約。

21. 可證偽效能研究：語言與編譯器是否值得存在

21.1 應評估的不是「編譯出多少行 LLVM」

語言的新穎性可在語義責任；效能研究則必須觀測真實的任務完成成本。對給定 workload 與等品質限制，主要指標應包含：成功正式提交的 useful work／秒、端到端 p50/p95/p99、平均與尾端 queueing delay、CPU 與 GPU 忙碌時間、cache miss、memory bandwidth、device copy bytes、能量／有效結果、因回滾或衝突浪費的 work 比率、以及 compile/build overhead。

21.2 實驗比較組

所有組別都必須在對應的功能與安全範圍中公平比較，不能拿沒有版本驗證、沒有 R2 品質開銷的弱基線，來宣稱完整協議加速。可以分別報告同品質、同硬體、同能源、同延遲上限的 Pareto frontier，而不是選擇對自己有利的單一跑分。

21.3 工作負載矩陣

• W1： 細粒度、有依賴的 DAG；對比 phase gating／同步成本。
• W2： 高頻小訊息；測量 credit ledger 和 queue 競爭。
• W3： 大量可批次比對；測試 CPU SIMD 與 GPU 的收支平衡。
• W4： 事件驅動工作流與不規律稀疏圖；測試多主工作流適用性。
• W5： 混合大小工作、熱點及負載不均；測試重綁與 cache locality。
• W6： R1 尾端延遲與共享故障源；測量複製不保證收益的負面情境。
• W7： 版本衝突、重試與持久化 commit；測試事務開銷。
• W8： 可控的稀疏／MoE 或模型推論 pipeline；保持模型、精度及品質相同。
• W9： 連續 Agent pipeline，區分計算進度與正式對外效果。
• W10： 長期訓練或梯度更新子系統；測量失敗／恢復與 deterministic training contract。

W8–W10 的意義不在於宣稱一定優於目前的 PyTorch／CUDA／分散式訓練系統，而是給予公平比較的特定應用候選。若密集張量計算在既有 GPU 高效率 kernel 下已非常好，額外相位與消息層很可能帶來純負收益。

21.4 V0 實驗的準則

V0 成功是能解析、拒絕、轉譯、重播與查核；例如 30 條 verifier 規則的每條 positive/negative fixture 皆可重現，同時對 PDAIS-IR 執行有限模型檢查。此時不得把 Python 或 VM 的運行耗時當成 CPU 架構優勢。未能支援的指令須明確列入 feature support matrix，而不是宣稱全部語言已完整實作。

21.5 V1 實驗的準則

從目前可用的一般 CPU／GPU 開始，不要求先購買昂貴的伺服器 CPU。對使用者目前仍屬舊款 AMD CPU、RTX 3070、32GB RAM 的桌機，可先研究 CPU-only 和有限 GPU 批次工作；如日後更新至有 P/E-core 的 Intel 或多 CCD 的 AMD 平台，再擴張 topology 比較。新平台不能在未購買前記為已完成實測。

需要固定或報告：OS、BIOS、微碼、電源計畫、CPU frequency、RAM channels、NUMA／cache topology、GPU driver、CUDA 版本、batch size、CPU affinity、compiler flags、樣本數、暖機和測量區間。若 GPU 不支援某 kernel，應展示 CPU-only 結果，而不是刪除該實驗樣本。

21.6 可推翻的具體假說

• H06-A： 在等品質／等硬體下，特定細粒度 workload 可因持續 flow 降低狀態重建或排程開銷。否證方式：優化後 actor/async 基線持續優於 SMPDC。
• H06-B： 有型別與效果系統能顯著降低特定跨協議安全缺陷率。否證方式：盲測開發者的錯誤率無改善或額外複雜度更高。
• H06-C： PDAIS-IR 可以讓 compiler 自動合法合批／局部化，減少手寫協議缺陷且不增加不可接受延遲。否證方式：所有 pass 在相同資源下沒有實際改進。
• H06-D： 在有明顯 tail latency 的路徑，R1 對特定 workload 的 p99 有益。否證方式：資源競爭與額外 bytes 抵銷收益。
• H06-E： GPU 對適當大批次關係運算有淨效益。否證方式：小訊息、資料搬移或核啟動主導。
• H06-F： 跨 P/E 或 CCD 的 topology-aware compiler/Runtime 配置可能改善特定工作負載。否證方式：OS 現有排程與快取局部性優化已達相同或更好水平。

假說皆是工作負載條件性的研究主張，不是對所有 CPU／GPU 平台的效能定理。

22. 語言、編譯器與成熟技術的比較邊界

22.1 資料流與 Actor 的成熟先例

Kahn process networks、Tagged-Token Dataflow、Actor 模型及 Dijkstra–Scholten 的 diffusing computation 已經建立訊息驅動、資料依賴與終止偵測的先例 [E10, E12, E14]。SMPDC-Lang 不能將「節點並行」本身當作首次發明。差別候選在於：把 phase-relevance、有限信用、資料來源血緣、暫態提交和設備可見性組合成可被一個 compiler 全程保留的安全契約。

22.2 MLIR 與 LLVM 已有的能力

MLIR 支援 dialect 定義、SSA、operation verifier、effect modelling、GPU 與 async lowering、conversion legality 等重要機制 [E1–E5]。LLVM 有成熟 memory model、原生機器碼生成及大量最佳化先例 [E6]。因此本研究傾向建立新 dialect／DSL，而不是從零打造所有 compiler backend。

22.3 Rust 與線性／仿射資源

Rust 的 move／borrow 與所有權模型可作為實作非可複製資源型別的基底，但一般 Drop、Send 與 borrow checker 不會自動保證跨網路 credit 守恆、失效 owner fencing、提交權威原子性或第三方效果 exactly-once。SMPDC 的額外契約可用 Rust 包裝部分實現；是否需要全新語言，要由比較實驗決定。

22.4 可驗證系統與形式工具

Verus 等工具提供對低層系統程式進行規格化驗證的途徑，但不是只要將程式放入 Rust／Verus 專案便自然得到安全性 [E9]。實際證明須對模型、假設、ffi 邊界、共享狀態及目標編譯器提出具體義務。Compiler correctness 更不能由少量單元測試代替。

22.5 GPU 與非同步框架

CUDA Graphs、MLIR GPU dialect、GPU kernel fusion，以及成熟 tensor compiler 早已對大批次 GPU 工作具有良好支援 [E3, E5]。SMPDC-Lang 應只處理它們尚未自然表達的跨工作流資訊協議和 authority boundary，不應因為語言使用 gpu 關鍵字就宣稱完成新的 GPU 演算法或 GPU 通訊硬體。

22.6 可能成立的有限原創性範圍

待證明的貢獻可以是：一個將多主持續工作流、相位耦合、有界傳播、R0–R3、推測和權威效果一起納入的協議型別／效果模型；一套能維持其可觀察語義的 PDAIS-IR 和 verifier；及在被明確限定的工作負載上成功保證安全、降低開發缺陷或提升效率。不能將已存在的單獨元件重述為全新數學或運算複雜度結果。

23. 版本化 ABI、模組協議與可重放證據

23.1 模組標頭沿用 Paper 05

PDAISModuleHeaderV0_1 {
    pdais_major: 0
    pdais_minor: 1
    required_features: Set[FeatureId]
    optional_features: Set[FeatureId]
    schema_registry_digest: Digest
    effect_policy_digest: Digest
    lowering_target: Virtual | HostCPU | HostGPU | Hybrid
}

Source language 版本與 PDAIS op-set 版本可以不同步演化，但編譯器必須公開轉譯目標與 schema digest。0.1 不是永遠允許任意不相容語義修改的藉口；只要改變觀察效果、resource ownership、failure model 或 commit semantics，就應提升相應相容性標記並拒絕未協商的舊模組。

23.2 受保護的基本封套

MessageEnvelopeV0_1 {
    flow_id: FlowId
    flow_generation: FlowGeneration
    event_epoch: EventEpoch
    topology_generation: TopologyGeneration
    authority_scope: AuthorityScope
    logical_result_id: ResultId
    candidate_id: CandidateId
    message_id: MessageId
    delivery_attempt_id: DeliveryAttemptId
    source_lineage_ref: EvidenceRef
    redundancy_mode: R0 | R1 | R2 | R3
    payload_type: SchemaId
    payload_digest: Digest
    send_credit_ref: OptionalCreditRef
    attempt_budget_ref: AttemptBudgetRef
    trace_parent: OptionalEventRef
}

哪些欄位可以透過 session 或受控 registry 還原，需由具體 transport ABI 定義。為了減少 bytes 而省略欄位，不能讓接收者失去辨識 stale epoch、同源 R1、異源 R2 或內容衝突的能力。若 hash 演算法、序列化格式或 ID 編碼規格改變，也應有一致的版本處理。

23.3 Compiler manifest 與可驗證責任

建議 compiler 輸出一份 CompileManifestV0_1，至少記錄：source digest、schema version、compiler build ID、PDAIS-IR digest、target triple、feature set、required guards、ownership checker policy、optimization passes、unlowered feature list、runtime ABI version、trace schema、可執行檔 digest、已通過的測試（如有），以及沒有執行的測試。Manifest 不能只寫 secure: true 或 proof_passed: true 這類不具可追查性宣告。

23.4 Trace 的因果性與跨設備對齊

最低 trace 欄位為 event_id、flow_id、operation_id、event_epoch、logical_clock_or_causal_parent、authority_scope、resource_debit、state_version、result_variant、device_event_ref、wall_time_if_available、source_span。跨 CPU/GPU 時鐘有不同尺度和校準誤差，不能直接以兩端 timestamp 差宣稱某訊息傳送耗時為負或零。建議保留各設備原生時間與共同的因果偏序，再做有誤差範圍的時間對齊。

23.5 版本相容性矩陣

24. 安全模型、資源封閉與供應鏈邊界

24.1 最小威脅模型

假設普通原始程式可能犯錯或惡意要求過量 credit、濫發 epoch、冒用另一個 source lineage、提交未授權資料、利用 FFI 繞過型別或在 GPU result 未完成時讀取 buffer。對受信任 Runtime 部分仍應考慮 crash、重啟、日誌不一致、競態、out-of-memory 與錯誤配置。編譯器可以降低一部分風險，但不能把硬體故障、惡意 OS、被入侵的外部權威或不可信 firmware 自動排除於研究之外而不標示。

24.2 繼承最小權限與失效關閉

即使某 AI scheduler 建議增加 fanout，也不可繞過已核發 credit 的上界。即使 kernel 想提前完成外部效果，也不可越過權威 commit barrier。權限不可由普通數值推導，且失效的 lease／capability 應在受保護資源使用時再次檢查。UnknownRequiredOperation、StaleAuthorityGeneration 及異常 FFI 路徑應 fail closed。

24.3 避免將密碼學與型別保證混同

如果 transport 需要真正的簽章、MAC 或 attestation，則這是另一個獨立的安全子系統。AuthorityCap<T> 的型別名稱不會自動使訊息具不可偽造性；真實安全性仍取決於密鑰管理、授權簽發者、撤銷、加密協定、可信域邊界和實作正確性。即使密碼學驗證通過，也不自動保證演算法的答案真實或業務交易合法。

24.4 防止編譯器信任膨脹

假設 compiler pass、外部 plugin 和 build cache 都可能出錯。重要的 PDAIS-IR 應能在 build pipeline 結尾重新由獨立 verifier 驗證；有必要時對目標 artifact 設置 runtime admission checks。某段生成機器碼如果有未被驗證的 unsafe code，不能因此宣稱已獲語義細化證明。

25. 與 EveMissLab 既有研究的精確關係

25.1 群星模型及早期電腦應用草稿

Neo.K 先前《群星模型：基於宇宙星系概念的 AI 模型設計方法論》與《群星架構在計算機系統中的應用與改良計畫》已提出節點自治、星系關係和硬體資源動態化的概念 [I6]。本篇將其向程式語義收斂，但不把星點的幾何類比直接變成 CPU 物理導線圖，也不把早期概念稿當成已完成硬體模擬的證據。

25.2 PCMT、GCCFT 與相位的真正範圍

PCMT 將相位本體、表示、演化機制及承載架構分離；GCCFT 探討計算場、耦合、相位和可證偽 Runtime [I7–I8]。SMPDC-Lang 只接收與具體工作流互動相關的相位效果，不在語言中宣稱所有計算皆必須使用同一種相位物理機制。

25.3 GCCWT／GCM 與跨世界規劃

GCCWT 與 GCM 的計算場、跨設備資源規劃及 AI-assisted orchestrator 屬更高層的資源和權限決策 [I9–I10]。本篇是靠近單機與近硬體執行的語言契約，可接收這些系統提出的候選 execution plan，但仍由合法 Runtime 和 authority scope 決定計算能否執行、提交或外發效果。

25.4 ISQL、NICA、24／72 作為可選上層表示

未來可將 ISQL 語義、NICA 之類架構、24 計算範式與 72 格的分類投影為 OperatorKind、PhaseKind、TaskContract 或 RepresentationPolicy 等附加 metadata；但第一版 Reference VM 應能獨立運行一般數學、普通資訊傳遞與 CPU-only workload。既有原創理論的整合是未來擴充方向，不得變成驗證 SMPDC-Lang 安全所必需的先驗前提。

25.5 與新一代 AI 計算的接口

具有長期狀態、稀疏觸發、工具調用與權威效果的 Agent workflow，是這套語言的一個候選應用域。大規模 dense training 或高速 GPU tensor kernels 是否需要額外的多主信息協議，必須另由 Paper 10 的實測判斷。若傳統 compiler/Runtime 已使 AI 模型達到更佳效能，本篇不預設要取代它。

26. 工程分期、研究完成定義與後續論文交接

26.1 V0-A：規範收斂

完成 lexer、restricted EBNF parser、名稱解析、源碼定位、TypeId／EffectId registry、PDAIS op schema，並能從語言模組產生具完整錯誤訊息的 typed AST。宣告的語法與實際 parser 必須相符；若簡化語法尚未支援，不得在文檔把它列為已實作。

26.2 V0-B：驗證器與 IR

完成 affine/linear checker、effect inference、authority-sensitive construction、R0–R3 evidence type、Unknown exhaustive match，以及 AST → PDAIS-IR。保留每條 op 的七段契約與 manifest。最低測試：30 條 C06 規則各一個 negative fixture、至少一個修正後正例，並包含跨 module／不同 build options 的回歸測試。

26.3 V0-C：參考 VM 與證據

實作抽象機器的最低核心：Flow、Epoch、Phase、Couple、Diffuse、Message、Reconcile、Speculation、Commit 及必要 Trace。GPU 可先用 deterministic mock events 模擬；若 mock 和實際設備語義不一致，應標記不受測功能。產出一組固定 seed 的 JSONL 追蹤及有限模型反例。這一階段的 PASS 只能稱 L2 子集，不等於整套 SMPDC 全部驗證完成。

26.4 V1-A：現有 CPU 實機運行

以已有的 x86／Windows 或 Linux 平台建立 CPU-only runtime，將 PDAIS-IR 的必要操作降為可信賴的同步、queue、atomic、版本與持久化機制。對 C++／Rust actor、dataflow 或 thread-pool 基線進行等品質測試。觀察後端可否達成 verifier 的 trace 契約，不直接推斷較高核心數必然較快。

26.5 V1-B：GPU adapter

僅對真正適合的 batch kernel，加入 MLIR GPU／CUDA 或其他設備 API 的事件、buffer、可見性與精度契約。基於實測給出 offload break-even 與負面 workload 範圍。若資料傳輸成本超過運算收益，允許正式得出 CPU-only 更優的結論。

26.6 Paper 07 的正式交接

交付 FlowRegistry、事件喚醒、core placement metadata、backpressure、epoch admission、authority guard、可選 AI proposal、worker migration／fencing、GPU adapter interface 及安全恢復。AI-free deterministic control 必須是一等可測路徑。 不得讓 AI 自動創造不可偽造資源或改寫權威歷史。

26.7 Paper 08 的正式交接

交付 GPU 工作切分、批次與事件依賴、host/device buffer lifetime、合法 memory visibility、數值精度、device fallback，以及可公平測量 CPU/GPU overhead 的全部 trace 欄位。GPU 不適合的工作負載要留下測試結果。

26.8 Paper 09 的正式交接

只在確定軟體協議瓶頸後，才選擇值得硬體化的操作。對 P/E core、CCD、cache、NUMA、NoC、custom instruction 和 FPGA 進行可量測的不同層級評估。除非有可用的模擬／RTL／原型結果，不宣稱物理 ISA 已設計成功。

26.9 Paper 10 的正式交接

在 AI 訓練、推論、稀疏模型與 Agent 系統設定同模型、同數據、同品質、同資源的比較。記錄 Token/s、steps/s 之外的有效提交品質、恢復成功率、GPU copy overhead、能源與失敗率。

26.10 Paper 11 的正式交接

最終應匯整支持、反證、受限適用、尚未完成與成本過高的結果。即使 SMPDC-Lang 的主要價值只是在更安全地表述並編譯既有協議，仍須如實給出研究結論，而不要求以速度突破來維持原創性敘事。

27. 結論：編譯器必須懂得責任，而不只懂得資料型別

這一篇的研究問題不在於替 send()、await()、commit() 找新的華麗拼字，而是：一段程式能否在每個 CPU 核心都可能承載獨立主工作流、資訊依相位進行有界擴散、GPU 有選擇地承接批次計算的情況下，仍保留可理解且可被機器檢查的權限、資源與證據責任。

本篇提出五個主要候選交付：

1. SMPDC-Lang 的嚴格語法子集，以及可持續、可重綁的 flow 執行模型。
2. 一套區分一般資料、affine/linear 資源、相位證據、暫態結果、提交權威與 GPU 可見性的型別／效果系統。
3. Source → Typed AST → Flow-HIR → PDAIS-IR → Reference VM／CPU／GPU backend 的契約保持編譯管線。
4. 三十條最低驗證規則、十六類最佳化合法性義務及七項有前提的安全命題。
5. 包含負面測試、A/B baseline、設備成本與版本證據的 V0–V1 研究方案。

本篇不聲稱新增實體 CPU/GPU opcode，不聲稱已可在任意硬體原生執行，更不聲稱完成真實 AI 訓練加速。它將前五篇的執行模型具體化為能被嚴格拒絕錯誤用法、保留正確權限邊界，並能隨硬體與 Runtime 演化的候選語言與編譯器架構。其價值需要下一階段的可執行實驗、形式證明與實機評測建立或否證。

附錄 A｜語言標準子集的最低測試集

A.1 必須接受的純函數

module MinimalPure version "0.1" {
  fn identity(x: u64) -> u64 effects [] {
    return x;
  }
}

這個例子用於 parser／type checker 的最低煙霧測試：普通值不需要擴散、權威或 GPU；沒有效果時不應編造一個外部狀態轉移。該語法是候選規格，不是已跑過的 compiler 產物。

A.2 必須拒絕的 credit 重複使用

module DoubleSpend version "0.1" {
  flow Bad(c: SendCredit<E0,C0>, edge: Edge, msg: Message)
    owns local: LocalState
    requires [CreditReserve] {
    linear let x = call DIFFUSE.RESERVE(edge, move c, msg);
    linear let y = call DIFFUSE.RESERVE(edge, move c, msg);
    return;
  }
}

預期 C06-02 CreditDuplicated。這段故意不完整，足以作為負面 fixture；允許 checker 在更早的 TypeMismatch 擋下該程序，但必須能辨認第二次使用同一 credit 的根因。

A.3 必須拒絕的局部結果權威提升

module IllegalPromotion version "0.1" {
  fn bad(x: SealedLocalOutcome<K31,Payload>) -> Committed<Payload,K31>
    effects [] {
    return cast_committed(x);
  }
}

預期 C06-14 LocalOutcomePromotion；不能透過自定義不安全 cast 繞過規範。

A.4 必須拒絕的 GPU 完成假設

module IllegalGpuRead version "0.1" {
  fn bad(event: GPUEvent<G0,W1>) -> HostVisible<Payload,B9>
    effects [] {
    return cast_host_visible(event);
  }
}

預期 C06-23 GpuVisibilityBypass。即使 GPU 工作已在某次執行中完成，原始程式也不能無條件省略版本、設備同步和 host visibility 契約。

A.5 必須拒絕的 commit Unknown 布林化

module UnsafeUnknown version "0.1" {
  fn bad(s: StepResult<CommitDecision<D0,K0>>) -> bool
    effects [] {
    return bool(s);
  }
}

預期 C06-20 LossyResultMatch。編譯器至少需能分辨 Unknown、Rejected、Pending 與 Failed，不能把未確認的正式效果誤判為單純成功／失敗。

附錄 B｜參考 repo 構想與可交付檔案

smpdc-lang/
  README.md
  LICENSE
  specification/
    language-grammar-v0.1.ebnf
    source-type-system-v0.1.md
    pdais-ir-v0.1.md
    effect-policy-v0.1.yaml
    abi-v0.1.json
    error-codes-v0.1.json
  compiler/
    lexer/
    parser/
    typed_ast/
    effect_checker/
    linear_resource_checker/
    flow_hir/
    pdais_ir/
    verifier/
    passes/
      phase_safety/
      credit_preservation/
      evidence_lineage/
      commit_barrier/
      gpu_visibility/
    backends/
      reference_vm/
      cpu_llvm/
      gpu_adapter/
  runtime/
    flow_registry/
    epoch_and_credit_ledger/
    message_registry/
    phase_and_coupling/
    reconcile/
    speculative_commit/
    effects_outbox/
    device_adapter/
  tests/
    grammar_positive/
    grammar_negative/
    type_effect_positive/
    type_effect_negative/
    runtime_finite_state/
    fault_injection/
    differential_trace/
    backend_conformance/
  benchmarks/
    traditional_baselines/
    cpu_only/
    cpu_gpu/
    trace_and_energy/
  evidence/
    compiler_manifests/
    model_checker_runs/
    conformance_reports/
    ablation_results/

注意： 本樹狀結構是後續實作計畫，不是已建立 GitHub 倉庫的聲明。程式實作後要另外提交可驗證的 commit、CI、test logs 和 benchmark data；不能從論文中的樹狀圖推斷實作已存在。

附錄 C｜跨篇接口與安全審核清單

1. FlowId 與 OS core ID 是否完全分離？
2. 所有線性資源是否具有唯一 owner？
3. 在中斷、cancel、panic、crash 下是否都有清償策略？
4. PHASE_SIGNAL 與依賴驗證是否分離？
5. 新拓撲世代是否能 fence 舊 edge？
6. Data credit、control budget、attempt budget 是否分開？
7. 所有新 logical emission 是否計量？
8. 同一 MessageId 的重送是否禁止重新造信用？
9. R1、R2、R3 的證據等級是否由受控建構器產生？
10. Local result 是否永遠不自動提升為 commit decision？
11. UnknownCommit 是否必須 query-first？
12. Commit key 是否穩定且受權威 scope 保護？
13. 版本與隔離等級是否符合業務不變量？
14. GPUEvent 是否保留實體非同步完成依賴？
15. Host read 是否有真正的 buffer visibility guard？
16. 外部效果是否在已提交 decision 後處理？
17. ABI feature negotiation 是否遇未知 required op 時拒絕？
18. 每個 optimization pass 是否留有 preservation obligation？
19. Source/IR/target trace 是否可互相追溯？
20. 每項效能結果是否有公平 baseline、品質契約及完整負面證據？

這些清單不是靠單一 true/false 靜態檢查就能自動完成。有些義務需要 compiler，另一些需要 Runtime、權威服務、特定 GPU driver、形式證明與人工審閱共同承擔。

附錄 D｜研究版本、原始碼與正式品質閘門

D.1 Canonical source

本研究正式原稿為 UTF-8 Markdown source artifact。所有數學源碼僅使用 $...$ 與 $$...$$ 作為唯一 canonical 分隔符；不得以渲染畫面反向重建、Unicode escape round-trip 或自動替換反斜線後宣稱保持原稿。其他衍生 PDF、網頁與展示圖都只是投影，不是正式 canonical source。

D.2 每次發佈前需實際執行的檢查

• 檔案以嚴格 UTF-8 解碼成功且沒有 NUL／異常替代字元；
• Markdown code fences 有配對，數學分隔符在碼框外無未閉合；
• YAML front matter 可解析且與論文序號、名稱和成熟度一致；
• 所有 [I*]／[E*] 引用有明確條目，沒有虛構的 DOI／commit／測試結果；
• 章節、附錄、版本號及下篇交接一致；
• 若內文聲稱可執行測試「已通過」，須有當次真實工具執行記錄；
• 若未經 L2／L3 驗證，須維持明確的「未實作／未實測」標示；
• Markdown 檔案以已確認的真實 container path 輸出，並記錄位元組數及 SHA-256。

D.3 研究誠實性聲明

本篇是完整的形式候選語言與編譯器研究原稿。現階段尚無一份已完成的完整 SMPDC-Lang compiler、PDAIS-IR toolchain、官方語言規範委員會、特定 CPU 加速器、或已取得實體硬體優勢的實驗報告。本文的命題以所列條件成立為前提，對比既有研究的分析不是第三方背書或已完成同行評審證明。所有後續實作與聲稱都必須能由可重現的原始碼和證據獨立查核。

參考文獻與前置原稿

內部 SMPDC 正式原稿

• [I0] Neo.K × Aletheia, SMPDC Paper 00 — Stellar Multi-Primary Persistent Diffusive Computing, v0.1, 2026-10-16。Canonical source：SMPDC_Paper00_Stellar_Multi_Primary_Persistent_Diffusive_Computing_v0.1_2026-10-16.md。
• [I1] Neo.K × Aletheia, SMPDC Paper 01 — Multi-Primary Workflow Nodes, v0.1, 2026-10-16。Canonical source：SMPDC_Paper01_Multi_Primary_Workflow_Nodes_v0.1_2026-10-16.md。
• [I2] Neo.K × Aletheia, SMPDC Paper 02 — Phase Coupling and Bounded Persistent Diffusion, v0.1, 2026-10-16。Canonical source：SMPDC_Paper02_Phase_Coupling_and_Bounded_Persistent_Diffusion_v0.1_2026-10-16.md。
• [I3] Neo.K × Aletheia, SMPDC Paper 03 — Redundant Information Flow and Primary Node Reconciliation, v0.1, 2026-10-16。Canonical source：SMPDC_Paper03_Redundant_Information_Flow_and_Primary_Node_Reconciliation_v0.1_2026-10-16.md。
• [I4] Neo.K × Aletheia, SMPDC Paper 04 — Speculative Execution and Deterministic Commit, v0.1, 2026-10-16。Canonical source：SMPDC_Paper04_Speculative_Execution_and_Deterministic_Commit_v0.1_2026-10-16.md。
• [I5] Neo.K × Aletheia, SMPDC Paper 05 — Persistent Diffusive Instruction Set and Executable Semantics, v0.1, 2026-10-16。Canonical source：SMPDC_Paper05_Persistent_Diffusive_Instruction_Set_and_Executable_Semantics_v0.1_2026-10-16.md。

先前雲端研究與相位／計算理論

• [I6] Neo.K, 群星模型：基於宇宙星系概念的 AI 模型設計方法論；群星架構在計算機系統中的應用與改良計畫。
• [I7] Neo.K, 相位計算機理論 v0.1，https://unboundedaxiom.org/p/lm-001850/。
• [I8] Neo.K × Aletheia, GCCFT Paper 06：從 Scheduler 到 Coupled Computation Planner；GCCFT Paper 02：計算相位與耦合激活。
• [I9] Neo.K, GCCWT Paper 04：計算場與資源激發，https://unboundedaxiom.org/p/lm-004846/。
• [I10] EveMissLab, GCM Phase C — AI-assisted Compute Orchestrator Engineering Blueprint v0.1。

外部研究與官方工程文件（研究查核：2026-10-16）

• [E1] LLVM／MLIR, Dialect Conversion, https://mlir.llvm.org/docs/DialectConversion/。對照合法化、全量／部分轉換、type converter 和 conversion target。
• [E2] LLVM／MLIR, Side Effects & Speculation, https://mlir.llvm.org/docs/Rationale/SideEffectsAndSpeculation/。對照對有副作用操作的移動、重排與 speculative optimization 限制。
• [E3] LLVM／MLIR, GPU Dialect, https://mlir.llvm.org/docs/Dialects/GPU/。對照設備端 async dependencies、buffer lifetime 與 kernel 生成語義。
• [E4] LLVM／MLIR, LLVM IR Target, https://mlir.llvm.org/docs/TargetLLVMIR/。對照 dialect 降階至 LLVM IR 的現有兩階段工程路徑。
• [E5] LLVM／MLIR, Async Dialect, https://mlir.llvm.org/docs/Dialects/AsyncDialect/；NVIDIA, CUDA Programming Guide — CUDA Graphs, https://docs.nvidia.com/cuda/cuda-programming-guide/04-special-topics/cuda-graphs.html。
• [E6] LLVM, LLVM Language Reference Manual, https://llvm.org/docs/LangRef.html。對照 concurrency、happens-before、atomic memory ordering。
• [E7] Rust Project, The Rust Programming Language — Understanding Ownership, https://doc.rust-lang.org/book/ch04-01-what-is-ownership.html。對照 move、borrow 和非可複製資源的語言基底。
• [E8] Chris Richardson, Transactional Outbox Pattern, https://microservices.io/patterns/data/transactional-outbox。對照狀態更新與外部訊息投遞之間的可靠性與去重義務。
• [E9] Verus Project, Verified Rust for Low-Level Systems Code, https://github.com/verus-lang/verus。可用於考察低層原子／資源管理的機器可檢查規格。
• [E10] Gilles Kahn (1974), The Semantics of a Simple Language for Parallel Programming, IFIP Congress proceedings。早期程序網絡及具決定性資料流語義的學術先例；本篇未額外宣稱其網頁連結或版本已獨立查驗。
• [E11] Jeffrey Dean and Luiz André Barroso (2013), The Tail at Scale, Communications of the ACM 56(2), 74–80, DOI: 10.1145/2408776.2408794, https://research.google/pubs/the-tail-at-scale/。
• [E12] E. W. Dijkstra and C. S. Scholten (1980), Termination Detection for Diffusing Computations, Information Processing Letters 11(1), 1–4, DOI: 10.1016/0020-0190(80)90021-6, https://research.tue.nl/en/publications/termination-detection-for-diffusing-computations/。
• [E13] Hal Berenson et al. (1995), A Critique of ANSI SQL Isolation Levels, SIGMOD proceedings。用於對照 snapshot／weak isolation 下 write skew 一類交易異常；此處只作歷史研究指向，不宣稱已完成形式化證明。
• [E14] Carl Hewitt, Peter Bishop and Richard Steiger (1973), A Universal Modular Actor Formalism for Artificial Intelligence, IJCAI proceedings。Actor 系統的經典研究先例；本篇不將其重新命名為 SMPDC 首創。

原創性、引用與證據說明

本研究源自 Neo.K 對群星式主要工作流、相位耦合、冗餘資訊流及連續擴散指令的提出，並由本篇進一步組織為可供實作及否證的候選程式語言與編譯器契約。MLIR、LLVM、Rust、資料流、Actor、分散式交易、尾端延遲與形式工具均已有獨立發展的成熟成果；本文不得將其聲稱為 SMPDC 的獨家首創。所有未經實測的安全與效能命題均維持明確的前提與研究成熟度標示。聊天渲染畫面不是本篇的正式數學原稿；可下載 UTF-8 Markdown 檔案才是 canonical research artifact。