豫言 / 豫言操作系统隔离运行 @ 0.1.0

把已编译的文件式豫言程序放进 Dynamic Worker 隔离运行一次:无网络、无平台绑定、限算时,取回标准输出与约定目录的输出文件。

源码浏览已生成;不能解析的文件以纯文本展示,不表示通过类型检查。

规范.汉语.md

# 隔离运行接口规范 0.1.0

本包让应用把一个**已编译的文件式程序**放进与调用者完全隔离的执行环境里运行一次,取回它的标准输出、标准错误和约定目录下的输出文件。文件式程序是豫言编译器面向文件式宿主(浏览器编译器宿主、Node 宿主)产出的 WasmGC 程序:它读写**内存文件系统**、用命令行参数与标准输出,不认识网络、平台绑定或操作系统。云工作台用它运行用户站点的程序;任何“运行不可信的、由用户或工具编译的豫言程序”的应用都可以用它。这是云工专用能力,使用 Worker Loader 绑定,需要在应用许可里授权 `LOADER` 绑定名。

## 函数

`运行隔离程序 运行器名 范围 产物摘要 程序 输入`,返回字符串。

| 参数 | 含义 |
| --- | --- |
| 运行器名 | 应用许可 `LOADER` 列表里授权的绑定名;未授权抛出豫言异常 |
| 范围 | 隔离缓存分区名,1 至 128 字节,不得含控制字符。同一(范围,产物摘要,宿主资源版本)的运行可复用同一隔离体;不同范围永不共用。云工宿主的运行资源(子入口与内存文件系统宿主)随构建固定,同一次部署里版本不变,所以隔离体标识就是“范围:产物摘要” |
| 产物摘要 | 解码后程序字节的 SHA-256,64 位小写十六进制。宿主运行前重算并比较,不符抛出「运行产物摘要不匹配」(防存储损坏或被替换) |
| 程序 | 编译产物的 Base64 文字(标准字母表,宽容 ASCII 空白与缺省填充,同 JS 的 `atob`),长度 1 至 4194304 个字符(解码后至多 3145728 字节),解码后必须是有效 Wasm。用 Base64 是因为产物总以 JSON 文字保存与传递 |
| 输入 | JSON 文字,至多 1572864 字节:`{"args":[…字符串],"files":{"路径":"文字"}}`。`args` 缺省为空数组,须是字符串数组;`files` 缺省为空对象,值须是字符串,路径按 `/` 规范化(去 `.`、折叠 `..`、补前导 `/`) |

## 运行环境

- 每次运行都是**全新的程序实例与全新的内存文件系统**,运行之间不保留任何状态;相同(范围,摘要,宿主资源版本)只共用已编译的模块,不共用数据。持久数据须由调用者放进输入的 `files`,再从输出的 `files` 取回。
- 无网络出站、无平台绑定、无环境变量、子请求数为 0;CPU 限额 1000 毫秒(宿主可降低,不得提高);标准输出与标准错误合计至多 64 KiB,超过则程序失败(`ok` 为假,带 `error`)。
- **算时的强制者是平台**:超过 CPU 限额时平台终止隔离体,调用者得到失败而不是程序返回值,`运行隔离程序` 抛出「隔离运行失败:…」。宿主的执行器另有 5 秒墙钟检查,但它只在程序回调宿主检查点时才起作用;当前编译器为文件式目标产出的程序不含检查点,所以死循环程序全靠平台的 CPU 限额终止。**本地 workerd 不强制 CPU 限额**(已验:死循环程序会一直占用 CPU 而不返回),本地验证与测试不得运行死循环程序。
- 标准输入为空;命令行程序名为 `/程序.wasm`,当前目录为 `/`。

## 返回

返回 JSON 文字:`{"ok":爻,"stdout":文字,"stderr":文字,"exitCode":整数,"files":{路径:文字},"error"?:文字}`。

