videospeed 控制器可见性契约：分层状态机、渲染优先级与 TLA+ 形式化验证-平芜编程栈

前端
音视频

【免费下载链接】videospeed

HTML5 video speed controller (for Google Chrome)

项目地址：https://gitcode.com/gh_mirrors/vi/videospeed

videospeed（HTML5 video speed controller for Google Chrome）的控制器可见性（Controller Visibility）不是"一个布尔值"或"一个粘性 CSS 类"，而是一套由用户意图、媒体状态、站点自动隐藏、瞬时反馈、不可用媒体、外部宿主 CSS 与控制器生命周期七类独立输入共同作用的分层状态机，且每一项都有显式的优先级。本文以仓库文档 docs/controller-visibility.md 为主线，结合 src/core/controller-visibility.js 的纯策略实现、specs/ControllerVisibility.tla 的 TLA+ 模型以及四层可执行验证，完整讲解可见性契约的状态定义、渲染优先级公式、用户切换转换、反馈与生命周期语义，并给出面向开发者的变更检查清单。读完本文，你将掌握"一次显示动作如何从渲染态采样出正确意图""广播与定向动作为何能各自独立过渡"以及"如何为一次可见性改动补齐模型、差分测试与 Chrome 矩阵"的完整方法论。

为什么可见性不能是"一个布尔值"

控制器可见性契约的出发点是一条硬性设计原则：可见性是分层状态机，它不是一个布尔值，也绝不能被实现成单个粘性 CSS 类。原因在于，同一个控制器在某一时刻的"可见/隐藏"由彼此独立的输入共同决定：

用户通过键盘或弹窗发出的显式覆盖意图（AUTO/SHOW/HIDE）；
来自startHidden设置、媒体可见性与音频控制器启用的自动层；
站点自有的自动隐藏（如 YouTube 的.ytp-autohide）；
临时性的视频反馈与持久性的音频反馈；
无媒体源（no-source）与外部宿主隐藏（host CSS）；
定向的与文档级（广播）的显示动作；
定时器到期与控制器销毁（release）。

如果只用一个布尔位或一个类去承载这些语义，任何一个输入的变化都会"踩踏"其它输入，用户显式SHOW会被站点自动隐藏悄悄夺走、过期的反馈类又可能让一个已被显式HIDE的控制器重新浮出水面。契约要求这些输入以明确的优先级组合成最终的渲染结果，且每个输入只影响自己所属的渲染层。

生产策略的唯一实现是 src/core/controller-visibility.js，其机器可检查的模型是 specs/ControllerVisibility.tla，DOM 与 CSS 一致性由 tests/integration/controller-visibility-differential.test.js 与 tests/e2e/display-toggle.e2e.js 双重把关。

契约范围（Scope）

契约明确覆盖以下内容：

每个控制器恰好一个显式覆盖：AUTO、SHOW或HIDE；
来自startHidden、媒体可见性与音频控制器启用的自动可见性；
站点自有自动隐藏，如 YouTube 的.ytp-autohide；
临时视频反馈（有界定时器）与持久音频反馈（无定时器）；
无媒体源隐藏与外部宿主隐藏；
定向与文档级（广播）显示动作；
定时器到期与控制器销毁。

同时契约划定了明确的边界：显式SHOW/HIDE意图在其控制器整个生命周期内保持有效；跨刷新持久化、跨 frame 同步、以及与页面脚本共享所有权都不属于本契约。文档特别强调：任何把这些能力加进来的改动都会改变并发模型，必须同时重新审视 TLA+ 状态空间与 DOM 适配器。

状态模型：九类状态的分层

契约把可见性状态抽象为一张对照表，每个概念在纯模型、TLA+ 模型与 DOM/适配器三层各有对应：

