diff --git a/.github/workflows/ib-html-prepaint-static.yml b/.github/workflows/ib-html-prepaint-static.yml
new file mode 100644
index 00000000..ff0307c8
--- /dev/null
+++ b/.github/workflows/ib-html-prepaint-static.yml
@@ -0,0 +1,31 @@
+name: IB independent Prepaint Version 1 oracle
+
+on:
+ pull_request:
+ paths:
+ - 'src/IB/HtmlPrepaint.idric'
+ - 'src/IB/HtmlLinks.idric'
+ - 'src/IB/Information.idric'
+ - 'src/IB/RecoveredInformation.idric'
+ - 'tests/prepaint_v1_oracle.c'
+ - 'tests/test_prepaint_oracle_static.sh'
+ - 'tests/fixtures/ib-html/**'
+ - '.github/workflows/ib-html-prepaint-static.yml'
+ workflow_dispatch:
+
+permissions:
+ contents: read
+
+jobs:
+ independent-wire:
+ runs-on: ubuntu-24.04
+ steps:
+ - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262
+ with:
+ ref: ${{ github.event.pull_request.head.sha || github.sha }}
+ persist-credentials: false
+ - name: Independently parse frozen Version 1 witnesses and reject mutants
+ run: |
+ test "$(git rev-parse HEAD)" = "${{ github.event.pull_request.head.sha || github.sha }}"
+ sh -n tests/test_prepaint_oracle_static.sh
+ sh tests/test_prepaint_oracle_static.sh
diff --git a/.github/workflows/idric-core.yml b/.github/workflows/idric-core.yml
index 5e802820..154d0800 100644
--- a/.github/workflows/idric-core.yml
+++ b/.github/workflows/idric-core.yml
@@ -101,6 +101,115 @@ jobs:
grep -Fx 'nonincreasing-revision-refused=True' /tmp/ib-canonical-information.txt
grep -Fx 'version1=serialized' /tmp/ib-canonical-information.txt
+ - name: Compile and exercise admitted HTML to Prepaint Version 1
+ working-directory: src
+ run: |
+ /tmp/idric/bin/idris2 HtmlPrepaintSmoke.idric -o ib-html-prepaint-smoke
+ test -x build/exec/ib-html-prepaint-smoke
+ build/exec/ib-html-prepaint-smoke | tee /tmp/html-prepaint-smoke.txt
+ grep -Fx 'version1=True' /tmp/html-prepaint-smoke.txt
+ grep -Fx 'heading-six=True' /tmp/html-prepaint-smoke.txt
+ grep -Fx 'digest-mismatch-refused=True' /tmp/html-prepaint-smoke.txt
+ /tmp/idric/bin/idris2 HtmlPrepaintCommand.idric -o ib-html-prepaint
+ test -x build/exec/ib-html-prepaint
+
+ - name: Check out independently accepted AI-CI Prepaint consumer
+ uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683
+ with:
+ repository: isomorphisms/ai-ci
+ ref: 0fb20839a2da68be0aafc10511e13c634bfa02b9
+ path: .tools/ai-ci-prepaint
+ persist-credentials: false
+
+ - name: Independently verify actual Idriç output and source-bound mutations
+ env:
+ IB_AICI_PREPAINT_VERIFIER: ${{ github.workspace }}/.tools/ai-ci-prepaint/ib-prepaint/verify.sh
+ IB_HTML_PREPAINT_RECEIPT_ROOT: ${{ runner.temp }}/ib-html-prepaint-receipts
+ run: |
+ test "$(git -C .tools/ai-ci-prepaint rev-parse HEAD)" = 0fb20839a2da68be0aafc10511e13c634bfa02b9
+ sh -n bin/ib_emit_html_prepaint.grease
+ sh -n bin/ib_arena_to_html_prepaint.grease
+ sh -n tests/test_arena_html_refusals.sh
+ sh tests/test_arena_html_refusals.sh
+ sh -n tests/test_html_prepaint.sh
+ sh .tools/ai-ci-prepaint/ib-prepaint/self-test.sh
+ sh tests/test_html_prepaint.sh
+ {
+ printf 'repository\tisomorphisms/ib\n'
+ printf 'source_commit\t%s\n' "$(git rev-parse HEAD)"
+ printf 'idric_commit\t%s\n' "$IDRIC_REF"
+ printf 'independent_ai_ci_commit\t0fb20839a2da68be0aafc10511e13c634bfa02b9\n'
+ printf 'compiler_version\t%s\n' "$(/tmp/idric/bin/idris2 --version)"
+ printf 'platform\t%s\n' "$(uname -sm)"
+ } > "$IB_HTML_PREPAINT_RECEIPT_ROOT/inputs.tsv"
+ sha256sum src/build/exec/ib-html-prepaint src/build/exec/ib-html-prepaint-smoke \
+ tests/prepaint_v1_oracle.c src/IB/HtmlPrepaint.idric src/IB/HtmlLinks.idric \
+ > "$IB_HTML_PREPAINT_RECEIPT_ROOT/artifact-inputs.sha256"
+ (cd "$IB_HTML_PREPAINT_RECEIPT_ROOT" && sha256sum *.prepaint > wire.sha256)
+
+ - name: Retain independently checked fixture receipts
+ uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
+ with:
+ name: ib-html-prepaint-idric-and-aici
+ path: ${{ runner.temp }}/ib-html-prepaint-receipts/
+ if-no-files-found: error
+
+ - name: Check out verified Arena v2 acquisition and reader implementation
+ uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262
+ with:
+ repository: isomorphisms/ib
+ ref: e2a2a17a4378b7c3845ec43f42d1d3360b12f051
+ path: .deps/ib-arena
+ persist-credentials: false
+
+ - name: Check out canonical append-fat userspace Arena
+ uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262
+ with:
+ repository: isomorphisms/sd-card-append-fat
+ ref: 05a0cb7246c5a9f46abfbe92925812e7b607f454
+ path: .deps/appendfat
+ persist-credentials: false
+
+ - name: Resolve qualified host ICK compiler
+ uses: isomorphisms/ai-ci/ick-host@015cc7901ae0b3ad262b476f24e129b53c56db95
+ id: ick
+
+ - name: Reopen real canonical Arena bytes and compile with actual Idriç converter
+ env:
+ ICK: ${{ steps.ick.outputs.compiler }}
+ IB_AICI_PREPAINT_VERIFIER: ${{ github.workspace }}/.tools/ai-ci-prepaint/ib-prepaint/verify.sh
+ IB_HTML_PREPAINT_RECEIPT_ROOT: ${{ runner.temp }}/ib-html-prepaint-receipts
+ run: |
+ test "$(git -C .deps/ib-arena rev-parse HEAD)" = e2a2a17a4378b7c3845ec43f42d1d3360b12f051
+ test "$(git -C .deps/appendfat rev-parse HEAD)" = 05a0cb7246c5a9f46abfbe92925812e7b607f454
+ mkdir -p build/ib-html-arena
+ "$ICK" -fno-link-libatomic -std=c11 -O2 -Wall -Wextra -Wpedantic -Werror \
+ .deps/appendfat/lib/appendfat_arena.c \
+ .deps/appendfat/tools/appendfat_arena.c \
+ -o build/ib-html-arena/appendfat_arena
+ cc -std=c11 -O2 -Wall -Wextra -Wpedantic -Werror \
+ .deps/ib-arena/native/android/ib_arena_slice.c \
+ -o build/ib-html-arena/ib-arena-slice
+ cc -std=c11 -O2 -Wall -Wextra -Wpedantic -Werror \
+ tests/prepaint_v1_oracle.c -o build/ib-html-arena/prepaint-oracle
+ export IB_APPEND_ARENA="$GITHUB_WORKSPACE/build/ib-html-arena/appendfat_arena"
+ export IB_ARENA_SLICE="$GITHUB_WORKSPACE/build/ib-html-arena/ib-arena-slice"
+ export IB_HTML_PREPAINT_EXEC="$GITHUB_WORKSPACE/src/build/exec/ib-html-prepaint"
+ export IB_PREPAINT_ORACLE="$GITHUB_WORKSPACE/build/ib-html-arena/prepaint-oracle"
+ sh -n tests/test_arena_v2_to_html_prepaint.sh
+ sh tests/test_arena_v2_to_html_prepaint.sh
+ sha256sum build/ib-html-arena/appendfat_arena build/ib-html-arena/ib-arena-slice \
+ build/ib-html-arena/prepaint-oracle \
+ > "$IB_HTML_PREPAINT_RECEIPT_ROOT/arena-host-executables.sha256"
+ (cd "$IB_HTML_PREPAINT_RECEIPT_ROOT" && sha256sum *.prepaint > wire.sha256)
+
+ - name: Retain qualified Arena-v2 mocked-origin integration evidence
+ uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
+ with:
+ name: ib-html-prepaint-arena-v2-mock
+ path: ${{ runner.temp }}/ib-html-prepaint-receipts/
+ if-no-files-found: error
+
- name: Exercise browser-owned Idriç core
run: sh bin/ci_browser_foundation.grease exercise-core
diff --git a/README.md b/README.md
index 3356f16b..bd90c72b 100644
--- a/README.md
+++ b/README.md
@@ -19,6 +19,7 @@ heap, form, and reconstruction outcomes separately. See
## Design notes
- `docs/architecture.md` — ownership and replaceable-service boundaries
+- `docs/source-byte-decoding.md` — source-bound HTML decoding without changing admission
- `docs/personal-workbench.md` — personal scope, task frontend, user stories, and latency targets
- `docs/prefetch-and-reading.md` — durable investigation frontiers, disposable fetches, and `~/reading`
- `docs/tab-categorization.md` — overlapping personal categories and adaptive refinement
diff --git a/bin/ib_arena_to_html_prepaint.grease b/bin/ib_arena_to_html_prepaint.grease
new file mode 100644
index 00000000..a497e1a9
--- /dev/null
+++ b/bin/ib_arena_to_html_prepaint.grease
@@ -0,0 +1,81 @@
+#!/bin/sh
+# Adapter ONLY for independently reopened committed PR #152 Arena ranges.
+# It requires future admitted ICU metadata; legacy UNOBSERVED v1 refuses.
+# The transport + store remain owned by #152; this imports no replacement.
+set -eu
+umask 077
+fail() { printf 'ib Arena → HTML prepaint: %s\n' "$1" >&2; exit 1; }
+test "$#" -eq 4 || fail 'usage: ib_arena_to_html_prepaint.grease REQUEST_ID PRIVATE_ARENA_ROOT EXPECTED_GENERATION OUTPUT'
+request=$1
+root=$2
+generation=$3
+output=$4
+case "$request" in
+ ''|.|..|*[!abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ0123456789._-]*) fail 'bad request identity' ;;
+esac
+case "$root" in /*) ;; *) fail 'Arena root must be absolute' ;; esac
+test -d "$root" && test ! -L "$root" || fail 'Arena root unavailable or linked'
+root=$(CDPATH='' cd -P -- "$root" && pwd -P)
+manifest="$root/receipts/$request.tsv"
+test -f "$manifest" && test ! -L "$manifest" || fail 'no committed receipt'
+test "$(wc -c < "$manifest" | tr -d '[:space:]')" -le 8192 || fail 'oversized producer receipt'
+awk -F '\t' '
+ NF != 2 || $1 !~ /^[a-z_][a-z_0-9]*$/ || $2 == "" || /\r/ { bad=1 }
+ { if (seen[$1]++) bad=1 }
+ END { if (bad || NR < 14) exit 1 }
+' "$manifest" || fail 'invalid or duplicate producer receipt keys'
+field() { awk -F '\t' -v key="$1" '$1 == key { print $2 }' "$manifest"; }
+test "$(field request_id)" = "$request" || fail 'request mismatch'
+test "$(field reopen_check)" = MATCH || fail 'source not independently reopened'
+test "$(field navigation_admitted)" = YES || fail 'navigation not admitted'
+test "$(field source_generation)" = "$generation" || fail 'out-of-order or missing generation'
+test "$(field acquisition_complete)" = YES || fail 'incomplete ICU acquisition'
+test "$(field mime_type)" = text/html || fail 'unadmitted content type'
+case "$(field charset)" in utf-8|UTF-8) ;; *) fail 'unobserved/unsupported charset' ;; esac
+test "$(field http_status)" = 200 || fail 'unadmitted status'
+requested=$(field requested_url)
+resolved=$(field resolved_url)
+test -n "$requested" && test -n "$resolved" && test "$resolved" != UNOBSERVED ||
+ fail 'actual ICU final URL missing'
+digest=$(field sha256)
+length=$(field byte_count)
+test -n "$digest" && test -n "$length" || fail 'source digest/length missing'
+case "$digest" in ''|*[!0123456789abcdef]*) fail 'source digest invalid' ;; esac
+test "$(printf %s "$digest" | wc -c | tr -d '[:space:]')" -eq 64 || fail 'source digest length invalid'
+case "$length" in ''|*[!0123456789]*) fail 'source length invalid' ;; esac
+test "$length" -gt 0 && test "$length" -le 4194304 || fail 'source length outside bound'
+expected_key="arena:$request"
+test "$(field source_key)" = "$expected_key" || fail 'untrusted source key'
+reader=$(printenv IB_ARENA_READ_EXEC 2>/dev/null || :)
+test -n "$reader" && test -x "$reader" || fail 'PR #152 verified Arena reader executable required'
+parent=$(dirname -- "$output")
+test -d "$parent" && test ! -L "$parent" || fail 'disposable output directory unavailable'
+work=$(mktemp -d "$parent/.ib-html-arena.XXXXXXXX") || fail 'cannot stage retained source'
+cleanup() { rm -rf "$work"; }
+trap cleanup EXIT HUP INT TERM
+# This MUST be PR #152's verified range-reading implementation. It performs
+# the canonical offset, used pointer, length and SHA check before any emission.
+"$reader" "$request" "$root" > "$work/body" ||
+ fail 'canonical committed readback refused'
+test "$(wc -c < "$work/body" | tr -d '[:space:]')" = "$length" ||
+ fail 'reopened committed source length changed'
+test "$(sha256sum "$work/body" | cut -d ' ' -f 1)" = "$digest" ||
+ fail 'reopened committed source digest changed'
+{
+ printf 'schema\tib-html-admission-v1\n'
+ printf 'source_kind\tarena\n'
+ printf 'source_key\t%s\n' "$expected_key"
+ printf 'source_generation\t%s\n' "$generation"
+ printf 'requested_url\t%s\n' "$requested"
+ printf 'resolved_url\t%s\n' "$resolved"
+ printf 'http_status\t200\n'
+ printf 'mime_type\ttext/html\n'
+ printf 'charset\t%s\n' "$(field charset)"
+ printf 'sha256\t%s\n' "$digest"
+ printf 'byte_count\t%s\n' "$length"
+ printf 'acquisition_complete\tYES\n'
+ printf 'arena_reopen\tMATCH\n'
+} > "$work/admitted.tsv"
+IB_EXPECTED_SOURCE_GENERATION="$generation" \
+ sh "$(dirname -- "$0")/ib_emit_html_prepaint.grease" \
+ "$work/admitted.tsv" "$work/body" "$expected_key" "$output"
diff --git a/bin/ib_decode_html_bytes.grease b/bin/ib_decode_html_bytes.grease
new file mode 100644
index 00000000..66cb8024
--- /dev/null
+++ b/bin/ib_decode_html_bytes.grease
@@ -0,0 +1,129 @@
+#!/usr/bin/env grease
+# Source-bound diagnostic decoding, not a canonical or reader-admission path.
+umask 077
+var owned_temporaries = []
+trap --add EXIT {
+ for temporary in (owned_temporaries) { rm -rf -- $temporary }
+}
+
+proc fail(message) {
+ write -- "ib source decoding: $message" >&2
+ exit 2
+}
+
+proc checked_path(path) {
+ if (not path.startsWith('/')) { fail 'path must be absolute' }
+ var current = path
+ while (current !== '/') {
+ if test -L $current { fail 'path crosses a symlink' }
+ setvar current = $(dirname -- $current)
+ }
+}
+
+proc regular_file(path, limit) {
+ checked_path $path
+ if test ! -f $path { fail 'regular input file unavailable' }
+ var count = $(wc -c < $path)
+ if (int(count) > limit) { fail 'file exceeds decoding bound' }
+}
+
+proc digest(path) {
+ sha256sum -- $path | cut -d ' ' -f 1
+}
+
+proc field(path, key) {
+ awk -F b'\t' -v key=$key '$1 == key { print $2 }' $path
+}
+
+if (len(ARGV) !== 4) {
+ fail 'usage: ib_decode_html_bytes.grease IDRIC_DECODER SOURCE.tsv RAW_BYTES NEW_DERIVATIVE_DIRECTORY'
+}
+var decoder = ARGV[0]
+var supplied_metadata = ARGV[1]
+var supplied_raw = ARGV[2]
+var destination = ARGV[3]
+checked_path $decoder
+if test ! -x $decoder { fail 'compiled Idriç decoder required' }
+regular_file $supplied_metadata 8192
+regular_file $supplied_raw 4194304
+checked_path $destination
+if test -e $destination { fail 'derivative destination already exists' }
+var parent = $(dirname -- $destination)
+if test ! -d $parent { fail 'derivative parent unavailable' }
+var stage = $(mktemp -d "$parent/.ib-decode.XXXXXX")
+call owned_temporaries->append(stage)
+
+# Freeze bounded inputs before interpreting claims or invoking the decoder.
+# The output retains this descriptor exactly; extra source fields are opaque
+# provenance, not an extension to this command's admission authority.
+head -c 8193 -- $supplied_metadata > "$stage/source.tsv"
+head -c 4194305 -- $supplied_raw > "$stage/input.raw"
+regular_file "$stage/source.tsv" 8192
+regular_file "$stage/input.raw" 4194304
+if ! awk -F b'\t' '
+ BEGIN {
+ split("source_key source_generation sha256 byte_count charset navigation_admitted", keys, " ")
+ for (i in keys) required[keys[i]]=1
+ }
+ NF!=2 || $1 !~ /^[a-z_][a-z_0-9]*$/ || $2=="" || /\r/ || seen[$1]++ {bad=1}
+ END {for (key in required) if (!seen[key]) bad=1; exit bad}
+' "$stage/source.tsv" { fail 'malformed or incomplete source descriptor' }
+var key = $(field "$stage/source.tsv" source_key)
+var generation = $(field "$stage/source.tsv" source_generation)
+if (len(key) > 256 or len(generation) > 256) { fail 'source identity exceeds bound' }
+var expected_hash = $(field "$stage/source.tsv" sha256)
+var expected_count = $(field "$stage/source.tsv" byte_count)
+try { printf '%s\t%s\n' $expected_hash $expected_count | awk -F b'\t' '
+ $1 !~ /^[0-9a-f]+$/ || length($1)!=64 ||
+ $2 !~ /^(0|[1-9][0-9]*)$/ || length($2)>7 || $2>4194304 {exit 1}
+' }
+if failed { fail 'invalid source digest or byte count' }
+var navigation = $(field "$stage/source.tsv" navigation_admitted)
+if (navigation !== 'YES' and navigation !== 'NO') { fail 'invalid original navigation observation' }
+var actual_count = $(wc -c < "$stage/input.raw" | tr -d '[:space:]')
+var actual_hash = $(digest "$stage/input.raw")
+if (actual_count !== expected_count) { fail 'source byte count mismatch' }
+if (actual_hash !== expected_hash) { fail 'source digest mismatch' }
+var charset = $(field "$stage/source.tsv" charset)
+var source_metadata_hash = $(digest "$stage/source.tsv")
+
+try { $decoder $charset "$stage/input.raw" "$stage/decoded.utf8" > "$stage/producer.tsv" }
+if failed { fail 'Idriç decoding producer refused or failed' }
+regular_file "$stage/producer.tsv" 1024
+if ! awk -F b'\t' '
+ BEGIN {
+ split("original_byte_count decoded_codepoint_count selected_encoding decoder_identity", keys, " ")
+ for (i in keys) required[keys[i]]=1
+ }
+ NF!=2 || !($1 in required) || $2=="" || seen[$1]++ || /\r/ {bad=1}
+ END {for (key in required) if (!seen[key]) bad=1; exit bad}
+' "$stage/producer.tsv" { fail 'invalid decoder result fields' }
+if ($(field "$stage/producer.tsv" original_byte_count) !== expected_count or
+ $(field "$stage/producer.tsv" decoded_codepoint_count) !== expected_count) {
+ fail 'decoder count disagrees with frozen source'
+}
+if ($(field "$stage/producer.tsv" selected_encoding) !== 'windows-1252' or
+ $(field "$stage/producer.tsv" decoder_identity) !== 'whatwg-windows-1252-e56d49d9176e9a4-v1') {
+ fail 'unsupported decoder result identity'
+}
+regular_file "$stage/decoded.utf8" $[int(expected_count) * 3]
+if ($(digest "$stage/input.raw") !== expected_hash) { fail 'source changed during decoding' }
+if ($(digest "$stage/source.tsv") !== source_metadata_hash) { fail 'source descriptor changed during decoding' }
+var output_count = $(wc -c < "$stage/decoded.utf8" | tr -d '[:space:]')
+var output_hash = $(digest "$stage/decoded.utf8")
+{
+ printf 'schema\tib-decoded-html-v1\n'
+ printf 'source_key\t%s\nsource_generation\t%s\n' $key $generation
+ printf 'source_sha256\t%s\nsource_byte_count\t%s\n' $expected_hash $expected_count
+ printf 'source_descriptor_sha256\t%s\n' $source_metadata_hash
+ printf 'declared_charset\t%s\nselected_encoding\twindows-1252\n' $charset
+ printf 'decoder_identity\twhatwg-windows-1252-e56d49d9176e9a4-v1\n'
+ printf 'decoded_charset\tutf-8\ndecoded_byte_count\t%s\n' $output_count
+ printf 'decoded_codepoint_count\t%s\ndecoded_sha256\t%s\n' $expected_count $output_hash
+ printf 'original_navigation_admitted\t%s\nreader_admission\tNOT_GRANTED\n' $navigation
+} > "$stage/decode.tsv"
+digest "$stage/decode.tsv" > "$stage/complete"
+rm -- "$stage/input.raw" "$stage/producer.tsv"
+mv -T --no-clobber -- $stage $destination
+if test -d $stage { fail 'derivative publication conflicted' }
+write -- $destination
diff --git a/bin/ib_emit_html_prepaint.grease b/bin/ib_emit_html_prepaint.grease
new file mode 100644
index 00000000..9364bbcf
--- /dev/null
+++ b/bin/ib_emit_html_prepaint.grease
@@ -0,0 +1,67 @@
+#!/bin/sh
+# Grease adapter for independently reopened and admitted HTML.
+# Does not acquire sources, network, or create a canonical store.
+set -eu
+umask 077
+fail() { printf 'ib html prepaint: %s\n' "$1" >&2; exit 1; }
+test "$#" -eq 4 || fail 'usage: ib_emit_html_prepaint.grease ADMISSION.tsv VERIFIED_BODY EXPECTED_SOURCE_KEY OUTPUT'
+manifest=$1
+body=$2
+expected_key=$3
+output=$4
+test -f "$manifest" && test ! -L "$manifest" || fail 'missing or linked admission'
+test -f "$body" && test ! -L "$body" || fail 'missing or linked admitted body'
+test ! -L "$output" || fail 'refusing output symlink'
+test "$(wc -c < "$manifest" | tr -d '[:space:]')" -le 4096 || fail 'oversized admission'
+awk -F '\t' '
+ NF != 2 || $1 !~ /^[a-z_][a-z_0-9]*$/ || $2 == "" || /\r/ { bad=1 }
+ { if (seen[$1]++) bad=1 }
+ END { if (bad || NR != 13) exit 1 }
+' "$manifest" || fail 'bad admission structure'
+field() { awk -F '\t' -v key="$1" '$1 == key { print $2 }' "$manifest"; }
+test "$(field schema)" = ib-html-admission-v1 || fail 'unsupported admission schema'
+test "$(field source_key)" = "$expected_key" || fail 'stale or modified source key'
+expected_generation=$(printenv IB_EXPECTED_SOURCE_GENERATION 2>/dev/null || :)
+test -n "$expected_generation" && test "$(field source_generation)" = "$expected_generation" || fail 'stale or unpinned generation'
+case "$(field source_kind)" in
+ arena) test "$(field arena_reopen)" = MATCH || fail 'Arena readback absent' ;;
+ fixture) test "$(printenv IB_ALLOW_FIXTURE 2>/dev/null || :)" = 1 || fail 'fixture not allowed as production source' ;;
+ *) fail 'unknown source kind' ;;
+esac
+test "$(field acquisition_complete)" = YES || fail 'source incomplete'
+test "$(field http_status)" = 200 || fail 'unadmitted HTTP status'
+test "$(field mime_type)" = text/html || fail 'not admitted HTML'
+case "$(field charset)" in utf-8|UTF-8) ;; *) fail 'unsupported charset' ;; esac
+test "$(field source_generation)" != UNOBSERVED || fail 'generation not observed'
+test "$(field resolved_url)" != UNOBSERVED || fail 'final URL not observed'
+test "$(field requested_url)" != UNOBSERVED || fail 'requested URL not observed'
+claimed=$(field sha256)
+bytes=$(field byte_count)
+case "$claimed" in *[!0123456789abcdef]*|'') fail 'invalid digest' ;; esac
+test "$(printf %s "$claimed" | wc -c | tr -d '[:space:]')" -eq 64 || fail 'invalid digest length'
+case "$bytes" in *[!0123456789]*|'') fail 'invalid byte count' ;; esac
+test "$bytes" -gt 0 && test "$bytes" -le 4194304 || fail 'body exceeds admission bound'
+observed_bytes=$(wc -c < "$body" | tr -d '[:space:]')
+test "$bytes" = "$observed_bytes" || fail 'body length differs from committed source'
+observed=$(sha256sum "$body" | cut -d ' ' -f 1)
+test "$claimed" = "$observed" || fail 'body digest differs from committed source'
+iconv -f UTF-8 -t UTF-8 "$body" >/dev/null || fail 'invalid UTF-8'
+converter=$(printenv IB_HTML_PREPAINT_EXEC 2>/dev/null || :)
+oracle=$(printenv IB_PREPAINT_ORACLE 2>/dev/null || :)
+test -n "$converter" && test -x "$converter" || fail 'compiled Idriç executable required'
+test -n "$oracle" && test -x "$oracle" || fail 'independent Version 1 consumer required'
+parent=$(dirname -- "$output")
+test -d "$parent" && test ! -L "$parent" || fail 'disposable output directory absent'
+work=$(mktemp -d "$parent/.ib-prepaint.XXXXXXXX") || fail 'cannot stage disposable output'
+cleanup() { rm -rf "$work"; }
+trap cleanup EXIT HUP INT TERM
+"$converter" "$(field source_key)" "$(field source_generation)" "$claimed" "$observed" \
+ "$bytes" "$observed_bytes" "$(field requested_url)" "$(field resolved_url)" \
+ "$(field mime_type)" "$(field charset)" "$(field http_status)" "$body" \
+ > "$work/projection" || fail 'Idriç converter refused admitted HTML'
+test "$(wc -c < "$work/projection" | tr -d '[:space:]')" -le 4194304 || fail 'prepaint exceeds display bound'
+"$oracle" "$work/projection" || fail 'independent Version 1 oracle refused output'
+test ! -L "$output" || fail 'output symlink changed'
+mv -f "$work/projection" "$output" || fail 'projection publication failed'
+printf 'conversion\tPASS\nsource_key\t%s\nsource_generation\t%s\nsource_sha256\t%s\nprepaint_sha256\t%s\n' \
+ "$expected_key" "$(field source_generation)" "$observed" "$(sha256sum "$output" | cut -d ' ' -f 1)"
diff --git a/docs/html-prepaint-admission.md b/docs/html-prepaint-admission.md
new file mode 100644
index 00000000..e3732940
--- /dev/null
+++ b/docs/html-prepaint-admission.md
@@ -0,0 +1,101 @@
+# IB-C67 HTML → typed Prepaint Version 1
+
+Status: **host fixture converter QUALIFIED / retained Arena HTML BLOCKED / physical C67 NOT_RUN**. Executed [IB CI run 38653082213](https://github.com/isomorphisms/ib/actions/runs/38653082213) passed both `idric-core` and `scientific-media` on `d228f78b00e56a34a93f9f58ca908977ef1c1249`; the pinned separate `isomorphisms/ai-ci@0fb20839a2da68be0aafc10511e13c634bfa02b9` independently consumed the actual generated fixture bytes and ran its wrong-output self-tests. [Retained artifact 11935167962](https://github.com/isomorphisms/ib/actions/runs/38653082213/artifacts/11935167962) SHA-256: `acfe20c464eb4955a75fd5f27a31f038dcaa806c1936557f01dc3e1a5b20f9c6`. These are offline fixtures, **not live ICU network data or a C67 device receipt**.
+
+## Owners and immutable starting points
+
+- Semantic base: PR #148, `work/linux-shared-contract`, originally
+ `2425d21d984de21e5b65ae0d2e09c586120239ee`.
+ This includes the types and existing serializer from #48/#123.
+- Upstream Arena producer and verified source reader: PR #152, whose
+ Version 2 candidate was pinned at
+ `e2a2a17a4378b7c3845ec43f42d1d3360b12f051`.
+ It now consumes ICU #35's *paired same-request* response body and actual
+ metadata, validates source key/generation, HTTP status, MIME/charset,
+ response completeness, final URL and SHA-256, and independently reopens the
+ committed canonical Arena range. Its legacy v1 body-only receipt remains
+ permanently navigation-denied. Its v2 host test passed at
+ [run 38652958137](https://github.com/isomorphisms/ib/actions/runs/38652958137),
+ **with mocked Shizuku/ICU transport**, not actual C67 HTTPS. The separate
+ converter now has a pinned cross-branch mock-integration test for the same
+ v2 producer/reader and the actual Idriç command; that test is not yet a
+ live device acceptance claim.
+- Separate reader-handoff owner: PR #153, original head
+ `9cf28c2f6c38cb12bb906a844e061ebfab34f943`.
+- C67 native Material reader: PR #129. It currently paints a pinned snapshot.
+- ICU final URL/redirect evidence: `dilapidated-shed/icu` PR #35.
+- The browser-foundation CI pins Idriç
+ `7050c116326c9c8e8d0a56c2db7baf2119cbae19`.
+ The underlying runner's compiled executable digest must be recorded from the
+ *actual* artifact; the source pin is not an executable receipt.
+
+## Byte and semantic boundaries
+
+1. A source owner must commit the original bytes, source generation, requested
+ and actual ICU-resolved URLs, status, content type, charset, byte count and
+ source digest. Unobserved or stale metadata is **not admitted**.
+2. Grease reopens and checks the exact readback bytes and SHA-256 and validates
+ the UTF-8 encoding. The source key/generation must match the browser-owned
+ navigation expectation. It must not mint a second persistent source store.
+3. The Idriç converter consumes an admitted immutable HTML string through
+ `IB.RecoveredInformation` and `IB.Information`, maps ordered items into
+ `IB.Strand`, then calls `prepaint_from_strand` and the existing
+ `IB.Prepaint.Version1.serialize_version1`.
+4. A newly emitted complete Version 1 stream is checked by a *different* C11
+ consumer and replaces the last valid disposable projection only after
+ success. A rejected source or converter failure never changes the prior
+ projection.
+5. Display width is not an input to semantic extraction; links remain navigation
+ candidates, never reader-fetch permissions. The Android reader/Binder/PFD
+ adapter must independently bind the publication to the retained source and
+ currently remains **NOT_RUN**.
+
+The Version 1 wire schema does **not** contain a source digest/generation. The
+`HtmlPrepaintResult` retains that metadata and the Grease receipt identifies
+the projection separately. The reader must keep that binding at handoff; a
+standalone `.prepaint` file must not be promoted to canonical source identity.
+
+`bin/ib_emit_html_prepaint.grease` consumes one thirteen-field source admission
+receipt and an **already verified** body path, then requires an exact expected
+source key and `IB_EXPECTED_SOURCE_GENERATION`. The receipt is authority only
+when supplied by the trusted source-store owner, not by an app/remote page.
+The `fixture` kind is prohibited unless `IB_ALLOW_FIXTURE=1`; tests always
+label fixtures. For a v2 Arena source, this adapter passes through the
+**unchanged pinned** #152 producer/verified reader. Mocked metadata proves only
+contract compatibility, never live acquisition or Android reader delivery.
+
+## Supported now / explicit limitations
+
+- Six distinct headings, nested inline text, paragraphs, lists as ordered text
+ blocks, table rows, basic character references, relative/absolute/query/
+ fragment links and a valid HTML base URL.
+- Missing closing heading/paragraph/list/cell/row tags are passed through the
+ existing recovered document log.
+- Forms are visible descriptions with **no submission**. Script, style,
+ canvas, video, SVG and other dynamic elements are excluded or noted.
+- Images have resolved acquisition-request URLs, alt text and available
+ title/figure captions. Without separate image admission only a text
+ placeholder is serialized. **No remote image URI is emitted for the reader
+ to fetch directly.**
+- Not a full HTML5/CSS/JavaScript/DOM parser. Unsupported charsets, unsafe
+ schemes and an unobserved final URL cause refusal or explicit limitations.
+- In-place width reflow and selection identity need graphical reader acceptance;
+ typed source-linked blocks alone are not that acceptance.
+
+## Acceptance matrix
+
+| Check | Authority | Current status |
+|---|---|---|
+| Idriç typecheck + actual executable | IB CI #38653082213 | **PASS**, Linux/host fixtures |
+| Offline example.com-shaped fixture | Actual Idriç output + independent C11/AI-CI oracle and frozen golden | **PASS** |
+| Offline arXiv-shaped fixture | Actual Idriç output + independent C11/AI-CI oracle and frozen golden | **PASS** |
+| Bad digest, generation, source ID, UTF-8 and incomplete admission | Grease refusal, last-valid byte comparison | **PASS**, fixture-only |
+| Mutated heading, link, dropped text and malformed escaping | C11 oracle + independent AI-CI + golden | **PASS**, fixture-only |
+| Mock ICU metadata → actual canonical Arena v2 → Idriç V1 | Pinned PR #152 + canonical appendfat + AICI | COMMITTED / exact-head CI queued |
+| Real ICU HTTPS → committed Arena → admitted metadata | ICU PR #35 + IB PR #152 | NOT_RUN on physical C67 |
+| Binder/PFD delivers new projection to reader | IB PR #153 | NOT_RUN |
+| Physical C67 paints example.com and navigates links | User-observed device + receipts | NOT_RUN |
+| ARM32 A1/C67, ARM64 C67 converter execution | Cat Food/CI evidence | NOT_RUN |
+
+Keep the PR draft and task open until independently admitted retained HTML
+actually produces a valid complete prepaint. Do not label an offline fixture live.
diff --git a/docs/source-byte-decoding.md b/docs/source-byte-decoding.md
new file mode 100644
index 00000000..b9bc2be5
--- /dev/null
+++ b/docs/source-byte-decoding.md
@@ -0,0 +1,95 @@
+# Decode retained bytes without changing source admission
+
+`IB.SourceDecoding` owns the bounded HTML byte-decoding step. Its first decoder
+implements the WHATWG windows-1252 index and the 17 HTML labels which select it,
+including ISO-8859-1, Latin1 and ASCII. It does not reinterpret a label based on
+whether the particular bytes happen to form valid UTF-8.
+
+ASCII whitespace is trimmed from labels and ASCII case is ignored. NBSP is not
+ASCII label whitespace. Every source octet has one Unicode scalar in this
+index, including the five C1 slots sometimes treated as undefined by other
+libraries. NUL, CR/LF and those C1 scalars remain present; HTML preprocessing,
+recovery and extraction have different owners.
+
+A recognized UTF-8/UTF-16 BOM selects a different HTML decoder. This bounded
+implementation explicitly refuses those BOMs rather than decoding their bytes
+under a conflicting windows-1252 label. UTF-8/UTF-16 decoder support and the
+full HTML encoding-prescan algorithm remain future work.
+
+## Binary command and disposable output
+
+`SourceDecodingCommand.idric` reads actual bytes using the existing binary
+Buffer/file interfaces. It checks file size before allocation, requires the
+actual read count to match, probes EOF, and writes actual UTF-8 bytes through
+a binary buffer. Input is bounded to 4 MiB; it still holds the whole bounded
+source and decoded value. This is not streaming ingestion.
+
+The native Grease adapter `bin/ib_decode_html_bytes.grease` takes an explicit
+compiled decoder, a source descriptor TSV, raw source path and a new disposable
+destination directory. Inputs and executable paths must be absolute. A source
+descriptor is bounded key/value data with distinct keys and these required
+fields:
+
+| Field | Meaning |
+| --- | --- |
+| `source_key` | Existing caller-supplied source reference |
+| `source_generation` | Existing caller-supplied version reference |
+| `sha256` | Expected original-byte SHA-256 |
+| `byte_count` | Expected original-byte count, at most 4 MiB |
+| `charset` | Original declared HTML encoding label |
+| `navigation_admitted` | Original YES/NO observation, never changed here |
+
+Additional well-formed fields are opaque provenance and are retained exactly.
+These are source claims supplied by the caller, not authentication or proof of
+an Arena reopen, current generation or permission to navigate.
+
+The adapter snapshots the bounded descriptor and raw input, verifies original
+count/digest, requires producer success and consistent decoder counts/identity,
+and checks that neither frozen input changed during decoding. It stages beneath
+the verified destination parent and publishes by a no-clobber same-filesystem
+directory rename. A failed producer or conflict cannot replace an earlier
+derivative. Static path checks do not promise containment against concurrent
+filesystem-topology replacement or power-loss durability.
+
+The output directory contains:
+
+- `source.tsv`: the exact supplied descriptor, including the original charset
+ and navigation observation;
+- `decoded.utf8`: disposable derived bytes;
+- `decode.tsv`: source and descriptor hashes, decoder identity, selected
+ encoding, output hash/count, decoded codepoint count and explicit
+ `reader_admission=NOT_GRANTED`;
+- `complete`: the derived metadata digest.
+
+The raw body is not duplicated into another persistent store. Byte offsets in
+the original source and decoded Unicode codepoint offsets are different units.
+The original `HtmlEvidence`, native source owner and Arena admission paths are
+unchanged; this receipt is not one of their accepted admission schemas.
+
+## Specification and acceptance
+
+The independent normative index fixture retains WHATWG identifier
+`e56d49d9176e9a412283cf29ac9bd613f5620462f2a080a84eceaf974cfa18b7`
+(2024-09-18) from:
+
+- https://encoding.spec.whatwg.org/#names-and-labels
+- https://encoding.spec.whatwg.org/#single-byte-decoder
+- https://encoding.spec.whatwg.org/index-windows-1252.txt
+- https://html.spec.whatwg.org/multipage/parsing.html#determining-the-character-encoding
+
+`SourceDecodingChecks.idric` checks all 256 octets against that fixture, label
+rules, special scalars and BOM refusals. `tests/source-decoding.grease` executes
+the real binary command and publication adapter, checks bad source claims and
+producer failures, and consumes the exact existing Google capture supplied by
+absolute path. `tests/source-decoding-mutations.grease` compiles and rejects
+actual naïve-Latin1 and undefined-byte-replacement decoders against the same
+normative oracle. These are host decoder/process results, not Android evidence.
+
+The retained Google capture from search source
+`dcbd86c0f7a69c4e0b381c0ab53f7c41f9966900` has 93,166 ASCII bytes, SHA-256
+`f71e991ab87271e77255fe2d2454cb4cb401fe47cdf953ea550c6e0fcd8afeb4`.
+Its derivative is therefore byte-identical, while the declared charset remains
+ISO-8859-1 and redirect count remains one. The test descriptor explicitly uses
+a fixture identity, not an invented live Arena generation. The missing redirect
+chain and native reader/DEX connection still prevent joined navigation
+acceptance. Decoding does not make those conditions true.
diff --git a/examples/autogenerated/prepaint-source-reflow/PrepaintReflowChecks.idric b/examples/autogenerated/prepaint-source-reflow/PrepaintReflowChecks.idric
new file mode 100644
index 00000000..f3d0d898
--- /dev/null
+++ b/examples/autogenerated/prepaint-source-reflow/PrepaintReflowChecks.idric
@@ -0,0 +1,125 @@
+module PrepaintReflowChecks
+
+import Data.Text
+import Data.Maybe
+import IB.Strand
+import IB.Prepaint
+import IB.Prepaint.Version1
+import IB.HtmlPrepaint
+import IB.Prepaint.Reflow
+import IB.Reflow
+import IB.Reflow.SourceBreaks
+import System
+
+codepoint_width : Text → Number
+codepoint_width text = length (unpack text)
+
+double_width : Text → Number
+double_width text = 2 × codepoint_width text
+
+visible_lines : List SourceLine → List Text
+visible_lines [] = []
+visible_lines (line :: rest) = line.visible_text :: visible_lines rest
+
+reconstruct : Text → List SourceLine → Text
+reconstruct source [] = ""
+reconstruct source (line :: rest) =
+ source_for_line source line ++ reconstruct source rest
+
+all_blocks_reconstruct : List BlockReflow → Bool
+all_blocks_reconstruct [] = True
+all_blocks_reconstruct (plan :: rest) =
+ (case plan.decoded_text of
+ Nothing ⇒ null plan.text_lines
+ Just text ⇒ reconstruct text plan.text_lines ≟ text) &&
+ all_blocks_reconstruct rest
+
+positions_match : Number → List BlockReflow → Bool
+positions_match position [] = True
+positions_match position (plan :: rest) =
+ plan.block_position ≟ position && positions_match (S position) rest
+
+same_original_blocks : List InformationBlock → List BlockReflow → Bool
+same_original_blocks [] [] = True
+same_original_blocks (block :: rest) (plan :: plans) =
+ same_block block plan.original_block && same_original_blocks rest plans
+ where
+ same_block : InformationBlock → InformationBlock → Bool
+ same_block (Heading left_level left) (Heading right_level right) =
+ heading_level_number left_level ≟ heading_level_number right_level && left ≟ right
+ same_block (TextBlock left) (TextBlock right) = left ≟ right
+ same_block (Link left left_ref) (Link right right_ref) =
+ left ≟ right && link_reference_value left_ref ≟ link_reference_value right_ref
+ same_block (TableRow left) (TableRow right) =
+ table_row_cells left ≟ table_row_cells right
+ same_block _ _ = False
+same_original_blocks _ _ = False
+
+source_identity : PrepaintRevision → Text
+source_identity revision = nonempty_text_value revision.source.reference
+
+cases : HtmlPrepaintResult → Bool
+cases original =
+ case (reflow_html_prepaint (Requirements 4 promptly) "codepoints-v1" codepoint_width original,
+ reflow_html_prepaint (Requirements 4 promptly) "double-codepoints-v1" double_width original) of
+ (Right result, Right wider) ⇒
+ let layout = result.revision_layout in
+ let wider_layout = wider.revision_layout in
+ let retained = layout.source_revision in
+ let same_source = source_identity retained ≟ source_identity original.revision &&
+ source_identity retained ≟ "arena-source;generation=generation-7;sha256=" ++
+ original.evidence.claimed_sha256 in
+ let same_revision = revision_sequence_value retained.sequence ≟
+ revision_sequence_value original.revision.sequence in
+ let same_wire = serialize_version1 [retained] ≟ Just original.wire in
+ let source_sidecar = result.source_result.evidence.source_generation ≟ "generation-7" &&
+ result.source_result.evidence.claimed_sha256 ≟ original.evidence.claimed_sha256 in
+ let same_blocks = same_original_blocks original.revision.blocks layout.block_plans in
+ let widths = case (layout.block_plans, wider_layout.block_plans) of
+ (heading :: paragraph :: link :: row :: [], wide_heading :: _) ⇒
+ visible_lines heading.text_lines ≟ ["漢字漢字"] &&
+ visible_lines wide_heading.text_lines ≟ ["漢字", "漢字"] &&
+ visible_lines paragraph.text_lines ≟ ["red", "blue"] &&
+ visible_lines link.text_lines ≟ ["next"] &&
+ isNothing row.decoded_text && null row.text_lines
+ _ ⇒ False in
+ same_source && same_revision && same_wire && source_sidecar && same_blocks && widths &&
+ positions_match 0 layout.block_plans && all_blocks_reconstruct layout.block_plans &&
+ layout.measurement_identity ≟ "codepoints-v1" &&
+ wider_layout.measurement_identity ≟ "double-codepoints-v1"
+ _ ⇒ False
+
+refused : Either Text PrepaintLayout → Bool
+refused (Left _) = True
+refused _ = False
+
+refusal_cases : PrepaintRevision → Bool
+refusal_cases revision =
+ refused (reflow_prepaint (Requirements 0 promptly) "metric" codepoint_width revision) &&
+ refused (reflow_prepaint (Requirements 4 promptly) " " codepoint_width revision) &&
+ refused (reflow_prepaint (Requirements 4 streamingly) "metric" codepoint_width revision) &&
+ refused (reflow_prepaint (Requirements 4 typographically) "metric" codepoint_width revision)
+
+nontext_refusal_cases : PrepaintRevision → Bool
+nontext_refusal_cases revision =
+ let empty_revision = record { blocks = [] } revision in
+ refused (reflow_prepaint (Requirements 4 streamingly) "metric" codepoint_width empty_revision) &&
+ refused (reflow_prepaint (Requirements 4 typographically) "metric" codepoint_width empty_revision) &&
+ refused (reflow_prepaint (Requirements 0 promptly) "metric" codepoint_width empty_revision)
+
+main : IO ()
+main = do
+ let digest = "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa"
+ let evidence = HtmlSourceEvidence "arena-source" "generation-7" digest digest
+ 123 123 "https://example.test/request" "https://example.test/resolved"
+ "text/html" "utf-8" "200" True True
+ let html = "
漢字漢字
red blue
next"
+ case convert_admitted_html evidence html of
+ Left problem ⇒ do
+ putStrLn ("prepaint-reflow-conversion=" ++ problem)
+ exitFailure
+ Right result ⇒ do
+ let passed = cases result && refusal_cases result.revision &&
+ nontext_refusal_cases result.revision
+ putStrLn ("prepaint-source-reflow-cases=" ++ show passed)
+ if passed then pure () else exitFailure
diff --git a/examples/autogenerated/prepaint-source-reflow/PrepaintReflowMoonChecks.idric b/examples/autogenerated/prepaint-source-reflow/PrepaintReflowMoonChecks.idric
new file mode 100644
index 00000000..94ffc3d0
--- /dev/null
+++ b/examples/autogenerated/prepaint-source-reflow/PrepaintReflowMoonChecks.idric
@@ -0,0 +1,134 @@
+module PrepaintReflowMoonChecks
+
+import Data.Text
+import Data.Maybe
+import IB.Strand
+import IB.Prepaint
+import IB.Prepaint.Version1
+import IB.Prepaint.Reflow
+import IB.Reflow
+import IB.Reflow.Source
+import IB.Reflow.SourceBreaks
+import System
+
+measure_codepoints : Text → Number
+measure_codepoints text = length (unpack text)
+
+source_name : PrepaintRevision → Text
+source_name revision = nonempty_text_value revision.source.reference
+
+original_blocks : List BlockReflow → List InformationBlock
+original_blocks plans = map (\plan ⇒ plan.original_block) plans
+
+same_origin : RepresentationOrigin → RepresentationOrigin → Bool
+same_origin HtmlSource HtmlSource = True
+same_origin PdfSource PdfSource = True
+same_origin PlainTextSource PlainTextSource = True
+same_origin DerivedSource DerivedSource = True
+same_origin OtherSource OtherSource = True
+same_origin _ _ = False
+
+same_completeness : RepresentationCompleteness → RepresentationCompleteness → Bool
+same_completeness PartialSource PartialSource = True
+same_completeness CompleteSource CompleteSource = True
+same_completeness _ _ = False
+
+same_revision : PrepaintRevision → PrepaintRevision → Bool
+same_revision expected actual =
+ source_name expected ≟ source_name actual &&
+ same_origin expected.source.origin actual.source.origin &&
+ same_completeness expected.source.completeness actual.source.completeness &&
+ serialize_version1 [expected] ≟ serialize_version1 [actual]
+
+contiguous : Number → Number → List SourceLine → Bool
+contiguous source_length offset [] = offset ≟ source_length
+contiguous source_length offset (line :: rest) =
+ line.first_codepoint ≟ offset &&
+ line.after_last_codepoint > offset &&
+ line.after_last_codepoint <= source_length &&
+ contiguous source_length line.after_last_codepoint rest
+
+-- Intentionally independent of the production source_for_line helper.
+recover_slices : Text → List SourceLine → Text
+recover_slices source [] = ""
+recover_slices source (line :: rest) =
+ let before_end = take line.after_last_codepoint (unpack source) in
+ pack (drop line.first_codepoint before_end) ++ recover_slices source rest
+
+text_plan_valid : BlockReflow → Bool
+text_plan_valid plan = case plan.decoded_text of
+ Nothing ⇒ null plan.text_lines
+ Just text ⇒ contiguous (measure_codepoints text) 0 plan.text_lines &&
+ recover_slices text plan.text_lines ≟ text
+
+positions_valid : Number → List BlockReflow → Bool
+positions_valid offset [] = True
+positions_valid offset (plan :: rest) =
+ plan.block_position ≟ offset && positions_valid (S offset) rest
+
+layout_valid : PrepaintRevision → PrepaintLayout → Bool
+layout_valid expected layout =
+ same_revision expected layout.source_revision &&
+ same_revision expected (record { blocks = original_blocks layout.block_plans } layout.source_revision) &&
+ positions_valid 0 layout.block_plans && all text_plan_valid layout.block_plans
+
+visible : List SourceLine → List Text
+visible lines = map (\line ⇒ line.visible_text) lines
+
+mixed_blocks : Maybe (List InformationBlock)
+mixed_blocks = do
+ link ← link_reference "https://example.test/next"
+ form ← form_reference "https://example.test/submit"
+ image ← image_reference "arena-image-id"
+ pure [Heading Heading2 "漢字漢字", TextBlock "a\r\nb", Link "abcd" link,
+ TableRow (table_row "first cell" ["second cell"]),
+ Form "form label" form, Image image "alternate" "caption" (Just link),
+ TextBlock "abcd", TextBlock "a b", TextBlock "éx", TextBlock "👩💻x"]
+
+check_revision : PrepaintRevision → Bool
+check_revision revision =
+ case (reflow_prepaint (Requirements 3 promptly) "cp-v1" measure_codepoints revision,
+ reflow_prepaint (Requirements 4 evenly) "cp-v2" measure_codepoints revision) of
+ (Right layout, Right changed) ⇒
+ let plans = layout.block_plans in
+ let same_mixed = layout_valid revision layout && layout_valid revision changed in
+ let geometry = case plans of
+ heading :: hard :: soft :: table :: form :: image :: zero :: no_break :: accent :: emoji :: [] ⇒
+ visible heading.text_lines ≟ ["漢字漢", "字"] &&
+ visible hard.text_lines ≟ ["a", "b"] &&
+ visible soft.text_lines ≟ ["ab-", "cd"] &&
+ isNothing table.decoded_text && isNothing form.decoded_text && isNothing image.decoded_text &&
+ visible zero.text_lines ≟ ["ab", "cd"] &&
+ visible no_break.text_lines ≟ ["a b"] &&
+ visible accent.text_lines ≟ ["éx"] &&
+ visible emoji.text_lines ≟ ["👩💻x"]
+ _ ⇒ False in
+ let dropped = record { block_plans = drop 1 plans } layout in
+ let reordered = record { block_plans = reverse plans } layout in
+ let new_revision = record { sequence = next_revision revision.sequence } revision in
+ let changed_source = case nonempty_text "another-arena-source" of
+ Nothing ⇒ revision
+ Just reference ⇒ record { source = record { reference = reference } revision.source } revision in
+ same_mixed && geometry &&
+ not (layout_valid revision dropped) && not (layout_valid revision reordered) &&
+ not (layout_valid new_revision layout) && not (layout_valid changed_source layout) &&
+ layout.measurement_identity ≟ "cp-v1" && changed.measurement_identity ≟ "cp-v2" &&
+ (case (layout.requirements, changed.requirements) of
+ (Requirements 3 promptly, Requirements 4 evenly) ⇒ True
+ _ ⇒ False)
+ _ ⇒ False
+
+main : IO ()
+main = do
+ let source = do
+ reference ← nonempty_text "arena-source;generation=7;sha256=fixture"
+ requested ← requested_address "https://example.test/requested"
+ resolved ← resolved_address "https://example.test/resolved"
+ blocks ← mixed_blocks
+ pure (Prepaint first_revision CompleteRevision
+ (Source reference HtmlSource CompleteSource) requested resolved (Just "title") blocks)
+ let passed = case source of
+ Nothing ⇒ False
+ Just revision ⇒ check_revision revision
+ putStrLn ("prepaint-moon-independent-cases=" ++ show passed)
+ if passed then pure () else exitFailure
diff --git a/examples/autogenerated/prepaint-source-reflow/attempt.md b/examples/autogenerated/prepaint-source-reflow/attempt.md
new file mode 100644
index 00000000..60b2fd81
--- /dev/null
+++ b/examples/autogenerated/prepaint-source-reflow/attempt.md
@@ -0,0 +1,132 @@
+# Typed Prepaint to source-bound reflow
+
+## Purpose and source boundaries
+
+Join existing typed Prepaint revisions to the existing Unicode source-bound
+reflow implementation. This is derived layout; the revision and each original
+information block remain unchanged. A block position identifies an occurrence
+only within the retained immutable revision, not across different revisions.
+
+The base is IB HTML-to-Prepaint commit
+`33191f743e2f3bc51ba950f499187db595d43ec2`. Reflow modules and their existing
+smokes are reused unchanged from commit
+`4a7380c5f25409443c5e8c1ae17bd358372012fc`. No line-breaking algorithm is added.
+
+## Values, operations, and invariants
+
+- Input: an existing `PrepaintRevision`, `ReflowRequirements`, a nonempty
+ measurement identity, and its `Text → Number` width callback.
+- Output: either a refusal or a derived layout retaining that exact revision,
+ requirement, measurement identity, original blocks and block positions.
+- Text headings, text paragraphs and link labels receive per-block
+ `SourceLine` plans. Table rows, forms and images remain explicitly unreflowed;
+ their semantic payloads are not flattened into invented text.
+- Offsets count decoded Unicode code points in each block's text. They are not
+ original HTML byte offsets, UTF-16 offsets, glyph positions or pixels.
+- The HTML-result entrypoint retains the complete `HtmlPrepaintResult`,
+ including `HtmlEvidence`. Version 1 wire bytes alone do not authenticate the
+ Arena source generation or digest.
+- Width zero, absent measurement identity and unsupported source-bound
+ streaming/typographic modes must refuse. Existing no-split and source
+ reconstruction rules remain authoritative.
+- All operations are pure. No I/O, networking, storage, native shaping, device
+ installation or renderer claim is introduced.
+
+## Intended signatures
+
+`reflow_prepaint : ReflowRequirements → Text → (Text → Number) →
+PrepaintRevision → Either Text PrepaintLayout`
+
+`reflow_html_prepaint : ReflowRequirements → Text → (Text → Number) →
+HtmlPrepaintResult → Either Text HtmlPrepaintLayout`
+
+## Compiler and verification
+
+The available Linux x86-64 compiler bundle identifies Idriç
+`94dfd99bd3e376507fedc8611053b7173b2519f0`, Chez 10.4.1, producer run
+`38090627721`, attempt 1. Use its actual `bin/idric` entrypoint and preserve
+the first compiler failure rather than substituting another runtime.
+
+Verification must execute the real typed HTML converter and adapter, compare
+known Unicode/width line plans, reconstruct exact decoded text through the
+source spans, retain wire/source/revision/block identity, and exercise refusals.
+Source-only or host execution does not prove native rendering or physical C67.
+
+## Result
+
+Implemented `IB.Prepaint.Reflow`. The adapter never reparses V1 wire output.
+It retains the input revision and original blocks, records the measurement
+identity, and delegates break selection to the unchanged source-bound solver.
+
+Actual host verification used a scratch copy of `src/` at
+`/workspace/scratch/22d72635f498/u3-source-check`, with the canonical
+`PrepaintReflowChecks.idric` copied into that source root. The compiler entrypoint
+was `/workspace/scratch/58fb4da72caa/tools/idric/idric-linux-x86_64-94dfd99bd3e376507fedc8611053b7173b2519f0/bin/idric`;
+its arguments were `PrepaintReflowChecks.idric -o prepaint-reflow-checks`.
+Then the generated `build/exec/prepaint-reflow-checks`
+was executed. It printed `prepaint-source-reflow-cases=True` and exited 0.
+The existing `SourceReflowSmoke.idric` was separately compiled and executed;
+it printed `source-reflow-unicode-offset-cases=True` and exited 0.
+`sh tests/idric-public-vocabulary.sh` passed.
+
+The first check compile exposed a missing `Data.Maybe` import in the new
+check program; adding the actual library import fixed it. No language or
+runtime fallback was used. These are Chez host semantic results, not DEX,
+Android layout, pixel/shaping or physical-device results.
+The check supplies an admission-evidence fixture to the real typed converter;
+it does not itself reopen or authenticate an Arena range.
+
+## Remaining language or integration work
+
+This slice does not make the whole-document HTML ingestion path bounded, remove
+its existing 4 MiB admission ceiling, implement source-bound streaming or
+typographic shaping, serialize source evidence into V1, or connect Android views.
+The first integration boundary is the native view consumer supplying its real
+measurement callback plus versioned measurement identity and consuming these
+per-block plans. Acceptance must independently compare its copied/source text
+and actual measured line geometry on the identified target.
+
+## Independent Moon checks
+
+The independent check program consumes the existing immutable revision and
+derived layout. Its input domain includes ordered mixed semantic blocks,
+Unicode decoded text, source/revision identities, line-codepoint intervals,
+measurement identities and explicit reflow requirements. Its output is a
+Boolean acceptance result with a failing process status for any mismatch.
+It reconstructs decoded source directly with `take`/`drop` over Unicode code
+points, independently of `source_for_line`. It compares serialized original
+blocks and explicit source identity separately because V1 does not serialize
+the source reference. It must reject a dropped/reordered block or changed
+source/revision/metric, and preserve table/form/image payloads without
+claiming those payloads received a text layout. Its only effects are checked
+host compilation, output and exit status; it neither authenticates Arena
+bytes nor performs native font measurement.
+
+Moon verified exact Earth commit
+`d3d6c710a9b29ea501eb12fca97888804c515cd2` in a separate worktree.
+The reused reflow paths match their declared `4a7380c5...` source exactly.
+The compiler bundle's complete `payload.sha256` verification exited 0 and
+`receipts/identity.txt` identifies `94dfd99b...`, Linux x86-64, Chez 10.4.1,
+producer run 38090627721 attempt 1.
+
+In a fresh staged source directory, the exact `bin/idric` entrypoint compiled
+`PrepaintReflowChecks.idric`, `PrepaintReflowMoonChecks.idric`, and
+`SourceReflowSmoke.idric`. Each generated executable was launched through the
+same bundle's absolute `bin/idric-env` entrypoint. The outputs were respectively
+`prepaint-source-reflow-cases=True`, `prepaint-moon-independent-cases=True`, and
+`source-reflow-unicode-offset-cases=True`, all with exit 0. The independent
+program covers mixed heading/text/link/table/form/image blocks, exact Unicode
+slice coverage, Han, CRLF, SHY, ZWSP, NBSP, combining marks, an overwide emoji
+ZWJ sequence, source/revision changes and width/manner/measurement records.
+
+A separate scratch production mutant changed the final adapter construction
+to use `reverse prepared`. The same independent check compiled successfully,
+printed `prepaint-moon-independent-cases=False` and exited 1. The maintained
+source was unchanged. The program also rejects dropped or reordered plans
+and a stale source or revision directly. Public vocabulary and whitespace
+checks passed. The first new fixture compile rejected the reserved word
+`total` as a parameter name; renaming that fixture parameter fixed it.
+
+These are independently reproduced host semantic results. They do not qualify
+bounded ingestion, native font measurement, Android/ART, Arena authentication,
+or physical C67/A1 execution.
diff --git a/examples/autogenerated/source-byte-decoding/SourceDecodingChecks.idric b/examples/autogenerated/source-byte-decoding/SourceDecodingChecks.idric
new file mode 100644
index 00000000..f17b3d84
--- /dev/null
+++ b/examples/autogenerated/source-byte-decoding/SourceDecodingChecks.idric
@@ -0,0 +1,131 @@
+module SourceDecodingChecks
+
+import Data.Text
+import Data.List
+import Data.Buffer
+import System
+import System.File
+import System.File.Buffer
+import IB.SourceDecoding
+
+index_identity : Text
+index_identity = "# Identifier: e56d49d9176e9a412283cf29ac9bd613f5620462f2a080a84eceaf974cfa18b7"
+
+position_in_digits : Char → Int → List Char → Maybe Int
+position_in_digits expected position [] = Nothing
+position_in_digits expected position (current :: rest) =
+ if current ≟ expected then Just position
+ else position_in_digits expected (position + 1) rest
+
+digit_value : Char → Maybe Int
+digit_value character = position_in_digits character 0 (unpack "0123456789")
+
+hex_value : Char → Maybe Int
+hex_value character =
+ case position_in_digits character 0 (unpack "0123456789abcdef") of
+ Just value ⇒ Just value
+ Nothing ⇒ position_in_digits character 0 (unpack "0123456789ABCDEF")
+
+digits_from : (Char → Maybe Int) → Int → Int → List Char → Maybe Int
+digits_from digit base value [] = Just value
+digits_from digit base value (character :: rest) = do
+ next ← digit character
+ digits_from digit base (value × base + next) rest
+
+decimal : Text → Maybe Int
+decimal value = case unpack value of
+ [] ⇒ Nothing
+ digits ⇒ digits_from digit_value 10 0 digits
+
+hexadecimal : Text → Maybe Int
+hexadecimal value = case unpack value of
+ '0' :: 'x' :: first :: rest ⇒ digits_from hex_value 16 0 (first :: rest)
+ _ ⇒ Nothing
+
+index_values : Int → List Text → Either Text (List Int)
+index_values expected [] =
+ if expected ≟ 128 then Right [] else Left "normative index has missing entries"
+index_values expected (line :: rest) =
+ case words line of
+ [] ⇒ index_values expected rest
+ "#" :: _ ⇒ index_values expected rest
+ pointer :: codepoint :: _ ⇒
+ case (decimal pointer, hexadecimal codepoint) of
+ (Just actual, Just scalar) ⇒
+ if actual ≟ expected && scalar >= 0 && scalar <= 0x10FFFF
+ then map (scalar ::) (index_values (expected + 1) rest)
+ else Left "normative index order or scalar invalid"
+ _ ⇒ Left "normative index numeric fields invalid"
+ _ ⇒ Left "normative index row invalid"
+
+assert_case : Text → Bool → IO ()
+assert_case label True = putStrLn ("PASS " ++ label)
+assert_case label False = die ("FAIL " ++ label)
+
+decoded_scalars : Text → List SourceOctet → Maybe (List Int)
+decoded_scalars label octets =
+ case decode_html_bytes label octets of
+ Left _ ⇒ Nothing
+ Right decoded ⇒ Just (map ord (unpack decoded.decoded_text))
+
+is_refused : Text → List SourceOctet → Bool
+is_refused label octets = case decode_html_bytes label octets of
+ Left _ ⇒ True
+ Right _ ⇒ False
+
+write_text_bytes : Text → Text → IO ()
+write_text_bytes path value = do
+ let count = stringByteLength value
+ Just buffer ← newBuffer count | Nothing ⇒ die "test UTF-8 allocation failed"
+ setString buffer 0 value
+ Right () ← writeBufferToFile path buffer count | Left _ ⇒ die "test UTF-8 write failed"
+ pure ()
+
+covering
+write_octet_fixture : Text → IO ()
+write_octet_fixture path = do
+ Just buffer ← newBuffer 256 | Nothing ⇒ die "test raw allocation failed"
+ fill buffer 0
+ Right () ← writeBufferToFile path buffer 256 | Left _ ⇒ die "test raw write failed"
+ pure ()
+ where
+ covering
+ fill : Buffer → Int → IO ()
+ fill buffer offset =
+ if offset >= 256 then pure () else do
+ setBits8 buffer offset (cast offset)
+ fill buffer (offset + 1)
+
+covering
+main : IO ()
+main = do
+ arguments ← getArgs
+ case arguments of
+ [_, index_path, all_octets_path, expected_utf8_path] ⇒ do
+ Right index ← readFile index_path | Left _ ⇒ die "normative index unreadable"
+ assert_case "normative index identity" (elem index_identity (lines index))
+ Right high_scalars ← pure (index_values 0 (lines index)) | Left reason ⇒ die reason
+ let expected_scalars = [0..127] ++ high_scalars
+ let octets : List SourceOctet = map cast (the (List Int) [0..255])
+ assert_case "all 256 octets match normative index"
+ (decoded_scalars "windows-1252" octets ≟ Just expected_scalars)
+ assert_case "NUL CR LF Euro quotes cafe NBSP and five C1 scalars"
+ (decoded_scalars "ISO-8859-1" [0,13,10,128,145,146,233,160,129,141,143,144,157] ≟
+ Just [0,13,10,0x20AC,0x2018,0x2019,0xE9,0xA0,0x81,0x8D,0x8F,0x90,0x9D])
+ assert_case "seventeen labels"
+ (all windows_1252_label ["ansi_x3.4-1968", "ascii", "cp1252", "cp819",
+ "csisolatin1", "ibm819", "iso-8859-1", "iso-ir-100", "iso8859-1",
+ "iso88591", "iso_8859-1", "iso_8859-1:1987", "l1", "latin1",
+ "us-ascii", "windows-1252", "x-cp1252"])
+ assert_case "ASCII trim and case" (windows_1252_label "\t ISO-8859-1\r\n")
+ assert_case "NBSP padding is not ASCII whitespace"
+ (not (windows_1252_label (pack [chr 160] ++ "windows-1252")))
+ assert_case "unknown label refused" (is_refused "utf-8" [65])
+ assert_case "UTF-8 BOM refuses wrong decoder" (is_refused "windows-1252" [0xEF,0xBB,0xBF,65])
+ assert_case "UTF-16 LE BOM refuses wrong decoder" (is_refused "windows-1252" [0xFF,0xFE,65,0])
+ assert_case "UTF-16 BE BOM refuses wrong decoder" (is_refused "windows-1252" [0xFE,0xFF,0,65])
+ assert_case "empty input decodes without acquiring admission" (decoded_scalars "latin1" [] ≟ Just [])
+ write_octet_fixture all_octets_path
+ write_text_bytes expected_utf8_path (pack (map chr expected_scalars))
+ putStrLn "PASS source byte decoding semantic controls"
+ _ ⇒ die "usage: source-decoding-checks NORMATIVE_INDEX ALL_OCTETS EXPECTED_UTF8"
diff --git a/examples/autogenerated/source-byte-decoding/attempt.md b/examples/autogenerated/source-byte-decoding/attempt.md
new file mode 100644
index 00000000..86404322
--- /dev/null
+++ b/examples/autogenerated/source-byte-decoding/attempt.md
@@ -0,0 +1,145 @@
+# Program attempt: source-byte-decoding
+
+Status: PASS for bounded host decoding and process checks; integration partial.
+
+## Purpose and intended behavior
+
+Decode a retained HTML source into a disposable UTF-8 representation without
+changing its original bytes, declared charset, generation or navigation
+admission. The current Google observation declares ISO-8859-1; HTML uses the
+WHATWG windows-1252 decoder for that label. Decoding alone cannot admit its
+redirected navigation or join the Android reader.
+
+## Type-system sketch
+
+The input domain is octets, not already-decoded Text. `SourceOctet` names the
+existing Bits8 raw boundary. `HtmlDecodedText` contains the exact supplied
+label, selected encoding, original octet count and decoded Unicode text.
+`decode_html_bytes : Text → List SourceOctet → Either Text HtmlDecodedText`
+is pure. The 17 windows-1252 labels use ASCII whitespace/case rules. All 256
+octets have defined mappings; CR/LF, NUL and C1 values remain unchanged where
+the index specifies them. HTML preprocessing belongs to the existing recovery
+owner. Recognized UTF-8/UTF-16 BOMs explicitly refuse in this bounded decoder
+instead of being misread as windows-1252.
+
+The command uses the compiler's binary Buffer interfaces, checks a bounded file
+size, the actual read count and EOF, then writes UTF-8 bytes through a binary
+buffer. Input is bounded to 4 MiB; this is not a streaming-ingestion repair.
+The command reports codepoint count separately from byte count.
+
+Grease owns source/derivative hashing, immutable input snapshots, producer exit
+checking and publication of a private staged directory by same-filesystem
+rename. It retains a caller-supplied source descriptor byte-for-byte, including
+source key, generation, original digest/count, declared charset and original
+navigation admission. Opaque extra descriptor fields are preserved as data.
+The derived receipt always says `reader_admission=NOT_GRANTED`; it cannot be
+used as an original UTF-8 `HtmlEvidence` or as an Arena admission receipt.
+
+## Specification and runtime boundary
+
+Primary specification: WHATWG Encoding names/labels and single-byte decoder;
+windows-1252 index identifier
+`e56d49d9176e9a412283cf29ac9bd613f5620462f2a080a84eceaf974cfa18b7`
+(2024-09-18), retained independently as a test fixture. In particular, 0x81,
+0x8D, 0x8F, 0x90 and 0x9D map to their C1 scalars; they are not replaced or
+rejected. HTML's BOM precedence is preserved by explicit refusal until BOM
+decoder paths exist.
+
+Use the verified Linux x86-64 Idriç host bundle at compiler commit
+`94dfd99bd3e376507fedc8611053b7173b2519f0`, archive SHA-256
+`0be57deab9410e8d4c09c7198bf7e8ee0ec3e24121f76640147efa4a53d120da`.
+No RefC, iconv, Python or Java decoder is a runtime substitute.
+
+## Planned acceptance
+
+Compile and execute actual Idriç code against all 256 bytes and the independent
+normative index; alias/ASCII-whitespace and BOM refusals; NUL/CRLF/Euro/quotes/
+café controls; real captured Google body identity; bad source count/hash and
+nonzero producer publication refusal. Known-bad Latin1 and replacement mutants
+must fail the same oracle. Preserve original admission and metadata.
+
+## Result, fallback and remaining boundary
+
+Fallback: none. DEX/ART,
+Android, canonical Arena admission, joined Prepaint and physical devices remain
+NOT_RUN. The existing native redirect-provenance and charset gates are unchanged.
+
+## Executed result
+
+The production module and binary-file command compiled with the exact verified
+94df host bundle. A fresh source staging directory received the current `src/`
+tree plus `SourceDecodingChecks.idric`, then executed these compiler arguments:
+
+```text
+SourceDecodingCommand.idric -o source-decoder
+SourceDecodingChecks.idric -o source-decoding-checks
+```
+
+`bin/idric` and the execution wrapper `bin/idric-env` were the absolute
+entrypoints inside that verified bundle, not ambient commands. Native Grease
+was the verified installed runtime with binary SHA-256
+`7e31cd05b7a9d8fb2a4a9e003a7f3fcb0159138506d17f0fb28da8cbe22aa85c`.
+Its inherited LeakSanitizer could not inspect this host's process-task data;
+`ASAN_OPTIONS=detect_leaks=0` was explicit for orchestration execution. Leak
+analysis is not an accepted result.
+
+Actual execution of the compiled checks and `tests/source-decoding.grease`
+passed with exit zero. The normative all-octet check matched all 256 scalars.
+The binary command produced exactly 401 UTF-8 bytes from the 256-octet fixture;
+independent byte checks retained the entire 128-byte ASCII prefix (including
+NUL and CR/LF) and verified Euro/C1, NBSP and café UTF-8 octets. Alias, ASCII
+trimming, BOM, unknown-label, size-bound, empty-input and input-as-output
+controls passed.
+
+Native process tests refused wrong source count/hash, a nonzero producer with
+partial output, and a producer which changed the frozen descriptor. No accepted
+derivative appeared; the earlier valid derivative remained exact. The real
+93,166-byte Google observation round-tripped byte-for-byte; its original
+ISO-8859-1 and redirect-count-one metadata were unchanged and the derived
+receipt still grants no reader admission. The test uses an explicit fixture
+identity rather than inventing a live Arena generation.
+
+`tests/source-decoding-mutations.grease` compiled two actual changed Idriç
+decoders in distinct temporary source roots. The naïve Latin1 decoder and the
+five-C1-slot replacement decoder both failed the same normative all-256 scalar
+assertion with nonzero exits. The real decoder passed that assertion.
+
+The final fresh command and check-program native `.so` hashes, source hashes,
+normative fixture and bounded outcomes are in `host-evidence.tsv`. Vocabulary
+and whitespace checks passed. Independent qualification normalized the fixture
+to the exact fetched primary bytes by removing an additional trailing newline,
+then reran the semantic, process and compiled-mutant checks. Its digest is
+`2c5fa192d566f92b8b9e6e116255b1f94016b4ece5b9dacb3b98be70b8c60795`;
+the index identifier and every numeric mapping are unchanged. See
+`moon-host.md` for the independent rebuild and publication controls.
+Existing `HtmlEvidence`, canonical-store and native reader admission source
+files are unchanged.
+
+The continuation recheck compared the maintained module, command and semantic
+check source byte-for-byte with the qualified staging tree, verified the
+recorded native program digests, then re-executed the full semantic/process
+controls and both freshly compiled mutant checks. They again passed with exit
+zero on this Ubuntu 24.04 x86-64 host. This repeated execution does not upgrade
+the Android, Arena or joined-navigation evidence boundary.
+
+## Earlier test-helper failures and language work
+
+The initial style-adjusted helper used Unicode `−`, which this 94df bundle
+parsed but could not resolve. Its source is retained under `initial/`. A
+subsequent reduced lookup attempt exposed that this pinned `Data.List` does not
+export the assumed `elemIndex`; that rejected assumption is also retained.
+The maintained helper uses a simple descriptive digit-position lookup, still
+entirely in Idriç. No external decoder or language substitution was introduced.
+
+Those compiler failures were not counted as acceptance. Final verification
+rebuilt from a fresh staging root and required successful compilation before
+running the new executable; earlier generated executables were not carried
+forward as final-head proof.
+
+The first remaining integration boundary is a verified decoded representation
+consumer which retains original byte identity and independently establishes
+reader admission. This diagnostic does not remove the missing redirect chain,
+implement bounded streaming, change the native original-UTF8 gate or execute
+the decoder under DEX/ART. The language bundle's missing canonical subtraction
+binding remains a separately identified compatibility gap; no language change
+was necessary to deliver this decoder slice.
diff --git a/examples/autogenerated/source-byte-decoding/host-evidence.tsv b/examples/autogenerated/source-byte-decoding/host-evidence.tsv
new file mode 100644
index 00000000..822621c1
--- /dev/null
+++ b/examples/autogenerated/source-byte-decoding/host-evidence.tsv
@@ -0,0 +1,35 @@
+schema ib-source-decoding-host-evidence-v1
+scope HOST_IDRIC_BYTES_AND_NATIVE_GREASE
+ib_starting_source ff8423697ef1d25140f4e77594b224ce7b87fef7
+compiler_source 94dfd99bd3e376507fedc8611053b7173b2519f0
+compiler_archive_sha256 0be57deab9410e8d4c09c7198bf7e8ee0ec3e24121f76640147efa4a53d120da
+grease_binary_sha256 7e31cd05b7a9d8fb2a4a9e003a7f3fcb0159138506d17f0fb28da8cbe22aa85c
+decoder_module_sha256 e3b81a3450878f23a9c5228ca6695e64692bae4367560e5abdabe6adaed327f5
+decoder_command_source_sha256 bb81e9512d5c211af777d7e0b5db978a806ce951410724693b2494153608d9ab
+decoder_native_program_sha256 8912f612d40b97845fc726a38064a3e606c92cec7099b4d86f420dbef4003d16
+semantic_check_native_program_sha256 66e4be6de322ad6972156b4fae3ac5e62a417d1221506119d0a54e6bfbfa72e5
+normative_index_sha256 2c5fa192d566f92b8b9e6e116255b1f94016b4ece5b9dacb3b98be70b8c60795
+all_256_scalars PASS
+all_octet_utf8_bytes 401
+binary_NUL_CR_LF_C1 PASS
+seventeen_labels_ASCII_trim_case PASS
+NBSP_label_padding REFUSED
+recognized_conflicting_BOMs REFUSED
+wrong_source_count_hash REFUSED_NO_DERIVATIVE
+nonzero_partial_producer REFUSED_NO_DERIVATIVE
+changed_frozen_descriptor REFUSED_NO_DERIVATIVE
+naive_Latin1_mutant REJECTED_NORMATIVE_SCALAR_ORACLE
+undefined_byte_replacement_mutant REJECTED_NORMATIVE_SCALAR_ORACLE
+actual_google_body_bytes 93166
+actual_google_body_sha256 f71e991ab87271e77255fe2d2454cb4cb401fe47cdf953ea550c6e0fcd8afeb4
+actual_google_derivative BYTE_IDENTICAL
+actual_google_declared_charset ISO-8859-1_UNCHANGED
+actual_google_redirect_count 1_UNCHANGED
+derived_reader_admission NOT_GRANTED
+existing_HtmlEvidence_native_Arena_gates UNCHANGED
+streaming_ingestion NOT_IMPLEMENTED
+joined_Prepaint NOT_RUN
+DEX_ART NOT_RUN
+Android_Binder NOT_RUN
+physical_C67 NOT_RUN
+physical_A1 NOT_RUN
diff --git a/examples/autogenerated/source-byte-decoding/initial/MissingDigitLookup.idric b/examples/autogenerated/source-byte-decoding/initial/MissingDigitLookup.idric
new file mode 100644
index 00000000..ecb0540f
--- /dev/null
+++ b/examples/autogenerated/source-byte-decoding/initial/MissingDigitLookup.idric
@@ -0,0 +1,10 @@
+module MissingDigitLookup
+
+import Data.Text
+import Data.List
+
+-- Reduced initial test-helper attempt: the pinned 94df library does not export
+-- elemIndex through Data.List. The maintained helper uses an explicit bounded
+-- position lookup instead; this file records the rejected library assumption.
+digit_value : Char → Maybe Int
+digit_value character = map cast (elemIndex character (unpack "0123456789"))
diff --git a/examples/autogenerated/source-byte-decoding/initial/MoonVerify.grease b/examples/autogenerated/source-byte-decoding/initial/MoonVerify.grease
new file mode 100644
index 00000000..2aec8ab5
--- /dev/null
+++ b/examples/autogenerated/source-byte-decoding/initial/MoonVerify.grease
@@ -0,0 +1,91 @@
+#!/usr/bin/env grease
+# Independent source-decoder rebuild and publication/admission controls.
+umask 077
+if (len(ARGV) !== 6) {
+ write -- 'usage: moon-verify.grease IDRIC GREASE GOOGLE_BODY GOOGLE_METADATA PRIMARY_INDEX NEW_EVIDENCE' >&2
+ exit 2
+}
+var compiler = ARGV[0]
+var grease = ARGV[1]
+var google = ARGV[2]
+var google_metadata = ARGV[3]
+var primary_index = ARGV[4]
+var evidence = ARGV[5]
+for path in (ARGV) {
+ if (not path.startsWith('/')) { write -- 'FAIL absolute input required' >&2; exit 2 }
+}
+if test -e $evidence { write -- 'FAIL refusing existing evidence' >&2; exit 2 }
+var example = $(dirname -- $0)
+var root = $(realpath -- "$example/../../..")
+var source = "$evidence/source"
+mkdir -p $source
+cp -R "$root/src/." "$source/"
+cp "$example/SourceDecodingChecks.idric" "$source/"
+sha256sum "$root/src/IB/SourceDecoding.idric" "$root/src/SourceDecodingCommand.idric" $primary_index > "$evidence/inputs.sha256"
+git -C $root rev-parse HEAD > "$evidence/source-ref.txt"
+var previous = $(pwd)
+cd $source
+$compiler SourceDecodingCommand.idric -o source-decoder > "$evidence/command-compile.log" 2>&1
+$compiler SourceDecodingChecks.idric -o source-decoding-checks > "$evidence/checks-compile.log" 2>&1
+cd $previous
+if rg -n '^[[:space:]]*(Error:|INTERNAL ERROR)' "$evidence/command-compile.log" "$evidence/checks-compile.log" {
+ write -- 'FAIL fresh compiler diagnostic' >&2
+ exit 1
+}
+var decoder = "$source/build/exec/source-decoder"
+var checks = "$source/build/exec/source-decoding-checks"
+sha256sum "${decoder}_app/source-decoder.so" "${checks}_app/source-decoding-checks.so" > "$evidence/programs.sha256"
+$checks $primary_index "$evidence/all.raw" "$evidence/expected.utf8" > "$evidence/primary-index.log"
+env GREASE=$grease $grease "$root/tests/source-decoding.grease" $checks $decoder $google $google_metadata > "$evidence/process.log" 2>&1
+env IDRIC=$compiler $grease "$root/tests/source-decoding-mutations.grease" > "$evidence/mutants.log" 2>&1
+
+var raw = "$evidence/all.raw"
+var descriptor = "$evidence/source.tsv"
+var hash = $(sha256sum $raw | cut -d ' ' -f 1)
+printf 'source_key\tmoon:source-generation\nsource_generation\t42-retained\nsha256\t%s\nbyte_count\t256\ncharset\tISO-8859-1\nnavigation_admitted\tYES\nredirect_count\t1\nopaque_origin\tretained provenance with spaces\n' $hash > $descriptor
+$grease "$root/bin/ib_decode_html_bytes.grease" $decoder $descriptor $raw "$evidence/yes-derived" > "$evidence/yes-result.log" 2>&1
+cmp $descriptor "$evidence/yes-derived/source.tsv"
+cmp "$evidence/expected.utf8" "$evidence/yes-derived/decoded.utf8"
+grep -Fx b'original_navigation_admitted\tYES' "$evidence/yes-derived/decode.tsv"
+grep -Fx b'reader_admission\tNOT_GRANTED' "$evidence/yes-derived/decode.tsv"
+grep -Fx b'opaque_origin\tretained provenance with spaces' "$evidence/yes-derived/source.tsv"
+printf '\033[32mPASS\033[0m source navigation YES and opaque provenance preserved without reader admission\n'
+
+cp $descriptor "$evidence/duplicate.tsv"
+printf 'charset\tISO-8859-1\n' >> "$evidence/duplicate.tsv"
+try { $grease "$root/bin/ib_decode_html_bytes.grease" $decoder "$evidence/duplicate.tsv" $raw "$evidence/duplicate-derived" > "$evidence/duplicate.log" 2>&1 }
+if (not _error.code) { write -- 'FAIL duplicate descriptor accepted' >&2; exit 1 }
+test ! -e "$evidence/duplicate-derived"
+grep -F 'malformed or incomplete source descriptor' "$evidence/duplicate.log"
+sed '/^source_generation\t/d' $descriptor > "$evidence/missing.tsv"
+try { $grease "$root/bin/ib_decode_html_bytes.grease" $decoder "$evidence/missing.tsv" $raw "$evidence/missing-derived" > "$evidence/missing.log" 2>&1 }
+if (not _error.code) { write -- 'FAIL missing source generation accepted' >&2; exit 1 }
+test ! -e "$evidence/missing-derived"
+grep -F 'malformed or incomplete source descriptor' "$evidence/missing.log"
+printf '\033[32mPASS\033[0m malformed descriptor refusals have no derivative\n'
+
+# A deterministic process fixture creates the winner after initial precheck.
+printf '#!%s\n' $grease > "$evidence/competing-producer"
+cat >> "$evidence/competing-producer" <<'EOF'
+var decoder = ENV.MOON_REAL_DECODER
+$decoder @ARGV
+var destination = ENV.MOON_COMPETING_DESTINATION
+mkdir $destination
+printf 'retained winner\n' > "$destination/winner"
+EOF
+chmod +x "$evidence/competing-producer"
+try {
+ env MOON_REAL_DECODER=$decoder MOON_COMPETING_DESTINATION="$evidence/competing-derived" \
+ $grease "$root/bin/ib_decode_html_bytes.grease" "$evidence/competing-producer" $descriptor $raw "$evidence/competing-derived" > "$evidence/competing.log" 2>&1
+}
+if (not _error.code) { write -- 'FAIL competing winner was reported as our publication' >&2; exit 1 }
+grep -F 'derivative publication conflicted' "$evidence/competing.log"
+test $(cat "$evidence/competing-derived/winner") = 'retained winner'
+test ! -e "$evidence/competing-derived/source.tsv"
+test ! -e "$evidence/competing-derived/decode.tsv"
+var leftovers = $(find $evidence -maxdepth 1 -name '.ib-decode.*' -print)
+if (leftovers !== '') { write -- 'FAIL discarded staging directory survived' >&2; exit 1 }
+cmp $descriptor "$evidence/yes-derived/source.tsv"
+cmp "$evidence/expected.utf8" "$evidence/yes-derived/decoded.utf8"
+printf '\033[32mPASS\033[0m competing winner and previous derivative survive; losing stage removed\n'
+printf 'fresh_Idric_build\tPASS\nprimary_index_all256\tPASS\nprovided_process_controls\tPASS\ncompiled_mutants_rejected\tPASS\noriginal_navigation_YES\tPRESERVED\nopaque_provenance\tPRESERVED\nreader_admission\tNOT_GRANTED\nmalformed_descriptor\tREFUSED\ncompeting_winner\tPRESERVED\nlosing_stage\tREMOVED\nART\tNOT_RUN\njoined_Prepaint\tNOT_RUN\nphysical_device\tNOT_RUN\n' > "$evidence/result.tsv"
diff --git a/examples/autogenerated/source-byte-decoding/initial/SourceDecodingChecks.idric b/examples/autogenerated/source-byte-decoding/initial/SourceDecodingChecks.idric
new file mode 100644
index 00000000..37440c8d
--- /dev/null
+++ b/examples/autogenerated/source-byte-decoding/initial/SourceDecodingChecks.idric
@@ -0,0 +1,131 @@
+module SourceDecodingChecks
+
+import Data.Text
+import Data.List
+import Data.Buffer
+import System
+import System.File
+import System.File.Buffer
+import IB.SourceDecoding
+
+index_identity : Text
+index_identity = "# Identifier: e56d49d9176e9a412283cf29ac9bd613f5620462f2a080a84eceaf974cfa18b7"
+
+digit_value : Char → Maybe Int
+digit_value character =
+ let scalar = ord character in
+ if scalar >= 48 && scalar <= 57 then Just (scalar − 48) else Nothing
+
+hex_value : Char → Maybe Int
+hex_value character =
+ case digit_value character of
+ Just value ⇒ Just value
+ Nothing ⇒
+ let scalar = ord character in
+ if scalar >= 65 && scalar <= 70 then Just (scalar − 55)
+ else if scalar >= 97 && scalar <= 102 then Just (scalar − 87)
+ else Nothing
+
+digits_from : (Char → Maybe Int) → Int → Int → List Char → Maybe Int
+digits_from digit base value [] = Just value
+digits_from digit base value (character :: rest) = do
+ next ← digit character
+ digits_from digit base (value × base + next) rest
+
+decimal : Text → Maybe Int
+decimal value = case unpack value of
+ [] ⇒ Nothing
+ digits ⇒ digits_from digit_value 10 0 digits
+
+hexadecimal : Text → Maybe Int
+hexadecimal value = case unpack value of
+ '0' :: 'x' :: first :: rest ⇒ digits_from hex_value 16 0 (first :: rest)
+ _ ⇒ Nothing
+
+index_values : Int → List Text → Either Text (List Int)
+index_values expected [] =
+ if expected ≟ 128 then Right [] else Left "normative index has missing entries"
+index_values expected (line :: rest) =
+ case words line of
+ [] ⇒ index_values expected rest
+ "#" :: _ ⇒ index_values expected rest
+ pointer :: codepoint :: _ ⇒
+ case (decimal pointer, hexadecimal codepoint) of
+ (Just actual, Just scalar) ⇒
+ if actual ≟ expected && scalar >= 0 && scalar <= 0x10FFFF
+ then map (scalar ::) (index_values (expected + 1) rest)
+ else Left "normative index order or scalar invalid"
+ _ ⇒ Left "normative index numeric fields invalid"
+ _ ⇒ Left "normative index row invalid"
+
+assert_case : Text → Bool → IO ()
+assert_case label True = putStrLn ("PASS " ++ label)
+assert_case label False = die ("FAIL " ++ label)
+
+decoded_scalars : Text → List SourceOctet → Maybe (List Int)
+decoded_scalars label octets =
+ case decode_html_bytes label octets of
+ Left _ ⇒ Nothing
+ Right decoded ⇒ Just (map ord (unpack decoded.decoded_text))
+
+is_refused : Text → List SourceOctet → Bool
+is_refused label octets = case decode_html_bytes label octets of
+ Left _ ⇒ True
+ Right _ ⇒ False
+
+write_text_bytes : Text → Text → IO ()
+write_text_bytes path value = do
+ let count = stringByteLength value
+ Just buffer ← newBuffer count | Nothing ⇒ die "test UTF-8 allocation failed"
+ setString buffer 0 value
+ Right () ← writeBufferToFile path buffer count | Left _ ⇒ die "test UTF-8 write failed"
+ pure ()
+
+covering
+write_octet_fixture : Text → IO ()
+write_octet_fixture path = do
+ Just buffer ← newBuffer 256 | Nothing ⇒ die "test raw allocation failed"
+ fill buffer 0
+ Right () ← writeBufferToFile path buffer 256 | Left _ ⇒ die "test raw write failed"
+ pure ()
+ where
+ covering
+ fill : Buffer → Int → IO ()
+ fill buffer offset =
+ if offset >= 256 then pure () else do
+ setBits8 buffer offset (cast offset)
+ fill buffer (offset + 1)
+
+covering
+main : IO ()
+main = do
+ arguments ← getArgs
+ case arguments of
+ [_, index_path, all_octets_path, expected_utf8_path] ⇒ do
+ Right index ← readFile index_path | Left _ ⇒ die "normative index unreadable"
+ assert_case "normative index identity" (elem index_identity (lines index))
+ Right high_scalars ← pure (index_values 0 (lines index)) | Left reason ⇒ die reason
+ let expected_scalars = [0..127] ++ high_scalars
+ let octets : List SourceOctet = map cast (the (List Int) [0..255])
+ assert_case "all 256 octets match normative index"
+ (decoded_scalars "windows-1252" octets ≟ Just expected_scalars)
+ assert_case "NUL CR LF Euro quotes cafe NBSP and five C1 scalars"
+ (decoded_scalars "ISO-8859-1" [0,13,10,128,145,146,233,160,129,141,143,144,157] ≟
+ Just [0,13,10,0x20AC,0x2018,0x2019,0xE9,0xA0,0x81,0x8D,0x8F,0x90,0x9D])
+ assert_case "seventeen labels"
+ (all windows_1252_label ["ansi_x3.4-1968", "ascii", "cp1252", "cp819",
+ "csisolatin1", "ibm819", "iso-8859-1", "iso-ir-100", "iso8859-1",
+ "iso88591", "iso_8859-1", "iso_8859-1:1987", "l1", "latin1",
+ "us-ascii", "windows-1252", "x-cp1252"])
+ assert_case "ASCII trim and case" (windows_1252_label "\t ISO-8859-1\r\n")
+ assert_case "NBSP padding is not ASCII whitespace"
+ (not (windows_1252_label (pack [chr 160] ++ "windows-1252")))
+ assert_case "unknown label refused" (is_refused "utf-8" [65])
+ assert_case "UTF-8 BOM refuses wrong decoder" (is_refused "windows-1252" [0xEF,0xBB,0xBF,65])
+ assert_case "UTF-16 LE BOM refuses wrong decoder" (is_refused "windows-1252" [0xFF,0xFE,65,0])
+ assert_case "UTF-16 BE BOM refuses wrong decoder" (is_refused "windows-1252" [0xFE,0xFF,0,65])
+ assert_case "empty input decodes without acquiring admission" (decoded_scalars "latin1" [] ≟ Just [])
+ write_octet_fixture all_octets_path
+ write_text_bytes expected_utf8_path (pack (map chr expected_scalars))
+ putStrLn "PASS source byte decoding semantic controls"
+ _ ⇒ die "usage: source-decoding-checks NORMATIVE_INDEX ALL_OCTETS EXPECTED_UTF8"
diff --git a/examples/autogenerated/source-byte-decoding/moon-host.md b/examples/autogenerated/source-byte-decoding/moon-host.md
new file mode 100644
index 00000000..1dbb59b6
--- /dev/null
+++ b/examples/autogenerated/source-byte-decoding/moon-host.md
@@ -0,0 +1,60 @@
+# Independent host qualification
+
+Prerequisite: decoder implementation commit
+`f6c1c195f71070014e7aa5b254beea20051f91e5`, tree
+`364684f10d4cfa95f5996a6c6cdb68b21d686955`.
+
+The settled semantics are an octet-to-Unicode decoding operation and a
+source-bound disposable derivative. Original navigation observations are
+preserved as data; derivative creation grants no reader admission, including
+when the original observation says YES. Grease owns process orchestration and
+same-filesystem no-clobber publication. The actual Idriç binary owns decoding.
+
+The independent check rebuilds the existing Idriç command and semantic oracle
+in a fresh source root, runs the provided controls and compiled mutants, then
+checks navigation-YES preservation, opaque descriptor retention, malformed
+descriptor refusal and a competing destination created after the initial
+precheck. The competing winner must survive and the staged loser must be
+removed. No decoder semantics or native admission gate is changed.
+
+The primary WHATWG index was fetched independently from
+https://encoding.spec.whatwg.org/index-windows-1252.txt. It has identifier
+`e56d49d9176e9a412283cf29ac9bd613f5620462f2a080a84eceaf974cfa18b7`,
+SHA-256 `2c5fa192d566f92b8b9e6e116255b1f94016b4ece5b9dacb3b98be70b8c60795`
+and 5,667 bytes. The initial retained fixture had one additional trailing
+newline; `diff -u` showed only that final blank line. The fixture is now exactly
+byte-identical to the independently fetched primary file. Its index identifier
+and every numeric mapping are unchanged. The fresh command must also pass
+against the fetched file.
+
+The first supplemental harness expected the adapter's post-rename conflict
+message. This host's `mv --no-clobber` refuses with exit 1 and “not replacing”
+before that message; the winner survived and the losing stage was removed.
+That failed harness is retained under `initial/MoonVerify.grease`. The updated
+check accepts either real conflict diagnostic while still requiring nonzero
+status, exact winner retention, no published loser, and removal of the stage.
+This is a corrected test assumption, not an implementation change.
+
+The complete fresh run at `moon-decoder-final-evidence` exited zero using the
+verified Idriç `94dfd99bd3e376507fedc8611053b7173b2519f0` bundle and native
+Grease executable SHA-256
+`7e31cd05b7a9d8fb2a4a9e003a7f3fcb0159138506d17f0fb28da8cbe22aa85c`.
+The archive digest and every `payload.sha256` entry were independently checked.
+`ASAN_OPTIONS=detect_leaks=0` was explicit for this host's orchestration;
+this is not leak-analysis acceptance. Both the primary and corrected retained
+index passed all 256 scalar checks; the existing alias, binary NUL/CRLF/C1,
+BOM, process/source-integrity, exact real-capture and two compiled-mutant
+controls passed. The supplemental checks passed as described above.
+
+The Idriç decoder and command source remain byte-identical to the prerequisite;
+their digests and the independently rebuilt programs are in `moon-host.tsv`.
+Chez program bytes depend on their build paths, so the independent program
+digests do not purport to equal the earlier staging-root digests. Vocabulary
+and full `git diff --check` passed with no fixture whitespace exception.
+
+These are Linux x86-64 host checks; DEX/ART, joined Prepaint/Arena admission,
+Android delivery and physical-device evidence remain NOT_RUN. No new blocking
+decoder capability was exposed. The next integration obligation remains a
+decoded-representation consumer that preserves original byte identity and
+independently establishes navigation/reader admission; this qualification does
+not supply the missing redirect chain or implement that consumer.
diff --git a/examples/autogenerated/source-byte-decoding/moon-host.tsv b/examples/autogenerated/source-byte-decoding/moon-host.tsv
new file mode 100644
index 00000000..bbd07e5b
--- /dev/null
+++ b/examples/autogenerated/source-byte-decoding/moon-host.tsv
@@ -0,0 +1,31 @@
+schema ib-source-decoding-independent-host-v1
+implementation_commit f6c1c195f71070014e7aa5b254beea20051f91e5
+implementation_tree 364684f10d4cfa95f5996a6c6cdb68b21d686955
+scope HOST_IDRIC_BYTES_AND_NATIVE_GREASE
+compiler_source 94dfd99bd3e376507fedc8611053b7173b2519f0
+compiler_archive_sha256 0be57deab9410e8d4c09c7198bf7e8ee0ec3e24121f76640147efa4a53d120da
+grease_binary_sha256 7e31cd05b7a9d8fb2a4a9e003a7f3fcb0159138506d17f0fb28da8cbe22aa85c
+decoder_module_sha256 e3b81a3450878f23a9c5228ca6695e64692bae4367560e5abdabe6adaed327f5
+decoder_command_source_sha256 bb81e9512d5c211af777d7e0b5db978a806ce951410724693b2494153608d9ab
+independent_decoder_program_sha256 1ea35627128729e92f9361e15c5c605bb8aca6f93b77fc6e553ebf20f7afa204
+independent_semantic_program_sha256 f6bd2f5ee695d9359f60435b83b7db56cabdd5eb100d83a172acb5ab5552bb21
+normative_index_primary_url https://encoding.spec.whatwg.org/index-windows-1252.txt
+normative_index_bytes 5667
+normative_index_sha256 2c5fa192d566f92b8b9e6e116255b1f94016b4ece5b9dacb3b98be70b8c60795
+retained_fixture_matches_primary BYTE_IDENTICAL
+all_256_scalars PASS
+provided_process_controls PASS
+compiled_mutants_rejected PASS
+original_navigation_YES PRESERVED
+opaque_source_provenance PRESERVED
+reader_admission NOT_GRANTED
+duplicate_or_missing_descriptor_fields REFUSED_NO_DERIVATIVE
+competing_destination_winner PRESERVED
+losing_stage REMOVED
+actual_google_body_bytes 93166
+actual_google_body_sha256 f71e991ab87271e77255fe2d2454cb4cb401fe47cdf953ea550c6e0fcd8afeb4
+actual_google_derivative BYTE_IDENTICAL
+joined_Prepaint_Arena NOT_RUN
+DEX_ART NOT_RUN
+Android_delivery NOT_RUN
+physical_device NOT_RUN
diff --git a/examples/autogenerated/source-byte-decoding/moon-verify.grease b/examples/autogenerated/source-byte-decoding/moon-verify.grease
new file mode 100644
index 00000000..0f45b844
--- /dev/null
+++ b/examples/autogenerated/source-byte-decoding/moon-verify.grease
@@ -0,0 +1,92 @@
+#!/usr/bin/env grease
+# Independent source-decoder rebuild and publication/admission controls.
+umask 077
+if (len(ARGV) !== 6) {
+ write -- 'usage: moon-verify.grease IDRIC GREASE GOOGLE_BODY GOOGLE_METADATA PRIMARY_INDEX NEW_EVIDENCE' >&2
+ exit 2
+}
+var compiler = ARGV[0]
+var grease = ARGV[1]
+var google = ARGV[2]
+var google_metadata = ARGV[3]
+var primary_index = ARGV[4]
+var evidence = ARGV[5]
+for path in (ARGV) {
+ if (not path.startsWith('/')) { write -- 'FAIL absolute input required' >&2; exit 2 }
+}
+if test -e $evidence { write -- 'FAIL refusing existing evidence' >&2; exit 2 }
+var example = $(dirname -- $0)
+var root = $(realpath -- "$example/../../..")
+var source = "$evidence/source"
+mkdir -p $source
+cmp $primary_index "$root/tests/fixtures/index-windows-1252.txt"
+cp -R "$root/src/." "$source/"
+cp "$example/SourceDecodingChecks.idric" "$source/"
+sha256sum "$root/src/IB/SourceDecoding.idric" "$root/src/SourceDecodingCommand.idric" $primary_index > "$evidence/inputs.sha256"
+git -C $root rev-parse HEAD > "$evidence/source-ref.txt"
+var previous = $(pwd)
+cd $source
+$compiler SourceDecodingCommand.idric -o source-decoder > "$evidence/command-compile.log" 2>&1
+$compiler SourceDecodingChecks.idric -o source-decoding-checks > "$evidence/checks-compile.log" 2>&1
+cd $previous
+if rg -n '^[[:space:]]*(Error:|INTERNAL ERROR)' "$evidence/command-compile.log" "$evidence/checks-compile.log" {
+ write -- 'FAIL fresh compiler diagnostic' >&2
+ exit 1
+}
+var decoder = "$source/build/exec/source-decoder"
+var checks = "$source/build/exec/source-decoding-checks"
+sha256sum "${decoder}_app/source-decoder.so" "${checks}_app/source-decoding-checks.so" > "$evidence/programs.sha256"
+$checks $primary_index "$evidence/all.raw" "$evidence/expected.utf8" > "$evidence/primary-index.log"
+env GREASE=$grease $grease "$root/tests/source-decoding.grease" $checks $decoder $google $google_metadata > "$evidence/process.log" 2>&1
+env IDRIC=$compiler $grease "$root/tests/source-decoding-mutations.grease" > "$evidence/mutants.log" 2>&1
+
+var raw = "$evidence/all.raw"
+var descriptor = "$evidence/source.tsv"
+var hash = $(sha256sum $raw | cut -d ' ' -f 1)
+printf 'source_key\tmoon:source-generation\nsource_generation\t42-retained\nsha256\t%s\nbyte_count\t256\ncharset\tISO-8859-1\nnavigation_admitted\tYES\nredirect_count\t1\nopaque_origin\tretained provenance with spaces\n' $hash > $descriptor
+$grease "$root/bin/ib_decode_html_bytes.grease" $decoder $descriptor $raw "$evidence/yes-derived" > "$evidence/yes-result.log" 2>&1
+cmp $descriptor "$evidence/yes-derived/source.tsv"
+cmp "$evidence/expected.utf8" "$evidence/yes-derived/decoded.utf8"
+grep -Fx b'original_navigation_admitted\tYES' "$evidence/yes-derived/decode.tsv"
+grep -Fx b'reader_admission\tNOT_GRANTED' "$evidence/yes-derived/decode.tsv"
+grep -Fx b'opaque_origin\tretained provenance with spaces' "$evidence/yes-derived/source.tsv"
+printf '\033[32mPASS\033[0m source navigation YES and opaque provenance preserved without reader admission\n'
+
+cp $descriptor "$evidence/duplicate.tsv"
+printf 'charset\tISO-8859-1\n' >> "$evidence/duplicate.tsv"
+try { $grease "$root/bin/ib_decode_html_bytes.grease" $decoder "$evidence/duplicate.tsv" $raw "$evidence/duplicate-derived" > "$evidence/duplicate.log" 2>&1 }
+if (not _error.code) { write -- 'FAIL duplicate descriptor accepted' >&2; exit 1 }
+test ! -e "$evidence/duplicate-derived"
+grep -F 'malformed or incomplete source descriptor' "$evidence/duplicate.log"
+sed '/^source_generation\t/d' $descriptor > "$evidence/missing.tsv"
+try { $grease "$root/bin/ib_decode_html_bytes.grease" $decoder "$evidence/missing.tsv" $raw "$evidence/missing-derived" > "$evidence/missing.log" 2>&1 }
+if (not _error.code) { write -- 'FAIL missing source generation accepted' >&2; exit 1 }
+test ! -e "$evidence/missing-derived"
+grep -F 'malformed or incomplete source descriptor' "$evidence/missing.log"
+printf '\033[32mPASS\033[0m malformed descriptor refusals have no derivative\n'
+
+# A deterministic process fixture creates the winner after initial precheck.
+printf '#!%s\n' $grease > "$evidence/competing-producer"
+cat >> "$evidence/competing-producer" <<'EOF'
+var decoder = ENV.MOON_REAL_DECODER
+$decoder @ARGV
+var destination = ENV.MOON_COMPETING_DESTINATION
+mkdir $destination
+printf 'retained winner\n' > "$destination/winner"
+EOF
+chmod +x "$evidence/competing-producer"
+try {
+ env MOON_REAL_DECODER=$decoder MOON_COMPETING_DESTINATION="$evidence/competing-derived" \
+ $grease "$root/bin/ib_decode_html_bytes.grease" "$evidence/competing-producer" $descriptor $raw "$evidence/competing-derived" > "$evidence/competing.log" 2>&1
+}
+if (not _error.code) { write -- 'FAIL competing winner was reported as our publication' >&2; exit 1 }
+grep -E 'not replacing|derivative publication conflicted' "$evidence/competing.log"
+test $(cat "$evidence/competing-derived/winner") = 'retained winner'
+test ! -e "$evidence/competing-derived/source.tsv"
+test ! -e "$evidence/competing-derived/decode.tsv"
+var leftovers = $(find $evidence -maxdepth 1 -name '.ib-decode.*' -print)
+if (leftovers !== '') { write -- 'FAIL discarded staging directory survived' >&2; exit 1 }
+cmp $descriptor "$evidence/yes-derived/source.tsv"
+cmp "$evidence/expected.utf8" "$evidence/yes-derived/decoded.utf8"
+printf '\033[32mPASS\033[0m competing winner and previous derivative survive; losing stage removed\n'
+printf 'fresh_Idric_build\tPASS\nprimary_index_all256\tPASS\nprovided_process_controls\tPASS\ncompiled_mutants_rejected\tPASS\noriginal_navigation_YES\tPRESERVED\nopaque_provenance\tPRESERVED\nreader_admission\tNOT_GRANTED\nmalformed_descriptor\tREFUSED\ncompeting_winner\tPRESERVED\nlosing_stage\tREMOVED\nART\tNOT_RUN\njoined_Prepaint\tNOT_RUN\nphysical_device\tNOT_RUN\n' > "$evidence/result.tsv"
diff --git a/src/HtmlPrepaintCommand.idric b/src/HtmlPrepaintCommand.idric
new file mode 100644
index 00000000..e1518b7c
--- /dev/null
+++ b/src/HtmlPrepaintCommand.idric
@@ -0,0 +1,34 @@
+module HtmlPrepaintCommand
+
+import IB.HtmlPrepaint
+import System
+import System.File
+
+-- Only Grease may invoke this command for a separately reopened and
+-- source-admitted body. This program never acquires or stores HTML sources.
+program_arguments : List String → List String
+program_arguments [] = []
+program_arguments (_ :: args) = args
+
+emit_prepaint : HtmlEvidence → String → IO ()
+emit_prepaint evidence html =
+ case convert_admitted_html evidence html of
+ Left reason ⇒ die ("html-prepaint: " ++ reason)
+ Right prepaint ⇒ putStr prepaint.wire
+
+covering
+main : IO ()
+main = do
+ arguments <- getArgs
+ case program_arguments arguments of
+ [source_id, generation, claimed_sha, reopened_sha,
+ claimed_bytes, reopened_bytes, requested, resolved,
+ mime, charset, status, body_path] ⇒ do
+ body_result <- readFile body_path
+ case body_result of
+ Left _ ⇒ die "html-prepaint: admitted body unreadable"
+ Right html ⇒ emit_prepaint
+ (HtmlSourceEvidence source_id generation claimed_sha reopened_sha
+ (cast claimed_bytes) (cast reopened_bytes)
+ requested resolved mime charset status True True) html
+ _ ⇒ die "usage: ib-html-prepaint SOURCE GENERATION CLAIM_SHA REOPEN_SHA CLAIM_COUNT REOPEN_COUNT REQUESTED FINAL MIME CHARSET STATUS ADMITTED_BODY_PATH"
diff --git a/src/HtmlPrepaintSmoke.idric b/src/HtmlPrepaintSmoke.idric
new file mode 100644
index 00000000..92c4bfab
--- /dev/null
+++ b/src/HtmlPrepaintSmoke.idric
@@ -0,0 +1,110 @@
+module HtmlPrepaintSmoke
+
+import IB.HtmlPrepaint
+import IB.HtmlLinks
+import IB.Strand
+import System
+
+source_sha : String
+source_sha = "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa"
+
+example : String
+example =
+ "A & B" ++
+ "First < example
Sixth
" ++
+ "beforeboldafter
" ++
+ "prefix link suffix
" ++
+ "smile: 🙂 RTL: שלום é
" ++
+ "" ++
+ "Unsafe" ++
+ "
" ++
+ ""
+
+evidence : HtmlEvidence
+evidence =
+ HtmlSourceEvidence "arena:fixture-example" "generation-1"
+ source_sha source_sha 500 500
+ "https://example.com/docs/page" "https://example.com/docs/page"
+ "text/html" "utf-8" "200" True True
+
+base_and_omissions : String
+base_and_omissions =
+ "" ++
+ "FirstSecond
A
BQuery" ++
+ "
"
+
+base_projection : String
+base_projection =
+ case convert_admitted_html evidence base_and_omissions of
+ Left reason ⇒ "REFUSED:" ++ reason
+ Right produced ⇒ produced.wire
+
+bad_evidence : HtmlEvidence
+bad_evidence =
+ HtmlSourceEvidence "arena:fixture-example" "generation-1"
+ source_sha "bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb"
+ 500 500 "https://example.com/" "https://example.com/"
+ "text/html" "utf-8" "200" True True
+
+contains : List Char → List Char → Bool
+contains needle [] = needle == []
+contains needle value@(_ :: rest) =
+ starts_with needle value || contains needle rest
+ where
+ starts_with : List Char → List Char → Bool
+ starts_with [] _ = True
+ starts_with (_ :: _) [] = False
+ starts_with (x :: xs) (y :: ys) =
+ x == y && starts_with xs ys
+
+has : String → String → Bool
+has sub value = contains (unpack sub) (unpack value)
+
+refused : Either String HtmlPrepaintResult → Bool
+refused (Left _) = True
+refused (Right _) = False
+
+check : List (String, Bool) → IO Bool
+check [] = pure True
+check ((name, passed) :: rest) = do
+ putStrLn (name ++ "=" ++ show passed)
+ more <- check rest
+ pure (passed && more)
+
+main : IO ()
+main =
+ case convert_admitted_html evidence example of
+ Left reason ⇒ die ("html-prepaint=" ++ reason)
+ Right output ⇒ do
+ let wire = output.wire
+ let tests =
+ [ ("version1", has "ib-prepaint\t1\nrevision\t0\tcomplete\n" wire)
+ , ("heading-one", has "heading\t1\tFirst < example\n" wire)
+ , ("heading-six", has "heading\t6\tSixth\n" wire)
+ , ("nested-inline", has "text\tbeforeboldafter\n" wire)
+ , ("relative-link", has "link\tlink\thttps://example.com/other?q=1\n" wire)
+ , ("paragraph-before-link", has "text\tprefix\n" wire)
+ , ("paragraph-after-link", has "text\tsuffix\n" wire)
+ , ("non-bmp", has "🙂" wire)
+ , ("rtl-preserved", has "שלום" wire)
+ , ("numeric-combining", has "é" wire)
+ , ("table-row", has "row\tA\tB\n" wire)
+ , ("unsafe-no-link", not (has "link\tUnsafe" wire))
+ , ("image-unretrieved", has "Image pending acquisition: diagram — caption" wire)
+ , ("script-excluded", not (has "hidden" wire))
+ , ("digest-mismatch-refused", refused (convert_admitted_html bad_evidence example))
+ , ("fragment", resolve_html_reference "https://example.com/a?q=1#old" "#new" ==
+ Just "https://example.com/a?q=1#new")
+ , ("query", resolve_html_reference "https://example.com/a?q=1" "?q=2" ==
+ Just "https://example.com/a?q=2")
+ , ("unsafe-scheme", resolve_html_reference "https://example.com/" "javascript:bad" ==
+ Nothing)
+ , ("html-base-query", has "link\tQuery\thttps://example.org/docs/?q=3\n" base_projection)
+ , ("implied-heading-two", has "heading\t2\tFirst\n" base_projection)
+ , ("implied-heading-three", has "heading\t3\tSecond\n" base_projection)
+ , ("implied-paragraph", has "text\tA\n" base_projection && has "text\tB\n" base_projection)
+ , ("list-alpha", has "text\tAlpha\n" base_projection)
+ , ("list-beta", has "text\tBeta\n" base_projection)
+ ]
+ okay <- check tests
+ if okay then pure () else exitFailure
diff --git a/src/IB/HtmlLinks.idric b/src/IB/HtmlLinks.idric
new file mode 100644
index 00000000..a8ab2c22
--- /dev/null
+++ b/src/IB/HtmlLinks.idric
@@ -0,0 +1,151 @@
+module IB.HtmlLinks
+
+import IB.Information
+
+-- Bounded by caller/admission; explicit conversion failures are returned.
+
+-- This is a deliberately bounded address resolver for admitted HTML links.
+-- It does not decode percent escapes or extend ICU's supported URL schemes.
+strip_prefix : List Char → List Char → Maybe (List Char)
+strip_prefix [] rest = Just rest
+strip_prefix (_ :: _) [] = Nothing
+strip_prefix (wanted :: following) (actual :: rest) =
+ if wanted == actual then strip_prefix following rest else Nothing
+
+starts : String → String → Bool
+starts sought_prefix value =
+ case strip_prefix (unpack sought_prefix) (unpack value) of
+ Nothing ⇒ False
+ Just _ ⇒ True
+
+before_character : Char → List Char → List Char
+before_character delimiter [] = []
+before_character delimiter (value :: rest) =
+ if value == delimiter then [] else value :: before_character delimiter rest
+
+before_either : List Char → List Char
+before_either [] = []
+before_either (value :: rest) =
+ if value == '/' || value == '?' || value == '#'
+ then [] else value :: before_either rest
+
+after_count : Nat → List Char → List Char
+after_count Z characters = characters
+after_count (S count) [] = []
+after_count (S count) (_ :: rest) = after_count count rest
+
+public export
+http_origin : String → Maybe String
+http_origin url =
+ if not (cheap_http_url url)
+ then Nothing
+ else if starts "https://" url
+ then Just ("https://" ++ pack (before_either (after_count 8 (unpack url))))
+ else if starts "http://" url
+ then Just ("http://" ++ pack (before_either (after_count 7 (unpack url))))
+ else Nothing
+
+url_tail : String → String → String
+url_tail origin url = pack (after_count (length (unpack origin)) (unpack url))
+
+strip_fragment : String → String
+strip_fragment value = pack (before_character '#' (unpack value))
+
+strip_query : String → String
+strip_query value = pack (before_character '?' (unpack value))
+
+url_path : String → String → String
+url_path origin url =
+ let rest = url_tail origin url in
+ case unpack rest of
+ '/' :: _ ⇒ strip_query (strip_fragment rest)
+ _ ⇒ "/"
+
+-- Directory of the final URL path, ending at its last slash.
+-- Removing the last *character* rather than the last segment breaks ../ links.
+at_last_slash : List Char → List Char
+at_last_slash [] = []
+at_last_slash ('/' :: rest) = '/' :: rest
+at_last_slash (_ :: rest) = at_last_slash rest
+
+parent_path : List Char → String
+parent_path path_chars = pack (reverse (at_last_slash (reverse path_chars)))
+
+-- Segment operations keep the origin outside the path stack.
+segments : List Char → List Char → List String → List String
+segments [] current done = reverse (pack (reverse current) :: done)
+segments ('/' :: rest) current done =
+ segments rest [] (pack (reverse current) :: done)
+segments (value :: rest) current done = segments rest (value :: current) done
+
+normalise : List String → List String → List String
+normalise [] stack = reverse stack
+normalise ("." :: rest) stack = normalise rest stack
+normalise (".." :: rest) [] = normalise rest []
+normalise (".." :: rest) (_ :: stack) = normalise rest stack
+normalise (value :: rest) stack = normalise rest (value :: stack)
+
+join_segments : List String → String
+join_segments [] = ""
+join_segments [value] = value
+join_segments (value :: rest) = value ++ "/" ++ join_segments rest
+
+split_path_suffix : List Char → List Char → (String, String)
+split_path_suffix [] path = (pack (reverse path), "")
+split_path_suffix chars@('?' :: _) path = (pack (reverse path), pack chars)
+split_path_suffix chars@('#' :: _) path = (pack (reverse path), pack chars)
+split_path_suffix (value :: rest) path = split_path_suffix rest (value :: path)
+
+path_normalised : String → String
+path_normalised path =
+ case unpack path of
+ '/' :: rest ⇒ "/" ++ join_segments (normalise (segments rest [] []) [])
+ rest ⇒ "/" ++ join_segments (normalise (segments rest [] []) [])
+
+has_scheme_colon : List Char → Bool
+has_scheme_colon [] = False
+has_scheme_colon ('/' :: _) = False
+has_scheme_colon ('?' :: _) = False
+has_scheme_colon ('#' :: _) = False
+has_scheme_colon (':' :: _) = True
+has_scheme_colon (_ :: rest) = has_scheme_colon rest
+
+checked_url : String → Maybe String
+checked_url address =
+ if cheap_http_url address then Just address else Nothing
+
+directory_for : String → String → String → String
+directory_for origin base relative =
+ if starts "/" relative
+ then ""
+ else parent_path (unpack (url_path origin base))
+
+relative_address : String → String → String → String
+relative_address origin base reference =
+ let (relative_path, suffix) = split_path_suffix (unpack reference) [] in
+ origin ++ path_normalised (directory_for origin base reference ++ relative_path) ++ suffix
+
+scheme_for : String → String
+scheme_for base = if starts "https://" base then "https:" else "http:"
+
+-- Returns a navigation *candidate*. ICU and navigation admission still decide
+-- whether another retrieval occurs; the renderer must never fetch a link.
+public export
+resolve_html_reference : String → String → Maybe String
+resolve_html_reference base reference =
+ if not (cheap_http_url base) || reference == ""
+ then Nothing
+ else if cheap_http_url reference
+ then Just reference
+ else if starts "//" reference
+ then checked_url (scheme_for base ++ reference)
+ else if has_scheme_colon (unpack reference)
+ then Nothing
+ else do
+ origin ← http_origin base
+ let current = strip_fragment base
+ if starts "#" reference
+ then checked_url (current ++ reference)
+ else if starts "?" reference
+ then checked_url (strip_query current ++ reference)
+ else checked_url (relative_address origin base reference)
diff --git a/src/IB/HtmlPrepaint.idric b/src/IB/HtmlPrepaint.idric
new file mode 100644
index 00000000..d61ccf16
--- /dev/null
+++ b/src/IB/HtmlPrepaint.idric
@@ -0,0 +1,243 @@
+module IB.HtmlPrepaint
+
+import IB.Information
+import IB.RecoveredInformation
+import IB.Strand
+import IB.Prepaint
+import IB.Prepaint.Version1
+import IB.HtmlLinks
+
+-- Bounded by caller/admission; explicit conversion failures are returned.
+
+-- A producer supplies this ONLY after checking the exact committed Arena range.
+-- Claimed and reopened digest/length are independent inputs, not a hash of an
+-- unverified String. Source admission and byte-level SHA-256 belong to Grease /
+-- the canonical Arena reader; semantic extraction belongs here.
+public export
+record HtmlEvidence where
+ constructor HtmlSourceEvidence
+ source_key : String
+ source_generation : String
+ claimed_sha256 : String
+ reopened_sha256 : String
+ claimed_bytes : Integer
+ reopened_bytes : Integer
+ requested_url : String
+ resolved_url : String
+ mime_type : String
+ charset : String
+ http_status : String
+ utf8_decoded : Bool
+ fully_acquired : Bool
+
+public export
+record PendingImage where
+ constructor NeedImageAcquisition
+ image_url : String
+ alternate : String
+ caption : String
+ image_source_key : String
+
+public export
+record HtmlPrepaintResult where
+ constructor MadeHtmlPrepaint
+ evidence : HtmlEvidence
+ recovered : RecoveredDocumentLog
+ information : InformationView
+ strand : Strand
+ revision : PrepaintRevision
+ wire : String
+ pending_images : List PendingImage
+ limitations : List String
+
+is_hex_character : Char → Bool
+is_hex_character character =
+ let number : Integer = cast (ord character) in
+ (number >= 48 && number <= 57) || (number >= 97 && number <= 102)
+
+is_digest : String → Bool
+is_digest value =
+ length (unpack value) == 64 && all is_hex_character (unpack value)
+
+metadata_safe : String → Bool
+metadata_safe value =
+ value /= "" && length (unpack value) <= 256 &&
+ not (elem '\t' (unpack value)) &&
+ not (elem '\n' (unpack value)) &&
+ not (elem '\r' (unpack value))
+
+public export
+source_admission_reason : HtmlEvidence → Maybe String
+source_admission_reason e =
+ if not (metadata_safe e.source_key) || not (metadata_safe e.source_generation)
+ then Just "bad-source-identity"
+ else if not (is_digest e.claimed_sha256) || e.claimed_sha256 /= e.reopened_sha256
+ then Just "missing-or-mismatched-sha256"
+ else if e.claimed_bytes <= 0 || e.claimed_bytes > 4194304 ||
+ e.claimed_bytes /= e.reopened_bytes
+ then Just "bad-reopened-byte-count"
+ else if e.mime_type /= "text/html" &&
+ e.mime_type /= "text/html; charset=utf-8" &&
+ e.mime_type /= "text/html; charset=UTF-8"
+ then Just "unsupported-mime"
+ else if e.charset /= "utf-8" && e.charset /= "UTF-8"
+ then Just "unsupported-charset"
+ else if e.http_status /= "200"
+ then Just "unadmitted-http-status"
+ else if not e.utf8_decoded
+ then Just "invalid-utf8"
+ else if not e.fully_acquired
+ then Just "incomplete-or-stale-source"
+ else if not (cheap_http_url e.requested_url) || not (cheap_http_url e.resolved_url)
+ then Just "unverified-requested-or-resolved-url"
+ else Nothing
+
+first_html_base : List DocumentEvent → Maybe String
+first_html_base [] = Nothing
+first_html_base (StartTag "base" tag :: events) =
+ case attribute_value "href" tag of
+ Nothing ⇒ first_html_base events
+ Just value ⇒ Just (decode_html_entities value)
+first_html_base (_ :: events) = first_html_base events
+
+link_base : String → RecoveredDocumentLog → (String, List String)
+link_base resolved log =
+ case first_html_base (document_log_events log) of
+ Nothing ⇒ (resolved, [])
+ Just href ⇒
+ case resolve_html_reference resolved href of
+ Nothing ⇒ (resolved, ["unsupported-html-base"])
+ Just value ⇒ (value, [])
+
+heading_number : String → Maybe HeadingLevel
+heading_number "h1" = heading_level 1
+heading_number "h2" = heading_level 2
+heading_number "h3" = heading_level 3
+heading_number "h4" = heading_level 4
+heading_number "h5" = heading_level 5
+heading_number "h6" = heading_level 6
+heading_number _ = Nothing
+
+checked_link : String → String → String →
+ (List InformationBlock, List String)
+checked_link base label href =
+ case resolve_html_reference base href of
+ Nothing ⇒ ([IB.Strand.TextBlock label], ["unusable-link:" ++ href])
+ Just url ⇒
+ case link_reference url of
+ Nothing ⇒ ([IB.Strand.TextBlock label], ["empty-link"])
+ Just ref ⇒ ([IB.Strand.Link label ref], [])
+
+request_image : HtmlEvidence → String → String → String → String → List PendingImage
+request_image evidence base address alternate caption =
+ case resolve_html_reference base address of
+ Nothing ⇒ []
+ Just absolute_address ⇒
+ [NeedImageAcquisition absolute_address alternate caption evidence.source_key]
+
+image_limitations : String → List PendingImage → List String
+image_limitations original [] = ["unsupported-image-reference:" ++ original]
+image_limitations original (_ :: _) = ["image-requires-separate-admission:" ++ original]
+
+image_navigation : String → String → String →
+ (List InformationBlock, List String)
+image_navigation base label "" = ([], [])
+image_navigation base label target = checked_link base label target
+
+map_item : HtmlEvidence → String → InformationItem →
+ (List InformationBlock, List PendingImage, List String)
+map_item e base (IB.Information.Heading text) =
+ ([IB.Strand.Heading Heading1 text], [], ["legacy-heading-level-unknown"])
+map_item e base (HeadingAt name text) =
+ case heading_number name of
+ Nothing ⇒ ([IB.Strand.TextBlock text], [], ["invalid-heading-level"])
+ Just level ⇒ ([IB.Strand.Heading level text], [], [])
+map_item e base (IB.Information.TextBlock text) =
+ ([IB.Strand.TextBlock text], [], [])
+map_item e base (FigureCaption caption) =
+ ([IB.Strand.TextBlock ("Figure caption: " ++ caption)], [],
+ ["orphaned-figure-caption"])
+map_item e base (IB.Information.Link text href) =
+ let (blocks, notes) = checked_link base text href in
+ (blocks, [], notes)
+map_item e base (IB.Information.Form description action) =
+ ([IB.Strand.TextBlock ("Form (submission unavailable): " ++ description)],
+ [], ["form-submission-unavailable:" ++ action])
+map_item e base (IB.Information.TableRow []) =
+ ([], [], ["empty-table-row"])
+map_item e base (IB.Information.TableRow (first :: cells)) =
+ ([IB.Strand.TableRow (table_row first cells)], [], [])
+map_item e base (IB.Information.Image url alt caption destination) =
+ let text = if alt == "" then "Unretrieved image" else alt in
+ let label = if caption == "" then text else text ++ " — " ++ caption in
+ let pending = request_image e base url alt caption in
+ let image_notes = image_limitations url pending in
+ let (linked, link_notes) = image_navigation base label destination in
+ (IB.Strand.TextBlock ("Image pending acquisition: " ++ label) :: linked,
+ pending, image_notes ++ link_notes)
+
+map_items : HtmlEvidence → String → List InformationItem →
+ (List InformationBlock, List PendingImage, List String)
+map_items e base [] = ([], [], [])
+map_items e base
+ (IB.Information.Image source alt caption target :: FigureCaption figure_text :: rest) =
+ let effective_caption = if figure_text == "" then caption else figure_text in
+ let (blocks, images, notes) =
+ map_item e base (IB.Information.Image source alt effective_caption target) in
+ let (other_blocks, other_images, other_notes) = map_items e base rest in
+ (blocks ++ other_blocks, images ++ other_images, notes ++ other_notes)
+map_items e base (item :: rest) =
+ let (block, images, notes) = map_item e base item in
+ let (other_blocks, other_images, other_notes) = map_items e base rest in
+ (block ++ other_blocks, images ++ other_images, notes ++ other_notes)
+
+unsupported_event : DocumentEvent → List String
+unsupported_event (StartTag name _) =
+ if elem name ["script", "style", "template", "canvas", "video",
+ "audio", "svg", "iframe", "object"]
+ then ["excluded-or-unsupported-element:" ++ name] else []
+unsupported_event _ = []
+
+unsupported_events : List DocumentEvent → List String
+unsupported_events [] = []
+unsupported_events (event :: rest) =
+ unsupported_event event ++ unsupported_events rest
+
+source_reference_text : HtmlEvidence → String
+source_reference_text evidence =
+ evidence.source_key ++ ";generation=" ++ evidence.source_generation ++
+ ";sha256=" ++ evidence.claimed_sha256
+
+make_html_strand : HtmlEvidence → InformationView →
+ List InformationBlock → Maybe Strand
+make_html_strand evidence view blocks = do
+ source_id ← nonempty_text (source_reference_text evidence)
+ requested ← requested_address evidence.requested_url
+ resolved ← resolved_address evidence.resolved_url
+ let source = Source source_id HtmlSource CompleteSource
+ let heading_title = if view_title view == "" then Nothing else Just (view_title view)
+ pure (MakeStrand source requested resolved heading_title blocks)
+
+public export
+convert_admitted_html : HtmlEvidence → String → Either String HtmlPrepaintResult
+convert_admitted_html admission html =
+ case source_admission_reason admission of
+ Just refusal ⇒ Left refusal
+ Nothing ⇒
+ let log = recover_document_log admission.source_key html in
+ let view = information_from_log admission.requested_url admission.resolved_url log in
+ let (base, base_notes) = link_base admission.resolved_url log in
+ let (blocks, images, notes) = map_items admission base (view_items view) in
+ if length blocks > 4096
+ then Left "prepaint-block-budget-exceeded"
+ else
+ case make_html_strand admission view blocks of
+ Nothing ⇒ Left "invalid-source-strand"
+ Just strand ⇒
+ let revision = prepaint_from_strand first_revision CompleteRevision strand in
+ case serialize_version1 [revision] of
+ Nothing ⇒ Left "version1-serialization-refused"
+ Just wire ⇒
+ Right (MadeHtmlPrepaint admission log view strand revision wire
+ images (base_notes ++ notes ++
+ unsupported_events (document_log_events log)))
diff --git a/src/IB/Information.idric b/src/IB/Information.idric
index ee53bef5..1821310c 100644
--- a/src/IB/Information.idric
+++ b/src/IB/Information.idric
@@ -5,6 +5,8 @@ import Data.Text
public export
data InformationItem
= Heading Text
+ | HeadingAt Text Text
+ | FigureCaption Text
| TextBlock Text
| Link Text Text
| Image Text Text Text Text
@@ -42,6 +44,7 @@ data Capture
= NoCapture
| CaptureTitle
| CaptureHeading Text
+ | CaptureCaption
| CaptureText Text
| CaptureLink Text Bool Capture
| CaptureForm Text
@@ -67,10 +70,91 @@ collapse_space_chars previous_space (value :: rest) =
else ' ' :: collapse_space_chars True rest
else value :: collapse_space_chars False rest
+-- Decode only explicit, bounded HTML character references. Unknown names
+-- and malformed numerical references remain visible, not fabricated Unicode.
+entity_digit : Char → Maybe Integer
+entity_digit digit =
+ let value : Integer = cast (ord digit) in
+ if value >= 48 && value <= 57 then Just (value - 48)
+ else if value >= 65 && value <= 70 then Just (value - 55)
+ else if value >= 97 && value <= 102 then Just (value - 87)
+ else Nothing
+
+entity_number : Integer → Integer → List Char → Maybe Integer
+entity_number base number [] =
+ if number > 0 && number <= 1114111 &&
+ not (number >= 55296 && number <= 57343)
+ then Just number else Nothing
+entity_number base number (digit :: rest) =
+ case entity_digit digit of
+ Nothing ⇒ Nothing
+ Just value ⇒
+ if value >= base || number > 1114111
+ then Nothing
+ else entity_number base (number * base + value) rest
+
+named_character : Text → Maybe Char
+named_character "amp" = Just '&'
+named_character "lt" = Just '<'
+named_character "gt" = Just '>'
+named_character "quot" = Just '"'
+named_character "apos" = Just '\''
+named_character "nbsp" = Just ' '
+named_character "copy" = Just '©'
+named_character "reg" = Just '®'
+named_character "ndash" = Just '–'
+named_character "mdash" = Just '—'
+named_character "hellip" = Just '…'
+named_character "bull" = Just '•'
+named_character "times" = Just '×'
+named_character "minus" = Just '−'
+named_character "alpha" = Just 'α'
+named_character "beta" = Just 'β'
+named_character "pi" = Just 'π'
+named_character _ = Nothing
+
+entity_character : Text → Maybe Char
+entity_character name =
+ case unpack name of
+ '#' :: 'x' :: digits ⇒ map (chr . cast) (entity_number 16 0 digits)
+ '#' :: 'X' :: digits ⇒ map (chr . cast) (entity_number 16 0 digits)
+ '#' :: digits ⇒ map (chr . cast) (entity_number 10 0 digits)
+ _ ⇒ named_character name
+
+scan_entity : Nat → List Char → List Char → Maybe (Text, List Char)
+scan_entity Z collected remaining = Nothing
+scan_entity (S fuel) collected [] = Nothing
+scan_entity (S fuel) collected (';' :: rest) = Just (pack (reverse collected), rest)
+scan_entity (S fuel) collected (value :: rest) =
+ scan_entity fuel (value :: collected) rest
+
+-- Each recursive call consumes one fuel unit even if an entity scan
+-- discards several input characters. This is total regardless of the scanner
+-- implementation, and source-length fuel suffices for every input code point.
+decode_entity_chars_fuel : Nat → List Char → List Char
+decode_entity_chars_fuel Z remaining = remaining
+decode_entity_chars_fuel (S fuel) [] = []
+decode_entity_chars_fuel (S fuel) ('&' :: rest) =
+ case scan_entity 16 [] rest of
+ Nothing ⇒ '&' :: decode_entity_chars_fuel fuel rest
+ Just (name, remaining) ⇒
+ case entity_character name of
+ Nothing ⇒ '&' :: decode_entity_chars_fuel fuel rest
+ Just value ⇒ value :: decode_entity_chars_fuel fuel remaining
+decode_entity_chars_fuel (S fuel) (value :: rest) =
+ value :: decode_entity_chars_fuel fuel rest
+
+decode_entity_chars : List Char → List Char
+decode_entity_chars chars = decode_entity_chars_fuel (length chars) chars
+
+public export
+decode_html_entities : Text → Text
+decode_html_entities value = pack (decode_entity_chars (unpack value))
+
public export
clean_text : Text → Text
clean_text text =
- let collapsed = collapse_space_chars False (unpack text) in
+ let collapsed = collapse_space_chars False (decode_entity_chars (unpack text)) in
let left_trimmed = drop_space_chars collapsed in
pack (reverse (drop_space_chars (reverse left_trimmed)))
@@ -245,27 +329,36 @@ read_attribute_value chars =
value ⇒ Just (pack (read_unquoted value))
_ ⇒ Nothing
-seek_attribute_fuel : Number → List Char → List Char → Maybe Text
-seek_attribute_fuel Z wanted chars = Nothing
-seek_attribute_fuel (S fuel) wanted [] = Nothing
-seek_attribute_fuel (S fuel) wanted chars@(_ :: rest) =
- if starts_with_chars wanted chars
+starts_with_attribute : List Char → List Char → Bool
+starts_with_attribute [] chars = True
+starts_with_attribute (_ :: _) [] = False
+starts_with_attribute (wanted :: wanted_rest) (actual :: rest) =
+ wanted == ascii_lower_char actual &&
+ starts_with_attribute wanted_rest rest
+
+-- Require the beginning of a complete HTML attribute name, not a suffix of
+-- data-href or characters inside a quoted attribute. Preserve value case.
+seek_attribute_fuel : Number → Bool → List Char → List Char → Maybe Text
+seek_attribute_fuel Z boundary wanted chars = Nothing
+seek_attribute_fuel (S fuel) boundary wanted [] = Nothing
+seek_attribute_fuel (S fuel) boundary wanted chars@(value :: rest) =
+ if boundary && starts_with_attribute wanted chars
then case read_attribute_value (drop_chars (length wanted) chars) of
Just found ⇒ Just found
- Nothing ⇒ seek_attribute_fuel fuel wanted rest
- else seek_attribute_fuel fuel wanted rest
+ Nothing ⇒ seek_attribute_fuel fuel (is_space_char value) wanted rest
+ else seek_attribute_fuel fuel (is_space_char value) wanted rest
public export
attribute_value : Text → Text → Maybe Text
attribute_value name tag =
let chars = tag_remainder tag in
- seek_attribute_fuel (length chars) (unpack name) chars
+ seek_attribute_fuel (length chars) True (unpack name) chars
attribute_or_empty : Text → Text → Text
attribute_or_empty name tag =
case attribute_value name tag of
Nothing ⇒ ""
- Just value ⇒ value
+ Just value ⇒ decode_html_entities value
skipped_tag : Text → Bool
skipped_tag name = elem name ["script", "style", "svg", "canvas", "video", "audio", "template"]
@@ -277,20 +370,23 @@ capture_target : Capture → Text
capture_target NoCapture = ""
capture_target CaptureTitle = "title"
capture_target (CaptureHeading name) = name
+capture_target CaptureCaption = "figcaption"
capture_target (CaptureText name) = name
capture_target (CaptureLink _ _ _) = "a"
capture_target (CaptureForm _) = "form"
capture_target (CaptureCell name) = name
append_capture_text : Text → List Char → List Char
-append_capture_text text chars = reverse (unpack text) ++ (' ' :: chars)
+append_capture_text text chars = reverse (unpack text) ++ chars
finish_capture : Capture → Text → Text → List InformationItem → Maybe (List Text) →
(Text, List InformationItem, Maybe (List Text))
finish_capture NoCapture text title items row = (title, items, row)
finish_capture CaptureTitle text title items row = (text, items, row)
-finish_capture (CaptureHeading _) text title items row =
- if text ≟ "" then (title, items, row) else (title, Heading text :: items, row)
+finish_capture (CaptureHeading name) text title items row =
+ if text ≟ "" then (title, items, row) else (title, HeadingAt name text :: items, row)
+finish_capture CaptureCaption text title items row =
+ if text ≟ "" then (title, items, row) else (title, FigureCaption text :: items, row)
finish_capture (CaptureText _) text title items row =
if text ≟ "" then (title, items, row) else (title, TextBlock text :: items, row)
finish_capture (CaptureLink href has_image parent) text title items row =
@@ -378,6 +474,8 @@ collect_information (OpenTag name tag :: rest) skip capture chars row title item
then collect_information rest NotSkipping (CaptureHeading name) [] row title items
else if name ≟ "p" || name ≟ "li"
then collect_information rest NotSkipping (CaptureText name) [] row title items
+ else if name ≟ "figcaption"
+ then collect_information rest NotSkipping CaptureCaption [] row title items
else if name ≟ "a"
then collect_information rest NotSkipping
(CaptureLink (attribute_or_empty "href" tag) False NoCapture) [] row title items
@@ -508,6 +606,8 @@ join_cells (value :: rest) = value ++ " " ++ join_cells rest
item_text : InformationItem → Text
item_text (Heading text) = text
+item_text (HeadingAt name text) = text
+item_text (FigureCaption text) = text
item_text (TextBlock text) = text
item_text (Link text href) = text ++ " " ++ href
item_text (Image source alt caption href) = alt ++ " " ++ source ++ " " ++ caption ++ " " ++ href
@@ -542,6 +642,8 @@ join_with separator (value :: rest) = value ++ separator ++ join_with separator
render_item : Number → InformationItem → Text
render_item width (Heading text) = clip_text width ("# " ++ text)
+render_item width (HeadingAt name text) = clip_text width ("# " ++ text)
+render_item width (FigureCaption text) = clip_text width ("caption: " ++ text)
render_item width (TextBlock text) = clip_text width text
render_item width (Link text href) = clip_text width ("link: " ++ text ++ " -> " ++ href)
render_item width (Image source alt caption href) =
diff --git a/src/IB/Prepaint/Reflow.idric b/src/IB/Prepaint/Reflow.idric
new file mode 100644
index 00000000..fc4483f7
--- /dev/null
+++ b/src/IB/Prepaint/Reflow.idric
@@ -0,0 +1,79 @@
+module IB.Prepaint.Reflow
+
+import Data.Text
+import IB.Strand
+import IB.Prepaint
+import IB.HtmlPrepaint
+import IB.Reflow
+import IB.Reflow.Source
+import IB.Reflow.SourceBreaks
+
+-- This is a derived plan over an immutable revision. The position identifies
+-- a block occurrence only within that retained revision. It is not a new
+-- durable block identifier or an anchor that survives a changed revision.
+public export
+record BlockReflow where
+ constructor PreparedBlock
+ block_position : Number
+ original_block : InformationBlock
+ decoded_text : Maybe Text
+ text_lines : List SourceLine
+
+public export
+record PrepaintLayout where
+ constructor PreparedRevision
+ source_revision : PrepaintRevision
+ requirements : ReflowRequirements
+ measurement_identity : Text
+ block_plans : List BlockReflow
+
+-- Keep the admission evidence, recovered log and semantic result alongside
+-- their layout. V1 wire bytes alone do not authenticate the source range.
+public export
+record HtmlPrepaintLayout where
+ constructor PreparedHtml
+ source_result : HtmlPrepaintResult
+ revision_layout : PrepaintLayout
+
+block_text : InformationBlock → Maybe Text
+block_text (Heading _ text) = Just text
+block_text (TextBlock text) = Just text
+block_text (Link text _) = Just text
+block_text _ = Nothing
+
+prepare_blocks : ReflowRequirements → (Text → Number) → Number →
+ List InformationBlock → Either Text (List BlockReflow)
+prepare_blocks request measure position [] = Right []
+prepare_blocks request measure position (block :: rest) =
+ case block_text block of
+ Nothing ⇒ do
+ remaining ← prepare_blocks request measure (S position) rest
+ Right (PreparedBlock position block Nothing [] :: remaining)
+ Just text ⇒ do
+ lines ← reflow_source request measure text
+ remaining ← prepare_blocks request measure (S position) rest
+ Right (PreparedBlock position block (Just text) lines :: remaining)
+
+-- The width callback and its nonempty identity describe the same measurement
+-- provider. Offsets belong to decoded text in each block, never HTML bytes,
+-- glyphs or UTF-16 units. No native shaping is implied by a Number result.
+-- Unsupported manners refuse even when the revision has no textual blocks.
+public export
+reflow_prepaint : ReflowRequirements → Text → (Text → Number) →
+ PrepaintRevision → Either Text PrepaintLayout
+reflow_prepaint request@(Requirements width manner) metric measure revision =
+ if trim metric ≟ "" then Left "Missing reflow measurement identity"
+ else case manner of
+ streamingly ⇒ Left "Source-bound streaming reflow is unavailable"
+ typographically ⇒ Left "Source-bound typographic reflow is unavailable"
+ _ ⇒ if width ≟ 0 then Left "Reflow width must be positive"
+ else do
+ prepared ← prepare_blocks request measure 0 revision.blocks
+ Right (PreparedRevision revision request metric prepared)
+
+public export
+reflow_html_prepaint : ReflowRequirements → Text → (Text → Number) →
+ HtmlPrepaintResult → Either Text HtmlPrepaintLayout
+reflow_html_prepaint request metric measure result = do
+ layout ← reflow_prepaint request metric measure result.revision
+ Right (PreparedHtml result layout)
diff --git a/src/IB/RecoveredInformation.idric b/src/IB/RecoveredInformation.idric
index 470e145c..283340f8 100644
--- a/src/IB/RecoveredInformation.idric
+++ b/src/IB/RecoveredInformation.idric
@@ -14,7 +14,8 @@ data DocumentEvent
public export
data RecoveredDocumentLog = DocumentLog String (List DocumentEvent)
-data RecoveryState = RecoverState (Maybe String) (Maybe String) Bool Bool
+data RecoveryState =
+ RecoverState (Maybe String) (Maybe String) Bool Bool (Maybe String)
heading_tag : String → Bool
heading_tag name = elem name ["h1", "h2", "h3", "h4", "h5", "h6"]
@@ -23,7 +24,7 @@ paragraph_boundary : String → Bool
paragraph_boundary name =
heading_tag name ||
elem name ["table", "tr", "div", "section", "article", "aside", "nav",
- "ul", "ol", "form"]
+ "ul", "ol", "form", "figure", "figcaption", "blockquote"]
close_matching : String → Maybe String → Maybe String
close_matching wanted Nothing = Nothing
@@ -35,63 +36,74 @@ close_maybe Nothing = []
close_maybe (Just name) = [ImpliedEndTag name]
eof_events : RecoveryState → List DocumentEvent
-eof_events (RecoverState paragraph cell row_open link_open) =
+eof_events (RecoverState paragraph cell row_open link_open heading) =
(if link_open then [ImpliedEndTag "a"] else []) ++
close_maybe cell ++
(if row_open then [ImpliedEndTag "tr"] else []) ++
- close_maybe paragraph
+ close_maybe paragraph ++ close_maybe heading
recover_tokens : List InformationToken → RecoveryState → List DocumentEvent
recover_tokens [] state = eof_events state
recover_tokens (TextToken text :: rest) state =
TextEvent text :: recover_tokens rest state
-recover_tokens (CloseTag name :: rest) (RecoverState paragraph cell row_open link_open) =
- if name == "p" || name == "li"
+recover_tokens (CloseTag name :: rest)
+ (RecoverState paragraph cell row_open link_open heading) =
+ if heading_tag name
then EndTag name :: recover_tokens rest
- (RecoverState (close_matching name paragraph) cell row_open link_open)
+ (RecoverState paragraph cell row_open link_open (close_matching name heading))
+ else if name == "p" || name == "li"
+ then EndTag name :: recover_tokens rest
+ (RecoverState (close_matching name paragraph) cell row_open link_open heading)
else if name == "td" || name == "th"
then EndTag name :: recover_tokens rest
- (RecoverState paragraph Nothing row_open link_open)
+ (RecoverState paragraph Nothing row_open link_open heading)
else if name == "tr"
then close_maybe cell ++ [EndTag "tr"] ++ recover_tokens rest
- (RecoverState paragraph Nothing False link_open)
+ (RecoverState paragraph Nothing False link_open heading)
else if name == "table"
then close_maybe cell ++
(if row_open then [ImpliedEndTag "tr"] else []) ++
[EndTag "table"] ++ recover_tokens rest
- (RecoverState paragraph Nothing False link_open)
+ (RecoverState paragraph Nothing False link_open heading)
else if name == "a"
then EndTag "a" :: recover_tokens rest
- (RecoverState paragraph cell row_open False)
+ (RecoverState paragraph cell row_open False heading)
else EndTag name :: recover_tokens rest
- (RecoverState paragraph cell row_open link_open)
-recover_tokens (OpenTag name tag :: rest) (RecoverState paragraph cell row_open link_open) =
- if name == "p" || name == "li"
- then close_maybe paragraph ++ [StartTag name tag] ++ recover_tokens rest
- (RecoverState (Just name) cell row_open link_open)
+ (RecoverState paragraph cell row_open link_open heading)
+recover_tokens (OpenTag name tag :: rest)
+ (RecoverState paragraph cell row_open link_open heading) =
+ if heading_tag name
+ then close_maybe heading ++ close_maybe paragraph ++
+ [StartTag name tag] ++ recover_tokens rest
+ (RecoverState Nothing cell row_open link_open (Just name))
+ else if name == "p" || name == "li"
+ then close_maybe heading ++ close_maybe paragraph ++
+ [StartTag name tag] ++ recover_tokens rest
+ (RecoverState (Just name) cell row_open link_open Nothing)
else if name == "tr"
- then close_maybe paragraph ++ close_maybe cell ++
+ then close_maybe heading ++ close_maybe paragraph ++ close_maybe cell ++
(if row_open then [ImpliedEndTag "tr"] else []) ++
[StartTag name tag] ++ recover_tokens rest
- (RecoverState Nothing Nothing True link_open)
+ (RecoverState Nothing Nothing True link_open Nothing)
else if name == "td" || name == "th"
then close_maybe cell ++ [StartTag name tag] ++ recover_tokens rest
- (RecoverState paragraph (Just name) row_open link_open)
+ (RecoverState paragraph (Just name) row_open link_open heading)
else if name == "a"
then (if link_open then [ImpliedEndTag "a"] else []) ++
[StartTag name tag] ++ recover_tokens rest
- (RecoverState paragraph cell row_open True)
+ (RecoverState paragraph cell row_open True heading)
else if paragraph_boundary name
- then close_maybe paragraph ++ [StartTag name tag] ++ recover_tokens rest
- (RecoverState Nothing cell row_open link_open)
+ then close_maybe heading ++ close_maybe paragraph ++
+ [StartTag name tag] ++ recover_tokens rest
+ (RecoverState Nothing cell row_open link_open Nothing)
else StartTag name tag :: recover_tokens rest
- (RecoverState paragraph cell row_open link_open)
+ (RecoverState paragraph cell row_open link_open heading)
public export
recover_document_log : String → String → RecoveredDocumentLog
recover_document_log source html =
DocumentLog source
- (recover_tokens (tokenize_information_html html) (RecoverState Nothing Nothing False False))
+ (recover_tokens (tokenize_information_html html) (RecoverState Nothing Nothing False False Nothing))
public export
document_log_contract : String
diff --git a/src/IB/Reflow.idric b/src/IB/Reflow.idric
new file mode 100644
index 00000000..f75c38ec
--- /dev/null
+++ b/src/IB/Reflow.idric
@@ -0,0 +1,85 @@
+module IB.Reflow
+
+import Data.Text
+import IB.Reflow.Greedy
+import IB.Reflow.Streaming
+import IB.Reflow.Balanced
+import IB.Reflow.Objectives
+import IB.Reflow.Threshold
+import IB.Reflow.KnuthPlass
+
+-- One verb; adverbs constrain its manner. The algorithm names occur only
+-- below this selector. Each choice makes a documented tradeoff.
+-- This initial selector makes an explicit *request* decision, not an unproven
+-- ARM32/ARM64/x86-64 benchmark-based choice.
+public export
+choice reflow_adverb one_of
+ promptly
+ streamingly
+ evenly
+ minimizing_raggedness
+ ignoring_final_line
+ minimizing_worst_gap
+ without_extra_lines
+ typographically
+
+public export
+choice reflow_way one_of
+ greedy
+ streaming_greedy
+ balanced
+ cubic
+ final_line_free
+ minimax
+ threshold_balanced
+ knuth_plass
+
+public export
+record ReflowRequirements where
+ constructor Requirements
+ available_width : Number
+ how : reflow_adverb
+
+public export
+select_reflow : ReflowRequirements → reflow_way
+select_reflow (Requirements _ promptly) = greedy
+select_reflow (Requirements _ streamingly) = streaming_greedy
+select_reflow (Requirements _ evenly) = balanced
+select_reflow (Requirements _ minimizing_raggedness) = cubic
+select_reflow (Requirements _ ignoring_final_line) = final_line_free
+select_reflow (Requirements _ minimizing_worst_gap) = minimax
+select_reflow (Requirements _ without_extra_lines) = threshold_balanced
+select_reflow (Requirements _ typographically) = knuth_plass
+
+-- A caller can alternatively use IB.Reflow.Streaming.feed_chunk, beginning
+-- with begin_stream and ending with finish_stream or end_paragraph, to consume
+-- raw decoded text chunks without constructing an entire paragraph.
+--
+-- Contract for this shared batch surface:
+-- * segments are atomic and in source order;
+-- * neighboring segments on a line are joined with one display space;
+-- * never change, drop, clip, or split a segment;
+-- * an individually overwide segment remains overwide on its own line;
+-- * the supplied width function determines whether a candidate line fits.
+--
+-- All methods share that contract, not necessarily their break positions.
+-- Complex-script shaping, Unicode line-break opportunities, source offsets,
+-- hyphenation, and CSS-like justification remain separate from this contract.
+public export
+reflow : ReflowRequirements → (Text → Number) → List Text →
+ Either Text (List Text)
+reflow (Requirements Z _) measure segments =
+ Left "Reflow width must be positive"
+reflow request@(Requirements width _) measure segments =
+ case select_reflow request of
+ greedy ⇒ Right (reflow_greedily measure width segments)
+ streaming_greedy ⇒ Right (reflow_streaming_segments measure width segments)
+ balanced ⇒ Right (reflow_balanced measure width segments)
+ cubic ⇒ Right (reflow_for_objective cubic_raggedness measure width segments)
+ final_line_free ⇒ Right (reflow_for_objective free_final_line measure width segments)
+ minimax ⇒ Right (reflow_for_objective minimax_raggedness measure width segments)
+ threshold_balanced ⇒ Right (reflow_threshold_balanced measure width segments)
+ knuth_plass ⇒
+ case reflow_knuth_plass (default_knuth_settings width) measure width segments of
+ Left reason ⇒ Left reason
+ Right plan ⇒ Right (plain_lines plan)
diff --git a/src/IB/Reflow/Arithmetic.idric b/src/IB/Reflow/Arithmetic.idric
new file mode 100644
index 00000000..6d150b94
--- /dev/null
+++ b/src/IB/Reflow/Arithmetic.idric
@@ -0,0 +1,31 @@
+module IB.Reflow.Arithmetic
+
+-- Number is the maintained nonnegative whole-number surface. Subtracting
+-- directly via (-) requires a Neg instance the pinned compiler does not have
+-- for Number. This saturating difference is total, explicit and portable.
+-- It is a correctness baseline, not a target-specific fast subtraction.
+public export
+nonnegative_difference : Number → Number → Number
+nonnegative_difference amount Z = amount
+nonnegative_difference Z (S taken) = Z
+nonnegative_difference (S amount) (S taken) =
+ nonnegative_difference amount taken
+
+-- Saturated division for TeX badness. The pinned Number/Nat surface lacks
+-- Integral, so div is not available. Compute the largest representable
+-- quotient <= 10000 using 14 descending binary weights; this is exact
+-- until the TeX badness saturation limit. No repeated-subtraction loop.
+quotient_bits : Number → Number → Number → List Number → Number
+quotient_bits numerator denominator accumulated [] = accumulated
+quotient_bits numerator denominator accumulated (weight :: rest) =
+ let proposal = accumulated + weight in
+ if proposal <= 10000 && proposal * denominator <= numerator
+ then quotient_bits numerator denominator proposal rest
+ else quotient_bits numerator denominator accumulated rest
+
+public export
+capped_badness_quotient : Number → Number → Number
+capped_badness_quotient numerator denominator =
+ if denominator ≟ 0 then 10000
+ else quotient_bits numerator denominator 0
+ [8192, 4096, 2048, 1024, 512, 256, 128, 64, 32, 16, 8, 4, 2, 1]
diff --git a/src/IB/Reflow/Balanced.idric b/src/IB/Reflow/Balanced.idric
new file mode 100644
index 00000000..9cf3328b
--- /dev/null
+++ b/src/IB/Reflow/Balanced.idric
@@ -0,0 +1,64 @@
+module IB.Reflow.Balanced
+
+import Data.Text
+import IB.Reflow.Arithmetic
+
+-- Optimize the entire paragraph rather than deciding each break immediately.
+-- Each suffix keeps its best known layout; candidate breaks are tested against
+-- those suffixes. The quadratic number of candidate breaks and retained plans
+-- cost more time/memory than greedy reflow, especially with Text concatenation.
+-- The metric is total squared unused width, INCLUDING the final line.
+-- Use the pinned compiler's executable ASCII arithmetic operators here;
+-- Unicode minus/multiply remain an Idriç frontend compatibility gap.
+-- Unbreakable overwide segments are kept intact and incur zero slack penalty;
+-- their overrun must be dealt with by the rendering boundary, not clipped here.
+record LinePlan where
+ constructor Planned
+ penalty : Number
+ lines : List Text
+
+unused_width : Number → Number → Number
+unused_width available used =
+ if used <= available then nonnegative_difference available used else 0
+
+candidate : (Text → Number) → Number → Text → LinePlan → LinePlan
+candidate measure width line (Planned tail_penalty tail_lines) =
+ let slack = unused_width width (measure line) in
+ Planned (slack * slack + tail_penalty) (line :: tail_lines)
+
+prefer : LinePlan → LinePlan → LinePlan
+prefer first second =
+ if first.penalty <= second.penalty then first else second
+
+-- The suffix plans align with the remaining input segments. An equal-cost
+-- choice retains the earlier (shorter first-line) candidate deterministically.
+consider_longer : (Text → Number) → Number → Text → List Text →
+ List LinePlan → LinePlan → LinePlan
+consider_longer measure width current [] plans best = best
+consider_longer measure width current words [] best = best
+consider_longer measure width current (next :: rest) (tail :: tails) best =
+ let extended = current ++ " " ++ next in
+ -- Check every candidate even after a non-fitting prefix.
+ if measure extended <= width
+ then consider_longer measure width extended rest tails
+ (prefer best (candidate measure width extended tail))
+ else consider_longer measure width extended rest tails best
+
+-- This is an executable suffix dynamic program, not an exponential search.
+-- The first plan in the returned list is for the full supplied suffix.
+suffix_plans : (Text → Number) → Number → List Text → List LinePlan
+suffix_plans measure width [] = [Planned 0 []]
+suffix_plans measure width (first :: rest) =
+ case suffix_plans measure width rest of
+ [] ⇒ []
+ tail :: later ⇒
+ let initial = candidate measure width first tail in
+ let best = consider_longer measure width first rest later initial in
+ best :: tail :: later
+
+public export
+reflow_balanced : (Text → Number) → Number → List Text → List Text
+reflow_balanced measure width segments =
+ case suffix_plans measure width segments of
+ [] ⇒ []
+ (Planned _ lines) :: _ ⇒ lines
diff --git a/src/IB/Reflow/Greedy.idric b/src/IB/Reflow/Greedy.idric
new file mode 100644
index 00000000..75a886f7
--- /dev/null
+++ b/src/IB/Reflow/Greedy.idric
@@ -0,0 +1,21 @@
+module IB.Reflow.Greedy
+
+import Data.Text
+
+-- Single forward pass through the supplied segments. This can be adapted to
+-- streaming input and retains only one unfinished line. A greedy line may
+-- leave the following lines ragged, and width measurement may itself be costly.
+-- Never discard or split a segment just to satisfy the line width.
+fill_line : (Text → Number) → Number → Text → List Text → List Text
+fill_line measure width current [] = [current]
+fill_line measure width current (next :: rest) =
+ let extended = current ++ " " ++ next in
+ if measure extended <= width
+ then fill_line measure width extended rest
+ else current :: fill_line measure width next rest
+
+public export
+reflow_greedily : (Text → Number) → Number → List Text → List Text
+reflow_greedily measure width [] = []
+reflow_greedily measure width (first :: rest) =
+ fill_line measure width first rest
diff --git a/src/IB/Reflow/Incremental.idric b/src/IB/Reflow/Incremental.idric
new file mode 100644
index 00000000..a593f005
--- /dev/null
+++ b/src/IB/Reflow/Incremental.idric
@@ -0,0 +1,61 @@
+module IB.Reflow.Incremental
+
+import Data.Text
+import IB.Reflow
+
+-- Incremental reflow is a cache strategy across revisions, not a competing
+-- line-break objective. Reuse a paragraph only when its source segments, width,
+-- chosen manner, and shaping/measurement identity all match.
+-- An editor or view owns paragraph IDs and separate cache entries; this module
+-- never becomes the canonical source and must not override source revisions.
+public export
+record ParagraphCache where
+ constructor CachedParagraph
+ cached_width : Number
+ cached_how : reflow_adverb
+ cached_metric_key : Text
+ cached_segments : List Text
+ cached_output : List Text
+
+public export
+record CacheResult where
+ constructor ParagraphResult
+ resulting_cache : ParagraphCache
+ reused_previous : Bool
+
+same_manner : reflow_adverb → reflow_adverb → Bool
+same_manner promptly promptly = True
+same_manner streamingly streamingly = True
+same_manner evenly evenly = True
+same_manner minimizing_raggedness minimizing_raggedness = True
+same_manner ignoring_final_line ignoring_final_line = True
+same_manner minimizing_worst_gap minimizing_worst_gap = True
+same_manner without_extra_lines without_extra_lines = True
+same_manner typographically typographically = True
+same_manner _ _ = False
+
+cache_matches : ReflowRequirements → Text → List Text →
+ ParagraphCache → Bool
+cache_matches (Requirements width manner) metric_key segments
+ (CachedParagraph old_width old_manner old_metric old_segments _) =
+ width ≟ old_width && same_manner manner old_manner &&
+ metric_key ≟ old_metric && segments ≟ old_segments
+
+public export
+reflow_incrementally : ReflowRequirements → Text → (Text → Number) →
+ List Text → Maybe ParagraphCache → Either Text CacheResult
+reflow_incrementally requirements@(Requirements width manner)
+ metric_key measure segments previous =
+ case previous of
+ Just cache ⇒
+ if width > 0 && cache_matches requirements metric_key segments cache
+ then Right (ParagraphResult cache True)
+ else rebuild
+ Nothing ⇒ rebuild
+ where
+ rebuild : Either Text CacheResult
+ rebuild =
+ case reflow requirements measure segments of
+ Left problem ⇒ Left problem
+ Right lines ⇒ Right (ParagraphResult
+ (CachedParagraph width manner metric_key segments lines) False)
diff --git a/src/IB/Reflow/KnuthPlass.idric b/src/IB/Reflow/KnuthPlass.idric
new file mode 100644
index 00000000..cd9e8d99
--- /dev/null
+++ b/src/IB/Reflow/KnuthPlass.idric
@@ -0,0 +1,237 @@
+module IB.Reflow.KnuthPlass
+
+import Data.Text
+import IB.Reflow.Arithmetic
+
+-- A real (deliberately restricted) Knuth–Plass box/glue line breaker:
+-- ordered word boxes; break opportunities at interword spaces; optional
+-- stretching/shrinking of those spaces; cubic adjustment badness; and an
+-- adjacent-line fitness demerit. There is NO dictionary hyphenation or
+-- discretionary penalty-node input yet. This is not TeX's complete engine.
+--
+-- In contrast with quadratic raggedness, candidates carry the amount of
+-- space adjustment required. Consumers wanting justification must use the
+-- annotated line plan, not merely its plain-text projection.
+public export
+record KnuthSettings where
+ constructor KnuthOptions
+ stretch_per_gap : Number
+ shrink_per_gap : Number
+ emergency_stretch : Number
+ badness_tolerance : Number
+ fixed_line_penalty : Number
+ abrupt_fitness_penalty : Number
+
+public export
+data SpaceAdjustment
+ = NoAdjustment
+ | SpreadSpaces Number Number
+ | CompressSpaces Number Number
+
+public export
+data Fitness
+ = VeryTight
+ | Tight
+ | Neutral
+ | Loose
+ | VeryLoose
+
+public export
+record JustifiedLine where
+ constructor Justified
+ line_text : Text
+ spacing : SpaceAdjustment
+ line_fitness : Fitness
+
+record KnuthPlan where
+ constructor PlannedKnuth
+ total_demerits : Number
+ justified_lines : List JustifiedLine
+
+-- Suffix plans are keyed by the fitness of the line immediately preceding
+-- the suffix. This retains all five states needed for the transition cost;
+-- keeping only one best suffix plan would give an incorrect optimum.
+record PlansForSuffix where
+ constructor SuffixPlans
+ from_very_tight : Maybe KnuthPlan
+ from_tight : Maybe KnuthPlan
+ from_neutral : Maybe KnuthPlan
+ from_loose : Maybe KnuthPlan
+ from_very_loose : Maybe KnuthPlan
+
+next_plan : Fitness → PlansForSuffix → Maybe KnuthPlan
+next_plan VeryTight plans = plans.from_very_tight
+next_plan Tight plans = plans.from_tight
+next_plan Neutral plans = plans.from_neutral
+next_plan Loose plans = plans.from_loose
+next_plan VeryLoose plans = plans.from_very_loose
+
+fitness_number : Fitness → Number
+fitness_number VeryTight = 0
+fitness_number Tight = 1
+fitness_number Neutral = 2
+fitness_number Loose = 3
+fitness_number VeryLoose = 4
+
+fitness_distance : Fitness → Fitness → Number
+fitness_distance first later =
+ let a = fitness_number first in
+ let b = fitness_number later in
+ if a >= b then nonnegative_difference a b else nonnegative_difference b a
+
+is_last : List Text → Bool
+is_last [] = True
+is_last (_ :: _) = False
+
+-- TeX-style cubic badness with an integer numerator and denominator. The
+-- exact ratio is also recorded, avoiding floating-point rounding in the plan.
+adjustment_badness : Number → Number → Number
+adjustment_badness amount capacity =
+ capped_badness_quotient
+ (100 * amount * amount * amount)
+ (capacity * capacity * capacity)
+
+within_tolerance : KnuthSettings → Number → Bool
+within_tolerance settings badness =
+ badness <= settings.badness_tolerance
+
+spread_fitness : Number → Number → Fitness
+spread_fitness amount capacity =
+ if amount ≟ 0 then Neutral
+ else if 2 * amount <= capacity then Neutral
+ else if amount <= capacity then Loose
+ else VeryLoose
+
+shrink_fitness : Number → Number → Fitness
+shrink_fitness amount capacity =
+ if 2 * amount <= capacity then Tight else VeryTight
+
+-- A sole overwide word remains intact and is charged an explicit emergency
+-- penalty. A multiword line cannot exceed the width unless its spaces have
+-- enough declared shrink capacity. A final line is left unjustified.
+shape_line : KnuthSettings → (Text → Number) → Number →
+ Text → Number → Bool → Maybe (JustifiedLine, Number)
+shape_line settings measure width line gaps last =
+ let natural = measure line in
+ if natural > width && gaps ≟ 0
+ then Just (Justified line NoAdjustment VeryTight, 10000)
+ else if last
+ then if natural <= width
+ then Just (Justified line NoAdjustment Neutral, 0)
+ else Nothing
+ else if natural <= width
+ then let unused = nonnegative_difference width natural in
+ if unused ≟ 0
+ then Just (Justified line NoAdjustment Neutral, 0)
+ else let capacity =
+ gaps * settings.stretch_per_gap +
+ settings.emergency_stretch in
+ let badness = adjustment_badness unused capacity in
+ if capacity ≟ 0 || not (within_tolerance settings badness)
+ then Nothing
+ else Just
+ (Justified line (SpreadSpaces unused capacity)
+ (spread_fitness unused capacity), badness)
+ else let excess = nonnegative_difference natural width in
+ let capacity = gaps * settings.shrink_per_gap in
+ let badness = adjustment_badness excess capacity in
+ if capacity ≟ 0 || excess > capacity ||
+ not (within_tolerance settings badness)
+ then Nothing
+ else Just
+ (Justified line (CompressSpaces excess capacity)
+ (shrink_fitness excess capacity), badness)
+
+consider : KnuthSettings → (Text → Number) → Number → Fitness →
+ Text → Number → Bool → PlansForSuffix → Maybe KnuthPlan
+consider settings measure width previous line gap_count last tail_plans =
+ case shape_line settings measure width line gap_count last of
+ Nothing ⇒ Nothing
+ Just (geometry, badness) ⇒
+ case next_plan geometry.line_fitness tail_plans of
+ Nothing ⇒ Nothing
+ Just (PlannedKnuth tail_cost tail_lines) ⇒
+ let line_cost = settings.fixed_line_penalty + badness in
+ let fitness_jump = fitness_distance previous geometry.line_fitness in
+ let change_penalty =
+ if fitness_jump > 1 then settings.abrupt_fitness_penalty else 0 in
+ Just (PlannedKnuth
+ (line_cost * line_cost + change_penalty + tail_cost)
+ (geometry :: tail_lines))
+
+prefer : Maybe KnuthPlan → Maybe KnuthPlan → Maybe KnuthPlan
+prefer Nothing second = second
+prefer first Nothing = first
+prefer (Just first) (Just second) =
+ if first.total_demerits <= second.total_demerits
+ then Just first else Just second
+
+explore : KnuthSettings → (Text → Number) → Number → Fitness →
+ Text → Number → List Text → List PlansForSuffix →
+ Maybe KnuthPlan → Maybe KnuthPlan
+explore settings measure width previous current gaps [] plans best = best
+explore settings measure width previous current gaps words [] best = best
+explore settings measure width previous current gaps
+ (word :: rest) (tail :: later) best =
+ let extended = current ++ " " ++ word in
+ let new_gaps = S gaps in
+ let proposal = consider settings measure width previous extended new_gaps (is_last rest) tail in
+ explore settings measure width previous extended new_gaps
+ rest later (prefer best proposal)
+
+best_from : KnuthSettings → (Text → Number) → Number → Fitness →
+ List Text → List PlansForSuffix → Maybe KnuthPlan
+best_from settings measure width previous [] plans = Nothing
+best_from settings measure width previous words [] = Nothing
+best_from settings measure width previous (word :: rest) (tail :: later) =
+ let initial = consider settings measure width previous word Z (is_last rest) tail in
+ explore settings measure width previous word Z rest later initial
+
+terminal_plans : PlansForSuffix
+terminal_plans =
+ let empty = Just (PlannedKnuth 0 []) in
+ SuffixPlans empty empty empty empty empty
+
+make_suffix_plan : KnuthSettings → (Text → Number) → Number →
+ List Text → List PlansForSuffix → PlansForSuffix
+make_suffix_plan settings measure width words tails =
+ let a = best_from settings measure width VeryTight words tails in
+ let b = best_from settings measure width Tight words tails in
+ let c = best_from settings measure width Neutral words tails in
+ let d = best_from settings measure width Loose words tails in
+ let e = best_from settings measure width VeryLoose words tails in
+ SuffixPlans a b c d e
+
+all_suffix_plans : KnuthSettings → (Text → Number) → Number →
+ List Text → List PlansForSuffix
+all_suffix_plans settings measure width [] = [terminal_plans]
+all_suffix_plans settings measure width words@(_ :: rest) =
+ let tails = all_suffix_plans settings measure width rest in
+ make_suffix_plan settings measure width words tails :: tails
+
+public export
+reflow_knuth_plass : KnuthSettings → (Text → Number) → Number →
+ List Text → Either Text (List JustifiedLine)
+reflow_knuth_plass settings measure width [] = Right []
+reflow_knuth_plass settings measure width words =
+ case all_suffix_plans settings measure width words of
+ [] ⇒ Left "Knuth-Plass could not construct suffix plans"
+ plans :: _ ⇒
+ case next_plan Neutral plans of
+ Nothing ⇒ Left "No admissible Knuth-Plass line-break plan"
+ Just (PlannedKnuth _ lines) ⇒ Right lines
+
+-- The defaults are a *policy*, not a benchmark finding: temporary stretch
+-- scales with the viewport so readable ragged text is still feasible.
+-- Shrink is disabled for the plain-text IB projection. A future native
+-- renderer that actually consumes SpaceAdjustment can enable it explicitly.
+public export
+default_knuth_settings : Number → KnuthSettings
+default_knuth_settings width =
+ KnuthOptions 2 0 width 10000 10 2000
+
+public export
+plain_lines : List JustifiedLine → List Text
+plain_lines [] = []
+plain_lines ((Justified text adjustment fitness) :: rest) =
+ text :: plain_lines rest
diff --git a/src/IB/Reflow/Objectives.idric b/src/IB/Reflow/Objectives.idric
new file mode 100644
index 00000000..a8e5a4c0
--- /dev/null
+++ b/src/IB/Reflow/Objectives.idric
@@ -0,0 +1,80 @@
+module IB.Reflow.Objectives
+
+import Data.Text
+import IB.Reflow.Arithmetic
+
+-- These three ways share the same suffix dynamic-programming engine, but ask
+-- different mathematical questions. They cannot be interchanged blindly:
+-- choosing a different objective may change observable line breaks.
+public export
+choice line_objective one_of
+ cubic_raggedness
+ free_final_line
+ minimax_raggedness
+
+record ObjectivePlan where
+ constructor PlannedObjective
+ objective_score : Number
+ objective_lines : List Text
+
+slack : Number → Number → Number
+slack width used =
+ if used <= width then nonnegative_difference width used else 0
+
+last_line : List Text → Bool
+last_line [] = True
+last_line (_ :: _) = False
+
+line_penalty : line_objective → Number → Bool → Number
+line_penalty cubic_raggedness unused is_last = unused * unused * unused
+line_penalty free_final_line unused True = 0
+line_penalty free_final_line unused False = unused * unused
+line_penalty minimax_raggedness unused is_last = unused
+
+combine_score : line_objective → Number → Number → Number
+combine_score minimax_raggedness first later =
+ if first >= later then first else later
+combine_score _ first later = first + later
+
+candidate : line_objective → (Text → Number) → Number →
+ Text → ObjectivePlan → ObjectivePlan
+candidate objective measure width line (PlannedObjective previous following) =
+ let unused = slack width (measure line) in
+ let penalty = line_penalty objective unused (last_line following) in
+ PlannedObjective (combine_score objective penalty previous) (line :: following)
+
+prefer : ObjectivePlan → ObjectivePlan → ObjectivePlan
+prefer left right =
+ if left.objective_score <= right.objective_score then left else right
+
+-- Do not prune later breakpoints after one line fails to fit: an arbitrary
+-- supplied shaped-text width metric is not guaranteed to be monotonic.
+check_longer : line_objective → (Text → Number) → Number → Text →
+ List Text → List ObjectivePlan → ObjectivePlan → ObjectivePlan
+check_longer objective measure width current [] plans best = best
+check_longer objective measure width current values [] best = best
+check_longer objective measure width current (word :: rest) (tail :: tails) best =
+ let extended = current ++ " " ++ word in
+ if measure extended <= width
+ then check_longer objective measure width extended rest tails
+ (prefer best (candidate objective measure width extended tail))
+ else check_longer objective measure width extended rest tails best
+
+suffix_plans : line_objective → (Text → Number) → Number →
+ List Text → List ObjectivePlan
+suffix_plans objective measure width [] = [PlannedObjective 0 []]
+suffix_plans objective measure width (word :: rest) =
+ case suffix_plans objective measure width rest of
+ [] ⇒ []
+ tail :: later ⇒
+ let initial = candidate objective measure width word tail in
+ let best = check_longer objective measure width word rest later initial in
+ best :: tail :: later
+
+public export
+reflow_for_objective : line_objective → (Text → Number) → Number →
+ List Text → List Text
+reflow_for_objective objective measure width words =
+ case suffix_plans objective measure width words of
+ [] ⇒ []
+ (PlannedObjective _ lines) :: _ ⇒ lines
diff --git a/src/IB/Reflow/Source.idric b/src/IB/Reflow/Source.idric
new file mode 100644
index 00000000..32a45081
--- /dev/null
+++ b/src/IB/Reflow/Source.idric
@@ -0,0 +1,221 @@
+module IB.Reflow.Source
+
+import Data.Text
+import IB.Reflow
+import IB.Reflow.Arithmetic
+import IB.Reflow.SourceBreaks
+
+-- Unlike the earlier atomic-word reflow, this preserves source character
+-- offsets and never normalizes or edits canonical source. The visible text is
+-- a derived projection: paragraph controls are hidden, trailing display
+-- spaces are suppressed, and a chosen soft-hyphen cut adds a visible "-".
+-- This simple hyphen glyph is a policy, NOT locale-specific shaping.
+hidden_character : Char → Bool
+hidden_character char =
+ let point = ord char in
+ point ≟ 173 || point ≟ 8203 ||
+ point ≟ 10 || point ≟ 13 ||
+ point ≟ 133 || point ≟ 8232 || point ≟ 8233
+
+without_controls : List Char → List Char
+without_controls [] = []
+without_controls (char :: rest) =
+ if hidden_character char
+ then without_controls rest
+ else char :: without_controls rest
+
+strip_trailing_space : List Char → List Char
+strip_trailing_space [] = []
+strip_trailing_space (' ' :: rest) = strip_trailing_space rest
+strip_trailing_space (char :: rest) = char :: rest
+
+display_break_mark : BreakKind → Text → Text
+display_break_mark DiscretionaryHyphen painted = painted ++ "-"
+display_break_mark _ painted = painted
+
+source_line : Text → Number → SourceBreak → SourceLine
+source_line source start (At finish kind) =
+ let span = FromSource start finish "" kind in
+ let raw = unpack (source_for_line source span) in
+ let painted = pack (reverse (strip_trailing_space (reverse (without_controls raw)))) in
+ FromSource start finish (display_break_mark kind painted) kind
+
+line_fits : (Text → Number) → Number → SourceLine → Bool
+line_fits measure width line =
+ measure line.visible_text <= width
+
+terminal : BreakKind → Bool
+terminal MandatoryBreak = True
+terminal SourceEnd = True
+terminal _ = False
+
+-- A greedy line chooses the farthest candidate that fits, stopping at the
+-- first mandatory boundary. If not even the earliest candidate fits, emit
+-- that atomic source run intact and report the overrun through line geometry.
+-- It never invents an illegal break to stay inside the width.
+last_fitting : Text → (Text → Number) → Number → Number →
+ SourceBreak → List SourceBreak → Maybe SourceBreak → SourceBreak
+last_fitting source measure width start first [] chosen =
+ case chosen of
+ Nothing ⇒ first
+ Just answer ⇒ answer
+last_fitting source measure width start first (candidate :: more) chosen =
+ let fits = line_fits measure width (source_line source start candidate) in
+ let best : Maybe SourceBreak = if fits then Just candidate else chosen in
+ if terminal candidate.break_kind
+ then case best of
+ Nothing ⇒ first
+ Just answer ⇒ answer
+ else last_fitting source measure width start first more best
+
+select_greedy : Text → (Text → Number) → Number → Number →
+ List SourceBreak → SourceBreak
+select_greedy source measure width start [] = At start SourceEnd
+select_greedy source measure width start (first :: later) =
+ if terminal first.break_kind
+ then first
+ else let first_fit = line_fits measure width
+ (source_line source start first) in
+ last_fitting source measure width start first later
+ (if first_fit then Just first else Nothing)
+
+after_cut : Number → List SourceBreak → List SourceBreak
+after_cut offset [] = []
+after_cut offset (cut :: rest) =
+ if cut.source_offset <= offset then after_cut offset rest
+ else cut :: rest
+
+-- A valid selection consumes at least one candidate. Bound recursive descent
+-- by the original candidate count; an exhausted budget refuses the projection
+-- rather than silently dropping source or asserting an unchecked termination.
+greedy_lines : Number → Text → (Text → Number) → Number → Number →
+ List SourceBreak → Either Text (List SourceLine)
+greedy_lines remaining_choices source measure width start [] = Right []
+greedy_lines Z source measure width start cuts =
+ Left "Reflow candidate budget exhausted"
+greedy_lines (S remaining_choices) source measure width start cuts =
+ let chosen = select_greedy source measure width start cuts in
+ case greedy_lines remaining_choices source measure width chosen.source_offset
+ (after_cut chosen.source_offset cuts) of
+ Left message ⇒ Left message
+ Right later_lines ⇒ Right (source_line source start chosen :: later_lines)
+
+record SourcePlan where
+ constructor PlannedSource
+ total_cost : Number
+ number_of_lines : Number
+ lines : List SourceLine
+
+badness : reflow_adverb → Number → Number → Bool → Number
+badness mode width used last =
+ let unused = nonnegative_difference width used in
+ if used > width
+ then let excess = nonnegative_difference used width in
+ 1000000000 + excess * excess
+ else case mode of
+ ignoring_final_line ⇒ if last then 0 else unused * unused
+ minimizing_raggedness ⇒ unused * unused * unused
+ _ ⇒ unused * unused
+
+combined_cost : reflow_adverb → Number → Number → Number
+combined_cost minimizing_worst_gap first later =
+ if first >= later then first else later
+combined_cost _ first later = first + later
+
+soft_hyphen_cost : BreakKind → Number
+soft_hyphen_cost DiscretionaryHyphen = 50
+soft_hyphen_cost _ = 0
+
+candidate_plan : Text → reflow_adverb → (Text → Number) → Number →
+ Number → SourceBreak → SourcePlan → SourcePlan
+candidate_plan source mode measure width start cut (PlannedSource tail_cost count tail) =
+ let line = source_line source start cut in
+ let last = cut.source_offset ≟ length (unpack source) in
+ let cost = badness mode width (measure line.visible_text) last in
+ let adjusted = cost + soft_hyphen_cost cut.break_kind in
+ PlannedSource (combined_cost mode adjusted tail_cost)
+ (S count) (line :: tail)
+
+prefer_plan : reflow_adverb → SourcePlan → SourcePlan → SourcePlan
+prefer_plan without_extra_lines first second =
+ if first.number_of_lines < second.number_of_lines then first
+ else if first.number_of_lines > second.number_of_lines then second
+ else if first.total_cost <= second.total_cost then first else second
+prefer_plan mode first second =
+ if first.total_cost <= second.total_cost then first else second
+
+update_best : reflow_adverb → Maybe SourcePlan → SourcePlan → Maybe SourcePlan
+update_best mode Nothing candidate = Just candidate
+update_best mode (Just current) candidate =
+ Just (prefer_plan mode current candidate)
+
+-- Candidate plans are aligned with the source offsets of cuts. The first
+-- candidate is always admissible, even if it exceeds the width; later ones
+-- must fit. Required boundaries cap the search, so a plan cannot cross them.
+consider_cuts : Text → reflow_adverb → (Text → Number) → Number →
+ Number → Bool → List SourceBreak → List SourcePlan →
+ Maybe SourcePlan → Maybe SourcePlan
+consider_cuts source mode measure width start first [] plans best = best
+consider_cuts source mode measure width start first cuts [] best = best
+consider_cuts source mode measure width start first
+ (cut :: rest) (tail :: tails) best =
+ let line = source_line source start cut in
+ let admissible = first || line_fits measure width line in
+ if terminal cut.break_kind
+ then if admissible
+ then update_best mode best (candidate_plan source mode measure width start cut tail)
+ else best
+ else if admissible
+ then consider_cuts source mode measure width start False rest tails
+ (update_best mode best (candidate_plan source mode measure width start cut tail))
+ else consider_cuts source mode measure width start False rest tails best
+
+plan_from : Text → reflow_adverb → (Text → Number) → Number →
+ Number → List SourceBreak → List SourcePlan → SourcePlan
+plan_from source mode measure width start cuts tails =
+ case consider_cuts source mode measure width start True cuts tails Nothing of
+ Just answer ⇒ answer
+ Nothing ⇒ PlannedSource 0 0 []
+
+suffix_plans : Text → reflow_adverb → (Text → Number) → Number →
+ List SourceBreak → List SourcePlan
+suffix_plans source mode measure width [] = [PlannedSource 0 0 []]
+suffix_plans source mode measure width (At offset kind :: later) =
+ let tails = suffix_plans source mode measure width later in
+ let plan = plan_from source mode measure width offset later tails in
+ plan :: tails
+
+optimal_lines : Text → reflow_adverb → (Text → Number) → Number →
+ List SourceBreak → List SourceLine
+optimal_lines source mode measure width cuts =
+ let tails = suffix_plans source mode measure width cuts in
+ let (PlannedSource _ _ lines) = plan_from source mode measure width 0 cuts tails in
+ lines
+
+-- On the source-bound representation the following requests are genuinely
+-- implemented: greedy, minimum squared/cubic/maximum slack, final-line-free
+-- and *exact* minimum-line-count/secondarily minimum-square-slack.
+-- The last differs from the atomic-word threshold heuristic, by design.
+-- Streaming requires a lifetime-aware source-offset accumulator, and TeX
+-- needs actual variable-width glue/penalty nodes, so those fail explicitly.
+public export
+reflow_at_breaks : ReflowRequirements → (Text → Number) → Text →
+ List SourceBreak → Either Text (List SourceLine)
+reflow_at_breaks (Requirements Z _) measure source cuts =
+ Left "Reflow width must be positive"
+reflow_at_breaks (Requirements width mode) measure source cuts =
+ if not (valid_source_breaks source cuts)
+ then Left "Invalid, unsafe or incomplete source break opportunities"
+ else case unpack source of
+ [] ⇒ Right []
+ _ ⇒ case mode of
+ promptly ⇒ greedy_lines (length cuts) source measure width 0 cuts
+ streamingly ⇒ Left "Source-offset streaming has not been qualified"
+ typographically ⇒ Left "Source-backed adjustable glue is not qualified"
+ _ ⇒ Right (optimal_lines source mode measure width cuts)
+
+public export
+reflow_source : ReflowRequirements → (Text → Number) → Text →
+ Either Text (List SourceLine)
+reflow_source requirements measure source =
+ reflow_at_breaks requirements measure source (source_breaks source)
diff --git a/src/IB/Reflow/SourceBreaks.idric b/src/IB/Reflow/SourceBreaks.idric
new file mode 100644
index 00000000..f7ba27cf
--- /dev/null
+++ b/src/IB/Reflow/SourceBreaks.idric
@@ -0,0 +1,201 @@
+module IB.Reflow.SourceBreaks
+
+import Data.Text
+import IB.Reflow.Arithmetic
+
+-- A source-bound list of possible line breaks. Offsets count decoded Unicode
+-- code points (elements of unpack), NOT UTF-8 bytes, UTF-16 units or glyphs.
+-- A break is the position immediately AFTER source_offset characters.
+-- The source text itself remains canonical. No renderer output is reparsed.
+public export
+data BreakKind
+ = PossibleBreak
+ | MandatoryBreak
+ | DiscretionaryHyphen
+ | ZeroWidthBreak
+ | SourceEnd
+
+public export
+record SourceBreak where
+ constructor At
+ source_offset : Number
+ break_kind : BreakKind
+
+public export
+record SourceLine where
+ constructor FromSource
+ first_codepoint : Number
+ after_last_codepoint : Number
+ visible_text : Text
+ ending : BreakKind
+
+is_han : Char → Bool
+is_han value =
+ let number = ord value in
+ (number >= 19968 && number <= 40959) ||
+ (number >= 13312 && number <= 19903)
+
+-- Deliberately bounded Unicode tailoring, NOT the complete UAX #14.
+-- ASCII SPACE, ZERO WIDTH SPACE, SOFT HYPHEN, hard line endings and selected
+-- Han–Han boundaries produce candidates. NBSP/WORD JOINER and emoji ZWJ do
+-- not generate breaks. Complete Unicode/locale break data can supply an
+-- independently qualified list of SourceBreak values to the same solver.
+hard_line_end : Char → List Char → Bool
+hard_line_end '\r' ('\n' :: _) = False
+hard_line_end '\r' _ = True
+hard_line_end '\n' _ = True
+hard_line_end value _ =
+ let number = ord value in
+ number ≟ 133 || number ≟ 8232 || number ≟ 8233
+
+classify : Char → List Char → Maybe BreakKind
+classify value rest =
+ if hard_line_end value rest then Just MandatoryBreak
+ else if ord value ≟ 173 then Just DiscretionaryHyphen
+ else if ord value ≟ 8203 then Just ZeroWidthBreak
+ else if value ≟ ' ' then
+ case rest of
+ next :: _ ⇒
+ if hard_line_end next [] || ord next ≟ 8205 || ord next ≟ 8288
+ then Nothing else Just PossibleBreak
+ [] ⇒ Nothing
+ else if is_han value then
+ case rest of
+ next :: _ ⇒ if is_han next then Just PossibleBreak else Nothing
+ [] ⇒ Nothing
+ else Nothing
+
+is_empty : List Char → Bool
+is_empty [] = True
+is_empty (_ :: _) = False
+
+scan_breaks : Number → List Char → List SourceBreak
+scan_breaks offset [] = [At offset SourceEnd]
+scan_breaks offset (value :: rest) =
+ let later = scan_breaks (S offset) rest in
+ case classify value rest of
+ Nothing ⇒ later
+ Just kind ⇒
+ if is_empty rest
+ then case kind of
+ MandatoryBreak ⇒ [At (S offset) MandatoryBreak]
+ _ ⇒ later
+ else At (S offset) kind :: later
+
+public export
+source_breaks : Text → List SourceBreak
+source_breaks text = scan_breaks 0 (unpack text)
+
+-- Checks do not establish all of UAX #14/#29. They *do* fail closed on
+-- malformed ranges, duplicate/reordered cuts, missing mandatory breaks, cuts
+-- inside CRLF or after ZWJ/word joiner, and cuts before common combining marks.
+-- Full segmentation is a separate, versioned provider qualification.
+at_position : Number → List Char → Maybe Char
+at_position Z [] = Nothing
+at_position Z (value :: _) = Just value
+at_position (S position) [] = Nothing
+at_position (S position) (_ :: rest) = at_position position rest
+
+before : Number → List Char → Maybe Char
+before Z chars = Nothing
+before (S previous) chars = at_position previous chars
+
+is_combining_mark : Char → Bool
+is_combining_mark value =
+ let number = ord value in
+ (number >= 768 && number <= 879) ||
+ (number >= 6832 && number <= 6911) ||
+ (number >= 7616 && number <= 7679) ||
+ (number >= 8400 && number <= 8447) ||
+ (number >= 65056 && number <= 65071)
+
+safe_cut : List Char → Number → BreakKind → Bool
+safe_cut chars offset kind =
+ case (before offset chars, at_position offset chars) of
+ (Just previous, Just next) ⇒
+ not (previous ≟ '\r' && next ≟ '\n') &&
+ not (ord previous ≟ 8205 || ord previous ≟ 8288) &&
+ not (ord next ≟ 8205 || ord next ≟ 8288) &&
+ (case kind of
+ MandatoryBreak ⇒ True
+ _ ⇒ not (is_combining_mark next)) &&
+ (case kind of
+ MandatoryBreak ⇒ True
+ _ ⇒ not (hard_line_end next []))
+ _ ⇒ True
+
+requires_break : List Char → Number → Bool
+requires_break chars offset =
+ case before offset chars of
+ Nothing ⇒ False
+ Just previous ⇒
+ let remaining = drop offset chars in
+ hard_line_end previous remaining
+
+same_kind : BreakKind → BreakKind → Bool
+same_kind PossibleBreak PossibleBreak = True
+same_kind MandatoryBreak MandatoryBreak = True
+same_kind DiscretionaryHyphen DiscretionaryHyphen = True
+same_kind ZeroWidthBreak ZeroWidthBreak = True
+same_kind SourceEnd SourceEnd = True
+same_kind _ _ = False
+
+-- For a declared mandatory cut, check that the source actually forces it.
+-- The end marker is allowed only at the exact end, except that a hard final
+-- newline is represented by MandatoryBreak instead.
+kind_is_sound : List Char → Number → BreakKind → Bool
+kind_is_sound chars offset MandatoryBreak = requires_break chars offset
+kind_is_sound chars offset DiscretionaryHyphen =
+ case before offset chars of
+ Just previous ⇒ ord previous ≟ 173
+ Nothing ⇒ False
+kind_is_sound chars offset ZeroWidthBreak =
+ case before offset chars of
+ Just previous ⇒ ord previous ≟ 8203
+ Nothing ⇒ False
+kind_is_sound chars offset PossibleBreak =
+ not (requires_break chars offset)
+kind_is_sound chars offset SourceEnd =
+ offset ≟ length chars && not (requires_break chars offset)
+
+well_ordered : List Char → Number → List SourceBreak → Bool
+well_ordered chars previous [] = previous ≟ length chars
+well_ordered chars previous (At offset kind :: rest) =
+ offset > previous && offset <= length chars &&
+ safe_cut chars offset kind &&
+ kind_is_sound chars offset kind &&
+ well_ordered chars offset rest
+
+has_mandatory : Number → List SourceBreak → Bool
+has_mandatory offset [] = False
+has_mandatory offset (At position kind :: rest) =
+ if offset ≟ position
+ then same_kind kind MandatoryBreak
+ else has_mandatory offset rest
+
+all_hard_breaks : Number → List Char → List SourceBreak → Bool
+all_hard_breaks offset [] breaks = True
+all_hard_breaks offset (value :: rest) breaks =
+ let next = S offset in
+ if hard_line_end value rest
+ then has_mandatory next breaks && all_hard_breaks next rest breaks
+ else all_hard_breaks next rest breaks
+
+public export
+valid_source_breaks : Text → List SourceBreak → Bool
+valid_source_breaks text breaks =
+ let chars = unpack text in
+ case chars of
+ [] ⇒ case breaks of
+ [] ⇒ True
+ [At Z SourceEnd] ⇒ True
+ _ ⇒ False
+ _ ⇒ well_ordered chars 0 breaks && all_hard_breaks 0 chars breaks
+
+-- Reconstruct EXACT decoded source from offsets, regardless of paint spelling.
+-- This is an independent identity oracle for layouts with discretionary marks.
+public export
+source_for_line : Text → SourceLine → Text
+source_for_line source line =
+ pack (take (nonnegative_difference line.after_last_codepoint line.first_codepoint)
+ (drop line.first_codepoint (unpack source)))
diff --git a/src/IB/Reflow/Streaming.idric b/src/IB/Reflow/Streaming.idric
new file mode 100644
index 00000000..0fab9185
--- /dev/null
+++ b/src/IB/Reflow/Streaming.idric
@@ -0,0 +1,101 @@
+module IB.Reflow.Streaming
+
+import Data.Text
+
+-- A real push interface: each chunk may end inside a word. The caller owns
+-- paragraph boundaries, and can emit completed lines before the source ends.
+-- Only the current line and one incomplete word are retained; an extremely
+-- long unbreakable word is necessarily retained until its next boundary.
+-- The list is reversed so receiving one character takes constant list work.
+public export
+record ReflowStream where
+ constructor Streaming
+ stream_width : Number
+ reversed_unfinished_word : List Char
+ unfinished_line : Maybe Text
+
+public export
+record StreamStep where
+ constructor Emitted
+ next_stream : ReflowStream
+ completed_lines : List Text
+
+public export
+begin_stream : Number → Either Text ReflowStream
+begin_stream Z = Left "Reflow width must be positive"
+begin_stream width = Right (Streaming width [] Nothing)
+
+-- We deliberately normalize whitespace to one display space. The source
+-- bytes and semantic spans remain owned by IB.Information, not this renderer.
+separator : Char → Bool
+separator char =
+ char ≟ ' ' || char ≟ '\n' || char ≟ '\r' || char ≟ '\t'
+
+-- A finished word may complete the previous line, which can be published
+-- immediately. Unlike the batch function, no future word is needed afterward.
+put_word : (Text → Number) → Number → Maybe Text → Text →
+ (Maybe Text, List Text)
+put_word measure width Nothing word = (Just word, [])
+put_word measure width (Just line) word =
+ let extended = line ++ " " ++ word in
+ if measure extended <= width
+ then (Just extended, [])
+ else (Just word, [line])
+
+complete_word : (Text → Number) → ReflowStream →
+ (ReflowStream, List Text)
+complete_word measure state@(Streaming width [] line) = (state, [])
+complete_word measure (Streaming width reversed_word line) =
+ let word = pack (reverse reversed_word) in
+ let (next_line, emitted) = put_word measure width line word in
+ (Streaming width [] next_line, emitted)
+
+scan_chunk : (Text → Number) → ReflowStream → List Char → List Text →
+ StreamStep
+scan_chunk measure state [] emitted_reversed =
+ Emitted state (reverse emitted_reversed)
+scan_chunk measure state@(Streaming width word line) (char :: rest) emitted_reversed =
+ if separator char
+ then let (next, emitted) = complete_word measure state in
+ scan_chunk measure next rest (reverse emitted ++ emitted_reversed)
+ else scan_chunk measure (Streaming width (char :: word) line)
+ rest emitted_reversed
+
+-- feed_chunk accepts arbitrarily split source chunks. No pending word is
+-- published prematurely at the end of a chunk.
+public export
+feed_chunk : (Text → Number) → ReflowStream → Text → StreamStep
+feed_chunk measure state chunk =
+ scan_chunk measure state (unpack chunk) []
+
+-- Explicit paragraph or stream completion flushes the last line.
+public export
+finish_stream : (Text → Number) → ReflowStream → List Text
+finish_stream measure state =
+ let (Streaming _ _ line, emitted) = complete_word measure state in
+ case line of
+ Nothing ⇒ emitted
+ Just value ⇒ emitted ++ [value]
+
+-- Paragraph boundaries are semantic input, not inferred from arbitrary
+-- transport chunking. The returned state can receive the next paragraph.
+public export
+end_paragraph : (Text → Number) → ReflowStream →
+ (ReflowStream, List Text)
+end_paragraph measure state@(Streaming width _ _) =
+ (Streaming width [] Nothing, finish_stream measure state)
+
+-- Batch adapter over the same one-word-at-a-time state transition. It does
+-- not materialize a joined paragraph or change token boundaries.
+-- Calling feed_chunk instead is the genuine streaming source interface.
+run_segments : (Text → Number) → Number → Maybe Text → List Text → List Text
+run_segments measure width Nothing [] = []
+run_segments measure width (Just line) [] = [line]
+run_segments measure width line (word :: rest) =
+ let (next, emitted) = put_word measure width line word in
+ emitted ++ run_segments measure width next rest
+
+public export
+reflow_streaming_segments : (Text → Number) → Number → List Text → List Text
+reflow_streaming_segments measure width segments =
+ run_segments measure width Nothing segments
diff --git a/src/IB/Reflow/Threshold.idric b/src/IB/Reflow/Threshold.idric
new file mode 100644
index 00000000..92ff9f60
--- /dev/null
+++ b/src/IB/Reflow/Threshold.idric
@@ -0,0 +1,27 @@
+module IB.Reflow.Threshold
+
+import Data.Text
+import IB.Reflow.Greedy
+
+-- A CSS text-wrap:balance-style approximation (not a browser's CSS engine).
+-- First determine the minimum greedy line count at the available width.
+-- Then repeatedly narrow the effective width while that count stays fixed.
+-- This often makes lines less uneven than greedy without quadratic DP state.
+-- Cost is repeated scans, up to available_width scans, and quality is only
+-- heuristic: the effective-width choice need not minimize raggedness.
+tighten : (Text → Number) → Number → Number → List Text →
+ List Text → List Text
+tighten measure Z wanted words best = best
+tighten measure (S Z) wanted words best = best
+tighten measure (S (S narrower)) wanted words best =
+ let candidate = reflow_greedily measure (S narrower) words in
+ if length candidate <= wanted
+ then tighten measure (S narrower) wanted words candidate
+ else best
+
+public export
+reflow_threshold_balanced : (Text → Number) → Number →
+ List Text → List Text
+reflow_threshold_balanced measure width words =
+ let first = reflow_greedily measure width words in
+ tighten measure width (length first) words first
diff --git a/src/IB/SourceDecoding.idric b/src/IB/SourceDecoding.idric
new file mode 100644
index 00000000..d8759c87
--- /dev/null
+++ b/src/IB/SourceDecoding.idric
@@ -0,0 +1,98 @@
+module IB.SourceDecoding
+
+import Data.Text
+import Data.List
+
+-- Named raw boundary: these are source octets, never decoded characters.
+public export
+SourceOctet : Type
+SourceOctet = Bits8
+
+public export
+record HtmlDecodedText where
+ constructor DecodedHtml
+ declared_label : Text
+ selected_encoding : Text
+ original_byte_count : Number
+ decoded_text : Text
+
+export
+decoder_identity : Text
+decoder_identity = "whatwg-windows-1252-e56d49d9176e9a4-v1"
+
+ascii_whitespace : Char → Bool
+ascii_whitespace character = elem (ord character) [9, 10, 12, 13, 32]
+
+ascii_lower : Char → Char
+ascii_lower character =
+ let scalar = ord character in
+ if scalar >= 65 && scalar <= 90 then chr (scalar + 32) else character
+
+normalized_label : Text → Text
+normalized_label label =
+ pack (map ascii_lower
+ (reverse (dropWhile ascii_whitespace
+ (reverse (dropWhile ascii_whitespace (unpack label))))))
+
+export
+windows_1252_label : Text → Bool
+windows_1252_label label = elem (normalized_label label)
+ ["ansi_x3.4-1968", "ascii", "cp1252", "cp819", "csisolatin1",
+ "ibm819", "iso-8859-1", "iso-ir-100", "iso8859-1", "iso88591",
+ "iso_8859-1", "iso_8859-1:1987", "l1", "latin1", "us-ascii",
+ "windows-1252", "x-cp1252"]
+
+-- WHATWG index-windows-1252.txt identifier e56d49d9176e9a4... (2024-09-18).
+-- ASCII and 0xA0..0xFF retain their scalar values. The 0x80..0x9F range
+-- includes both punctuation and the five deliberately retained C1 controls.
+windows_1252_scalar : SourceOctet → Int
+windows_1252_scalar octet =
+ let value : Int = cast octet in
+ case value of
+ 128 ⇒ 0x20AC
+ 129 ⇒ 0x0081
+ 130 ⇒ 0x201A
+ 131 ⇒ 0x0192
+ 132 ⇒ 0x201E
+ 133 ⇒ 0x2026
+ 134 ⇒ 0x2020
+ 135 ⇒ 0x2021
+ 136 ⇒ 0x02C6
+ 137 ⇒ 0x2030
+ 138 ⇒ 0x0160
+ 139 ⇒ 0x2039
+ 140 ⇒ 0x0152
+ 141 ⇒ 0x008D
+ 142 ⇒ 0x017D
+ 143 ⇒ 0x008F
+ 144 ⇒ 0x0090
+ 145 ⇒ 0x2018
+ 146 ⇒ 0x2019
+ 147 ⇒ 0x201C
+ 148 ⇒ 0x201D
+ 149 ⇒ 0x2022
+ 150 ⇒ 0x2013
+ 151 ⇒ 0x2014
+ 152 ⇒ 0x02DC
+ 153 ⇒ 0x2122
+ 154 ⇒ 0x0161
+ 155 ⇒ 0x203A
+ 156 ⇒ 0x0153
+ 157 ⇒ 0x009D
+ 158 ⇒ 0x017E
+ 159 ⇒ 0x0178
+ _ ⇒ value
+
+recognized_bom : List SourceOctet → Bool
+recognized_bom (0xEF :: 0xBB :: 0xBF :: _) = True
+recognized_bom (0xFE :: 0xFF :: _) = True
+recognized_bom (0xFF :: 0xFE :: _) = True
+recognized_bom _ = False
+
+export
+decode_html_bytes : Text → List SourceOctet → Either Text HtmlDecodedText
+decode_html_bytes label octets =
+ if not (windows_1252_label label) then Left "unsupported-html-encoding-label"
+ else if recognized_bom octets then Left "bom-selects-an-unimplemented-decoder"
+ else Right (DecodedHtml label "windows-1252" (length octets)
+ (pack (map (chr . windows_1252_scalar) octets)))
diff --git a/src/ReflowSmoke.idric b/src/ReflowSmoke.idric
new file mode 100644
index 00000000..e4f8431a
--- /dev/null
+++ b/src/ReflowSmoke.idric
@@ -0,0 +1,187 @@
+module ReflowSmoke
+
+import Data.Text
+import IB.Reflow
+import IB.Reflow.Streaming
+import IB.Reflow.KnuthPlass
+import IB.Reflow.Incremental
+import IB.Reflow.Arithmetic
+import System
+
+character_width : Text → Number
+character_width value = length (unpack value)
+
+matches : List Text → Either Text (List Text) → Bool
+matches wanted (Right actual) = wanted ≟ actual
+matches wanted _ = False
+
+join_lines : List Text → Text
+join_lines [] = ""
+join_lines [line] = line
+join_lines (line :: rest) = line ++ " " ++ join_lines rest
+
+keeps_words : List Text → Either Text (List Text) → Bool
+keeps_words original (Right wrapped) =
+ join_lines original ≟ join_lines wrapped
+keeps_words original _ = False
+
+has_error : Either Text (List Text) → Bool
+has_error (Left _) = True
+has_error _ = False
+
+-- Transport chunks are not tokens. In particular "eee" + "eee" must
+-- remain one six-character word. We also assert early line emission.
+streaming_case : (Bool, Bool)
+streaming_case =
+ case begin_stream 8 of
+ Left _ ⇒ (False, False)
+ Right start ⇒
+ let Emitted next1 published1 = feed_chunk character_width start "aa bb cc dd " in
+ let Emitted next2 published2 = feed_chunk character_width next1 "eee" in
+ let Emitted next3 published3 = feed_chunk character_width next2 "eee" in
+ let all_lines =
+ published1 ++ published2 ++ published3 ++ finish_stream character_width next3 in
+ (published1 ≟ ["aa bb cc"], all_lines ≟ ["aa bb cc", "dd", "eeeeee"])
+
+paragraph_case : Bool
+paragraph_case =
+ case begin_stream 8 of
+ Left _ ⇒ False
+ Right initial ⇒
+ let Emitted before _ = feed_chunk character_width initial "aa bb" in
+ let (after, first_paragraph) = end_paragraph character_width before in
+ let Emitted last _ = feed_chunk character_width after "cc dd" in
+ first_paragraph ≟ ["aa bb"] && finish_stream character_width last ≟ ["cc dd"]
+
+preserves_in_every_mode : List reflow_adverb → List Text → Bool
+preserves_in_every_mode [] words = True
+preserves_in_every_mode (mode :: more) words =
+ keeps_words words (reflow (Requirements 10 mode) character_width words) &&
+ preserves_in_every_mode more words
+
+overwide_in_every_mode : List reflow_adverb → Bool
+overwide_in_every_mode [] = True
+overwide_in_every_mode (mode :: more) =
+ matches ["abcdefghij", "x"]
+ (reflow (Requirements 8 mode) character_width ["abcdefghij", "x"]) &&
+ overwide_in_every_mode more
+
+empty_in_every_mode : List reflow_adverb → Bool
+empty_in_every_mode [] = True
+empty_in_every_mode (mode :: more) =
+ matches [] (reflow (Requirements 8 mode) character_width []) &&
+ empty_in_every_mode more
+
+zero_refused_in_every_mode : List reflow_adverb → Bool
+zero_refused_in_every_mode [] = True
+zero_refused_in_every_mode (mode :: more) =
+ has_error (reflow (Requirements 0 mode) character_width ["x"]) &&
+ zero_refused_in_every_mode more
+
+has_adjustment : List JustifiedLine → Bool
+has_adjustment [] = False
+has_adjustment ((Justified _ NoAdjustment _) :: rest) = has_adjustment rest
+has_adjustment (_ :: _) = True
+
+knuth_plan_case : Bool
+knuth_plan_case =
+ case reflow_knuth_plass (default_knuth_settings 8) character_width 8 ["aa", "bb", "cc", "dd", "eeeeee"] of
+ Left _ ⇒ False
+ Right lines ⇒
+ has_adjustment lines &&
+ join_lines (plain_lines lines) ≟ "aa bb cc dd eeeeee"
+
+incremental_case : Bool
+incremental_case =
+ let request = Requirements 8 evenly in
+ let words = ["aa", "bb", "cc", "dd", "eeeeee"] in
+ case reflow_incrementally request "font-1" character_width words Nothing of
+ Left _ ⇒ False
+ Right built ⇒
+ case reflow_incrementally request "font-1" character_width words (Just built.resulting_cache) of
+ Left _ ⇒ False
+ Right reused ⇒
+ case reflow_incrementally request "font-1" character_width ["aa", "bb", "changed"] (Just built.resulting_cache) of
+ Left _ ⇒ False
+ Right edited ⇒
+ case reflow_incrementally (Requirements 7 evenly) "font-1" character_width words (Just built.resulting_cache) of
+ Left _ ⇒ False
+ Right resized ⇒
+ case reflow_incrementally request "font-2" character_width words (Just built.resulting_cache) of
+ Left _ ⇒ False
+ Right new_metric ⇒
+ not built.reused_previous &&
+ reused.reused_previous &&
+ not edited.reused_previous &&
+ not resized.reused_previous &&
+ not new_metric.reused_previous
+
+begin_zero_refused : Bool
+begin_zero_refused =
+ case begin_stream 0 of
+ Left _ ⇒ True
+ Right _ ⇒ False
+
+main : IO ()
+main = do
+ let words = ["aa", "bb", "cc", "dd", "eeeeee"]
+ let greedy_lines = ["aa bb cc", "dd", "eeeeee"]
+ let evenly_lines = ["aa bb", "cc dd", "eeeeee"]
+ let greedy_ok = matches greedy_lines (reflow (Requirements 8 promptly) character_width words)
+ let streaming_ok = matches greedy_lines (reflow (Requirements 8 streamingly) character_width words)
+ let balanced_ok = matches evenly_lines (reflow (Requirements 8 evenly) character_width words)
+ let threshold_ok = matches evenly_lines (reflow (Requirements 8 without_extra_lines) character_width words)
+
+ -- This paragraph discriminates different dynamic-programming objectives.
+ let odd = ["xxxx", "xxxxx", "xx", "xx", "xxxxxx", "x", "xx"]
+ let cubic_ok = matches ["xxxx xxxxx", "xx xx", "xxxxxx", "x xx"] (reflow (Requirements 10 minimizing_raggedness) character_width odd)
+ let final_free_ok = matches ["xxxx xxxxx", "xx xx", "xxxxxx x", "xx"] (reflow (Requirements 10 ignoring_final_line) character_width odd)
+ let minimax_ok = matches ["xxxx", "xxxxx", "xx xx", "xxxxxx", "x xx"] (reflow (Requirements 10 minimizing_worst_gap) character_width odd)
+ let squared_ok = matches ["xxxx", "xxxxx xx", "xx xxxxxx", "x xx"] (reflow (Requirements 10 evenly) character_width odd)
+
+ let modes = [promptly, streamingly, evenly, minimizing_raggedness,
+ ignoring_final_line, minimizing_worst_gap, without_extra_lines,
+ typographically]
+ let content_preserved = preserves_in_every_mode modes odd
+ let long_word_intact = overwide_in_every_mode modes
+ let empty_intact = empty_in_every_mode modes
+ let zero_refused = zero_refused_in_every_mode modes
+ let (emits_early, chunk_invariant) = streaming_case
+ let paragraphs_ok = paragraph_case
+ let arithmetic_ok =
+ capped_badness_quotient 18 3 ≟ 6 &&
+ capped_badness_quotient 11000 1 ≟ 10000 &&
+ capped_badness_quotient 0 100 ≟ 0 &&
+ nonnegative_difference 10 3 ≟ 7 &&
+ nonnegative_difference 3 10 ≟ 0
+ let knuth_ok = knuth_plan_case
+ let incremental_ok = incremental_case
+ let zero_stream_refused = begin_zero_refused
+
+ putStrLn ("reflow-greedy=" ++ show greedy_ok)
+ putStrLn ("reflow-streaming-batch=" ++ show streaming_ok)
+ putStrLn ("reflow-streaming-early=" ++ show emits_early)
+ putStrLn ("reflow-streaming-chunks=" ++ show chunk_invariant)
+ putStrLn ("reflow-streaming-paragraphs=" ++ show paragraphs_ok)
+ putStrLn ("reflow-balanced=" ++ show balanced_ok)
+ putStrLn ("reflow-cubic=" ++ show cubic_ok)
+ putStrLn ("reflow-final-line-free=" ++ show final_free_ok)
+ putStrLn ("reflow-minimax=" ++ show minimax_ok)
+ putStrLn ("reflow-threshold=" ++ show threshold_ok)
+ putStrLn ("reflow-squared-discriminates=" ++ show squared_ok)
+ putStrLn ("reflow-preserves-content=" ++ show content_preserved)
+ putStrLn ("reflow-overwide-intact=" ++ show long_word_intact)
+ putStrLn ("reflow-empty=" ++ show empty_intact)
+ putStrLn ("reflow-zero-refused=" ++ show zero_refused)
+ putStrLn ("reflow-stream-zero-refused=" ++ show zero_stream_refused)
+ putStrLn ("reflow-knuth-spacings=" ++ show knuth_ok)
+ putStrLn ("reflow-incremental-revisions=" ++ show incremental_ok)
+ putStrLn ("reflow-arithmetic=" ++ show arithmetic_ok)
+
+ if greedy_ok && streaming_ok && emits_early && chunk_invariant &&
+ paragraphs_ok && balanced_ok && cubic_ok && final_free_ok &&
+ minimax_ok && threshold_ok && squared_ok && content_preserved &&
+ long_word_intact && empty_intact && zero_refused && zero_stream_refused &&
+ knuth_ok && incremental_ok && arithmetic_ok
+ then pure ()
+ else exitFailure
diff --git a/src/SourceDecodingCommand.idric b/src/SourceDecodingCommand.idric
new file mode 100644
index 00000000..2515d600
--- /dev/null
+++ b/src/SourceDecodingCommand.idric
@@ -0,0 +1,85 @@
+module SourceDecodingCommand
+
+import Data.Text
+import Data.Buffer
+import System
+import System.File
+import System.File.Buffer
+import IB.SourceDecoding
+
+-- This command reads a bounded frozen byte file. It neither acquires a source
+-- nor supplies canonical-store, redirect or navigation admission evidence.
+source_byte_limit : Int
+source_byte_limit = 4194304
+
+covering
+read_source_octets : Text → IO (Either Text (List SourceOctet))
+read_source_octets path = do
+ opened ← openFile path Read
+ case opened of
+ Left _ ⇒ pure (Left "source-open-failed")
+ Right file ⇒ do
+ sized ← fileSize file
+ result ← case sized of
+ Left _ ⇒ pure (Left "source-size-unavailable")
+ Right count ⇒
+ if count < 0 || count > source_byte_limit
+ then pure (Left "source-outside-four-mebibyte-bound")
+ else do
+ allocated ← newBuffer count
+ case allocated of
+ Nothing ⇒ pure (Left "source-buffer-unavailable")
+ Just buffer ⇒ do
+ read_result ← readBufferData file buffer 0 count
+ case read_result of
+ Left _ ⇒ pure (Left "source-read-failed")
+ Right actual_count ⇒
+ if not (actual_count ≟ count) then pure (Left "short-source-read")
+ else do
+ probe ← newBuffer 1
+ case probe of
+ Nothing ⇒ pure (Left "source-probe-unavailable")
+ Just tail_buffer ⇒ do
+ tail_result ← readBufferData file tail_buffer 0 1
+ case tail_result of
+ Right 0 ⇒ map Right (bufferData' buffer)
+ _ ⇒ pure (Left "source-size-changed-or-eof-unavailable")
+ closeFile file
+ pure result
+
+write_decoded_utf8 : Text → Text → IO (Either Text ())
+write_decoded_utf8 path text = do
+ let count = stringByteLength text
+ allocated ← newBuffer count
+ case allocated of
+ Nothing ⇒ pure (Left "decoded-buffer-unavailable")
+ Just buffer ⇒ do
+ setString buffer 0 text
+ written ← writeBufferToFile path buffer count
+ case written of
+ Left _ ⇒ pure (Left "decoded-write-failed")
+ Right () ⇒ pure (Right ())
+
+covering
+main : IO ()
+main = do
+ arguments ← getArgs
+ case arguments of
+ [_, label, input_path, output_path] ⇒ do
+ if input_path ≟ output_path then die "source-decoding: output-is-input" else pure ()
+ read_result ← read_source_octets input_path
+ case read_result of
+ Left reason ⇒ die ("source-decoding: " ++ reason)
+ Right octets ⇒
+ case decode_html_bytes label octets of
+ Left reason ⇒ die ("source-decoding: " ++ reason)
+ Right decoded ⇒ do
+ written ← write_decoded_utf8 output_path decoded.decoded_text
+ case written of
+ Left reason ⇒ die ("source-decoding: " ++ reason)
+ Right () ⇒ do
+ putStrLn ("original_byte_count\t" ++ show decoded.original_byte_count)
+ putStrLn ("decoded_codepoint_count\t" ++ show (length (unpack decoded.decoded_text)))
+ putStrLn ("selected_encoding\t" ++ decoded.selected_encoding)
+ putStrLn ("decoder_identity\t" ++ decoder_identity)
+ _ ⇒ die "usage: ib-source-decoder LABEL RAW_BYTES DISPOSABLE_UTF8"
diff --git a/src/SourceReflowSmoke.idric b/src/SourceReflowSmoke.idric
new file mode 100644
index 00000000..41d0c7d9
--- /dev/null
+++ b/src/SourceReflowSmoke.idric
@@ -0,0 +1,114 @@
+module SourceReflowSmoke
+
+import Data.Text
+import IB.Reflow
+import IB.Reflow.Source
+import IB.Reflow.SourceBreaks
+import System
+
+codepoint_width : Text → Number
+codepoint_width value = length (unpack value)
+
+display_lines : List SourceLine → List Text
+display_lines [] = []
+display_lines (line :: rest) =
+ line.visible_text :: display_lines rest
+
+matches : List Text → Either Text (List SourceLine) → Bool
+matches wanted (Right lines) = wanted ≟ display_lines lines
+matches wanted _ = False
+
+refused : Either Text (List SourceLine) → Bool
+refused (Left _) = True
+refused _ = False
+
+join_raw : Text → List SourceLine → Text
+join_raw source [] = ""
+join_raw source (line :: rest) =
+ source_for_line source line ++ join_raw source rest
+
+contiguous : Text → Number → List SourceLine → Bool
+contiguous source offset [] = offset ≟ length (unpack source)
+contiguous source offset (line :: rest) =
+ line.first_codepoint ≟ offset &&
+ line.after_last_codepoint > offset &&
+ line.after_last_codepoint <= length (unpack source) &&
+ contiguous source line.after_last_codepoint rest
+
+source_unchanged : Text → Either Text (List SourceLine) → Bool
+source_unchanged source (Right lines) =
+ join_raw source lines ≟ source &&
+ contiguous source 0 lines
+source_unchanged source _ = False
+
+kind_is : BreakKind → BreakKind → Bool
+kind_is PossibleBreak PossibleBreak = True
+kind_is MandatoryBreak MandatoryBreak = True
+kind_is DiscretionaryHyphen DiscretionaryHyphen = True
+kind_is ZeroWidthBreak ZeroWidthBreak = True
+kind_is SourceEnd SourceEnd = True
+kind_is _ _ = False
+
+has_cut : Number → BreakKind → List SourceBreak → Bool
+has_cut offset wanted [] = False
+has_cut offset wanted (cut :: rest) =
+ (offset ≟ cut.source_offset && kind_is wanted cut.break_kind) ||
+ has_cut offset wanted rest
+
+some_breaks_are_refused : Bool
+some_breaks_are_refused =
+ let source = "a\r\nb" in
+ let no_mandatory = [At 4 SourceEnd] in
+ let inside_crlf = [At 2 PossibleBreak, At 3 MandatoryBreak, At 4 SourceEnd] in
+ let duplicate = [At 2 PossibleBreak, At 2 PossibleBreak, At 3 SourceEnd] in
+ not (valid_source_breaks source no_mandatory) &&
+ not (valid_source_breaks source inside_crlf) &&
+ not (valid_source_breaks "a b" duplicate) &&
+ not (valid_source_breaks "éx" [At 1 PossibleBreak, At 3 SourceEnd]) &&
+ not (valid_source_breaks "👩💻x" [At 2 PossibleBreak, At 4 SourceEnd])
+
+all_modes_preserve : Text → List reflow_adverb → Bool
+all_modes_preserve source [] = True
+all_modes_preserve source (mode :: rest) =
+ source_unchanged source
+ (reflow_source (Requirements 2 mode) codepoint_width source) &&
+ all_modes_preserve source rest
+
+run_cases : Bool
+run_cases =
+ let basic = matches ["red", "blue"] (reflow_source (Requirements 4 promptly) codepoint_width "red blue") in
+ let soft = "abcd" in
+ let soft_short = matches ["ab-", "cd"] (reflow_source (Requirements 3 promptly) codepoint_width soft) in
+ let soft_long = matches ["abcd"] (reflow_source (Requirements 4 evenly) codepoint_width soft) in
+ let soft_source = source_unchanged soft (reflow_source (Requirements 3 promptly) codepoint_width soft) in
+ let zero_width_space = matches ["ab", "cd"] (reflow_source (Requirements 2 promptly) codepoint_width "abcd") in
+ let han = matches ["漢字", "漢字"] (reflow_source (Requirements 2 evenly) codepoint_width "漢字漢字") in
+ let crlf = matches ["a", "b"] (reflow_source (Requirements 1 promptly) codepoint_width "a\r\nb") in
+ let crlf_source = source_unchanged "a\r\nb" (reflow_source (Requirements 1 promptly) codepoint_width "a\r\nb") in
+ let blank_line = matches ["a", "", "b"] (reflow_source (Requirements 1 promptly) codepoint_width "a\n\nb") in
+ let nbspace = matches ["a b", "c"] (reflow_source (Requirements 3 promptly) codepoint_width "a b c") in
+ let right_to_left = matches ["שלום", "hello"] (reflow_source (Requirements 5 promptly) codepoint_width "שלום hello") in
+ let final_newline = matches ["end"] (reflow_source (Requirements 5 promptly) codepoint_width "end\n") in
+ let no_break_before_joiner = not (has_cut 2 PossibleBreak (source_breaks "a b")) in
+ let correct_kinds =
+ has_cut 3 MandatoryBreak (source_breaks "a\r\nb") &&
+ has_cut 3 DiscretionaryHyphen (source_breaks "abcd") &&
+ has_cut 3 ZeroWidthBreak (source_breaks "abcd") in
+ let preserves_every_mode = all_modes_preserve "a\r\n漢字 abcd" [promptly, evenly, minimizing_raggedness, ignoring_final_line, minimizing_worst_gap, without_extra_lines] in
+ let unsupported_modes =
+ refused (reflow_source (Requirements 5 typographically) codepoint_width "aa bb") &&
+ refused (reflow_source (Requirements 5 streamingly) codepoint_width "aa bb") in
+ let bad_width = refused (reflow_source (Requirements 0 promptly) codepoint_width "abc") in
+ let bad_breaks = refused (reflow_at_breaks (Requirements 5 promptly) codepoint_width "a\r\nb" [At 4 SourceEnd]) in
+ let empty_input = matches [] (reflow_source (Requirements 5 promptly) codepoint_width "") in
+ basic && soft_short && soft_long && soft_source && zero_width_space &&
+ han && crlf && crlf_source && blank_line && nbspace && right_to_left &&
+ final_newline && no_break_before_joiner && correct_kinds &&
+ preserves_every_mode && unsupported_modes && bad_width && bad_breaks &&
+ empty_input && some_breaks_are_refused
+
+main : IO ()
+main = do
+ let passed = run_cases
+ putStrLn ("source-reflow-unicode-offset-cases=" ++ show passed)
+ if passed then pure () else exitFailure
diff --git a/tests/fixtures/ib-html/arxiv.html b/tests/fixtures/ib-html/arxiv.html
new file mode 100644
index 00000000..a6f34219
--- /dev/null
+++ b/tests/fixtures/ib-html/arxiv.html
@@ -0,0 +1,9 @@
+
+Article & algebra
+2 Introduction
+A word with é and 🙂.
+
+See abstract afterward.
+
Figure 1
+
+
diff --git a/tests/fixtures/ib-html/arxiv.prepaint b/tests/fixtures/ib-html/arxiv.prepaint
new file mode 100644
index 00000000..cdc93cb8
--- /dev/null
+++ b/tests/fixtures/ib-html/arxiv.prepaint
@@ -0,0 +1,13 @@
+ib-prepaint 1
+revision 0 complete
+requested-url https://arxiv.org/html/2401.00100
+resolved-url https://arxiv.org/html/2401.00100
+title Article & algebra
+heading 2 2 Introduction
+text A word with é and 🙂.
+row Name Value
+text See
+link abstract https://arxiv.org/abs/2401.00100
+text afterward.
+text Image pending acquisition: Diagram — Figure 1
+end
diff --git a/tests/fixtures/ib-html/example.html b/tests/fixtures/ib-html/example.html
new file mode 100644
index 00000000..e8770261
--- /dev/null
+++ b/tests/fixtures/ib-html/example.html
@@ -0,0 +1,6 @@
+
+Example Domain
+Example Domain
+This domain is for use in illustrative examples.
+Learn more
+
diff --git a/tests/fixtures/ib-html/example.prepaint b/tests/fixtures/ib-html/example.prepaint
new file mode 100644
index 00000000..abdabec9
--- /dev/null
+++ b/tests/fixtures/ib-html/example.prepaint
@@ -0,0 +1,9 @@
+ib-prepaint 1
+revision 0 complete
+requested-url https://example.com/
+resolved-url https://example.com/
+title Example Domain
+heading 1 Example Domain
+text This domain is for use in illustrative examples.
+link Learn more https://www.iana.org/domains/example
+end
diff --git a/tests/fixtures/index-windows-1252.txt b/tests/fixtures/index-windows-1252.txt
new file mode 100644
index 00000000..af1edbcd
--- /dev/null
+++ b/tests/fixtures/index-windows-1252.txt
@@ -0,0 +1,134 @@
+# For details on index index-windows-1252.txt see the Encoding Standard
+# https://encoding.spec.whatwg.org/
+#
+# Identifier: e56d49d9176e9a412283cf29ac9bd613f5620462f2a080a84eceaf974cfa18b7
+# Date: 2024-09-18
+
+ 0 0x20AC € (EURO SIGN)
+ 1 0x0081 ()
+ 2 0x201A ‚ (SINGLE LOW-9 QUOTATION MARK)
+ 3 0x0192 ƒ (LATIN SMALL LETTER F WITH HOOK)
+ 4 0x201E „ (DOUBLE LOW-9 QUOTATION MARK)
+ 5 0x2026 … (HORIZONTAL ELLIPSIS)
+ 6 0x2020 † (DAGGER)
+ 7 0x2021 ‡ (DOUBLE DAGGER)
+ 8 0x02C6 ˆ (MODIFIER LETTER CIRCUMFLEX ACCENT)
+ 9 0x2030 ‰ (PER MILLE SIGN)
+ 10 0x0160 Š (LATIN CAPITAL LETTER S WITH CARON)
+ 11 0x2039 ‹ (SINGLE LEFT-POINTING ANGLE QUOTATION MARK)
+ 12 0x0152 Œ (LATIN CAPITAL LIGATURE OE)
+ 13 0x008D ()
+ 14 0x017D Ž (LATIN CAPITAL LETTER Z WITH CARON)
+ 15 0x008F ()
+ 16 0x0090 ()
+ 17 0x2018 ‘ (LEFT SINGLE QUOTATION MARK)
+ 18 0x2019 ’ (RIGHT SINGLE QUOTATION MARK)
+ 19 0x201C “ (LEFT DOUBLE QUOTATION MARK)
+ 20 0x201D ” (RIGHT DOUBLE QUOTATION MARK)
+ 21 0x2022 • (BULLET)
+ 22 0x2013 – (EN DASH)
+ 23 0x2014 — (EM DASH)
+ 24 0x02DC ˜ (SMALL TILDE)
+ 25 0x2122 ™ (TRADE MARK SIGN)
+ 26 0x0161 š (LATIN SMALL LETTER S WITH CARON)
+ 27 0x203A › (SINGLE RIGHT-POINTING ANGLE QUOTATION MARK)
+ 28 0x0153 œ (LATIN SMALL LIGATURE OE)
+ 29 0x009D ()
+ 30 0x017E ž (LATIN SMALL LETTER Z WITH CARON)
+ 31 0x0178 Ÿ (LATIN CAPITAL LETTER Y WITH DIAERESIS)
+ 32 0x00A0 (NO-BREAK SPACE)
+ 33 0x00A1 ¡ (INVERTED EXCLAMATION MARK)
+ 34 0x00A2 ¢ (CENT SIGN)
+ 35 0x00A3 £ (POUND SIGN)
+ 36 0x00A4 ¤ (CURRENCY SIGN)
+ 37 0x00A5 ¥ (YEN SIGN)
+ 38 0x00A6 ¦ (BROKEN BAR)
+ 39 0x00A7 § (SECTION SIGN)
+ 40 0x00A8 ¨ (DIAERESIS)
+ 41 0x00A9 © (COPYRIGHT SIGN)
+ 42 0x00AA ª (FEMININE ORDINAL INDICATOR)
+ 43 0x00AB « (LEFT-POINTING DOUBLE ANGLE QUOTATION MARK)
+ 44 0x00AC ¬ (NOT SIGN)
+ 45 0x00AD (SOFT HYPHEN)
+ 46 0x00AE ® (REGISTERED SIGN)
+ 47 0x00AF ¯ (MACRON)
+ 48 0x00B0 ° (DEGREE SIGN)
+ 49 0x00B1 ± (PLUS-MINUS SIGN)
+ 50 0x00B2 ² (SUPERSCRIPT TWO)
+ 51 0x00B3 ³ (SUPERSCRIPT THREE)
+ 52 0x00B4 ´ (ACUTE ACCENT)
+ 53 0x00B5 µ (MICRO SIGN)
+ 54 0x00B6 ¶ (PILCROW SIGN)
+ 55 0x00B7 · (MIDDLE DOT)
+ 56 0x00B8 ¸ (CEDILLA)
+ 57 0x00B9 ¹ (SUPERSCRIPT ONE)
+ 58 0x00BA º (MASCULINE ORDINAL INDICATOR)
+ 59 0x00BB » (RIGHT-POINTING DOUBLE ANGLE QUOTATION MARK)
+ 60 0x00BC ¼ (VULGAR FRACTION ONE QUARTER)
+ 61 0x00BD ½ (VULGAR FRACTION ONE HALF)
+ 62 0x00BE ¾ (VULGAR FRACTION THREE QUARTERS)
+ 63 0x00BF ¿ (INVERTED QUESTION MARK)
+ 64 0x00C0 À (LATIN CAPITAL LETTER A WITH GRAVE)
+ 65 0x00C1 Á (LATIN CAPITAL LETTER A WITH ACUTE)
+ 66 0x00C2 Â (LATIN CAPITAL LETTER A WITH CIRCUMFLEX)
+ 67 0x00C3 Ã (LATIN CAPITAL LETTER A WITH TILDE)
+ 68 0x00C4 Ä (LATIN CAPITAL LETTER A WITH DIAERESIS)
+ 69 0x00C5 Å (LATIN CAPITAL LETTER A WITH RING ABOVE)
+ 70 0x00C6 Æ (LATIN CAPITAL LETTER AE)
+ 71 0x00C7 Ç (LATIN CAPITAL LETTER C WITH CEDILLA)
+ 72 0x00C8 È (LATIN CAPITAL LETTER E WITH GRAVE)
+ 73 0x00C9 É (LATIN CAPITAL LETTER E WITH ACUTE)
+ 74 0x00CA Ê (LATIN CAPITAL LETTER E WITH CIRCUMFLEX)
+ 75 0x00CB Ë (LATIN CAPITAL LETTER E WITH DIAERESIS)
+ 76 0x00CC Ì (LATIN CAPITAL LETTER I WITH GRAVE)
+ 77 0x00CD Í (LATIN CAPITAL LETTER I WITH ACUTE)
+ 78 0x00CE Î (LATIN CAPITAL LETTER I WITH CIRCUMFLEX)
+ 79 0x00CF Ï (LATIN CAPITAL LETTER I WITH DIAERESIS)
+ 80 0x00D0 Ð (LATIN CAPITAL LETTER ETH)
+ 81 0x00D1 Ñ (LATIN CAPITAL LETTER N WITH TILDE)
+ 82 0x00D2 Ò (LATIN CAPITAL LETTER O WITH GRAVE)
+ 83 0x00D3 Ó (LATIN CAPITAL LETTER O WITH ACUTE)
+ 84 0x00D4 Ô (LATIN CAPITAL LETTER O WITH CIRCUMFLEX)
+ 85 0x00D5 Õ (LATIN CAPITAL LETTER O WITH TILDE)
+ 86 0x00D6 Ö (LATIN CAPITAL LETTER O WITH DIAERESIS)
+ 87 0x00D7 × (MULTIPLICATION SIGN)
+ 88 0x00D8 Ø (LATIN CAPITAL LETTER O WITH STROKE)
+ 89 0x00D9 Ù (LATIN CAPITAL LETTER U WITH GRAVE)
+ 90 0x00DA Ú (LATIN CAPITAL LETTER U WITH ACUTE)
+ 91 0x00DB Û (LATIN CAPITAL LETTER U WITH CIRCUMFLEX)
+ 92 0x00DC Ü (LATIN CAPITAL LETTER U WITH DIAERESIS)
+ 93 0x00DD Ý (LATIN CAPITAL LETTER Y WITH ACUTE)
+ 94 0x00DE Þ (LATIN CAPITAL LETTER THORN)
+ 95 0x00DF ß (LATIN SMALL LETTER SHARP S)
+ 96 0x00E0 à (LATIN SMALL LETTER A WITH GRAVE)
+ 97 0x00E1 á (LATIN SMALL LETTER A WITH ACUTE)
+ 98 0x00E2 â (LATIN SMALL LETTER A WITH CIRCUMFLEX)
+ 99 0x00E3 ã (LATIN SMALL LETTER A WITH TILDE)
+100 0x00E4 ä (LATIN SMALL LETTER A WITH DIAERESIS)
+101 0x00E5 å (LATIN SMALL LETTER A WITH RING ABOVE)
+102 0x00E6 æ (LATIN SMALL LETTER AE)
+103 0x00E7 ç (LATIN SMALL LETTER C WITH CEDILLA)
+104 0x00E8 è (LATIN SMALL LETTER E WITH GRAVE)
+105 0x00E9 é (LATIN SMALL LETTER E WITH ACUTE)
+106 0x00EA ê (LATIN SMALL LETTER E WITH CIRCUMFLEX)
+107 0x00EB ë (LATIN SMALL LETTER E WITH DIAERESIS)
+108 0x00EC ì (LATIN SMALL LETTER I WITH GRAVE)
+109 0x00ED í (LATIN SMALL LETTER I WITH ACUTE)
+110 0x00EE î (LATIN SMALL LETTER I WITH CIRCUMFLEX)
+111 0x00EF ï (LATIN SMALL LETTER I WITH DIAERESIS)
+112 0x00F0 ð (LATIN SMALL LETTER ETH)
+113 0x00F1 ñ (LATIN SMALL LETTER N WITH TILDE)
+114 0x00F2 ò (LATIN SMALL LETTER O WITH GRAVE)
+115 0x00F3 ó (LATIN SMALL LETTER O WITH ACUTE)
+116 0x00F4 ô (LATIN SMALL LETTER O WITH CIRCUMFLEX)
+117 0x00F5 õ (LATIN SMALL LETTER O WITH TILDE)
+118 0x00F6 ö (LATIN SMALL LETTER O WITH DIAERESIS)
+119 0x00F7 ÷ (DIVISION SIGN)
+120 0x00F8 ø (LATIN SMALL LETTER O WITH STROKE)
+121 0x00F9 ù (LATIN SMALL LETTER U WITH GRAVE)
+122 0x00FA ú (LATIN SMALL LETTER U WITH ACUTE)
+123 0x00FB û (LATIN SMALL LETTER U WITH CIRCUMFLEX)
+124 0x00FC ü (LATIN SMALL LETTER U WITH DIAERESIS)
+125 0x00FD ý (LATIN SMALL LETTER Y WITH ACUTE)
+126 0x00FE þ (LATIN SMALL LETTER THORN)
+127 0x00FF ÿ (LATIN SMALL LETTER Y WITH DIAERESIS)
diff --git a/tests/prepaint_v1_oracle.c b/tests/prepaint_v1_oracle.c
new file mode 100644
index 00000000..ccf0e4f3
--- /dev/null
+++ b/tests/prepaint_v1_oracle.c
@@ -0,0 +1,177 @@
+/*
+ * Independent narrow Version 1 *consumer*, not a renderer or alternate HTML
+ * parser. The producer/Idriç serializer is not linked into this executable.
+ * It validates the published complete projection's grammar and unsafe targets.
+ */
+#define _POSIX_C_SOURCE 200809L
+#include
+#include
+#include
+#include
+#include
+
+enum { LIMIT_BYTES = 4194304, LIMIT_BLOCKS = 4096, LIMIT_REVISIONS = 32 };
+static int starts(const char *value, const char *prefix) {
+ return strncmp(value, prefix, strlen(prefix)) == 0;
+}
+static int http_url(const char *value) {
+ const char *host;
+ if (starts(value, "https://")) host = value + 8;
+ else if (starts(value, "http://")) host = value + 7;
+ else return 0;
+ if (!*host || *host == '/' || *host == '?' || *host == '#') return 0;
+ for (const char *p = host; *p && *p != '/' && *p != '?' && *p != '#'; ++p) {
+ if ((unsigned char)*p <= 32 || (unsigned char)*p >= 127 || *p == '@') return 0;
+ }
+ for (const unsigned char *p = (const unsigned char *)value; *p; ++p)
+ if (*p <= 32 || *p >= 127) return 0;
+ return 1;
+}
+static int local_image(const char *value) {
+ return starts(value, "content:") || starts(value, "asset:") ||
+ starts(value, "resource:") || starts(value, "file:");
+}
+/* Reject malformed UTF-8, overlong sequences, surrogates and >U+10FFFF. */
+static int valid_utf8(const unsigned char *p, size_t n) {
+ for (size_t i = 0; i < n;) {
+ unsigned c = p[i++];
+ if (c < 0x80) { if (c == 0) return 0; continue; }
+ unsigned need, min;
+ if (c >= 0xc2 && c <= 0xdf) { need = 1; min = 0x80; c &= 0x1f; }
+ else if (c >= 0xe0 && c <= 0xef) { need = 2; min = 0x800; c &= 0x0f; }
+ else if (c >= 0xf0 && c <= 0xf4) { need = 3; min = 0x10000; c &= 0x07; }
+ else return 0;
+ if (i + need > n) return 0;
+ for (unsigned j = 0; j < need; ++j) {
+ unsigned d = p[i++];
+ if ((d & 0xc0) != 0x80) return 0;
+ c = (c << 6) | (d & 0x3f);
+ }
+ if (c < min || c > 0x10ffff || (c >= 0xd800 && c <= 0xdfff)) return 0;
+ }
+ return 1;
+}
+static int number(const char *value, unsigned long *out) {
+ if (!*value) return 0;
+ unsigned long x = 0;
+ for (const unsigned char *p = (const unsigned char *)value; *p; ++p) {
+ if (*p < '0' || *p > '9' || x > (ULONG_MAX - (*p - '0')) / 10) return 0;
+ x = x * 10 + *p - '0';
+ }
+ *out = x;
+ return 1;
+}
+/* Every tab is a structural delimiter; literal tabs in values must be \\t. */
+static int fields(char *line, char **parts, size_t *count) {
+ size_t n = 0;
+ parts[n++] = line;
+ for (char *p = line; *p; ++p) {
+ if (*p == '\r' || *p == '\n') return 0;
+ if (*p == '\\') {
+ if (!p[1] || !(p[1] == 'n' || p[1] == 'r' ||
+ p[1] == 't' || p[1] == '\\')) return 0;
+ ++p;
+ } else if (*p == '\t') {
+ if (n >= LIMIT_BLOCKS + 5) return 0;
+ *p = 0;
+ parts[n++] = p + 1;
+ }
+ }
+ *count = n;
+ return 1;
+}
+static int check_file(const char *filename) {
+ FILE *f = fopen(filename, "rb");
+ if (!f) return 0;
+ if (fseek(f, 0, SEEK_END) != 0) { fclose(f); return 0; }
+ long length = ftell(f);
+ if (length < 0 || length > LIMIT_BYTES || fseek(f, 0, SEEK_SET) != 0) {
+ fclose(f); return 0;
+ }
+ size_t n = (size_t)length;
+ char *buf = malloc(n + 1);
+ char **parts = malloc((LIMIT_BLOCKS + 5) * sizeof *parts);
+ if (!buf || !parts) { free(buf); free(parts); fclose(f); return 0; }
+ int ok = fread(buf, 1, n, f) == n && !ferror(f);
+ fclose(f);
+ if (!ok || !valid_utf8((const unsigned char *)buf, n)) {
+ free(buf); free(parts); return 0;
+ }
+ buf[n] = 0;
+ unsigned long previous = 0;
+ unsigned revisions = 0, blocks = 0;
+ /* state 0=header, 1=revision, 2=requested, 3=resolved,
+ * 4=title, 5=blocks/end */
+ int state = 0;
+ size_t cursor = 0;
+ for (; cursor < n && ok;) {
+ char *line = buf + cursor;
+ char *end = memchr(line, '\n', n - cursor);
+ if (!end) { ok = 0; break; }
+ *end = 0;
+ cursor = (size_t)(end - buf) + 1;
+ size_t fields_count = 0;
+ if (!fields(line, parts, &fields_count)) { ok = 0; break; }
+ const char *kind = parts[0];
+ if (state == 0) {
+ ok = fields_count == 2 && strcmp(kind, "ib-prepaint") == 0 &&
+ strcmp(parts[1], "1") == 0;
+ state = 1;
+ } else if (state == 1) {
+ unsigned long seq = 0;
+ ok = fields_count == 3 && strcmp(kind, "revision") == 0 &&
+ number(parts[1], &seq) && (revisions == 0 || seq > previous) &&
+ strcmp(parts[2], "complete") == 0 &&
+ ++revisions <= LIMIT_REVISIONS;
+ previous = seq; blocks = 0; state = 2;
+ } else if (state == 2) {
+ ok = fields_count == 2 && strcmp(kind, "requested-url") == 0 &&
+ http_url(parts[1]); state = 3;
+ } else if (state == 3) {
+ ok = fields_count == 2 && strcmp(kind, "resolved-url") == 0 &&
+ http_url(parts[1]); state = 4;
+ } else if (state == 4) {
+ ok = fields_count == 2 && strcmp(kind, "title") == 0;
+ state = 5;
+ } else if (strcmp(kind, "end") == 0) {
+ ok = fields_count == 1;
+ state = 1;
+ } else {
+ ++blocks;
+ ok = blocks <= LIMIT_BLOCKS;
+ if (strcmp(kind, "heading") == 0) {
+ ok = ok && fields_count == 3 && strlen(parts[1]) == 1 &&
+ parts[1][0] >= '1' && parts[1][0] <= '6';
+ } else if (strcmp(kind, "text") == 0) {
+ ok = ok && fields_count == 2;
+ } else if (strcmp(kind, "link") == 0) {
+ ok = ok && fields_count == 3 && http_url(parts[2]);
+ } else if (strcmp(kind, "row") == 0) {
+ ok = ok && fields_count >= 2;
+ } else if (strcmp(kind, "form") == 0) {
+ /* The current converter emits non-interactive form descriptions. */
+ ok = 0;
+ } else if (strcmp(kind, "image") == 0) {
+ ok = ok && (fields_count == 4 || fields_count == 5) &&
+ local_image(parts[1]) &&
+ (fields_count != 5 || http_url(parts[4]));
+ } else ok = 0;
+ }
+ }
+ ok = ok && revisions > 0 && state == 1 && cursor == n;
+ free(buf);
+ free(parts);
+ return ok;
+}
+int main(int argc, char **argv) {
+ if (argc != 2) {
+ fprintf(stderr, "usage: prepaint-v1-oracle FILE\n");
+ return 2;
+ }
+ if (!check_file(argv[1])) {
+ fprintf(stderr, "independent-prepaint-v1: REFUSED\n");
+ return 1;
+ }
+ puts("independent-prepaint-v1: PASS");
+ return 0;
+}
diff --git a/tests/source-decoding-mutations.grease b/tests/source-decoding-mutations.grease
new file mode 100644
index 00000000..dddda40c
--- /dev/null
+++ b/tests/source-decoding-mutations.grease
@@ -0,0 +1,40 @@
+#!/usr/bin/env grease
+# Compile actual known-bad decoders; never edit the implementation under test.
+umask 077
+var tests_directory = $(dirname -- $0)
+var root = $(realpath -- "$tests_directory/..")
+var compiler = ENV.IDRIC
+var temporary = $(mktemp -d)
+trap --add EXIT { rm -rf -- $temporary }
+
+proc compile_and_reject(source, name) {
+ var directory = "$temporary/$name"
+ mkdir -p -- "$directory/IB"
+ cp -- $source "$directory/IB/SourceDecoding.idric"
+ cp -- "$root/examples/autogenerated/source-byte-decoding/SourceDecodingChecks.idric" "$directory/SourceDecodingChecks.idric"
+ var previous = $(pwd)
+ cd $directory
+ $compiler SourceDecodingChecks.idric -o checks > "$directory/compile.log" 2>&1
+ cd $previous
+ try {
+ "$directory/build/exec/checks" "$root/tests/fixtures/index-windows-1252.txt" "$directory/unused.raw" "$directory/unused.utf8" > "$directory/result.log" 2>&1
+ }
+ if (not _error.code) { write -- "FAIL $name mutant passed normative oracle" >&2; exit 1 }
+ grep -F 'FAIL all 256 octets match normative index' "$directory/result.log" > /dev/null
+ write -- "PASS compiled $name mutant rejected by normative scalar oracle"
+}
+
+# Wrong mechanism: interpret every source octet as the identically numbered
+# Unicode scalar, ignoring HTML's windows-1252 punctuation mapping.
+sed 's/chr \. windows_1252_scalar/chr . cast/' "$root/src/IB/SourceDecoding.idric" > "$temporary/latin1.idric"
+if cmp -s "$root/src/IB/SourceDecoding.idric" "$temporary/latin1.idric" { exit 1 }
+compile_and_reject "$temporary/latin1.idric" 'naive-latin1'
+
+# Wrong mechanism: a non-WHATWG undefined-byte policy replaces five C1 slots.
+sed -e 's/129 ⇒ 0x0081/129 ⇒ 0xFFFD/' \
+ -e 's/141 ⇒ 0x008D/141 ⇒ 0xFFFD/' \
+ -e 's/143 ⇒ 0x008F/143 ⇒ 0xFFFD/' \
+ -e 's/144 ⇒ 0x0090/144 ⇒ 0xFFFD/' \
+ -e 's/157 ⇒ 0x009D/157 ⇒ 0xFFFD/' \
+ "$root/src/IB/SourceDecoding.idric" > "$temporary/replacement.idric"
+compile_and_reject "$temporary/replacement.idric" 'undefined-byte-replacement'
diff --git a/tests/source-decoding.grease b/tests/source-decoding.grease
new file mode 100644
index 00000000..128374d8
--- /dev/null
+++ b/tests/source-decoding.grease
@@ -0,0 +1,130 @@
+#!/usr/bin/env grease
+# Actual Idriç binary decoding and source-bound derivative publication.
+umask 077
+var tests_directory = $(dirname -- $0)
+var root = $(realpath -- "$tests_directory/..")
+var runner = ENV.GREASE
+if (len(ARGV) !== 4) {
+ write -- 'usage: source-decoding.grease SEMANTIC_CHECKS DECODER GOOGLE_BODY GOOGLE_HTTP_METADATA' >&2
+ exit 2
+}
+var checks = ARGV[0]
+var decoder = ARGV[1]
+var google = ARGV[2]
+var google_metadata = ARGV[3]
+var temporary = $(mktemp -d)
+trap --add EXIT { rm -rf -- $temporary }
+
+proc descriptor(raw, path, charset='ISO-8859-1') {
+ var hash = $(sha256sum -- $raw | cut -d ' ' -f 1)
+ var count = $(wc -c < $raw | tr -d '[:space:]')
+ printf 'source_key\tfixture:retained-byte-decoding\nsource_generation\tfixture-generation-1\nsha256\t%s\nbyte_count\t%s\ncharset\t%s\nnavigation_admitted\tNO\nredirect_count\t1\n' $hash $count $charset > $path
+}
+
+proc publish(producer, metadata, raw, destination) {
+ $runner "$root/bin/ib_decode_html_bytes.grease" $producer $metadata $raw $destination
+}
+
+proc refuse(producer, metadata, raw, destination, expected, error) {
+ try { publish $producer $metadata $raw $destination > /dev/null 2> $error }
+ if (not _error.code) { write -- 'FAIL expected derivative refusal' >&2; exit 1 }
+ grep -F -- $expected $error > /dev/null
+ test ! -e $destination
+}
+
+$checks "$root/tests/fixtures/index-windows-1252.txt" "$temporary/all.raw" "$temporary/expected.utf8"
+$decoder ' ISO-8859-1 ' "$temporary/all.raw" "$temporary/direct.utf8" > "$temporary/direct.tsv"
+cmp -- "$temporary/expected.utf8" "$temporary/direct.utf8"
+test $(wc -c < "$temporary/all.raw") -eq 256
+# Independent byte-level controls avoid relying only on the test's shared
+# UTF-8 buffer writer: 128 ASCII bytes + 81 indexed bytes + 192 Latin bytes.
+test $(wc -c < "$temporary/direct.utf8") -eq 401
+head -c 128 -- "$temporary/all.raw" > "$temporary/ascii.raw"
+head -c 128 -- "$temporary/direct.utf8" > "$temporary/ascii.utf8"
+cmp -- "$temporary/ascii.raw" "$temporary/ascii.utf8"
+test $(od -An -v -tx1 -j 128 -N 5 "$temporary/direct.utf8" | tr -d ' \n') = 'e282acc281'
+test $(od -An -v -tx1 -j 209 -N 2 "$temporary/direct.utf8" | tr -d ' \n') = 'c2a0'
+test $(od -An -v -tx1 -j 355 -N 2 "$temporary/direct.utf8" | tr -d ' \n') = 'c3a9'
+write -- 'PASS binary command preserves every indexed scalar including NUL and C1'
+try { $decoder 'ISO-8859-1' "$temporary/all.raw" "$temporary/all.raw" > /dev/null 2> "$temporary/same-path-error" }
+if (not _error.code) { write -- 'FAIL decoder overwrote its input' >&2; exit 1 }
+grep -F 'output-is-input' "$temporary/same-path-error" > /dev/null
+test $(wc -c < "$temporary/all.raw") -eq 256
+
+descriptor "$temporary/all.raw" "$temporary/source.tsv"
+publish $decoder "$temporary/source.tsv" "$temporary/all.raw" "$temporary/derived" > /dev/null
+cmp -- "$temporary/source.tsv" "$temporary/derived/source.tsv"
+cmp -- "$temporary/expected.utf8" "$temporary/derived/decoded.utf8"
+grep -Fx b'reader_admission\tNOT_GRANTED' "$temporary/derived/decode.tsv" > /dev/null
+grep -Fx b'original_navigation_admitted\tNO' "$temporary/derived/decode.tsv" > /dev/null
+grep -Fx b'declared_charset\tISO-8859-1' "$temporary/derived/decode.tsv" > /dev/null
+test ! -e "$temporary/derived/input.raw"
+test ! -e "$temporary/derived/producer.tsv"
+var complete = $(sha256sum "$temporary/derived/decode.tsv" | cut -d ' ' -f 1)
+test $(cat "$temporary/derived/complete") = $complete
+write -- 'PASS disposable derivative preserves original evidence and grants no reader admission'
+
+sed 's/^byte_count\t256$/byte_count\t255/' "$temporary/source.tsv" > "$temporary/bad-count.tsv"
+refuse $decoder "$temporary/bad-count.tsv" "$temporary/all.raw" "$temporary/bad-count" 'source byte count mismatch' "$temporary/error"
+awk -F b'\t' 'BEGIN {OFS="\t"} $1=="sha256" {$2=sprintf("%064d",0)} {print}' "$temporary/source.tsv" > "$temporary/bad-hash.tsv"
+refuse $decoder "$temporary/bad-hash.tsv" "$temporary/all.raw" "$temporary/bad-hash" 'source digest mismatch' "$temporary/error"
+descriptor "$temporary/all.raw" "$temporary/unknown.tsv" 'utf-8'
+refuse $decoder "$temporary/unknown.tsv" "$temporary/all.raw" "$temporary/unknown" 'unsupported-html-encoding-label' "$temporary/error"
+printf '\357\273\277x' > "$temporary/bom.raw"
+descriptor "$temporary/bom.raw" "$temporary/bom.tsv"
+refuse $decoder "$temporary/bom.tsv" "$temporary/bom.raw" "$temporary/bom" 'bom-selects-an-unimplemented-decoder' "$temporary/error"
+write -- 'PASS wrong source claims, unknown labels and BOMs never publish a derivative'
+truncate -s 4194305 "$temporary/too-large.raw"
+descriptor "$temporary/too-large.raw" "$temporary/too-large.tsv"
+refuse $decoder "$temporary/too-large.tsv" "$temporary/too-large.raw" "$temporary/too-large" 'file exceeds decoding bound' "$temporary/error"
+touch "$temporary/empty.raw"
+descriptor "$temporary/empty.raw" "$temporary/empty.tsv"
+publish $decoder "$temporary/empty.tsv" "$temporary/empty.raw" "$temporary/empty" > /dev/null
+test ! -s "$temporary/empty/decoded.utf8"
+grep -Fx b'decoded_codepoint_count\t0' "$temporary/empty/decode.tsv" > /dev/null
+grep -Fx b'reader_admission\tNOT_GRANTED' "$temporary/empty/decode.tsv" > /dev/null
+write -- 'PASS size bound and empty representation preserve decoding/admission separation'
+
+# These fixture producers run under the same verified Grease entrypoint.
+printf '#!%s\n' $runner > "$temporary/nonzero"
+cat >> "$temporary/nonzero" <<'EOF'
+printf 'partial' > $[ARGV[2]]
+exit 19
+EOF
+chmod +x "$temporary/nonzero"
+refuse "$temporary/nonzero" "$temporary/source.tsv" "$temporary/all.raw" "$temporary/nonzero-result" 'Idriç decoding producer refused or failed' "$temporary/error"
+printf '#!%s\n' $runner > "$temporary/change-metadata"
+cat >> "$temporary/change-metadata" <<'EOF'
+var producer = ENV.IB_REAL_SOURCE_DECODER
+$producer @ARGV
+var parent = $(dirname -- $[ARGV[2]])
+printf 'changed\tmetadata\n' >> "$parent/source.tsv"
+EOF
+chmod +x "$temporary/change-metadata"
+try {
+ env IB_REAL_SOURCE_DECODER=$decoder $runner "$root/bin/ib_decode_html_bytes.grease" "$temporary/change-metadata" "$temporary/source.tsv" "$temporary/all.raw" "$temporary/changed-metadata" > /dev/null 2> "$temporary/error"
+}
+if (not _error.code) { write -- 'FAIL changed source descriptor accepted' >&2; exit 1 }
+grep -F 'source descriptor changed during decoding' "$temporary/error" > /dev/null
+test ! -e "$temporary/changed-metadata"
+cmp -- "$temporary/source.tsv" "$temporary/derived/source.tsv"
+write -- 'PASS partial nonzero producer and source-evidence mutation preserve last valid derivative'
+
+# The observation is the exact existing capture, not another canonical source.
+var observed_hash = $(sha256sum -- $google | cut -d ' ' -f 1)
+if (observed_hash !== 'f71e991ab87271e77255fe2d2454cb4cb401fe47cdf953ea550c6e0fcd8afeb4') { exit 1 }
+test $(wc -c < $google) -eq 93166
+grep -Fx b'content_type\ttext/html; charset=ISO-8859-1' $google_metadata > /dev/null
+grep -Fx b'redirect_count\t1' $google_metadata > /dev/null
+cp -- $google_metadata "$temporary/google-before.tsv"
+descriptor $google "$temporary/google-source.tsv"
+publish $decoder "$temporary/google-source.tsv" $google "$temporary/google-derived" > /dev/null
+cmp -- $google "$temporary/google-derived/decoded.utf8"
+cmp -- $google_metadata "$temporary/google-before.tsv"
+cmp -- "$temporary/google-source.tsv" "$temporary/google-derived/source.tsv"
+grep -Fx b'charset\tISO-8859-1' "$temporary/google-derived/source.tsv" > /dev/null
+grep -Fx b'redirect_count\t1' "$temporary/google-derived/source.tsv" > /dev/null
+grep -Fx b'reader_admission\tNOT_GRANTED' "$temporary/google-derived/decode.tsv" > /dev/null
+write -- 'PASS actual retained Google bytes round-trip without relabeling or redirect admission'
+
+write -- 'PASS native Grease source-decoding process controls; Android and Arena admission remain separate'
diff --git a/tests/test_arena_html_refusals.sh b/tests/test_arena_html_refusals.sh
new file mode 100644
index 00000000..fe295d17
--- /dev/null
+++ b/tests/test_arena_html_refusals.sh
@@ -0,0 +1,50 @@
+#!/bin/sh
+# A v1 body-only PR #152 receipt must never become an admitted HTML page.
+set -eu
+root=$(CDPATH='' cd -- "$(dirname -- "$0")/.." && pwd)
+work=$(mktemp -d)
+trap 'rm -rf "$work"' EXIT HUP INT TERM
+mkdir -p "$work/arena/receipts"
+manifest="$work/arena/receipts/request-1.tsv"
+cat > "$manifest" <<'EOF'
+schema ib-icu-arena-v1
+request_id request-1
+requested_url https://example.com/
+resolved_url UNOBSERVED
+http_status UNOBSERVED
+mime_type UNOBSERVED
+transport icu-app-process-via-binder-shizuku
+arena_name responses.arena
+arena_offset 0
+arena_end 2
+byte_count 2
+sha256 aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa
+reopen_check MATCH
+navigation_admitted NO
+EOF
+page="$work/display.prepaint"
+cp "$root/tests/fixtures/ib-html/example.prepaint" "$page"
+cp "$page" "$work/last-valid"
+refuse() {
+ reason=$1
+ if sh "$root/bin/ib_arena_to_html_prepaint.grease" \
+ request-1 "$work/arena" generation-1 "$page" \
+ > "$work/result" 2> "$work/error"; then
+ echo "unexpected admitted source: $reason" >&2
+ exit 1
+ fi
+ grep -F "$reason" "$work/error"
+ cmp -s "$page" "$work/last-valid"
+}
+refuse 'navigation not admitted'
+sed 's/navigation_admitted.*$/navigation_admitted YES/' "$manifest" > "$work/replaced"
+mv "$work/replaced" "$manifest"
+refuse 'out-of-order or missing generation'
+{
+ printf 'source_generation\tgeneration-1\n'
+ printf 'acquisition_complete\tYES\n'
+} >> "$manifest"
+sed 's@^mime_type.*@mime_type\tUNOBSERVED@' "$manifest" > "$work/replaced"
+mv "$work/replaced" "$manifest"
+refuse 'unadmitted content type'
+printf 'arena-v1-unobserved-refused\tPASS\n'
diff --git a/tests/test_arena_v2_to_html_prepaint.sh b/tests/test_arena_v2_to_html_prepaint.sh
new file mode 100644
index 00000000..73cd7fb3
--- /dev/null
+++ b/tests/test_arena_v2_to_html_prepaint.sh
@@ -0,0 +1,141 @@
+#!/bin/sh
+# Host-only integration against the EXACT external PR #152 ICU/Arena producer
+# and reader with a marked MOCK ICU packet. No live network or Android device.
+set -eu
+root=$(CDPATH='' cd -- "$(dirname -- "$0")/.." && pwd)
+test -f "$root/.deps/ib-arena/bin/ib_android_icu_arena.grease" || {
+ echo 'pinned upstream Arena source unavailable' >&2; exit 2;
+}
+arena_tool=${IB_APPEND_ARENA:-}
+slice_tool=${IB_ARENA_SLICE:-}
+converter=${IB_HTML_PREPAINT_EXEC:-}
+oracle=${IB_PREPAINT_ORACLE:-}
+test -x "$arena_tool" && test -x "$slice_tool" &&
+ test -x "$converter" && test -x "$oracle" || {
+ echo 'compiled Arena/Idriç/independent consumer executables required' >&2; exit 2;
+ }
+work=$(mktemp -d)
+trap 'rm -rf "$work"' EXIT HUP INT TERM
+mkdir -p "$work/lib" "$work/bin" "$work/private" "$work/output"
+chmod 700 "$work/private"
+cp "$root/.deps/ib-arena/bin/ib_android_icu_arena.grease" "$work/bin/"
+cp "$root/.deps/ib-arena/bin/ib_android_arena_read.grease" "$work/bin/"
+cp "$root/.deps/ib-arena/lib/android_shizuku_icu_provider.grease" "$work/lib/"
+cp "$root/.deps/ib-arena/lib/android_binder_icu.grease" "$work/lib/"
+
+# This mock replaces *only* the Shizuku command invocation. Production
+# ICU PR #35 capture, framing, validation, canonical Arena and source
+# reopen logic remain unchanged, from exact upstream SHA.
+cat > "$work/lib/android_shizuku_host.grease" <<'MOCK'
+ib_shizuku_authority() { printf 'shell\n'; }
+ib_shizuku_run_bounded() {
+ test "$1" = 30 || return 90
+ case "$2" in *ICU_CAPTURE_BODY_PATH*ICU_CAPTURE_METADATA_PATH*Idric.Generated\ get*) ;; *) return 91 ;; esac
+ body=$IB_MOCK_SOURCE_BODY
+ test -f "$body" || return 92
+ body_bytes=$(wc -c < "$body" | tr -d '[:space:]')
+ {
+ printf 'http_status\t200\n'
+ printf 'content_type\ttext/html; charset=utf-8\n'
+ printf 'content_encoding\tidentity\n'
+ printf 'declared_length\t%s\n' "$body_bytes"
+ printf 'received_length\t%s\n' "$body_bytes"
+ printf 'utf8\tvalid\n'
+ printf 'resolved_url\thttps://example.com/\n'
+ printf 'redirect_count\t0\n'
+ } > "$IB_MOCK_METADATA"
+ metadata_bytes=$(wc -c < "$IB_MOCK_METADATA" | tr -d '[:space:]')
+ printf 'IBICU01 %08d %08d\n' "$metadata_bytes" "$body_bytes"
+ cat "$IB_MOCK_METADATA"
+ cat "$body"
+}
+MOCK
+
+export IB_MOCK_SOURCE_BODY="$root/tests/fixtures/ib-html/example.html"
+export IB_MOCK_METADATA="$work/mock-icu-metadata.tsv"
+export IB_APPEND_ARENA="$arena_tool"
+export IB_ARENA_SLICE="$slice_tool"
+export IB_C67_ICU_DEX=/data/local/tmp/ib-icu/classes.dex
+export IB_C67_ICU_SO=/data/local/tmp/ib-icu/libicu_transport.so
+export IB_C67_ICU_DEX_SHA256=aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa
+export IB_C67_ICU_SO_SHA256=bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb
+export IB_HTML_PREPAINT_EXEC="$converter"
+export IB_PREPAINT_ORACLE="$oracle"
+"$arena_tool" create "$work/private/responses.arena" 16777216 >/dev/null
+sh "$work/bin/ib_android_icu_arena.grease" host-example \
+ https://example.com/ "$work/private" 17 > "$work/producer.tsv"
+grep -Fx "$(printf 'committed\thost-example\t0\t%s\tYES' \
+ "$(wc -c < "$IB_MOCK_SOURCE_BODY" | tr -d '[:space:]')")" "$work/producer.tsv"
+receipt="$work/private/receipts/host-example.tsv"
+test "$(awk -F '\t' '$1=="schema" {print $2}' "$receipt")" = ib-icu-arena-v2
+test "$(awk -F '\t' '$1=="source_generation" {print $2}' "$receipt")" = 17
+test "$(awk -F '\t' '$1=="navigation_admitted" {print $2}' "$receipt")" = YES
+
+# Host sh entrypoint for the unmodified upstream verified Arena reader.
+cat > "$work/ib-arena-reader" <<'WRAPPER'
+#!/bin/sh
+exec sh "$IB_TEST_READER_SCRIPT" "$@"
+WRAPPER
+chmod 700 "$work/ib-arena-reader"
+export IB_TEST_READER_SCRIPT="$work/bin/ib_android_arena_read.grease"
+export IB_ARENA_READ_EXEC="$work/ib-arena-reader"
+source_digest=$(sha256sum "$IB_MOCK_SOURCE_BODY" | cut -d ' ' -f 1)
+source_length=$(wc -c < "$IB_MOCK_SOURCE_BODY" | tr -d '[:space:]')
+sh "$IB_ARENA_READ_EXEC" host-example "$work/private" > "$work/reopened.html"
+cmp "$work/reopened.html" "$IB_MOCK_SOURCE_BODY"
+
+projection="$work/output/host-example.prepaint"
+sh "$root/bin/ib_arena_to_html_prepaint.grease" \
+ host-example "$work/private" 17 "$projection" > "$work/conversion.tsv"
+cmp "$root/tests/fixtures/ib-html/example.prepaint" "$projection"
+"$IB_PREPAINT_ORACLE" "$projection"
+
+if test -n "${IB_AICI_PREPAINT_VERIFIER:-}"; then
+ {
+ printf 'source_key\tarena:host-example\n'
+ printf 'source_generation\t17\n'
+ printf 'source_sha256\t%s\n' "$source_digest"
+ printf 'source_bytes\t%s\n' "$source_length"
+ } > "$work/source-admission.tsv"
+ sh "$IB_AICI_PREPAINT_VERIFIER" "$projection" \
+ "$root/tests/fixtures/ib-html/example.prepaint" \
+ "$work/source-admission.tsv" "$work/reopened.html" arena:host-example 17
+fi
+
+cp "$projection" "$work/last-valid.prepaint"
+cp "$receipt" "$work/valid-receipt.tsv"
+refuse() {
+ case_name=$1
+ if sh "$root/bin/ib_arena_to_html_prepaint.grease" \
+ host-example "$work/private" 17 "$projection" \
+ > "$work/refused.out" 2> "$work/refused.err"; then
+ echo "accepted mutated v2 Arena source: $case_name" >&2
+ exit 1
+ fi
+ cmp "$projection" "$work/last-valid.prepaint"
+ printf 'arena-v2-refusal\t%s\tPASS\n' "$case_name"
+}
+sed 's@^sha256.*@sha256\t0000000000000000000000000000000000000000000000000000000000000000@' \
+ "$work/valid-receipt.tsv" > "$receipt"
+refuse corrupted_arena_digest
+sed 's@^source_generation.*@source_generation\t18@' "$work/valid-receipt.tsv" > "$receipt"
+refuse stale_source_generation
+sed 's@^navigation_admitted.*@navigation_admitted\tNO@' "$work/valid-receipt.tsv" > "$receipt"
+refuse unadmitted_navigation
+cp "$work/valid-receipt.tsv" "$receipt"
+
+if test -n "${IB_HTML_PREPAINT_RECEIPT_ROOT:-}"; then
+ mkdir -p "$IB_HTML_PREPAINT_RECEIPT_ROOT"
+ cp "$projection" "$IB_HTML_PREPAINT_RECEIPT_ROOT/arena-mocked.prepaint"
+ cp "$work/valid-receipt.tsv" "$IB_HTML_PREPAINT_RECEIPT_ROOT/arena-mocked-source.tsv"
+ cp "$work/conversion.tsv" "$IB_HTML_PREPAINT_RECEIPT_ROOT/arena-mocked-conversion.tsv"
+ {
+ printf 'source_kind\tMOCKED_ICU_V2_NOT_LIVE\n'
+ printf 'source_sha256\t%s\n' "$source_digest"
+ printf 'source_bytes\t%s\n' "$source_length"
+ printf 'source_generation\t17\n'
+ printf 'upstream_source_commit\t%s\n' "$(git -C "$root/.deps/ib-arena" rev-parse HEAD)"
+ } > "$IB_HTML_PREPAINT_RECEIPT_ROOT/arena-mocked-provenance.tsv"
+fi
+printf 'arena-v2-mock-through-actual-idric\tPASS\n'
+printf 'real-icu-https\tNOT_RUN\nphysical-c67\tNOT_RUN\n'
diff --git a/tests/test_html_prepaint.sh b/tests/test_html_prepaint.sh
new file mode 100644
index 00000000..6ac62906
--- /dev/null
+++ b/tests/test_html_prepaint.sh
@@ -0,0 +1,147 @@
+#!/bin/sh
+set -eu
+root=$(CDPATH='' cd -- "$(dirname -- "$0")/.." && pwd)
+cd "$root"
+work=$(mktemp -d)
+trap 'rm -rf "$work"' EXIT HUP INT TERM
+cc -std=c11 -O2 -Wall -Wextra -Wpedantic -Werror \
+ tests/prepaint_v1_oracle.c -o "$work/prepaint-v1-oracle"
+export IB_PREPAINT_ORACLE="$work/prepaint-v1-oracle"
+export IB_HTML_PREPAINT_EXEC="${IB_HTML_PREPAINT_EXEC:-$root/src/build/exec/ib-html-prepaint}"
+export IB_ALLOW_FIXTURE=1
+export IB_EXPECTED_SOURCE_GENERATION=generation-1
+test -x "$IB_HTML_PREPAINT_EXEC"
+
+make_manifest() {
+ kind=$1 body=$2 url=$3 manifest=$4
+ sha=$(sha256sum "$body" | cut -d ' ' -f 1)
+ bytes=$(wc -c < "$body" | tr -d '[:space:]')
+ {
+ printf 'schema\tib-html-admission-v1\n'
+ printf 'source_kind\tfixture\n'
+ printf 'source_key\tfixture:%s\n' "$kind"
+ printf 'source_generation\tgeneration-1\n'
+ printf 'requested_url\t%s\n' "$url"
+ printf 'resolved_url\t%s\n' "$url"
+ printf 'http_status\t200\n'
+ printf 'mime_type\ttext/html\n'
+ printf 'charset\tutf-8\n'
+ printf 'sha256\t%s\n' "$sha"
+ printf 'byte_count\t%s\n' "$bytes"
+ printf 'acquisition_complete\tYES\n'
+ printf 'arena_reopen\tNOT_RUN\n'
+ } > "$manifest"
+}
+run_fixture() {
+ kind=$1 url=$2
+ body="tests/fixtures/ib-html/$kind.html"
+ key="fixture:$kind"
+ expected="tests/fixtures/ib-html/$kind.prepaint"
+ manifest="$work/$kind.tsv"
+ output="$work/$kind.prepaint"
+ make_manifest "$kind" "$body" "$url" "$manifest"
+ sh bin/ib_emit_html_prepaint.grease "$manifest" "$body" "$key" "$output" \
+ > "$work/$kind.receipt"
+ "$IB_PREPAINT_ORACLE" "$output"
+ cmp "$expected" "$output"
+ if test -n "${IB_AICI_PREPAINT_VERIFIER:-}"; then
+ test -f "$IB_AICI_PREPAINT_VERIFIER" || exit 1
+ {
+ printf 'source_key\t%s\n' "$key"
+ printf 'source_generation\tgeneration-1\n'
+ printf 'source_sha256\t%s\n' "$(sha256sum "$body" | cut -d ' ' -f 1)"
+ printf 'source_bytes\t%s\n' "$(wc -c < "$body" | tr -d '[:space:]')"
+ } > "$work/$kind.ai-source.tsv"
+ sh "$IB_AICI_PREPAINT_VERIFIER" "$output" "$expected" \
+ "$work/$kind.ai-source.tsv" "$body" "$key" generation-1
+ fi
+ if test -n "${IB_HTML_PREPAINT_RECEIPT_ROOT:-}"; then
+ mkdir -p "$IB_HTML_PREPAINT_RECEIPT_ROOT"
+ cp "$output" "$IB_HTML_PREPAINT_RECEIPT_ROOT/$kind.prepaint"
+ cp "$manifest" "$IB_HTML_PREPAINT_RECEIPT_ROOT/$kind.admission.tsv"
+ cp "$work/$kind.receipt" "$IB_HTML_PREPAINT_RECEIPT_ROOT/$kind.conversion.tsv"
+ fi
+ grep -Fx "$(printf 'conversion\tPASS')" "$work/$kind.receipt"
+ printf 'fixture\t%s\tPASS\n' "$kind"
+}
+run_fixture example https://example.com/
+run_fixture arxiv https://arxiv.org/html/2401.00100
+
+sourcefile="$work/example.prepaint"
+manifest="$work/example.tsv"
+body=tests/fixtures/ib-html/example.html
+key=fixture:example
+cp "$sourcefile" "$work/last_valid"
+test_failure_preserves() {
+ label=$1
+ if sh bin/ib_emit_html_prepaint.grease "$manifest" "$body" "$key" "$sourcefile" \
+ > "$work/mutant.out" 2> "$work/mutant.err"; then
+ echo "failure accepted: $label" >&2
+ exit 1
+ fi
+ cmp "$sourcefile" "$work/last_valid"
+ printf 'refusal\t%s\tPASS\n' "$label"
+}
+cp "$manifest" "$work/good.tsv"
+sed 's@^sha256.*@sha256\t0000000000000000000000000000000000000000000000000000000000000000@' \
+ "$work/good.tsv" > "$manifest"
+test_failure_preserves wrong_digest
+cp "$work/good.tsv" "$manifest"
+sed 's@^source_key.*@source_key\tfixture:wrong@' "$work/good.tsv" > "$manifest"
+test_failure_preserves changed_source_identity
+cp "$work/good.tsv" "$manifest"
+IB_EXPECTED_SOURCE_GENERATION=generation-2
+export IB_EXPECTED_SOURCE_GENERATION
+test_failure_preserves stale_source_generation
+IB_EXPECTED_SOURCE_GENERATION=generation-1
+export IB_EXPECTED_SOURCE_GENERATION
+sed 's@^mime_type.*@mime_type\tapplication/octet-stream@' "$work/good.tsv" > "$manifest"
+test_failure_preserves unsupported_mime
+cp "$work/good.tsv" "$manifest"
+sed 's@^charset.*@charset\tiso-8859-1@' "$work/good.tsv" > "$manifest"
+test_failure_preserves unsupported_charset
+cp "$work/good.tsv" "$manifest"
+sed 's@^byte_count.*@byte_count\t4194305@' "$work/good.tsv" > "$manifest"
+test_failure_preserves oversized_body
+cp "$work/good.tsv" "$manifest"
+sed 's@^resolved_url.*@resolved_url\tUNOBSERVED@' "$work/good.tsv" > "$manifest"
+test_failure_preserves unobserved_final_url
+cp "$work/good.tsv" "$manifest"
+sed 's@^acquisition_complete.*@acquisition_complete\tNO@' "$work/good.tsv" > "$manifest"
+test_failure_preserves incomplete_source
+cp "$work/good.tsv" "$manifest"
+# Same published metadata, mutated body: cannot publish changed bytes.
+printf '\377' > "$work/invalid.html"
+body="$work/invalid.html"
+test_failure_preserves corrupted_source
+make_manifest example "$body" https://example.com/ "$manifest"
+test_failure_preserves invalid_utf8
+body=tests/fixtures/ib-html/example.html
+cp "$work/good.tsv" "$manifest"
+
+# Wrong-output mutants must not pass independent expected-content comparison.
+mutation_refused() {
+ label=$1
+ test ! "$1" = ""
+ if cmp -s "$sourcefile" "$work/$label.prepaint"; then
+ echo "undetected mutation: $label" >&2; exit 1
+ fi
+ printf 'semantic-mutant\t%s\tREFUSED_BY_GOLDEN\n' "$label"
+}
+sed '/^text\tThis domain/d' "$sourcefile" > "$work/dropped_text.prepaint"
+mutation_refused dropped_text
+sed 's@^heading\t1\t@heading\t2\t@' "$sourcefile" > "$work/wrong_heading.prepaint"
+mutation_refused wrong_heading
+sed 's@www.iana.org/domains/example@www.iana.org/domains/wrong@' "$sourcefile" > "$work/wrong_link.prepaint"
+mutation_refused wrong_link
+sed 's@^heading\t1\t@heading\t7\t@' "$sourcefile" > "$work/invalid_heading.prepaint"
+if "$IB_PREPAINT_ORACLE" "$work/invalid_heading.prepaint"; then
+ echo 'independent oracle accepted heading 7' >&2; exit 1
+fi
+printf 'syntax-mutant\tinvalid_heading\tREFUSED\n'
+sed 's@^title\t.*@title\tbad\\q@' "$sourcefile" > "$work/invalid_escaping.prepaint"
+if "$IB_PREPAINT_ORACLE" "$work/invalid_escaping.prepaint"; then
+ echo 'independent oracle accepted invalid escape' >&2; exit 1
+fi
+printf 'syntax-mutant\tinvalid_escaping\tREFUSED\n'
+printf 'semantic\tPASS\n'
diff --git a/tests/test_prepaint_oracle_static.sh b/tests/test_prepaint_oracle_static.sh
new file mode 100644
index 00000000..c11ea2af
--- /dev/null
+++ b/tests/test_prepaint_oracle_static.sh
@@ -0,0 +1,27 @@
+#!/bin/sh
+set -eu
+root=$(CDPATH='' cd -- "$(dirname -- "$0")/.." && pwd)
+cd "$root"
+work=$(mktemp -d)
+trap 'rm -rf "$work"' EXIT HUP INT TERM
+cc -std=c11 -O2 -Wall -Wextra -Wpedantic -Werror \
+ tests/prepaint_v1_oracle.c -o "$work/oracle"
+for case_name in example arxiv; do
+ "$work/oracle" "tests/fixtures/ib-html/$case_name.prepaint"
+ printf 'independent-golden\t%s\tPASS\n' "$case_name"
+done
+cp tests/fixtures/ib-html/example.prepaint "$work/sample"
+sed 's@^heading\t1\t@heading\t7\t@' "$work/sample" > "$work/level"
+if "$work/oracle" "$work/level"; then exit 1; fi
+sed 's@^title\t.*@title\tbad\\q@' "$work/sample" > "$work/escape"
+if "$work/oracle" "$work/escape"; then exit 1; fi
+sed 's@^link\tLearn more\t.*@link\tLearn more\tjavascript:alert(1)@' "$work/sample" > "$work/link"
+if "$work/oracle" "$work/link"; then exit 1; fi
+# Valid but semantically wrong content MUST fail the independent frozen golden.
+sed '/^text\tThis domain/d' "$work/sample" > "$work/drop"
+if cmp -s "$work/drop" tests/fixtures/ib-html/example.prepaint; then exit 1; fi
+sed 's@^heading\t1\t@heading\t2\t@' "$work/sample" > "$work/wrong-level"
+if cmp -s "$work/wrong-level" tests/fixtures/ib-html/example.prepaint; then exit 1; fi
+sed 's@www.iana.org/domains/example@www.iana.org/domains/wrong@' "$work/sample" > "$work/wrong-target"
+if cmp -s "$work/wrong-target" tests/fixtures/ib-html/example.prepaint; then exit 1; fi
+printf 'prepaint-oracle-static\tPASS\n'