- `ok`:程序以退出码 0 结束。`exitCode` 为程序的退出码;程序因运行错误(陷阱、输出超限、未捕获的豫言异常、宿主检查点超时)而终止时 `ok` 为假、`exitCode` 为 1,并带 `error` 说明(未捕获的豫言异常在宿主里表现为 `illegal cast`,输出超限为「输出超过 64 KB」)。程序失败是**返回值**,不是异常;已写入标准输出与标准错误的内容在 `stdout`、`stderr` 里照常返回(超限的那一次写入除外)。
- `files`:只含运行结束时内存文件系统里 `/数据/` 与 `/响应/` 开头的文件(输入里给出而程序没有改动的 `/数据/…` 文件也在其中),每个按严格 UTF-8 解码成文字;至多 256 个文件、合计至多 1048576 字节(按字节计),超限或某个文件不是有效 UTF-8,则整个运行判为接口失败(抛出豫言异常「隔离运行失败:500:…」)。其他路径(含输入里的 `/请求/…`)不会返回。
- 输入或程序违规(摘要不符、越限、`args` 类型错、非有效 Wasm)、运行器未授权、隔离体创建或调用失败,都抛出可捕获的豫言异常,消息说明原因(见下「失败情形」)。宿主失败一律走可捕获的异常,不得中止当前事件。

## 失败情形

| 情形 | 类别与消息 |
| --- | --- |
| 运行器名不是 1 至 128 字节;范围不是 1 至 128 字节或含控制字符;产物摘要不是 64 位小写十六进制;程序文字长度不在 1 至 4194304;输入超过 1572864 字节 | 违规,可捕获,消息依次为 `运行器名无效`、`隔离范围无效`、`产物摘要无效`、`运行产物无效`、`运行输入超过上限` |
| 程序文字不是有效 Base64 | 违规:`运行产物无效:不是有效的 Base64` |
| 解码后字节的 SHA-256 与产物摘要不符 | 违规:`运行产物摘要不匹配` |
| 运行器名不在应用许可的 `LOADER` 列表;绑定不存在;隔离体创建失败;解码后不是有效 Wasm;隔离体崩溃或超过平台限额 | 可捕获:`隔离运行失败:<原因>`(未授权时原因为 `未授权的LOADER绑定:<名>`,非有效 Wasm 时为 `动态 Worker 程序不是有效 Wasm`) |
| 输入不是有效 JSON,`args` 不是字符串数组,`files` 不是路径到文字的对象 | 违规:`隔离运行输入无效:<原因>` |
| 输出文件超过 256 个或合计超过 1048576 字节,或有文件不是有效 UTF-8 | 接口失败:`隔离运行失败:500:<原因>` |
| 程序自身失败(退出码非零、陷阱、未捕获的豫言异常、输出超过 64 KiB) | **不是异常**:返回值 `ok` 为假 |

## 一致性样例

设程序甲读取 `/请求/路径.txt`(不存在按空处理),写入 `/数据/记录.txt`、`/响应/正文.txt`、`/其他/密.txt` 各一行,并向标准输出打印一行“你好”。以输入 `{"args":["echo"],"files":{"/请求/路径.txt":"/x","/数据/旧.txt":"旧"}}` 运行:

- 返回 `ok` 为真、`exitCode` 为 0、`stdout` 为“你好”加换行;`files` 恰含 `/数据/旧.txt`、`/数据/记录.txt`、`/响应/正文.txt`,不含 `/其他/密.txt` 与任何 `/请求/…`。
- 程序以退出码 3 结束:返回 `ok` 为假、`exitCode` 为 3、没有 `error`(返回值,不抛异常)。未捕获的豫言异常:`ok` 为假、`exitCode` 为 1、`error` 非空。向标准输出写 65537 字节:`ok` 为假、`error` 为「输出超过 64 KB」。
- 写 256 个 `/数据/` 文件(各 1 字节)全部返回;写 257 个抛出「隔离运行失败:500:运行数据超过上限」。写合计恰 1048576 字节的一个文件返回,再多 1 字节抛出同一异常。写一个不是有效 UTF-8 的文件抛出「隔离运行失败:500:…」。
- 摘要多一位、含大写、或与程序不符,分别抛出「产物摘要无效」「产物摘要无效」「运行产物摘要不匹配」;程序文字含 `@` 抛出「运行产物无效:不是有效的 Base64」;范围为空、129 字节、含控制字符抛出「隔离范围无效」,128 字节可用;未授权的运行器名抛出「隔离运行失败:未授权的LOADER绑定:…」,运行器名为空抛出「运行器名无效」。
- 输入为「不是JSON」、`{"args":[1]}`、`{"files":{"/a":1}}` 分别抛出「隔离运行输入无效:…」;非 Wasm 字节(摘要正确)抛出「隔离运行失败:动态 Worker 程序不是有效 Wasm」。
- 同一事件里连续运行 1000 次(含 1000 次全部失败的情形)都正常完成,不耗尽宿主的句柄表。同一(范围,摘要)取得同一隔离体标识,范围不同标识不同。