概念	纯模型	TLA+	DOM/适配器
生命周期	`attached`	`attached[i]`	`video.vsc`、已连接的`<vsc-controller>`、`StateManager`成员关系
用户意图	`override`	`overrideMode[i]`	无`data-vsc-visibility`属性，或`show`/`hide`
自动层	`automaticHidden`	`automaticHidden[i]`	宿主上的`vsc-hidden`类
不可用媒体	`noSource`	`noSource[i]`	`vsc-nosource`类
站点自动隐藏	`siteAutohide`	`siteAutohide[i]`	按域名作用域的宿主 CSS，观察页面自有状态如`.ytp-autohide`
外部宿主隐藏	`hostHidden`	`hostHidden[i]`	`<vsc-controller>`上计算出的`display`/`visibility`
反馈	`flash`	`flashMode[i]`	`vsc-show`类加可选的`flashTimer`
偏好设置	`startHidden`	`startHidden`	实时设置值，供未来的自动显示与反馈事件查阅
媒体种类	`mediaType`	`AudioControllers`	媒体标签名

startHidden：初始化自动层，但不是永久硬隐藏位

startHidden只负责初始化自动层，它本身不是一个永久性的硬隐藏位。对startHidden的实时修改是非追溯的（non-retroactive）：

它不会立即重写一个已存在的控制器；
它不会取消正在进行的反馈（flash）；
它只阻止未来的自动显示（AUTOMATIC_SHOW）与反馈请求，直到被重新关闭。

这一点在 src/core/controller-visibility.js 中由allowsFlash与step的AUTOMATIC_SHOW分支落实：allowsFlash只在startHidden为 false 时放行反馈请求，而SET_START_HIDDEN事件只改startHidden字段本身，不触碰automaticHidden与flash（见step中SET_START_HIDDEN分支）。单元测试tests/unit/core/controller-visibility.test.js中的 "treats startHidden changes as non-retroactive but blocks automatic show" 与 "blocks new flash under startHidden or explicit HIDE without retroactive cancellation" 两条用例正是对这一语义的逐点校验。

normalizeOverride：抵御伪造值

纯模型对覆盖值做了防御性归一化：normalizeOverride只承认三个声明值（auto/show/hide），把缺失的或页面伪造的任何其它值一律归为AUTO。注释明确指出这样做的原因：避免产生"第四个状态"，因为 CSS 层与形式化模型都不认识它。单元测试 "normalizes only the three declared override values" 覆盖了undefined与'forged'两种输入。

渲染优先级：唯一真相公式

对于任一控制器i，最终渲染结果由如下递推公式决定（这也是 src/core/controller-visibility.js 中isVisible的逐行对应实现）：

hardHidden = !attached || hostHidden || noSource || override == HIDE forcedShown = override == SHOW || flash != NONE visible = !hardHidden && (forcedShown || (!automaticHidden && !siteAutohide))

等效的优先级表述，从高到低：

external host hide / no source / FORCE_HIDE > FORCE_SHOW / flash > automatic hide / site autohide

几个必须注意的语义细节：

SHOW故意压过vsc-hidden与站点自动隐藏，但它不能复活一个已销毁的控制器、让不可用媒体变得可用、或击败页面 CSS 对 light-DOM 宿主本身的隐藏。
HIDE可以击败一个过期残留的 flash 类——这是hardHidden中override == HIDE置于最高层的原因。
opacity 被排除在离散可见性谓词之外：因为淡入淡出（fade）会途经 0，而采样需要离散状态。因此采样只看宿主与 shadow 控制器上计算后的display与visibility。

单元测试通过枚举全部有效状态断言isVisible与独立预期的expectedVisible完全一致（详见后文"可执行验证层次"）。差分集成测试则把hostHidden映射为controller.div.style.display === 'none'、把siteAutohide映射为容器上的ytp-autohide类，在真实 DOM 适配器上验证同一套优先级（见 tests/integration/controller-visibility-differential.test.js 的pipelineState与createWorld）。

CSS 侧的落地：shadow 选择器与 light-DOM 宿主规则

优先级在 CSS 层由两套机制共同实现：

shadow 内部规则（src/ui/shadow-dom.js 中createShadowDOM内嵌的样式）：
- :host(.vsc-hidden) #controller→ 隐藏（自动层，不扰动任何显式覆盖）；
- :host([data-vsc-visibility="show"]) #controller, :host(.vsc-show) #controller→ 强制显示（显式 SHOW 与瞬时反馈同权，压过startHidden、媒体可见性与站点自动隐藏）；
- :host([data-vsc-visibility="hide"]) #controller, :host(.vsc-nosource) #controller→ 最终隐藏（flash 与用户 SHOW 都不得揭示它们）。
light-DOM 宿主规则：站点自动隐藏等由域名作用域的宿主 CSS 处理，基础规则位于 src/styles/inject.css（manifest 加载、先于任何 JS），站点特定覆盖位于 src/styles/controller-css-defaults.js。

