sprawling-documents 0.0.8

-- This Source Code Form is subject to the terms of the Mozilla Public
-- License, v. 2.0. If a copy of the MPL was not distributed with this
-- file, You can obtain one at https://mozilla.org/MPL/2.0/.
-- Copyright (c) 2026 2youg1 and the sprawling contributors

/-!
# encoding：一个版本的字节拼出哪些字符

规定 `crates/documents/src/encoding.rs`（`documents::Encoding`、`Reading::of`、`Encoding::of_mark`、`Encoding::decode`）。Rust 代码是「怎样守住」的权威；本模型是「必须守住哪些性质」的权威。

字节顺序标记先判：有标记就照标记读，没有就是 UTF-8 或什么都不是（D4）。某串字节在 UTF-8、UTF-16LE、UTF-16BE 下是否合法是参数 `Validity`：那是 Unicode 的事实，Rust 用标准库的 `str::from_utf8` 与 `char::decode_utf16` 判它，模型不重述。

证明的性质：

1. **带标记的 UTF-16 是文本，不管里面有多少 NUL**（`marked_utf16le_is_text`）：旧的判法凭 NUL 判二进制，正好把每个 ASCII 字符旁边都有一个 NUL 的 UTF-16 文件判成二进制（refrain 路线图附录 C）。
2. **没有标记而含 NUL 的不是文本**（`nul_without_mark_is_opaque`）：文本文件不含 NUL，城自己存的东西（redb、CAS 里的块）含。
3. **判成文本的，在它的编码下拼得出**（`text_is_spelled`）：判定与解码读同一条规则，所以一个判成文本的版本，它的每个窗口都解得出（窗口切在字符边界上，`spec/Window.lean`）。

**照旧的 NUL 判法，带标记的 UTF-16 文件就成了不透明的**（`nulJudgement_calls_wide_text_opaque`）：本模型咬得动的演示。
-/

namespace Documents.Encoding

inductive Encoding where
  | utf8
  | utf8Bom
  | utf16Le
  | utf16Be
  deriving DecidableEq, Repr

inductive Reading where
  | text (encoding : Encoding)
  | opaque
  deriving DecidableEq, Repr

/-- 三种编码各自的合法性，由 Unicode 定义，是模型的参数。 -/
structure Validity where
  utf8 : List Nat → Bool
  utf16Le : List Nat → Bool
  utf16Be : List Nat → Bool

/-- 前三个字节里的标记说的编码；没有标记就是 UTF-8。 -/
def ofMark : List Nat → Encoding
  | 0xEF :: 0xBB :: 0xBF :: _ => .utf8Bom
  | 0xFF :: 0xFE :: _ => .utf16Le
  | 0xFE :: 0xFF :: _ => .utf16Be
  | _ => .utf8

/-- 一串字节在这种编码下拼不拼得出文本。 -/
def spells (v : Validity) : Encoding → List Nat → Bool
  | .utf8, s => v.utf8 s && !s.contains 0
  | .utf8Bom, s => v.utf8 s
  | .utf16Le, s => v.utf16Le s
  | .utf16Be, s => v.utf16Be s

/-- `Reading::of`：标记先判，再看字节拼不拼得出。 -/
def reading (v : Validity) (s : List Nat) : Reading :=
  if spells v (ofMark s) s then .text (ofMark s) else .opaque

theorem marked_utf16le_is_text (v : Validity) (rest : List Nat)
    (valid : v.utf16Le (0xFF :: 0xFE :: rest) = true) :
    reading v (0xFF :: 0xFE :: rest) = .text .utf16Le := by
  simp [reading, ofMark, spells, valid]

theorem nul_without_mark_is_opaque (v : Validity) (s : List Nat)
    (unmarked : ofMark s = .utf8) (nul : 0 ∈ s) : reading v s = .opaque := by
  simp [reading, unmarked, spells, nul]

theorem text_is_spelled (v : Validity) (s : List Nat) (e : Encoding)
    (judged : reading v s = .text e) : spells v e s = true := by
  unfold reading at judged
  split at judged
  · rename_i spelled
    cases judged
    exact spelled
  · cases judged

/-!
## 咬得动的演示

旧的判法：含 NUL 就是二进制，否则当 UTF-8 读。一个带标记的 UTF-16LE 文件 `"a"` 是 `FF FE 61 00`，它被判成不透明的。
-/

def nulJudgement (s : List Nat) : Reading :=
  if s.contains 0 then .opaque else .text .utf8

theorem nulJudgement_calls_wide_text_opaque :
    nulJudgement [0xFF, 0xFE, 0x61, 0x00] = .opaque := by
  decide

end Documents.Encoding