## 边界

本包不含编译;程序须已编译。不提供多次调用之间共享的存储、网络或定时能力。不同宿主可以用不同隔离技术实现(Dynamic Worker、进程沙箱、WebAssembly 独立实例),只要满足上述环境与限额,并对同一程序、同一输入给出同一 `stdout`、`stderr`、`exitCode` 与 `files`。

规范.文言.md

# 隔离运行公约 0.1.0

此包使客置一**已编之文件式程序**于与己全隔之室,运行一次,取其标准出、标准误与约定目录之文。文件式程序者,豫言编器为文件式宿主(浏览器编器宿主、节点宿主)所出之 WasmGC 程序:读写**内存文件系**,用命令行参数与标准出,不识网、平台之绑定与操作系。云工作台以之运用户站点之程序;凡运不可信而由人或器所编之豫言程序者,皆可用之。此乃云工专用之能,用 Worker Loader 绑定,应用之许须授 `LOADER` 绑定之名。

## 术

`运行隔离程序 运行器名 范围 产物摘要 程序 输入`,返字符串。

| 参 | 义 |
| --- | --- |
| 运行器名 | 应用之许 `LOADER` 列中所授之绑定名;未授则抛豫言之异 |
| 范围 | 隔离缓存之分区名,一至一百二十八字节,不得含控制之字。同(范围,产物摘要,宿主资源版)之运,可共一隔离体;异范围永不共。云工宿主之运行资源(子入口与内存文件系之宿主)随构建而定,同一次部署之内其版不变,故隔离体之标识即「范围:产物摘要」 |
| 产物摘要 | 解码后程序字节之 SHA-256,六十四位小写十六进制。宿主运前重算而较之,不符则抛「运行产物摘要不匹配」(防存储损坏或被易) |
| 程序 | 编译产物之 Base64 文(标准字母表,宽容 ASCII 空白与缺省之填充,同 JS 之 `atob`),长一至四百一十九万四千三百零四字,解码后至多三百一十四万五千七百二十八字节,须为有效 Wasm。用 Base64 者,以产物恒以 JSON 文存与传也 |
| 输入 | JSON 文,至多一百五十七万二千八百六十四字节:`{"args":[…字符串],"files":{"路径":"文"}}`。`args` 缺则空列,须为字符串列;`files` 缺则空对象,值须为字符串,路径依 `/` 规整(去 `.`、折 `..`、补首 `/`) |

## 室

- 每运皆**新程序实例、新内存文件系**,运与运之间不留任何状;同(范围,摘要,宿主资源版)惟共已编之模块,不共其数。久存之数,当由客置于输入之 `files`,复自输出之 `files` 取之。
- 无外发之网、无平台绑定、无环境变量、子请求为零;算时之限一千毫秒(宿主可减不可增);标准出与标准误合至多六万五千五百三十六字节,逾则程序败(`ok` 为假而带 `error`)。
- **算时之限,平台执之**:逾算时之限,则平台止其隔离体,客得败而不得程序之返值,`运行隔离程序` 抛「隔离运行失败:…」。宿主之执行器虽另设五秒墙钟之察,然惟程序回调宿主之检点时方行;今编器为文件式所出之程序无检点,故死循环之程全赖平台之算时限以止之。**本地 workerd 不执算时之限**(已验:死循环之程恒占算力而不返),本地验测不得运死循环之程。
- 标准入为空;命令行之程序名为 `/程序.wasm`,当前目录为 `/`。

## 返

返 JSON 文:`{"ok":爻,"stdout":文,"stderr":文,"exitCode":整数,"files":{路径:文},"error"?:文}`。

- `ok`:程序以退出码零终。`exitCode` 为程序之退出码;程序因运行之误(陷阱、出逾限、未捕之豫言异、宿主检点逾时)而终,则 `ok` 为假、`exitCode` 为一,而带 `error` 以说其故(未捕之豫言异于宿主表为 `illegal cast`,出逾限为「输出超过 64 KB」)。程序之败乃**返值**,非异;已书于标准出与标准误者,仍于 `stdout`、`stderr` 返之(逾限之一书除外)。
- `files`:惟含运毕时内存文件系中以 `/数据/`、`/响应/` 起首之文(输入所予而程序未改之 `/数据/…` 亦在其中),各依严格 UTF-8 解为文;至多二百五十六件,合至多一百零四万八千五百七十六字节(以字节计);逾限,或有文非有效 UTF-8,则整运判为接口之败(抛豫言异「隔离运行失败:500:…」)。他径(含输入之 `/请求/…`)不返。
- 输入或程序违规(摘要不符、越限、`args` 类型误、非有效 Wasm)、运行器未授、隔离体之造或用败,皆抛可捕之豫言异,其消息明其故(见下「败之情形」)。宿主之败一律走可捕之异,不得中止当前之事。