YouTube 站点自动隐藏的落地方式

文档明确指出 YouTube 站点自动隐藏的实现原则：用域名作用域的 light-DOM CSS 作用在<vsc-controller>上，而不是把页面状态复制进扩展自有的 DOM，更不依赖已被废弃的:host-context()选择器。

src/styles/controller-css-defaults.js 中对应的生产规则为：

:root[style*='--vsc-domain: "youtube.com"'] .ytp-autohide vsc-controller:not([data-vsc-visibility="show"]):not(.vsc-show) { visibility: hidden !important; opacity: 0 !important; transition: opacity 0.25s cubic-bezier(0.4, 0, 0.2, 1); }

其设计要点：

该规则用:root[style*='--vsc-domain: "DOMAIN"']语法按域名包裹，注入阶段会把匹配域名的选择器剥掉（规则无条件生效），不匹配的则替换为永不匹配的[data-vsc-never]；--vsc-domain变量并不会真正设置在:root上（模块头部注释）。这样 YouTube 的.ytp-autohide祖先类永远不会让非 YouTube 站点为无关逻辑付出匹配成本。
宿主规则通过:not([data-vsc-visibility="show"]):not(.vsc-show)排除显式SHOW与vsc-show反馈之后，才应用visibility: hidden；而 shadow 内部选择器继续维护自动隐藏、显式HIDE与 no-source 的最终优先级（youtube-nocookie.com 有一份完全相同的复制块）。
文档特别警告：改动任何一侧（light-DOM 规则或 shadow 规则）都必须跑 Chrome 矩阵测试，而不是只跑单元测试——jsdom 无法复现宿主与 shadow 的完整级联。

用户切换转换：先采样渲染态，再决定意图

显示动作（display action）的核心规则是：在取消反馈之前先采样当前渲染态。转换关系如下：

当前覆盖	动作前渲染态	下一个覆盖	动作后反馈
`AUTO`	可见	`HIDE`	none
`AUTO`	隐藏	`SHOW`	none
`SHOW`	任意	`HIDE`	none
`HIDE`	任意	`SHOW`	none

行为语义是：

第一次按键反对用户当前所见：AUTO + 站点自动隐藏 + flash时，控制器实际上可见，动作必须选择HIDE而非SHOW——这解释了"采样先于清除vsc-show"为何对第一次按键至关重要。
后续按键在持久的SHOW/HIDE意图间交替，这样播放器自动隐藏无法静默夺回控制权；
AUTO只在控制器被销毁并创建全新控制器时才会重新进入——显式意图一旦离开AUTO，在 release 之前不能返回（这正是 TLA+ 属性ManualIntentPersistsUntilRelease的表述）。

在纯模型中，nextOverride是一个纯函数：对SHOW返回HIDE，对HIDE返回SHOW；对AUTO则要求传入renderedVisible布尔值（否则抛TypeError），返回其反相。单元测试 "maps toggle %s with rendered=%s to %s" 六种组合逐一验证了该映射。

广播动作与定向动作：各自独立采样

键盘与弹窗的显示动作是文档级广播，作用于每一个已挂载控制器；每个控制器独立采样自己的第一次转换。因此同一次广播可能在一个可见控制器上产生HIDE、在另一个隐藏控制器上产生SHOW；后续广播则让这些控制器以相反的相位交替。定向（targeted）适配器动作只影响它所属的控制器；已销毁的控制器不在广播范围之内，也不可能被一个过期定时器改写。

E2E 测试在双视频 fixture（dual-video.html）上验证了这一语义：预置 video1 为automaticHidden + flash（渲染可见）、video2 为automaticHidden（渲染隐藏），一次v键广播后 video1 变HIDE、video2 变SHOW，第二次广播则各自反向交替（见 tests/e2e/display-toggle.e2e.js 的 "broadcast independently flips rendered state" 与 "broadcast independently alternates persistent intent"）；随后用executeAction('display', 0, media, null)验证定向动作只改变目标控制器，以及 release 后控制器不再参与广播。

