perf(lean): lower byte literals through explicit typed octets

.github/workflows/ci.yml

@@ -15,11 +15,17 @@
 # whose contents may change after review, which R6 does not allow for the
 # code in the crate and should not allow for the code that gates it.
 name: ci
+run-name: ${{ inputs.write_example_evidence && 'Review-only example writer' || 'LexLean CI' }} · ${{ github.sha }}
 
 on:
   push: { branches: [main] }
   pull_request:
   workflow_dispatch:
+    inputs:
+      write_example_evidence:
+        description: Generate review-only example verification records, not acceptance
+        type: boolean
+        default: false
 
 # Read-only: nothing in this workflow writes to the repository or publishes a
 # package. The acceptance log is retained as CI evidence; `release.yml` asks
@@ -28,7 +34,7 @@ permissions:
   contents: read
 
 concurrency:
-  group: ci-${{ github.ref }}
+  group: ${{ inputs.write_example_evidence && 'example-writer' || 'ci' }}-${{ github.ref }}
   cancel-in-progress: ${{ github.event_name == 'pull_request' }}
 
 env:
@@ -39,8 +45,51 @@ env:
   CARGO_INCREMENTAL: "0"
 
 jobs:
+  write-example-evidence:
+    name: Generate review-only example verification records
+    if: github.event_name == 'workflow_dispatch' && inputs.write_example_evidence
+    runs-on: ubuntu-24.04
+    timeout-minutes: 360
+    steps:
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1
+        with:
+          persist-credentials: false
+      - name: Install the pinned Rust toolchain
+        run: rustup toolchain install
+      - name: Install elan and the pinned Lean toolchain
+        run: |
+          set -euo pipefail
+          curl https://elan.lean-lang.org/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+          "$HOME/.elan/bin/elan" toolchain install "$(cat lean-toolchain)"
+      - name: Reserve bounded overflow memory for native Atlas
+        run: |
+          set -euo pipefail
+          sudo fallocate -l 4G "$RUNNER_TEMP/lexlean-atlas.swap"
+          sudo chmod 600 "$RUNNER_TEMP/lexlean-atlas.swap"
+          sudo mkswap "$RUNNER_TEMP/lexlean-atlas.swap"
+          sudo swapon "$RUNNER_TEMP/lexlean-atlas.swap"
+          sudo sysctl vm.swappiness=10
+      - name: Execute the unchanged complete verification writer
+        shell: bash
+        run: |
+          set -euo pipefail
+          mkdir -p ci-evidence
+          cargo xtask verify-examples --write 2>&1 | tee ci-evidence/example-writer.txt
+      - uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a
+        if: always()
+        with:
+          name: review-only-example-verification
+          path: |
+            examples/*/expected/verify/
+            compiler/expected/verify/
+            ci-evidence/
+          if-no-files-found: error
+          retention-days: 14
+
   vv:
-    name: just vv
+    name: ${{ inputs.write_example_evidence && 'Maintenance does not run acceptance' || 'just vv' }}
+    if: github.event_name != 'workflow_dispatch' || !inputs.write_example_evidence
     runs-on: ubuntu-24.04
     # Native Atlas elaboration, per-module kernel replay, and per-module axiom
     # audit are intentionally the long pole. GitHub-hosted jobs permit six
@@ -111,7 +160,8 @@ jobs:
   # reports which ones it skipped; on Linux x86-64 the same gate makes the
   # toolchain mandatory, so nothing passes vacuously where it matters.
   host-matrix:
-    name: build and non-Lean tests (${{ matrix.target }})
+    name: ${{ inputs.write_example_evidence && 'Maintenance does not qualify host' || 'build and non-Lean tests' }} (${{ matrix.target }})
+    if: github.event_name != 'workflow_dispatch' || !inputs.write_example_evidence
     strategy:
       fail-fast: false
       matrix:

SPEC.md

@@ -2462,6 +2462,14 @@ source/IR limits, kernel replay, and exact axiom policies remain unchanged.
 Exhausting a finite Lean budget still fails verification; the budgets do not
 assert that every resource-bounded source can be verified on every host.
 
+Semantic Lean backend revisions 10 (language 1.1) and 17 (language 1.2)
+emit byte-array elements as explicit `UInt8.ofNat (nat_lit n)` applications,
+where `n` is the decoded byte in 0..255. This avoids overloaded numeral
+elaboration without changing byte values, order, or empty arrays. Canonical
+LaTeX retains its decimal rendering. These revisions change the 1.1 and 1.2
+compiler-semantics identities; existing locks require explicit regeneration.
+Language 1.0 artifacts remain unchanged.
+
 ### 17.12 Language 1.2 and the compatibility/migration contract
 
 Language 1.2 is selected by `language = "1.2"` in `lexlean.toml`. It is a

VERIFICATION.md

@@ -38,6 +38,37 @@ Outside `vv`:
 
 ## Falsifiability records
 
+### explicit byte lowering can fail
+
+SM-19 verifies and independently observes all 256 byte values, empty arrays,
+and mixed non-UTF-8 arrays under languages 1.1 and 1.2. Its existing large
+repeated/varied nested-byte cases remain mandatory. Changing the actual Lean
+lowerer to increment each byte modulo 256 failed the observed-value assertion
+after successful kernel verification (4.08 seconds). Restoring exact byte
+construction retains the complete acceptance inventory. The spelling unit
+test first failed against overloaded decimal emission and passes with explicit
+`UInt8.ofNat (nat_lit n)` construction; LaTeX remains unchanged.
+
+On the integration backport based on `1a96a19c`, the non-root pinned
+container passed complete SM-19 in 69.35 seconds and
+workspace all-target Clippy. A separately generated 53-module PrismPM corpus
+compiled in 273.289 seconds within its unchanged 300-second deadline. This
+is a component diagnostic, not full LexLean or downstream release acceptance.
+Raw logs are retained in the integration workspace as
+`typed-byte-value-mutant.log`, `typed-byte-verified-gates.log`, and
+`typed-byte-full-corpus-diagnostic-retry.log`.
+
+The port onto `6b198ee6` retains its complete language-1.2 implementation and
+uses semantic-module/2 for the 1.2 byte observer. Complete SM-19 passes in
+103.33 seconds; all 290 model/specification rows, source golden generation
+(including the compiler project), and all-target Clippy pass. Verification
+records for twelve examples were regenerated by actual verification; independent
+review of all 469 expected records found only generated namespace identity
+changes. The complete local writer failed at Atlas `CensusCert10` with LLV7002
+under a 12 GiB container limit. This partial result does not qualify Atlas, the
+compiler project's later verification, or the complete acceptance gate. The
+unchanged full writer must succeed before those records are accepted.
+
 Each gate below was made to fail by planting a defect, running the gate's command, recording the failure, and removing the defect. The observed lines are verbatim gate output (paths abbreviated to the repository root). `cargo xtask release-check` requires a `### <gate> can fail` record for every gate and audit named in `repo_model::release::GATES`.
 
 ### release inventory can fail

compiler/expected/build/maps/Compiler/Main.map.json

@@ -1 +1 @@
-{"artifacts":[{"id":0,"kind":"lean","path":"modules/Compiler/Main.lean"},{"id":1,"kind":"tex","path":"modules/Compiler/Main.tex"}],"mappings":[{"artifact":0,"gen_end":359,"gen_start":0,"node":0,"role":"declaration","source":0,"src_end":891,"src_start":0},{"artifact":0,"gen_end":574,"gen_start":359,"node":1,"role":"declaration","source":0,"src_end":817,"src_start":309},{"artifact":0,"gen_end":593,"gen_start":574,"node":0,"role":"declaration","source":0,"src_end":891,"src_start":0},{"artifact":1,"gen_end":134,"gen_start":0,"node":2,"role":"declaration","source":0,"src_end":891,"src_start":0},{"artifact":1,"gen_end":497,"gen_start":134,"node":3,"role":"declaration","source":0,"src_end":817,"src_start":309},{"artifact":1,"gen_end":512,"gen_start":497,"node":2,"role":"declaration","source":0,"src_end":891,"src_start":0}],"module":"Main","nodes":[{"id":0,"kind":"semantic-lean-module"},{"id":1,"kind":"semantic-declaration"},{"id":2,"kind":"semantic-latex-module"},{"id":3,"kind":"semantic-declaration"}],"semantic_id":"1377796023a32d16f638e997e89f5162ae0731039b574111c9eefe0cf26d0eb7","source_id":"d20b90154e589426e4541232a435199f84dd51144b7952ed09a148f87e1b3228","sources":[{"id":0,"kind":"file","path":"src/Main.lex.tex","sha256":"e77d5068d66d7c463f830c9ddf1689bfe095de52a9fc0e99bcfbc59907620f61"}],"spec":"lexlean/source-map/1"}
+{"artifacts":[{"id":0,"kind":"lean","path":"modules/Compiler/Main.lean"},{"id":1,"kind":"tex","path":"modules/Compiler/Main.tex"}],"mappings":[{"artifact":0,"gen_end":359,"gen_start":0,"node":0,"role":"declaration","source":0,"src_end":891,"src_start":0},{"artifact":0,"gen_end":574,"gen_start":359,"node":1,"role":"declaration","source":0,"src_end":817,"src_start":309},{"artifact":0,"gen_end":593,"gen_start":574,"node":0,"role":"declaration","source":0,"src_end":891,"src_start":0},{"artifact":1,"gen_end":134,"gen_start":0,"node":2,"role":"declaration","source":0,"src_end":891,"src_start":0},{"artifact":1,"gen_end":497,"gen_start":134,"node":3,"role":"declaration","source":0,"src_end":817,"src_start":309},{"artifact":1,"gen_end":512,"gen_start":497,"node":2,"role":"declaration","source":0,"src_end":891,"src_start":0}],"module":"Main","nodes":[{"id":0,"kind":"semantic-lean-module"},{"id":1,"kind":"semantic-declaration"},{"id":2,"kind":"semantic-latex-module"},{"id":3,"kind":"semantic-declaration"}],"semantic_id":"c7501f2257bae65e4205ba4ea24beee6556dd219e0d6cc623525e568232ce757","source_id":"a30f78eb9c0d6981f49899843cc96c668ae5ed9351236b8af4d01af64725c260","sources":[{"id":0,"kind":"file","path":"src/Main.lex.tex","sha256":"e77d5068d66d7c463f830c9ddf1689bfe095de52a9fc0e99bcfbc59907620f61"}],"spec":"lexlean/source-map/1"}

compiler/expected/build/maps/Compiler/TargetOracle.map.json

@@ -1 +1 @@
-{"artifacts":[{"id":0,"kind":"lean","path":"modules/Compiler/TargetOracle.lean"},{"id":1,"kind":"tex","path":"modules/Compiler/TargetOracle.tex"}],"mappings":[{"artifact":0,"gen_end":190,"gen_start":0,"node":0,"role":"declaration","source":0,"src_end":6818,"src_start":0},{"artifact":0,"gen_end":431,"gen_start":190,"node":1,"role":"declaration","source":0,"src_end":1006,"src_start":180},{"artifact":0,"gen_end":672,"gen_start":431,"node":2,"role":"declaration","source":0,"src_end":1833,"src_start":1007},{"artifact":0,"gen_end":911,"gen_start":672,"node":3,"role":"declaration","source":0,"src_end":2658,"src_start":1834},{"artifact":0,"gen_end":1156,"gen_start":911,"node":4,"role":"declaration","source":0,"src_end":3489,"src_start":2659},{"artifact":0,"gen_end":1409,"gen_start":1156,"node":5,"role":"declaration","source":0,"src_end":4328,"src_start":3490},{"artifact":0,"gen_end":1767,"gen_start":1409,"node":6,"role":"declaration","source":0,"src_end":5495,"src_start":4329},{"artifact":0,"gen_end":2138,"gen_start":1767,"node":7,"role":"declaration","source":0,"src_end":6744,"src_start":5496},{"artifact":0,"gen_end":2165,"gen_start":2138,"node":0,"role":"declaration","source":0,"src_end":6818,"src_start":0},{"artifact":1,"gen_end":134,"gen_start":0,"node":8,"role":"declaration","source":0,"src_end":6818,"src_start":0},{"artifact":1,"gen_end":572,"gen_start":134,"node":9,"role":"declaration","source":0,"src_end":1006,"src_start":180},{"artifact":1,"gen_end":1010,"gen_start":572,"node":10,"role":"declaration","source":0,"src_end":1833,"src_start":1007},{"artifact":1,"gen_end":1446,"gen_start":1010,"node":11,"role":"declaration","source":0,"src_end":2658,"src_start":1834},{"artifact":1,"gen_end":1888,"gen_start":1446,"node":12,"role":"declaration","source":0,"src_end":3489,"src_start":2659},{"artifact":1,"gen_end":2338,"gen_start":1888,"node":13,"role":"declaration","source":0,"src_end":4328,"src_start":3490},{"artifact":1,"gen_end":2893,"gen_start":2338,"node":14,"role":"declaration","source":0,"src_end":5495,"src_start":4329},{"artifact":1,"gen_end":3461,"gen_start":2893,"node":15,"role":"declaration","source":0,"src_end":6744,"src_start":5496},{"artifact":1,"gen_end":3476,"gen_start":3461,"node":8,"role":"declaration","source":0,"src_end":6818,"src_start":0}],"module":"TargetOracle","nodes":[{"id":0,"kind":"semantic-lean-module"},{"id":1,"kind":"semantic-declaration"},{"id":2,"kind":"semantic-declaration"},{"id":3,"kind":"semantic-declaration"},{"id":4,"kind":"semantic-declaration"},{"id":5,"kind":"semantic-declaration"},{"id":6,"kind":"semantic-declaration"},{"id":7,"kind":"semantic-declaration"},{"id":8,"kind":"semantic-latex-module"},{"id":9,"kind":"semantic-declaration"},{"id":10,"kind":"semantic-declaration"},{"id":11,"kind":"semantic-declaration"},{"id":12,"kind":"semantic-declaration"},{"id":13,"kind":"semantic-declaration"},{"id":14,"kind":"semantic-declaration"},{"id":15,"kind":"semantic-declaration"}],"semantic_id":"1377796023a32d16f638e997e89f5162ae0731039b574111c9eefe0cf26d0eb7","source_id":"d20b90154e589426e4541232a435199f84dd51144b7952ed09a148f87e1b3228","sources":[{"id":0,"kind":"file","path":"src/TargetOracle.lex.tex","sha256":"08d589074d04c4ab13c161cc1245cc3475e8723d233ce2dab2cdda15bf56d9cf"}],"spec":"lexlean/source-map/1"}
+{"artifacts":[{"id":0,"kind":"lean","path":"modules/Compiler/TargetOracle.lean"},{"id":1,"kind":"tex","path":"modules/Compiler/TargetOracle.tex"}],"mappings":[{"artifact":0,"gen_end":190,"gen_start":0,"node":0,"role":"declaration","source":0,"src_end":6818,"src_start":0},{"artifact":0,"gen_end":431,"gen_start":190,"node":1,"role":"declaration","source":0,"src_end":1006,"src_start":180},{"artifact":0,"gen_end":672,"gen_start":431,"node":2,"role":"declaration","source":0,"src_end":1833,"src_start":1007},{"artifact":0,"gen_end":911,"gen_start":672,"node":3,"role":"declaration","source":0,"src_end":2658,"src_start":1834},{"artifact":0,"gen_end":1156,"gen_start":911,"node":4,"role":"declaration","source":0,"src_end":3489,"src_start":2659},{"artifact":0,"gen_end":1409,"gen_start":1156,"node":5,"role":"declaration","source":0,"src_end":4328,"src_start":3490},{"artifact":0,"gen_end":1767,"gen_start":1409,"node":6,"role":"declaration","source":0,"src_end":5495,"src_start":4329},{"artifact":0,"gen_end":2138,"gen_start":1767,"node":7,"role":"declaration","source":0,"src_end":6744,"src_start":5496},{"artifact":0,"gen_end":2165,"gen_start":2138,"node":0,"role":"declaration","source":0,"src_end":6818,"src_start":0},{"artifact":1,"gen_end":134,"gen_start":0,"node":8,"role":"declaration","source":0,"src_end":6818,"src_start":0},{"artifact":1,"gen_end":572,"gen_start":134,"node":9,"role":"declaration","source":0,"src_end":1006,"src_start":180},{"artifact":1,"gen_end":1010,"gen_start":572,"node":10,"role":"declaration","source":0,"src_end":1833,"src_start":1007},{"artifact":1,"gen_end":1446,"gen_start":1010,"node":11,"role":"declaration","source":0,"src_end":2658,"src_start":1834},{"artifact":1,"gen_end":1888,"gen_start":1446,"node":12,"role":"declaration","source":0,"src_end":3489,"src_start":2659},{"artifact":1,"gen_end":2338,"gen_start":1888,"node":13,"role":"declaration","source":0,"src_end":4328,"src_start":3490},{"artifact":1,"gen_end":2893,"gen_start":2338,"node":14,"role":"declaration","source":0,"src_end":5495,"src_start":4329},{"artifact":1,"gen_end":3461,"gen_start":2893,"node":15,"role":"declaration","source":0,"src_end":6744,"src_start":5496},{"artifact":1,"gen_end":3476,"gen_start":3461,"node":8,"role":"declaration","source":0,"src_end":6818,"src_start":0}],"module":"TargetOracle","nodes":[{"id":0,"kind":"semantic-lean-module"},{"id":1,"kind":"semantic-declaration"},{"id":2,"kind":"semantic-declaration"},{"id":3,"kind":"semantic-declaration"},{"id":4,"kind":"semantic-declaration"},{"id":5,"kind":"semantic-declaration"},{"id":6,"kind":"semantic-declaration"},{"id":7,"kind":"semantic-declaration"},{"id":8,"kind":"semantic-latex-module"},{"id":9,"kind":"semantic-declaration"},{"id":10,"kind":"semantic-declaration"},{"id":11,"kind":"semantic-declaration"},{"id":12,"kind":"semantic-declaration"},{"id":13,"kind":"semantic-declaration"},{"id":14,"kind":"semantic-declaration"},{"id":15,"kind":"semantic-declaration"}],"semantic_id":"c7501f2257bae65e4205ba4ea24beee6556dd219e0d6cc623525e568232ce757","source_id":"a30f78eb9c0d6981f49899843cc96c668ae5ed9351236b8af4d01af64725c260","sources":[{"id":0,"kind":"file","path":"src/TargetOracle.lex.tex","sha256":"08d589074d04c4ab13c161cc1245cc3475e8723d233ce2dab2cdda15bf56d9cf"}],"spec":"lexlean/source-map/1"}