Operator-Native RDSS：Bounded Backtracking Equivalence 與 Cause-Sensitive Verification

Runtime Verification Grades between HP and Full HHP

版本： v0.14 Working Verification Draft
日期： 2026-08-10
作者：Neo.K
機構：EveMissLab／一言諾科技有限公司
定位： ON-RDSS Branch Quotient 的 bounded-backtracking Runtime approximation／Cause-Sensitive HHP 接口
前置： ON-RDSS v0.11–v0.13

摘要

v0.13 已完成經典：

\boxed{ HP=true,\qquad HHP=false }

regression，並驗證：

plain HP forward checker；
explicit backward HHP checker；
hereditary downward-closure HHP checker；

能在同一有限 benchmark 上正確分離 HP 與 HHP。

本版進一步建立：

\boxed{ BHHP_k }

作為 ON-RDSS Runtime 的有限 backtracking verification grade。

本版採用保守命名：

ON-RDSS BHHP $_k$ 是受到 bounded-backtracking HP/HHP hierarchy 啟發的 Runtime approximation。

在尚未逐條形式對照 Fröschle–Hildebrandt 1999 原始 indexing 前，不宣稱本版 $BHHP_k$ 與該論文 bounded bisimulation 的定義完全相同。

第一代定義：

\boxed{ BHHP_0=HP. }

而：

BHHP_{k+1}

在保持 current-level forward matching 的同時，要求所有沿當前 history mapping 的一階 backward move 必須落入：

BHHP_k.

因此：

\boxed{ BHHP_{k+1}\subseteq BHHP_k. }

在經典 HP-not-HHP regression 上，checker 得到：

\boxed{ BHHP_0=true, }

但：

\boxed{ BHHP_1=false. }

所以該 fixture 只需一層 mapped backtracking 就已被區分。

1. 外部理論接口

Fröschle–Hildebrandt 研究 HP 與 HHP 之間的差異，並定義 bounded backtracking hierarchy。

其結果包括：

每個有限 bounded level 可判定；
hierarchy 是 strict；
所以不存在一個固定有限 bound 可一般替代 full HHP。

因此 ON-RDSS 不應把：

BHHP_1

或任一固定：

BHHP_k

誤稱為 full HHP。

2. Runtime 為什麼仍需要有限 $k$ ？

Full HHP 的強度適合：

formal folding；
irreversible StateMerge；
governance-critical quotient；
offline proof。

但即時 Runtime 常需要：

bounded cost；
local decision；
incremental revalidation；
budget-aware verification。

所以定義：

\boxed{ VerificationGrade = BHHP_k. }

它不是「比較不真的等價」，而是：

在最多 $k$ 層 mapped historical rollback obligation 下通過驗證。

3. Base Level

令：

R_0 = R_{HP}^{\ast}.

也就是所有滿足：

history/profile isomorphism；
forward-left matching；
forward-right matching；

的 greatest fixed point。

因此：

\boxed{ BHHP_0=HP. }

4. Recursive Level

假設：

R_k

已定義。

$R_{k+1}$ 先限制於：

R_k,

再要求：

Forward

所有 forward extensions 在：

R_{k+1}

內互相匹配。

Backward-left

若：

(C_1,f,C_2)\in R_{k+1}

且：

C_1\xleftarrow{e_1}C_1',

令：

e_2=f(e_1).

必須：

C_2\xleftarrow{e_2}C_2'

並：