适配器侧如何采样

src/core/action-handler.js 的toggleControllerVisibility演示了采样时序：先normalizeOverride读取宿主data-vsc-visibility，当覆盖为AUTO时才调用isControllerVisible采样（因为只有从AUTO出发才需要渲染态参数）；isControllerVisible分别getComputedStyle宿主与 shadow 内层控制器，要求二者的display !== 'none'且visibility !== 'hidden'才判定可见。这样站点 CSS 始终是自动隐藏真相的唯一来源，而 opacity 因淡入淡出经过零值被刻意排除。

自动、反馈与生命周期转换

契约对这些转换逐一规定了精确语义：

自动隐藏只设置automaticHidden，不改覆盖、不动反馈；
自动显示仅当startHidden为 false 时才清除automaticHidden；
媒体源、站点自动隐藏、外部宿主变化只影响各自所属的渲染层；
视频反馈（被允许时）进入TIMED_ARMED；定时器推进进入TIMED_DUE；到期返回NONE。重复请求会重新武装定时器（re-arm）；
音频反馈（被允许时）进入PERSISTENT：没有定时器，一直持续到一次显示切换或 release；
startHidden与显式HIDE会阻止新的反馈请求；已存在的反馈在之后实时把startHidden改为 true 时仍然存活并正常到期；
Release 对抽象控制器原子地清除覆盖与反馈、取消生产环境的定时器、移除StateManager成员关系、断开video.vsc、并移除宿主。Release 对该控制器身份是终结性的；此后控制同一媒体的行为属于用当前输入重新初始化的全新控制器。

在 src/core/controller-visibility.js 中，FLASH_REQUEST分支按mediaType区分：视频进TIMED_ARMED，音频进PERSISTENT；TIMER_TICK只在TIMED_ARMED时推进到TIMED_DUE；FLASH_EXPIRE只在TIMED_DUE时回到NONE。assertState则从不变式层面拒绝非法组合：音频不能携带定时反馈（TIMED_ARMED/TIMED_DUE）、视频不能携带PERSISTENT、显式HIDE不能与任何反馈共存、已销毁控制器必须是AUTO且无反馈。单元测试 "models timed video flash and persistent audio flash" 用视频的三段推进与音频对TIMER_TICK/FLASH_EXPIRE的免疫验证了这条媒体相关语义。

形式化模型：TLA+ 双控制器

specs/ControllerVisibility.tla 使用两个控制器（一个视频、一个音频）来建模：因为键盘/弹窗显示命令是文档级广播，模型必须同时检查局部非干扰与独立的广播转换。模型探索的动作空间包括：局部切换、广播切换、自动与环境变化、实时startHidden变化、反馈请求、有界定时器推进、到期与 release。

StopTimerRefresh是一个辅助环境动作：无论它是否发生，安全性检查都成立；而它的 false 状态标记了一段"不再有视频反馈请求重新武装定时器"的后缀——这是让"最终清除"成为一条显式、非空（non-vacuous）的活性性质的关键（对应属性TimedFlashEventuallyClearsAfterRefreshStops）。

TLC 检查的属性

类型与媒体特定的反馈不变式（TypeOK、FlashMatchesMediaType）；
显式HIDE与反馈互斥（HideHasNoFlash）；
已销毁控制器的惰性（DetachedControllerIsInert、VisibleImpliesAttached）；
定向动作的局部性与广播独立性（LocalActionsAreLocal、ToggleOneContract、ToggleAllContract）；
渲染感知的第一次切换与后续显式SHOW/HIDE交替（StickyToggleIntentContract）；
环境与设置不干扰用户意图（EnvironmentPreservesIntent、StartHiddenSettingIsNonRetroactive）；
意图只通过切换或 release 改变，且显式意图在 release 之前不能返回AUTO（IntentChangesOnlyByToggleOrRelease、ManualIntentPersistsUntilRelease）；
已武装/已到期的视频定时器阶段的弱公平最终推进（ArmedFlashEventuallyAdvances、DueFlashEventuallyHandled，对应规格中的WF_vars）；
环境停止重新武装定时器后，视频反馈最终清除或 release（TimedFlashEventuallyClearsAfterRefreshStops）。