## 败之情形

| 情形 | 类与消息 |
| --- | --- |
| 运行器名非一至一百二十八字节;范围非一至一百二十八字节或含控制之字;产物摘要非六十四位小写十六进制;程序文长不在一至四百一十九万四千三百零四;输入逾一百五十七万二千八百六十四字节 | 违规,可捕,消息依次为 `运行器名无效`、`隔离范围无效`、`产物摘要无效`、`运行产物无效`、`运行输入超过上限` |
| 程序文非有效 Base64 | 违规:`运行产物无效:不是有效的 Base64` |
| 解码后字节之 SHA-256 与产物摘要不符 | 违规:`运行产物摘要不匹配` |
| 运行器名不在应用许可之 `LOADER` 列;绑定不存在;隔离体之造败;解码后非有效 Wasm;隔离体崩溃或逾平台之限 | 可捕:`隔离运行失败:<故>`(未授则故为 `未授权的LOADER绑定:<名>`,非有效 Wasm 则为 `动态 Worker 程序不是有效 Wasm`) |
| 输入非有效 JSON,`args` 非字符串列,`files` 非路径至文之对象 | 违规:`隔离运行输入无效:<故>` |
| 出文逾二百五十六件或合逾一百零四万八千五百七十六字节,或有文非有效 UTF-8 | 接口之败:`隔离运行失败:500:<故>` |
| 程序自身之败(退出码非零、陷阱、未捕之豫言异、出逾六万五千五百三十六字节) | **非异**:返值 `ok` 为假 |

## 一致性样例

设程序甲读 `/请求/路径.txt`(无则视为空),书 `/数据/记录.txt`、`/响应/正文.txt`、`/其他/密.txt` 各一行,并于标准出印一行“你好”。以输入 `{"args":["echo"],"files":{"/请求/路径.txt":"/x","/数据/旧.txt":"旧"}}` 运之:

- 返 `ok` 为真、`exitCode` 为零、`stdout` 为“你好”加换行;`files` 恰含 `/数据/旧.txt`、`/数据/记录.txt`、`/响应/正文.txt`,不含 `/其他/密.txt` 与诸 `/请求/…`。
- 程序以退出码三终:返 `ok` 为假、`exitCode` 为三、无 `error`(返值,非抛异)。未捕之豫言异:`ok` 为假、`exitCode` 为一、`error` 非空。于标准出书六万五千五百三十七字节:`ok` 为假、`error` 为「输出超过 64 KB」。
- 书二百五十六件 `/数据/` 文(各一字节)悉返;书二百五十七件则抛「隔离运行失败:500:运行数据超过上限」。书一文合恰一百零四万八千五百七十六字节则返,多一字节则抛同异。书一非有效 UTF-8 之文,抛「隔离运行失败:500:…」。
- 摘要多一位、含大写、或与程序不符,分别抛「产物摘要无效」「产物摘要无效」「运行产物摘要不匹配」;程序文含 `@` 则抛「运行产物无效:不是有效的 Base64」;范围为空、一百二十九字节、含控制字,抛「隔离范围无效」,一百二十八字节则可;运行器名未授则抛「隔离运行失败:未授权的LOADER绑定:…」,运行器名为空则抛「运行器名无效」。
- 输入为「不是JSON」、`{"args":[1]}`、`{"files":{"/a":1}}`,分别抛「隔离运行输入无效:…」;非 Wasm 之字节(摘要无误)抛「隔离运行失败:动态 Worker 程序不是有效 Wasm」。
- 于同一事中连运一千次(含一千次尽败之情形)皆正常而毕,不竭宿主之句柄表。同(范围,摘要)得同一隔离体之标识,范围异则标识异。

## 界

此包不含编译,程序须已编。不供多次调用间共享之存、网或定时之能。异宿主可以异隔离之术实现(Dynamic Worker、进程沙箱、WebAssembly 独立实例),惟须合上述之室与限,且于同程序同输入,所返 `stdout`、`stderr`、`exitCode` 与 `files` 相同。