diff --git a/.github/workflows/bone-sea-s13-local-offset-image.yml b/.github/workflows/bone-sea-s13-local-offset-image.yml new file mode 100644 index 0000000..10f5892 --- /dev/null +++ b/.github/workflows/bone-sea-s13-local-offset-image.yml @@ -0,0 +1,71 @@ +name: BONE SEA S13 Segment Local Image + +on: + workflow_dispatch: + push: + branches: + - ecosystem/shinesea-s13-local-offset-image + paths: + - .github/workflows/bone-sea-s13-local-offset-image.yml + - config/bone_sea_s13.json + - docs/BONE_SEA_S13.md + - tools/bone-sea/Cargo.lock + - tools/bone-sea/Cargo.toml + - tools/bone-sea/s10/image.rs + - tools/bone-sea/s13/** + - tools/bone-sea/src/lib.rs + - tools/bone-sea/src/s3_adapter.rs + - tools/bone-sea/src/bin/bone-sea-s13.rs + pull_request: + paths: + - .github/workflows/bone-sea-s13-local-offset-image.yml + - config/bone_sea_s13.json + - docs/BONE_SEA_S13.md + - tools/bone-sea/Cargo.lock + - tools/bone-sea/Cargo.toml + - tools/bone-sea/s10/image.rs + - tools/bone-sea/s13/** + - tools/bone-sea/src/lib.rs + - tools/bone-sea/src/s3_adapter.rs + - tools/bone-sea/src/bin/bone-sea-s13.rs + +permissions: + contents: read + +jobs: + verify-s13: + runs-on: ubuntu-latest + timeout-minutes: 20 + + steps: + - name: Checkout exact BONEBOX history + uses: actions/checkout@v4 + with: + fetch-depth: 0 + + - name: Checkout exact SHINESEA authority + uses: actions/checkout@v4 + with: + repository: Deadbytes101/SHINESEA + ref: 3bc6343ecaeae27f0d01c6301cab01a0e77bfb96 + path: SHINESEA + fetch-depth: 0 + + - name: Install Rust target + run: rustup target add i686-unknown-linux-gnu + + - name: Python syntax gate + run: python3 -m py_compile tools/bone-sea/s13/prove.py + + - name: Native exact-head tests + env: + RUSTFLAGS: -Dwarnings + run: cargo test --locked --all-targets --manifest-path tools/bone-sea/Cargo.toml + + - name: S13 segment-local image proof + run: >- + cargo run --locked --release + --manifest-path tools/bone-sea/Cargo.toml + --bin bone-sea-s13 -- + verify + --shinesea "$GITHUB_WORKSPACE/SHINESEA" diff --git a/config/bone_sea_s13.json b/config/bone_sea_s13.json new file mode 100644 index 0000000..1a3313c --- /dev/null +++ b/config/bone_sea_s13.json @@ -0,0 +1,115 @@ +{ + "schema": 1, + "architecture": "BONE/SEA", + "phase": "S13-SEGMENT-LOCAL-IMAGE", + "status": "IMPLEMENTATION-CANDIDATE", + "claim_allowed": false, + "runtime_claim_allowed": false, + "write_authority": false, + "parent_head": "56f9697f094fd848b0cf659861f21407b3a9ea75", + "n6_base": "93ea5ffb59ff31e87ab7fd5ecb5570c89b29ffee", + "n6_nano_sha256": "581d1a6c59580fedca7fca97035449521231f9450ca4a3c2cf35d6ed07640855", + "shinesea_head": "3bc6343ecaeae27f0d01c6301cab01a0e77bfb96", + "source_image": "tools/bone-sea/s10/image.rs", + "linker_script": "tools/bone-sea/s13/link.ld", + "target": "i686-unknown-linux-gnu", + "crate_name": "bone_sea_s13_local_image", + "segment": { + "base": 131072, + "limit": 458751, + "bytes": 458752, + "entry_offset": 0, + "code_selector": 15, + "data_selector": 23, + "ldt_selector": 56, + "byte_granularity": true, + "default_operand_bits": 32, + "dpl": 3 + }, + "translation_law": { + "local_start": 0, + "local_end_exclusive": 458752, + "physical_start": 131072, + "physical_end_exclusive": 589824, + "formula": "physical = segment_base + local", + "elf_vma_is_local": true, + "elf_lma_is_physical": true, + "absolute_physical_vma_forbidden": true + }, + "regions": [ + { + "name": "code_rodata_static", + "local": 0, + "physical": 131072, + "bytes_max": 65536 + }, + { + "name": "stack", + "local": 65536, + "physical": 196608, + "bytes": 16384 + }, + { + "name": "ata_block_bounce", + "local": 81920, + "physical": 212992, + "bytes": 4096 + }, + { + "name": "protocol_scratch", + "local": 86016, + "physical": 217088, + "bytes": 12288 + }, + { + "name": "linker_growth_reserve", + "local": 98304, + "physical": 229376, + "bytes": 32768 + }, + { + "name": "allocator_arena", + "local": 131072, + "physical": 262144, + "bytes": 262144 + }, + { + "name": "zero_padding_reserve", + "local": 393216, + "physical": 524288, + "bytes": 65536 + } + ], + "proof": { + "builds": 2, + "exact_elf_repeatability": true, + "exact_flat_repeatability": true, + "load_segments": 7, + "undefined_symbols": 0, + "dynamic_segments": 0, + "entry_is_local_zero": true, + "all_loads_obey_translation": true, + "reserved_physical_bytes_zero": true, + "vma_adversary_required": true, + "lma_adversary_required": true, + "temporary_outputs_retained": false + }, + "ecosystem": { + "cinder16_head": "9eadc22d03b0782373d5ca23290bb76768df5e4f", + "loom_head": "444937bd0aef2e5b17ed253deb7677a778225d7e", + "cinder16_reuse": "exact identity and validation before publication", + "loom_reuse": "freestanding binary geometry and adversarial judging", + "cinder16_vm_code_copied": false, + "loom_runtime_code_copied": false + }, + "claims": { + "segment_local_elf": true, + "physical_flat_image": true, + "ring3_transfer": false, + "sea_entry_executed": false, + "n6_io_gate_execution": false, + "shinesea_runtime_mount": false, + "runtime_allocator_pass": false, + "write_authority": false + } +} diff --git a/docs/BONE_SEA_S13.md b/docs/BONE_SEA_S13.md new file mode 100644 index 0000000..311d13a --- /dev/null +++ b/docs/BONE_SEA_S13.md @@ -0,0 +1,274 @@ +BONE/SEA S13 SEGMENT-LOCAL IMAGE CONTRACT +========================================= + +ARCHITECTURE BONE/SEA +PHASE S13 +STATUS IMPLEMENTATION CANDIDATE +PARENT HEAD 56f9697f094fd848b0cf659861f21407b3a9ea75 +SHINESEA HEAD 3bc6343ecaeae27f0d01c6301cab01a0e77bfb96 +RUNTIME CLAIM DISALLOWED +WRITE AUTHORITY DISALLOWED + + +CLASSIFY +-------- + +S12 proved that the exact S10 physical flat image can be read by the actual N6 +root, checked by full-byte CRC32, and published under the S2 SEA LDT. + +S12 intentionally did not transfer to `_start`. + +Before that transfer can be authorized, the executable address model must agree +with the descriptor model. The S2/S12 SEA descriptor has: + + BASE 00020000 + LIMIT 0006FFFF + SIZE 00070000 + +A ring3 instruction therefore sees addresses as local offsets and the processor +forms physical addresses with: + + PHYSICAL = 00020000 + LOCAL + +The S10 linker instead assigned physical addresses as ELF virtual addresses: + + CODE VMA 00020000 + SCRATCH VMA 00035000 + ARENA VMA 00040000 + +Executing those addresses through a segment whose base is already 00020000 +would add the base twice. For example: + + S10 SCRATCH VMA 00035000 + PLUS SEGMENT BASE 00020000 + OBSERVED PHYSICAL 00055000 + REQUIRED PHYSICAL 00035000 + +S13 classifies this as an address-model mismatch, not as a runtime failure and +not as permission to weaken the descriptor base to zero. + + +ONE DECISION +------------ + +Keep the bounded S2 segment exactly as designed. + +Relink the unchanged S10 source graph with segment-local VMAs and the original +physical LMAs. + +Do not transfer to ring3 in S13. + + +SEGMENT-LOCAL LEDGER +-------------------- + + OWNER LOCAL VMA PHYSICAL LMA BYTES + ------------------------ ----------------- ----------------- -------- + CODE / RODATA / STATIC 00000000-0000FFFF 00020000-0002FFFF <=65536 + RING3 STACK 00010000-00013FFF 00030000-00033FFF 16384 + ATA BLOCK BOUNCE 00014000-00014FFF 00034000-00034FFF 4096 + PROTOCOL SCRATCH 00015000-00017FFF 00035000-00037FFF 12288 + LINKER GROWTH RESERVE 00018000-0001FFFF 00038000-0003FFFF 32768 + ALLOCATOR ARENA 00020000-0005FFFF 00040000-0007FFFF 262144 + ZERO PADDING RESERVE 00060000-0006FFFF 00080000-0008FFFF 65536 + +The local ledger is contiguous from 00000000 through 0006FFFF. + +The physical ledger remains contiguous from 00020000 through 0008FFFF. + +Every region obeys: + + PHYSICAL LMA = 00020000 + LOCAL VMA + +The ELF entry is local offset zero. A later root can enter it with SEA code +selector 000Fh and EIP 00000000h. + + +SOURCE LAW +---------- + +S13 does not rewrite the SHINESEA core or the S10 no_std image source. + +Frozen source paths relative to exact parent S12: + + tools/bone-sea/src/lib.rs + tools/bone-sea/src/s3_adapter.rs + tools/bone-sea/s10/image.rs + +The only new executable-layout authority is: + + tools/bone-sea/s13/link.ld + +Its VMA/LMA split is explicit through linker `AT(...)` expressions. + + +JUDGE +----- + +The S13 proof builds the same ELF twice with: + + TARGET i686-unknown-linux-gnu + CRATE NAME bone_sea_s13_local_image + PANIC abort + LTO fat + RELOCATION MODEL static + DEFAULT LIBRARIES disabled + PIE disabled + +Both complete ELF files must be byte-identical. + +Both reconstructed 458752-byte physical images must be byte-identical. + +The ELF judge requires: + + ELF32 little-endian ET_EXEC / EM_386 + entry offset 00000000 + exactly seven PT_LOAD segments + no PT_DYNAMIC + no PT_INTERP + no undefined symbols + `_start` at local offset zero + all alloc sections owned by the SEA ledger + all NOLOAD segments with zero file bytes + all reserved physical bytes zero + p_paddr = 00020000 + p_vaddr for every PT_LOAD + +The observed ELF SHA256 and physical-flat SHA256 are evidence values. They are +not guessed or frozen before the exact-head build runs. + + +ADVERSARIAL JUDGE +----------------- + +ABSOLUTE VMA ADVERSARY + +The judge changes the first load segment VMA from local zero to physical +00020000. It must reject the image because an absolute physical VMA survived. + +LMA OFFSET ADVERSARY + +The judge moves the first physical LMA by one sector while leaving the VMA +unchanged. It must reject the image because the base translation law no longer +holds. + +Neither adversary executes code. + + +DEADBYTE ECOSYSTEM REUSE +------------------------ + +CINDER-16 authority: + + 9eadc22d03b0782373d5ca23290bb76768df5e4f + +Reused discipline: + + exact identity + validation before publication + no global host mutation + +LOOM authority: + + 444937bd0aef2e5b17ed253deb7677a778225d7e + +Reused discipline: + + freestanding linker boundary + binary geometry judge + adversarial rejection before runtime claims + +No CINDER-16 VM code and no LOOM runtime code is copied into S13. + + +RUN +--- + + cd D:\TECHNICAL\BONEBOX-01 + + git fetch origin --prune + git switch ecosystem/shinesea-s13-local-offset-image + git reset --hard origin/ecosystem/shinesea-s13-local-offset-image + + rustup target add i686-unknown-linux-gnu + + $env:RUSTFLAGS = '-Dwarnings' + + cargo test ` + --locked ` + --all-targets ` + --manifest-path .\tools\bone-sea\Cargo.toml + + cargo run ` + --locked ` + --release ` + --manifest-path .\tools\bone-sea\Cargo.toml ` + --bin bone-sea-s13 ` + -- ` + verify ` + --shinesea D:\TECHNICAL\SHINESEA + +Expected native total after adding S13: + + 126 / 126 PASS + WARNINGS 0 + +Required S13 terminal: + + BONE/SEA S13 SEGMENT-LOCAL IMAGE VERIFY PASS + + +OBSERVED VALUES REQUIRED +------------------------ + + exact BONEBOX head + exact SHINESEA head + ELF byte count + ELF SHA256 + code byte count + code headroom + physical flat byte count + physical flat SHA256 + seven PT_LOAD segments + zero undefined symbols + repeated ELF identity PASS + repeated flat identity PASS + absolute VMA adversary REJECTED + LMA offset adversary REJECTED + temporary output cleanup PASS + + +NON-CLAIMS +---------- + +S13 does not claim: + + N6 transfers to SEA ring3 + S13 `_start` executes + N6 I/O gates service SEA reads + SHINESEA mounts the S1 image + allocator runtime behavior passes + write authority exists + + +DEFINE DONE +----------- + +S13 is complete only when the exact branch observes: + + tracked tree clean + native tests PASS with zero warnings + exact SHINESEA authority PASS + frozen S10 source paths PASS + segment-local section ledger PASS + physical LMA ledger PASS + seven PT_LOAD segments PASS + VMA/LMA translation PASS + repeat ELF identity PASS + repeat physical image identity PASS + both address adversaries REJECTED + temporary output cleanup PASS + +Only then may S14 attempt a bounded ring3 entry transfer using local EIP zero. + +REPORTS ARE CLAIMS, NOT EVIDENCE. +NO COSTUME RIGOR. diff --git a/tools/bone-sea/s13/LICENSE-NOTICE.txt b/tools/bone-sea/s13/LICENSE-NOTICE.txt new file mode 100644 index 0000000..d2ebb61 --- /dev/null +++ b/tools/bone-sea/s13/LICENSE-NOTICE.txt @@ -0,0 +1,15 @@ +BONE/SEA S13 LICENSE NOTICE +=========================== + +The S13 proof compiles the existing BONE/SEA and SHINESEA GPL-2.0-or-later +source graph into temporary ELF and flat-image artifacts for deterministic +address-model verification. + +The proof does not publish or retain those generated artifacts. Temporary +files are removed before a successful terminal verdict is emitted. + +S13 adds no CINDER-16 VM code and no LOOM runtime code. Their pinned commits +are cited only as engineering-contract authorities for exact identity, +freestanding layout judging, and adversarial rejection. + +No warranty is provided. diff --git a/tools/bone-sea/s13/link.ld b/tools/bone-sea/s13/link.ld new file mode 100644 index 0000000..9329c34 --- /dev/null +++ b/tools/bone-sea/s13/link.ld @@ -0,0 +1,126 @@ +/* SPDX-License-Identifier: GPL-2.0-or-later */ +OUTPUT_FORMAT(elf32-i386) +OUTPUT_ARCH(i386) +ENTRY(_start) + +PHDRS +{ + sea_code PT_LOAD FLAGS(5); + sea_stack PT_LOAD FLAGS(6); + sea_bounce PT_LOAD FLAGS(6); + sea_scratch PT_LOAD FLAGS(6); + sea_linker PT_LOAD FLAGS(6); + sea_arena PT_LOAD FLAGS(6); + sea_zero PT_LOAD FLAGS(6); +} + +SECTIONS +{ + /* + * VMA is the offset visible through the SEA LDT whose base is 0x00020000. + * LMA is the physical publication address used by the N6 loader. + */ + .sea_code 0x00000000 : AT(0x00020000) + { + __sea_code_start = .; + KEEP(*(.text.entry)) + *(.text .text.*) + *(.rodata .rodata.*) + *(.data .data.*) + *(.bss .bss.*) + *(COMMON) + . = ALIGN(16); + __sea_code_end = .; + } :sea_code + + .sea_stack 0x00010000 (NOLOAD) : AT(0x00030000) + { + __sea_stack_start = .; + . += 0x00004000; + __sea_stack_end = .; + } :sea_stack + + .sea_bounce 0x00014000 (NOLOAD) : AT(0x00034000) + { + __sea_bounce_start = .; + KEEP(*(.sea_bounce)) + __sea_bounce_end = .; + } :sea_bounce + + .sea_scratch 0x00015000 (NOLOAD) : AT(0x00035000) + { + __sea_scratch_start = .; + KEEP(*(.sea_scratch)) + __sea_scratch_end = .; + } :sea_scratch + + .sea_linker 0x00018000 (NOLOAD) : AT(0x00038000) + { + __sea_linker_start = .; + . += 0x00008000; + __sea_linker_end = .; + } :sea_linker + + .sea_arena 0x00020000 (NOLOAD) : AT(0x00040000) + { + __sea_arena_start = .; + KEEP(*(.sea_arena)) + __sea_arena_end = .; + } :sea_arena + + .sea_zero 0x00060000 (NOLOAD) : AT(0x00080000) + { + __sea_zero_start = .; + . += 0x00010000; + __sea_zero_end = .; + } :sea_zero + + ASSERT(ADDR(.sea_code) == 0x00000000, "S13 SEA code VMA drift") + ASSERT(LOADADDR(.sea_code) == 0x00020000, "S13 SEA code LMA drift") + ASSERT(SIZEOF(.sea_code) > 0, "S13 SEA code is empty") + ASSERT(SIZEOF(.sea_code) <= 0x00010000, "S13 SEA code exceeds 64 KiB window") + ASSERT(__sea_code_end <= 0x00010000, "S13 SEA code overlaps local stack") + + ASSERT(ADDR(.sea_stack) == 0x00010000, "S13 SEA stack VMA drift") + ASSERT(LOADADDR(.sea_stack) == 0x00030000, "S13 SEA stack LMA drift") + ASSERT(SIZEOF(.sea_stack) == 0x00004000, "S13 SEA stack size drift") + + ASSERT(ADDR(.sea_bounce) == 0x00014000, "S13 SEA bounce VMA drift") + ASSERT(LOADADDR(.sea_bounce) == 0x00034000, "S13 SEA bounce LMA drift") + ASSERT(SIZEOF(.sea_bounce) == 0x00001000, "S13 SEA bounce size drift") + + ASSERT(ADDR(.sea_scratch) == 0x00015000, "S13 SEA scratch VMA drift") + ASSERT(LOADADDR(.sea_scratch) == 0x00035000, "S13 SEA scratch LMA drift") + ASSERT(SIZEOF(.sea_scratch) == 0x00003000, "S13 SEA scratch size drift") + + ASSERT(ADDR(.sea_linker) == 0x00018000, "S13 SEA reserve VMA drift") + ASSERT(LOADADDR(.sea_linker) == 0x00038000, "S13 SEA reserve LMA drift") + ASSERT(SIZEOF(.sea_linker) == 0x00008000, "S13 SEA reserve size drift") + + ASSERT(ADDR(.sea_arena) == 0x00020000, "S13 SEA arena VMA drift") + ASSERT(LOADADDR(.sea_arena) == 0x00040000, "S13 SEA arena LMA drift") + ASSERT(SIZEOF(.sea_arena) == 0x00040000, "S13 SEA arena size drift") + + ASSERT(ADDR(.sea_zero) == 0x00060000, "S13 SEA zero VMA drift") + ASSERT(LOADADDR(.sea_zero) == 0x00080000, "S13 SEA zero LMA drift") + ASSERT(SIZEOF(.sea_zero) == 0x00010000, "S13 SEA zero size drift") + ASSERT(__sea_zero_end == 0x00070000, "S13 SEA local domain end drift") + ASSERT(LOADADDR(.sea_zero) + SIZEOF(.sea_zero) == 0x00090000, + "S13 SEA physical domain end drift") + + /DISCARD/ : + { + *(.comment) + *(.note*) + *(.eh_frame*) + *(.gcc_except_table*) + *(.got*) + *(.plt*) + *(.rel*) + *(.rela*) + *(.init_array*) + *(.fini_array*) + *(.ctors*) + *(.dtors*) + } +} diff --git a/tools/bone-sea/s13/prove.py b/tools/bone-sea/s13/prove.py new file mode 100644 index 0000000..ed99db9 --- /dev/null +++ b/tools/bone-sea/s13/prove.py @@ -0,0 +1,640 @@ +#!/usr/bin/env python3 +"""Build and judge the BONE/SEA S13 segment-local SEA image.""" + +from __future__ import annotations + +import argparse +import hashlib +import os +import struct +import subprocess +import sys +import tempfile +from dataclasses import dataclass +from pathlib import Path +from typing import Sequence + +ROOT = Path(__file__).resolve().parents[3] +if str(ROOT) not in sys.path: + sys.path.insert(0, str(ROOT)) + +from bone import BoneError, run_checked # noqa: E402 + +PARENT_HEAD = "56f9697f094fd848b0cf659861f21407b3a9ea75" +SHINESEA_HEAD = "3bc6343ecaeae27f0d01c6301cab01a0e77bfb96" +TARGET = "i686-unknown-linux-gnu" +CRATE_NAME = "bone_sea_s13_local_image" + +SEA_PHYS = 0x0002_0000 +SEA_BYTES = 0x0007_0000 +SEA_END = SEA_PHYS + SEA_BYTES +SEA_LIMIT = SEA_BYTES - 1 +CODE_BYTES_MAX = 0x0001_0000 + +ELFCLASS32 = 1 +ELFDATA2LSB = 1 +ET_EXEC = 2 +EM_386 = 3 +PT_LOAD = 1 +PT_DYNAMIC = 2 +PT_INTERP = 3 +SHT_PROGBITS = 1 +SHT_SYMTAB = 2 +SHT_NOBITS = 8 +SHF_ALLOC = 0x2 + +REGIONS = ( + (".sea_code", 0x0000_0000, 0x0002_0000, None, 5, True), + (".sea_stack", 0x0001_0000, 0x0003_0000, 0x0000_4000, 6, False), + (".sea_bounce", 0x0001_4000, 0x0003_4000, 0x0000_1000, 6, False), + (".sea_scratch", 0x0001_5000, 0x0003_5000, 0x0000_3000, 6, False), + (".sea_linker", 0x0001_8000, 0x0003_8000, 0x0000_8000, 6, False), + (".sea_arena", 0x0002_0000, 0x0004_0000, 0x0004_0000, 6, False), + (".sea_zero", 0x0006_0000, 0x0008_0000, 0x0001_0000, 6, False), +) + +FROZEN_SOURCE_PATHS = ( + "tools/bone-sea/src/lib.rs", + "tools/bone-sea/src/s3_adapter.rs", + "tools/bone-sea/s10/image.rs", +) + +FORBIDDEN_SECTIONS = ( + ".dynamic", + ".dynsym", + ".dynstr", + ".interp", + ".plt", + ".got", + ".got.plt", + ".rel.dyn", + ".rela.dyn", + ".gnu.version", +) + + +@dataclass(frozen=True) +class Segment: + kind: int + offset: int + virtual: int + physical: int + file_size: int + memory_size: int + flags: int + alignment: int + + +@dataclass(frozen=True) +class Section: + name: str + kind: int + flags: int + address: int + offset: int + size: int + link: int + entry_size: int + + +@dataclass(frozen=True) +class Symbol: + name: str + value: int + section_index: int + + +def parser() -> argparse.ArgumentParser: + cli = argparse.ArgumentParser(prog="bone-sea-s13", description=__doc__) + cli.add_argument("--shinesea", type=Path, required=True) + return cli + + +def capture(args: Sequence[str | os.PathLike[str]], cwd: Path) -> str: + result = subprocess.run( + [str(value) for value in args], + cwd=cwd, + text=True, + capture_output=True, + check=False, + ) + if result.returncode != 0: + if result.stdout: + print(result.stdout, end="", file=sys.stderr) + if result.stderr: + print(result.stderr, end="", file=sys.stderr) + raise BoneError(f"command failed ({result.returncode}): {' '.join(map(str, args))}") + return result.stdout + + +def git_head(repository: Path) -> str: + return capture(["git", "-C", repository, "rev-parse", "HEAD"], repository).strip() + + +def require_clean(repository: Path) -> None: + for cached in (False, True): + command = ["git", "-C", repository, "diff"] + if cached: + command.append("--cached") + command.extend(["--quiet", "--ignore-submodules", "--"]) + result = subprocess.run(command, cwd=repository, check=False) + if result.returncode == 1: + raise BoneError(f"tracked working tree is dirty: {repository}") + if result.returncode != 0: + raise BoneError(f"git cleanliness check failed: {repository}") + + +def require_ancestor(repository: Path, ancestor: str, descendant: str) -> None: + result = subprocess.run( + ["git", "-C", repository, "merge-base", "--is-ancestor", ancestor, descendant], + cwd=repository, + check=False, + ) + if result.returncode == 1: + raise BoneError(f"{ancestor} is not an ancestor of {descendant}") + if result.returncode != 0: + raise BoneError("git merge-base failed") + + +def require_paths_unchanged(repository: Path, authority: str, paths: Sequence[str]) -> None: + result = subprocess.run( + ["git", "-C", repository, "diff", "--quiet", authority, "--", *paths], + cwd=repository, + check=False, + ) + if result.returncode == 1: + raise BoneError(f"frozen source paths differ from {authority}") + if result.returncode != 0: + raise BoneError("frozen source-path judge failed") + + +def require_target() -> None: + installed = capture(["rustup", "target", "list", "--installed"], ROOT) + if TARGET not in {line.strip() for line in installed.splitlines()}: + raise BoneError(f"missing Rust target {TARGET}; run rustup target add {TARGET}") + + +def rust_lld_path() -> Path: + verbose = capture(["rustc", "-vV"], ROOT) + host = next( + (line.removeprefix("host: ") for line in verbose.splitlines() if line.startswith("host: ")), + None, + ) + if not host: + raise BoneError("rustc did not report a host triple") + sysroot = Path(capture(["rustc", "--print", "sysroot"], ROOT).strip()) + executable = "rust-lld.exe" if os.name == "nt" else "rust-lld" + linker = sysroot / "lib" / "rustlib" / host / "bin" / executable + if not linker.is_file(): + raise BoneError(f"rust-lld not found: {linker}") + return linker + + +def compile_rlib(crate: str, source: Path, output: Path, cwd: Path) -> None: + run_checked( + [ + "rustc", + "--crate-name", + crate, + "--crate-type=rlib", + "--edition=2021", + "--target", + TARGET, + "-Dwarnings", + "-Copt-level=z", + "-Cpanic=abort", + "-Ccodegen-units=1", + "-Cembed-bitcode=yes", + source, + "-o", + output, + ], + cwd=cwd, + ) + + +def compile_image(linker: Path, bone_sea: Path, shine: Path, output: Path) -> None: + run_checked( + [ + "rustc", + "--crate-name", + CRATE_NAME, + "--crate-type=bin", + "--edition=2021", + "--target", + TARGET, + "-Dwarnings", + "-Copt-level=z", + "-Cpanic=abort", + "-Ccodegen-units=1", + "-Clto=fat", + "-Crelocation-model=static", + "-Cdefault-linker-libraries=no", + "-Cno-redzone=yes", + f"-Clinker={linker}", + "-Clinker-flavor=ld.lld", + f"-Clink-arg=-T{ROOT / 'tools/bone-sea/s13/link.ld'}", + "-Clink-arg=--gc-sections", + "-Clink-arg=--build-id=none", + "-Clink-arg=--no-undefined", + "-Clink-arg=--fatal-warnings", + "-Clink-arg=-nostdlib", + "-Clink-arg=-static", + "-Clink-arg=-no-pie", + "-Clink-arg=-z", + "-Clink-arg=max-page-size=4096", + ROOT / "tools/bone-sea/s10/image.rs", + "--extern", + f"bone_sea={bone_sea}", + "--extern", + f"shinesea={shine}", + "-o", + output, + ], + cwd=ROOT, + ) + + +def checked_slice(data: bytes, offset: int, size: int) -> bytes: + end = offset + size + if offset < 0 or size < 0 or end < offset or end > len(data): + raise BoneError(f"ELF range outside file offset={offset} bytes={size}") + return data[offset:end] + + +def u16(data: bytes, offset: int) -> int: + return struct.unpack_from(" int: + return struct.unpack_from(" str: + if offset < 0 or offset >= len(table): + raise BoneError("ELF string offset outside table") + tail = table[offset:] + length = tail.find(b"\0") + if length < 0: + length = len(tail) + return tail[:length].decode("utf-8") + + +def parse_elf(data: bytes) -> tuple[int, list[Segment], list[Section], list[Symbol]]: + if len(data) < 52 or data[:4] != b"\x7fELF": + raise BoneError("S13 output is not ELF") + if data[4] != ELFCLASS32 or data[5] != ELFDATA2LSB or data[6] != 1: + raise BoneError("S13 ELF identity is not ELF32 little-endian version 1") + if u16(data, 16) != ET_EXEC or u16(data, 18) != EM_386 or u32(data, 20) != 1: + raise BoneError("S13 ELF type, machine, or version drift") + if u16(data, 40) != 52: + raise BoneError("S13 ELF header-size drift") + + entry = u32(data, 24) + phoff = u32(data, 28) + shoff = u32(data, 32) + phentsize = u16(data, 42) + phnum = u16(data, 44) + shentsize = u16(data, 46) + shnum = u16(data, 48) + shstrndx = u16(data, 50) + if phentsize != 32 or shentsize != 40 or shnum == 0 or shstrndx >= shnum: + raise BoneError("S13 ELF table geometry drift") + + segments: list[Segment] = [] + for index in range(phnum): + base = phoff + index * phentsize + checked_slice(data, base, phentsize) + segments.append( + Segment( + kind=u32(data, base), + offset=u32(data, base + 4), + virtual=u32(data, base + 8), + physical=u32(data, base + 12), + file_size=u32(data, base + 16), + memory_size=u32(data, base + 20), + flags=u32(data, base + 24), + alignment=u32(data, base + 28), + ) + ) + + raw_sections: list[tuple[int, int, int, int, int, int, int, int]] = [] + for index in range(shnum): + base = shoff + index * shentsize + checked_slice(data, base, shentsize) + raw_sections.append( + ( + u32(data, base), + u32(data, base + 4), + u32(data, base + 8), + u32(data, base + 12), + u32(data, base + 16), + u32(data, base + 20), + u32(data, base + 24), + u32(data, base + 36), + ) + ) + + shstr = raw_sections[shstrndx] + names = checked_slice(data, shstr[4], shstr[5]) + sections = [ + Section( + name=string_at(names, raw[0]), + kind=raw[1], + flags=raw[2], + address=raw[3], + offset=raw[4], + size=raw[5], + link=raw[6], + entry_size=raw[7], + ) + for raw in raw_sections + ] + + for section in sections: + if section.kind != SHT_NOBITS: + checked_slice(data, section.offset, section.size) + + symbols: list[Symbol] = [] + for section in sections: + if section.kind != SHT_SYMTAB: + continue + if section.entry_size != 16 or section.link >= len(sections): + raise BoneError("S13 symbol-table geometry drift") + string_section = sections[section.link] + strings = checked_slice(data, string_section.offset, string_section.size) + count = section.size // section.entry_size + for index in range(count): + base = section.offset + index * section.entry_size + checked_slice(data, base, section.entry_size) + symbols.append( + Symbol( + name=string_at(strings, u32(data, base)), + value=u32(data, base + 4), + section_index=u16(data, base + 14), + ) + ) + + return entry, segments, sections, symbols + + +def unique_section(sections: Sequence[Section], name: str) -> Section: + matches = [section for section in sections if section.name == name] + if len(matches) != 1: + raise BoneError(f"S13 expected one section {name}, observed {len(matches)}") + return matches[0] + + +def load_segments(segments: Sequence[Segment]) -> list[Segment]: + if any(segment.kind in (PT_DYNAMIC, PT_INTERP) for segment in segments): + raise BoneError("S13 ELF contains dynamic or interpreter segment") + loads = [segment for segment in segments if segment.kind == PT_LOAD] + if len(loads) != len(REGIONS): + raise BoneError(f"S13 PT_LOAD count drift expected=7 actual={len(loads)}") + return loads + + +def verify_translation(loads: Sequence[Segment]) -> None: + for segment in loads: + virtual = segment.virtual + physical = segment.physical + if physical != SEA_PHYS + virtual: + raise BoneError( + f"S13 VMA/LMA translation drift virtual=0x{virtual:08x} physical=0x{physical:08x}" + ) + if virtual + segment.memory_size > SEA_BYTES: + raise BoneError("S13 segment exceeds the local SEA domain") + if physical + segment.memory_size > SEA_END: + raise BoneError("S13 segment exceeds the physical SEA domain") + + +def verify_image(data: bytes) -> tuple[bytes, dict[str, int | str]]: + entry, segments, sections, symbols = parse_elf(data) + if entry != 0: + raise BoneError(f"S13 entry is not local zero: 0x{entry:08x}") + + allowed = {region[0] for region in REGIONS} + for section in sections: + if section.name in FORBIDDEN_SECTIONS: + raise BoneError(f"S13 ELF contains forbidden section {section.name}") + if section.flags & SHF_ALLOC and section.name not in allowed: + raise BoneError(f"S13 ELF contains unowned alloc section {section.name}") + + code = unique_section(sections, ".sea_code") + if ( + code.kind != SHT_PROGBITS + or code.address != 0 + or code.size == 0 + or code.size > CODE_BYTES_MAX + ): + raise BoneError("S13 code-section geometry failed") + code_bytes = code.size + + for name, virtual, _physical, size, _flags, has_file in REGIONS: + section = unique_section(sections, name) + if section.address != virtual: + raise BoneError(f"S13 section VMA drift: {name}") + if has_file: + if section.kind != SHT_PROGBITS or section.size != code_bytes: + raise BoneError("S13 code section type or size drift") + elif section.kind != SHT_NOBITS or section.size != size: + raise BoneError(f"S13 NOLOAD section geometry drift: {name}") + + undefined = [symbol for symbol in symbols if symbol.section_index == 0 and symbol.name] + if undefined: + names = ", ".join(symbol.name for symbol in undefined) + raise BoneError(f"S13 ELF retains undefined symbols: {names}") + starts = [symbol for symbol in symbols if symbol.name == "_start" and symbol.section_index != 0] + if len(starts) != 1 or starts[0].value != 0: + raise BoneError("S13 _start symbol is not exact local zero") + + loads = load_segments(segments) + verify_translation(loads) + for name, virtual, physical, size, flags, has_file in REGIONS: + matches = [segment for segment in loads if segment.virtual == virtual] + if len(matches) != 1: + raise BoneError(f"S13 missing or duplicate load segment for {name}") + segment = matches[0] + expected_size = code_bytes if size is None else size + if ( + segment.physical != physical + or segment.memory_size != expected_size + or segment.flags != flags + or segment.alignment != 4096 + ): + raise BoneError(f"S13 load-segment geometry drift: {name}") + if has_file: + if segment.file_size == 0 or segment.file_size > expected_size: + raise BoneError("S13 code-segment file-size drift") + elif segment.file_size != 0: + raise BoneError(f"S13 NOLOAD segment retains file bytes: {name}") + + flat = bytearray(SEA_BYTES) + for segment in loads: + destination = segment.physical - SEA_PHYS + if segment.file_size: + source = checked_slice(data, segment.offset, segment.file_size) + flat[destination : destination + len(source)] = source + if not any(flat[:code_bytes]): + raise BoneError("S13 physical code image is zero") + if any(flat[code_bytes:]): + raise BoneError("S13 physical reserved bytes are nonzero") + + metrics: dict[str, int | str] = { + "elf_bytes": len(data), + "elf_sha256": hashlib.sha256(data).hexdigest(), + "code_bytes": code_bytes, + "code_headroom": CODE_BYTES_MAX - code_bytes, + "flat_bytes": len(flat), + "flat_sha256": hashlib.sha256(flat).hexdigest(), + "load_segments": len(loads), + "undefined_symbols": len(undefined), + } + return bytes(flat), metrics + + +def require_adversaries(data: bytes) -> None: + _entry, segments, _sections, _symbols = parse_elf(data) + loads = load_segments(segments) + + first = loads[0] + vma_adversary = [ + Segment( + kind=segment.kind, + offset=segment.offset, + virtual=SEA_PHYS if segment is first else segment.virtual, + physical=segment.physical, + file_size=segment.file_size, + memory_size=segment.memory_size, + flags=segment.flags, + alignment=segment.alignment, + ) + for segment in loads + ] + try: + verify_translation(vma_adversary) + except BoneError: + pass + else: + raise BoneError("S13 absolute-VMA adversary was accepted") + + lma_adversary = [ + Segment( + kind=segment.kind, + offset=segment.offset, + virtual=segment.virtual, + physical=segment.physical + 512 if segment is first else segment.physical, + file_size=segment.file_size, + memory_size=segment.memory_size, + flags=segment.flags, + alignment=segment.alignment, + ) + for segment in loads + ] + try: + verify_translation(lma_adversary) + except BoneError: + pass + else: + raise BoneError("S13 LMA-offset adversary was accepted") + + +def prove(args: argparse.Namespace) -> None: + shinesea = args.shinesea.resolve() + if not (shinesea / "Cargo.toml").is_file() or not (shinesea / "src/lib.rs").is_file(): + raise BoneError(f"invalid SHINESEA checkout: {shinesea}") + + head = git_head(ROOT) + require_ancestor(ROOT, PARENT_HEAD, head) + require_clean(ROOT) + require_paths_unchanged(ROOT, PARENT_HEAD, FROZEN_SOURCE_PATHS) + + shine_head = git_head(shinesea) + if shine_head != SHINESEA_HEAD: + raise BoneError(f"SHINESEA head mismatch expected={SHINESEA_HEAD} actual={shine_head}") + require_clean(shinesea) + require_target() + linker = rust_lld_path() + + temporary_path: Path | None = None + result: dict[str, int | str] = {} + with tempfile.TemporaryDirectory(prefix="bone-sea-s13-") as name: + temporary = Path(name) + temporary_path = temporary + bone_sea = temporary / "libbone_sea_s13.rlib" + shine = temporary / "libshinesea_s13.rlib" + compile_rlib("bone_sea", ROOT / "tools/bone-sea/src/lib.rs", bone_sea, ROOT) + compile_rlib("shinesea", shinesea / "src/lib.rs", shine, shinesea) + + image = temporary / "bone-sea-s13.elf" + compile_image(linker, bone_sea, shine, image) + first_data = image.read_bytes() + first_flat, first_metrics = verify_image(first_data) + + image.unlink() + compile_image(linker, bone_sea, shine, image) + second_data = image.read_bytes() + if first_data != second_data: + raise BoneError("S13 repeated ELF builds are not byte-identical") + second_flat, second_metrics = verify_image(second_data) + if first_flat != second_flat or first_metrics != second_metrics: + raise BoneError("S13 repeated physical images are not byte-identical") + + require_adversaries(first_data) + result = first_metrics + + if temporary_path is None or temporary_path.exists(): + raise BoneError("S13 temporary tree survived cleanup") + + print("BONE/SEA S13 SEGMENT-LOCAL IMAGE VERIFIED") + print(f"BONEBOX HEAD {head}") + print(f"S13 PARENT HEAD {PARENT_HEAD}") + print(f"SHINESEA HEAD {shine_head}") + print(f"TARGET {TARGET}") + print(f"CRATE NAME {CRATE_NAME}") + print("ELF ENTRY OFFSET 0x00000000") + print(f"SEA SEGMENT BASE 0x{SEA_PHYS:08X}") + print(f"SEA SEGMENT LIMIT 0x{SEA_LIMIT:08X}") + print("SEA LOCAL RANGE 0x00000000..0x0006FFFF") + print(f"SEA PHYSICAL RANGE 0x{SEA_PHYS:08X}..0x{SEA_END - 1:08X}") + print(f"ELF BYTES {result['elf_bytes']}") + print(f"ELF SHA256 {result['elf_sha256']}") + print(f"CODE BYTES {result['code_bytes']}") + print(f"CODE HEADROOM {result['code_headroom']}") + print(f"FLAT BYTES {result['flat_bytes']}") + print(f"FLAT SHA256 {result['flat_sha256']}") + print(f"PT_LOAD SEGMENTS {result['load_segments']}") + print(f"UNDEFINED SYMBOLS {result['undefined_symbols']}") + print("VMA/LMA TRANSLATION PASS") + print("REPEATED ELF IDENTITY PASS") + print("REPEATED FLAT IDENTITY PASS") + print("ABSOLUTE VMA ADVERSARY REJECTED") + print("LMA OFFSET ADVERSARY REJECTED") + print("RING3 TRANSFER NOT PERFORMED") + print("SEA ENTRY EXECUTED NO") + print("WRITE AUTHORITY DISABLED") + print("TEMPORARY OUTPUTS REMOVED ON EXIT") + print("S13 local-offset image contract complete; this is not a ring3 execution PASS claim.") + print("BONE/SEA S13 SEGMENT-LOCAL IMAGE VERIFY PASS") + + +def main(argv: Sequence[str] | None = None) -> int: + args = parser().parse_args(argv) + try: + prove(args) + return 0 + except ( + BoneError, + IndexError, + OSError, + UnicodeError, + ValueError, + struct.error, + subprocess.SubprocessError, + ) as error: + print(f"BONE/SEA S13 ERROR: {error}", file=sys.stderr) + return 1 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/tools/bone-sea/src/bin/bone-sea-s13.rs b/tools/bone-sea/src/bin/bone-sea-s13.rs new file mode 100644 index 0000000..91dbcfd --- /dev/null +++ b/tools/bone-sea/src/bin/bone-sea-s13.rs @@ -0,0 +1,271 @@ +#![deny(warnings)] + +use std::env; +use std::ffi::{OsStr, OsString}; +use std::path::{Path, PathBuf}; +use std::process::{Command, ExitCode, Stdio}; + +const CONFIG_TEXT: &str = include_str!("../../../../config/bone_sea_s13.json"); +const LINKER_TEXT: &str = include_str!("../../s13/link.ld"); +const PROOF_TEXT: &str = include_str!("../../s13/prove.py"); +const IMAGE_TEXT: &str = include_str!("../../s10/image.rs"); + +const PARENT_HEAD: &str = "56f9697f094fd848b0cf659861f21407b3a9ea75"; +const SHINESEA_HEAD: &str = "3bc6343ecaeae27f0d01c6301cab01a0e77bfb96"; +const CINDER_HEAD: &str = "9eadc22d03b0782373d5ca23290bb76768df5e4f"; +const LOOM_HEAD: &str = "444937bd0aef2e5b17ed253deb7677a778225d7e"; + +const SEA_BASE: u64 = 0x0002_0000; +const SEA_BYTES: u64 = 0x0007_0000; +const SEA_END: u64 = SEA_BASE + SEA_BYTES; +const SEA_LIMIT: u64 = SEA_BYTES - 1; +const ENTRY_OFFSET: u64 = 0; + +const LOCAL_REGIONS: [(u64, u64); 7] = [ + (0x0000_0000, 0x0001_0000), + (0x0001_0000, 0x0000_4000), + (0x0001_4000, 0x0000_1000), + (0x0001_5000, 0x0000_3000), + (0x0001_8000, 0x0000_8000), + (0x0002_0000, 0x0004_0000), + (0x0006_0000, 0x0001_0000), +]; + +const PHYSICAL_REGIONS: [(u64, u64); 7] = [ + (0x0002_0000, 0x0001_0000), + (0x0003_0000, 0x0000_4000), + (0x0003_4000, 0x0000_1000), + (0x0003_5000, 0x0000_3000), + (0x0003_8000, 0x0000_8000), + (0x0004_0000, 0x0004_0000), + (0x0008_0000, 0x0001_0000), +]; + +type SeaResult = Result; + +fn usage() -> &'static str { + "usage: cargo run --locked --release --manifest-path tools/bone-sea/Cargo.toml --bin bone-sea-s13 -- verify --shinesea PATH" +} + +fn repository_root() -> SeaResult { + PathBuf::from(env!("CARGO_MANIFEST_DIR")) + .parent() + .and_then(Path::parent) + .map(Path::to_path_buf) + .ok_or_else(|| "cannot resolve BONEBOX repository root".to_owned()) +} + +fn compiled_identity() -> SeaResult<()> { + if PARENT_HEAD.len() != 40 + || SHINESEA_HEAD.len() != 40 + || CINDER_HEAD.len() != 40 + || LOOM_HEAD.len() != 40 + || ENTRY_OFFSET != 0 + || SEA_END != 0x0009_0000 + || SEA_LIMIT != 0x0006_ffff + || LOCAL_REGIONS[0].0 != 0 + || LOCAL_REGIONS[6].0 + LOCAL_REGIONS[6].1 != SEA_BYTES + || PHYSICAL_REGIONS[0].0 != SEA_BASE + || PHYSICAL_REGIONS[6].0 + PHYSICAL_REGIONS[6].1 != SEA_END + { + return Err("compiled S13 authority identity failed".to_owned()); + } + Ok(()) +} + +fn verify_static_contract() -> SeaResult<()> { + for token in [ + "\"phase\": \"S13-SEGMENT-LOCAL-IMAGE\"", + "\"parent_head\": \"56f9697f094fd848b0cf659861f21407b3a9ea75\"", + "\"entry_offset\": 0", + "\"formula\": \"physical = segment_base + local\"", + "\"elf_vma_is_local\": true", + "\"elf_lma_is_physical\": true", + "\"absolute_physical_vma_forbidden\": true", + "\"exact_elf_repeatability\": true", + "\"exact_flat_repeatability\": true", + "\"ring3_transfer\": false", + "\"sea_entry_executed\": false", + "\"write_authority\": false", + ] { + if !CONFIG_TEXT.contains(token) { + return Err(format!("S13 config missing token: {token}")); + } + } + + for token in [ + "ENTRY(_start)", + ".sea_code 0x00000000 : AT(0x00020000)", + ".sea_stack 0x00010000 (NOLOAD) : AT(0x00030000)", + ".sea_bounce 0x00014000 (NOLOAD) : AT(0x00034000)", + ".sea_scratch 0x00015000 (NOLOAD) : AT(0x00035000)", + ".sea_linker 0x00018000 (NOLOAD) : AT(0x00038000)", + ".sea_arena 0x00020000 (NOLOAD) : AT(0x00040000)", + ".sea_zero 0x00060000 (NOLOAD) : AT(0x00080000)", + "S13 SEA local domain end drift", + "S13 SEA physical domain end drift", + ] { + if !LINKER_TEXT.contains(token) { + return Err(format!("S13 linker missing token: {token}")); + } + } + for forbidden in [ + ".sea_code 0x00020000 :", + ".sea_scratch 0x00035000", + "ENTRY(0x00020000)", + ] { + if LINKER_TEXT.contains(forbidden) { + return Err(format!("S13 linker retains forbidden physical VMA: {forbidden}")); + } + } + + for token in [ + "verify_translation", + "physical != SEA_PHYS + virtual", + "repeated ELF builds are not byte-identical", + "repeated physical images are not byte-identical", + "absolute-VMA adversary was accepted", + "LMA-offset adversary was accepted", + "RING3 TRANSFER NOT PERFORMED", + "TEMPORARY OUTPUTS REMOVED ON EXIT", + ] { + if !PROOF_TEXT.contains(token) { + return Err(format!("S13 proof missing token: {token}")); + } + } + + for token in [ + "#![no_std]", + "#![no_main]", + "#[link_section = \".sea_bounce\"]", + "#[link_section = \".sea_scratch\"]", + "#[link_section = \".sea_arena\"]", + "pub extern \"C\" fn _start() -> !", + ] { + if !IMAGE_TEXT.contains(token) { + return Err(format!("frozen image source missing token: {token}")); + } + } + Ok(()) +} + +fn python_program(root: &Path) -> SeaResult { + for candidate in ["python", "python3"] { + let status = Command::new(candidate) + .arg("--version") + .current_dir(root) + .stdin(Stdio::null()) + .stdout(Stdio::null()) + .stderr(Stdio::null()) + .status(); + if matches!(status, Ok(status) if status.success()) { + return Ok(OsString::from(candidate)); + } + } + Err("python interpreter not found".to_owned()) +} + +fn run() -> SeaResult<()> { + compiled_identity()?; + verify_static_contract()?; + + let mut arguments = env::args_os().skip(1); + match arguments.next().as_deref() { + Some(command) if command == OsStr::new("verify") => {} + _ => return Err(usage().to_owned()), + } + let forwarded: Vec = arguments.collect(); + if !forwarded.iter().any(|argument| argument == OsStr::new("--shinesea")) { + return Err(usage().to_owned()); + } + + let root = repository_root()?; + let python = python_program(&root)?; + let status = Command::new(python) + .arg(root.join("tools/bone-sea/s13/prove.py")) + .args(forwarded) + .current_dir(&root) + .stdin(Stdio::null()) + .status() + .map_err(|error| format!("cannot execute S13 proof: {error}"))?; + if status.success() { + Ok(()) + } else { + Err(format!("S13 proof failed with status {status}")) + } +} + +fn main() -> ExitCode { + match run() { + Ok(()) => ExitCode::SUCCESS, + Err(error) => { + eprintln!("BONE/SEA S13 ERROR: {error}"); + ExitCode::FAILURE + } + } +} + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn identities_are_exact() { + compiled_identity().unwrap(); + } + + #[test] + fn static_contract_passes() { + verify_static_contract().unwrap(); + } + + #[test] + fn local_ledger_is_contiguous() { + for pair in LOCAL_REGIONS.windows(2) { + assert_eq!(pair[0].0 + pair[0].1, pair[1].0); + } + assert_eq!(LOCAL_REGIONS[0].0, 0); + assert_eq!(LOCAL_REGIONS[6].0 + LOCAL_REGIONS[6].1, SEA_BYTES); + } + + #[test] + fn physical_ledger_is_contiguous() { + for pair in PHYSICAL_REGIONS.windows(2) { + assert_eq!(pair[0].0 + pair[0].1, pair[1].0); + } + assert_eq!(PHYSICAL_REGIONS[0].0, SEA_BASE); + assert_eq!(PHYSICAL_REGIONS[6].0 + PHYSICAL_REGIONS[6].1, SEA_END); + } + + #[test] + fn every_region_obeys_base_translation() { + for (local, physical) in LOCAL_REGIONS.iter().zip(PHYSICAL_REGIONS.iter()) { + assert_eq!(physical.0, SEA_BASE + local.0); + assert_eq!(physical.1, local.1); + } + } + + #[test] + fn entry_is_segment_local_zero() { + assert_eq!(ENTRY_OFFSET, 0); + assert!(LINKER_TEXT.contains(".sea_code 0x00000000 : AT(0x00020000)")); + assert!(!LINKER_TEXT.contains(".sea_code 0x00020000 :")); + } + + #[test] + fn deterministic_and_adversarial_gates_are_frozen() { + assert!(PROOF_TEXT.contains("first_data != second_data")); + assert!(PROOF_TEXT.contains("virtual=SEA_PHYS if segment is first else segment.virtual")); + assert!(PROOF_TEXT.contains( + "physical=segment.physical + 512 if segment is first else segment.physical" + )); + } + + #[test] + fn execution_and_write_claims_remain_forbidden() { + assert!(CONFIG_TEXT.contains("\"ring3_transfer\": false")); + assert!(CONFIG_TEXT.contains("\"sea_entry_executed\": false")); + assert!(CONFIG_TEXT.contains("\"write_authority\": false")); + assert!(PROOF_TEXT.contains("RING3 TRANSFER NOT PERFORMED")); + } +}