文档还澄清了两类属性的边界：HardHideDominates、ForceShowDominatesAutomatic、FlashDominatesAutomatic、AutoLayerIsExact这些硬隐藏/强制显示/反馈/自动层优先级属性，都是对派生谓词Visible的一致性引理（consistency lemmas）——它们让渲染定义可审阅，但不是独立的转换安全性证明：把定义代入后它们会变成同义反复（tautology）。真正的独立检查是Chrome 矩阵，它验证真实样式表确实精化了该谓词。

此外，有界定时器建模的是次序与最终推进，而不是墙钟毫秒数；CSS 选择器、计算样式、DOM 连接、JavaScript 定时器所有权与事件派发都属于适配器关注点，刻意放在 TLA+ 之外验证。

可执行验证层次：四层答案不同的问题

契约给出了四个验证层次，各自回答不同的问题：

npm run test:tlc穷尽检查双控制器的时态模型。当前配置达到49,152 个不同状态、生成724,800 个状态，并检查三条非空的视频定时器活性分支（脚本入口 scripts/tlc.mjs）。
tests/unit/core/controller-visibility.test.js枚举448 个有效局部状态（2 种媒体 × 各自合法的 flash 集合 × 2 的 5 次方布尔组合 × 3 覆盖，扣除不合法组合）与6,720 个状态/事件对，对纯 JavaScript 转换策略做穷尽断言。
tests/integration/controller-visibility-differential.test.js用同一事件流同时驱动纯模型与真实的ActionHandler/VideoController适配器（一个视频控制器 + 一个真实<audio>控制器），回放局部与广播动作、视频与音频反馈、环境变化、实时设置、到期与 release，每个操作后都断言适配器管线状态与纯模型逐字段相等。
tests/e2e/display-toggle.e2e.js在真实 Chrome 中检查文档与 shadow 的完整级联：对3 overrides × 2 automaticHidden × 2 siteAutohide × 2 flash × 2 noSource × 2 hostHidden = 96种渲染组合逐一断言（测试在注入的临时样式表上只关闭 transition 以消除过渡时序干扰，生产选择器级联本身仍是测试对象），随后验证混合双控制器的局部、广播、flash 采样与 release 行为。

文档给出的结论是严格的互补关系：TLA+ 跑绿不能证明 CSS 源码顺序正确；浏览器矩阵跑绿也不能证明定时器活性或跨所有动作序列的非干扰。两者都是本契约改动的必要条件（对应脚本见 package.json 的test:tlc、test:e2e与前置发布链路prerelease）。

变更检查清单

任何可见性改动都必须满足以下六步，缺一不可：

说明哪一条转换或优先级规则发生了变化；
更新 src/core/controller-visibility.js 及其有界 JavaScript 测试；
当抽象状态、动作字母表、安全不变式或活性期望变化时，更新 specs/ControllerVisibility.tla；
当 DOM 类、属性、定时器所有权、派发作用域或生命周期映射变化时，更新差分适配器测试；
当选择器、宿主渲染或级联优先级变化时，更新 Chrome 矩阵；
依次运行npm test、npm run test:tlc、npm run build与node tests/e2e/run-e2e.js display。

最后还有两条红线式的实现边界：

不得改写页面自有的<html>或<body>来持久化 VSC 状态；data-vsc-visibility只允许出现在扩展自有的<vsc-controller>宿主上；
站点自有的祖先状态只允许通过计算样式观察，核心可见性逻辑绝不能复制站点的自动隐藏状态机——那是站点自己的领域。

结语

videospeed 的控制器可见性契约演示了一种把"显示/隐藏"从临时 CSS 修补提升到工程规范的路径：以七类独立输入构建分层状态机，用一份显式的优先级公式统一纯模型、TLA+ 与 DOM 适配器三方的"可见"定义，再通过穷举单元测试、差分回放与 Chrome 渲染矩阵从不同侧面互相补足。对于希望在浏览器扩展中可靠实现播放器控制显隐、抵御站点自动隐藏干扰、或为状态机引入形式化验证的开发者，本仓库的这份契约文档连同 specs/ControllerVisibility.tla 与 tests/e2e/display-toggle.e2e.js 是一份可以直接参照的完整范本。