\boxed{ (C_1',f|_{C_1'},C_2')\in R_k. }

Backward-right

對稱成立。

5. 為什麼 Backward Target 是 $R_k$ ？

這使：

R_{k+1}

比：

R_k

多承擔一層不可重新映射的歷史 obligation。

直覺：

BHHP_0

只看 forward。

BHHP_1

問：

如果現在退一步，原 mapping 還站得住嗎？

BHHP_2

再問：

退一步後的 relation 本身，還能再退一步嗎？

依此類推。

6. Monotonicity Candidate

由構造：

\boxed{ R_{k+1}\subseteq R_k. }

所以安全強度單調增加：

\boxed{ BHHP_0 \succeq BHHP_1 \succeq BHHP_2 \succeq \cdots }

此處 $\succeq$ 表示「前者等價關係較粗」。

7. Full HHP 的位置

理想極限：

\boxed{ R_\infty = \bigcap_{k\ge0}R_k. }

是否對本定義在一般所選模型類中恰等於 standard HHP，需要另行形式證明。

目前只將：

FullHHP

保留為獨立 exact checker。

所以：

\boxed{ BHHP_k \neq FullHHP }

除非另有證書。

8. 經典 Fixture

沿用 v0.13：

A= ((a+c)\parallel b) + (a\parallel b) + (a\parallel(b+c)),

B= ((a+c)\parallel b) + (a\parallel(b+c)).

已知：

HP(A,B)=true,

HHP(A,B)=false.

9. $BHHP_0$

Checker：

\boxed{ BHHP_0(A,B)=true. }

relation size：

\boxed{ |R_0|=17. }

10. $BHHP_1$

加入一層 mapped backward obligation 後：

\boxed{ BHHP_1(A,B)=false. }

relation size：

\boxed{ |R_1|=10. }

所以該 fixture 的最低分離層：

\boxed{ k_{\min}=1. }

11. 更深層 Relation Size

Checker 得：

|R_0|=17,

|R_1|=10,

|R_2|=4,

|R_3|=0.

之後維持：

0.

驗證：

\boxed{ |R_{k+1}| \le |R_k|. }

12. 這不代表一層 Backtracking 永遠足夠

原 bounded-backtracking literature 證明 hierarchy strict。

所以必然存在更複雜系統，使：

BHHP_1

不足、

需要更深 historical challenge。

因此經典 fixture 只是：

\boxed{ \text{cheap but meaningful regression}. }

不是 hierarchy collapse 的證據。

13. Runtime Verification Grade

建議正式定義：

\boxed{ VG \in \{ Obs, Future, HP, BHHP_1, BHHP_2, \ldots, FullHHP, FullHHP+Gov \}. }

14. Verification Certificate

\boxed{ VQCert = ( Mode, k, Scope, SnapshotVersion, RelationHash, CheckerVersion, ProfileRegime, AuthorityRegime, ResidualRegime ). }

若：

Mode=BHHP,

則必須明示：

k.

15. 不能把 $BHHP_k$ 通過寫成 Full HHP

例如：

BHHP_2(C_1,C_2)=true

只能輸出：

\boxed{ CertifiedEquivalent[ Grade=BHHP_2 ]. }

不能輸出：

HHP=true.

16. Stronger Check Residual

如果 Runtime budget 到：

k=2

就停止，

可以輸出：

\boxed{ Residual[ StrongerHistoryEquivalenceUnchecked( CurrentGrade=BHHP_2 ) ]. }

這符合 ON-RDSS explicit residual semantics。

17. Verification Budget

定義：

\boxed{ VB = ( Grade, MaxBacktrack, Scope, TimeBudget, MemoryBudget, CertificateLevel ). }

例如：

UI state grouping

VB=(HP,0,local,low).

planner cache merge

VB=(BHHP_1,1,local,medium).

governance state merge

VB=(FullHHP,\infty,affected-subgraph,high).

18. Adaptive Verification

可以先：

HP.

若 parent state 後續要：

write；
commit；
delete；
schema change；

才逐步提升：

HP \to BHHP_1 \to BHHP_2 \to FullHHP.

因此 verification strength 可以按 decision risk 動態加碼。

19. 不同 Grade 的 State Identity

Parent-state registry 可寫：

\boxed{ StateIdentity = ( ClassID, Q, Version, Grade, CertID ). }

因此：

SameClassID

但：

Grade=HP

與：

Grade=HHP

仍是不同 verification claims。

20. Meta 造成 Grade 失效

若：

\mathfrak E_v \to \mathfrak E_{v+1},

原：

BHHP_k^v

certificate 應標：

Stale.

然後重新驗證：

BHHP_k^{v+1}.

Meta 不可直接繼承舊 relation。

21. Cause-Sensitive HHP 的資料接口

v0.12：

\widehat C = (C,\pi,\le_\pi,v).

因此 bounded checker 未來應由：

(C_1,f,C_2)

升級成：

\boxed{ ( \widehat C_1, f_r, \widehat C_2 ). }

22. Causal Realization

每次具體 event occurrence：

\boxed{ \widetilde e = (e,\kappa,v). }

其中：

$e$ ：surface event；
$\kappa$ ：chosen enabling witness；
$v$ ：semantics version。

23. Cause-Sensitive Forward Move

\widehat C \xrightarrow{\widetilde e} \widehat C'.

若：

\widetilde e_1

要匹配：

\widetilde e_2,

至少要求：

Profile(e_1)=Profile(e_2)

並且 chosen causes 在現有 mapping 下對應：

\boxed{ f_r(\kappa_1) \simeq \kappa_2. }

24. Cause-Sensitive Backward Move

只有 concrete causal history 中 maximal occurrence 可回退：

\boxed{ \widehat C \xleftarrow{\widetilde e} \widehat C'. }

另一邊必須回退：

f_r(\widetilde e).

不能只找任意：

q(\widetilde e') = q(\widetilde e).

25. Surface HHP 與 Cause-Sensitive HHP

定義：

\boxed{ SurfaceHHP }

只保存 surface event identity / history。

而：

\boxed{ CauseHHP }

保存 causal realization：

(e,\kappa,v).

一般：

\boxed{ CauseHHP \Rightarrow SurfaceHHP }

但反向不應預設成立。

26. ForgetCause Certificate

若想把：

CauseHHP

降為：

SurfaceHHP,

需要：

\boxed{ ForgetCauseCert. }

也就是所有 task-relevant causal realizations在 quotient scope 中可被安全商掉。

27. Cause-Sensitive $BHHP_k$

自然定義：

\boxed{ CBHHP_k }

其中：

CBHHP_0 = \text{cause-sensitive forward HP},

而每增加一層：

k+1

都要求沿：

f_r

回退一個 concrete causal realization後落入：

CBHHP_k.

28. Verification Grade 二維化

因此最終 Grade 不一定只是一條軸。

可以寫：

\boxed{ Grade = ( HistoryStrength, CauseMode ). }

其中：

HistoryStrength \in \{ HP, BHHP_k, HHP \},

CauseMode \in \{ Surface, CauseSensitive \}.

29. Grade 範例

(HP,Surface)

最便宜。

(BHHP_2,Surface)

加入有限 rollback。

(BHHP_2,CauseSensitive)

有限 rollback + 原因保真。

(HHP,CauseSensitive)

最強、最昂貴。

30. Governance 再成第三軸

若再加：

GovernanceMode \in \{ BehaviourOnly, Auth, Auth+Residual, FullGoverned \},

完整 Verification Grade：

\boxed{ VG = ( HistoryStrength, CauseMode, GovernanceMode ). }

這開始像真正可調 Runtime verification lattice。

31. Verification Lattice

不是一條單線：

HP<HHP.

而更像多軸偏序。

例如：

(BHHP_1,CauseSensitive)

與：

(BHHP_2,Surface)

未必可直接說誰「絕對更強」。

前者更保 cause，

後者更深 backtracking。

因此：

\boxed{ VerificationGrade }

應該是 partial order，而不是單一整數。

32. 這和 RDSS 的判定域吻合

驗證結果必須綁定：

\boxed{ Domain + Scope + Grade. }

不能離開判定域後說：

這兩個 states 就是同一個。

正確是：

在 $Q$ 、version $v$ 、grade $g$ 下，這兩個 histories 被證明可安全商化。

33. 下一步：Strict-Hierarchy Regression Family

既有文獻說 bounded hierarchy strict。

所以 ON-RDSS test suite 不應只有：

k_{\min}=1.

未來需要建立：

\boxed{ Fixture_k }

使：

BHHP_{k-1}=true,

BHHP_k=false.

至少做：

k=1,2,3

作 regression family。

34. 下一步：General CEES Checker

把 prime structure 的：

forward\_events, backward\_events

替換成 decorated history：

forward(\widehat C)

與：

backward(\widehat C).

然後直接重用：

BHHP_k

greatest-fixed-point engine。

35. 下一步：Certificate Cost Curve

記錄：

Cost(BHHP_k)

包括：

triple count；
mapping count；
fixed-point rounds；
memory；
elapsed time。

建立：

\boxed{ Strength \leftrightarrow VerificationCost. }

這會直接用於 Runtime adaptive verification。

36. 有限實驗結果

經典 fixture：

Grade	Initial Related	Relation Size
$BHHP_0$	Yes	17
$BHHP_1$	No	10
$BHHP_2$	No	4
$BHHP_3$	No	0

所以：

\boxed{ k_{\min}=1. }

而 relation size 單調下降。

37. 暫定結論

ON-RDSS 現在不必在：

HP

與：

FullHHP

之間二選一。

可以建立：

\boxed{ HP = BHHP_0 \supseteq BHHP_1 \supseteq BHHP_2 \supseteq \cdots }

作 Runtime 有限歷史驗證層。

同時，v0.12 的 causal realization 又提供第二條 verification axis：

\boxed{ Surface \to CauseSensitive. }

所以真正的 ON-RDSS verification grade 更像：

\boxed{ VG = ( BacktrackingDepth, CauseSensitivity, GovernanceStrength, Scope, Version ). }

這代表：

「這兩個 State 是否相同」不再只有 Yes/No，而是必須同時回答：在哪個觀測域、哪個版本、保留多少因果歷史、允許回退多深、是否保留具體原因、以及治理義務檢查到哪一層。

ON_RDSS_Bounded_Backtracking_CauseSensitive_Verification_v0.14