From 24901aaf200c2d1d4f51a29e1f81be9bde3fc180 Mon Sep 17 00:00:00 2001 From: DEADBYTE Date: Wed, 5 Aug 2026 06:49:47 +0700 Subject: [PATCH 1/9] add the S13 segment-local SEA linker contract --- tools/bone-sea/s13/link.ld | 126 +++++++++++++++++++++++++++++++++++++ 1 file changed, 126 insertions(+) create mode 100644 tools/bone-sea/s13/link.ld 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*) + } +} From 63b0b4e3b12125316d6c0c457f3ff9d452fcc786 Mon Sep 17 00:00:00 2001 From: DEADBYTE Date: Wed, 5 Aug 2026 06:50:12 +0700 Subject: [PATCH 2/9] freeze the S13 segment-local image contract --- config/bone_sea_s13.json | 115 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 115 insertions(+) create mode 100644 config/bone_sea_s13.json 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 + } +} From 463606d03e0851115db89c4a8eba685527f5d47d Mon Sep 17 00:00:00 2001 From: DEADBYTE Date: Wed, 5 Aug 2026 06:51:42 +0700 Subject: [PATCH 3/9] add the S13 segment-local ELF adversarial judge --- tools/bone-sea/s13/prove.py | 590 ++++++++++++++++++++++++++++++++++++ 1 file changed, 590 insertions(+) create mode 100644 tools/bone-sea/s13/prove.py diff --git a/tools/bone-sea/s13/prove.py b/tools/bone-sea/s13/prove.py new file mode 100644 index 0000000..24636cb --- /dev/null +++ b/tools/bone-sea/s13/prove.py @@ -0,0 +1,590 @@ +#!/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 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", +) + + +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( + shinesea: Path, + 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=shinesea, + ) + + +def checked_slice(data: bytes, offset: int, size: int) -> bytes: + end = offset + size + if offset < 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) -> dict[str, object]: + 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[dict[str, int]] = [] + for index in range(phnum): + base = phoff + index * phentsize + checked_slice(data, base, phentsize) + segments.append( + { + "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: list[dict[str, int | str]] = [] + for raw in raw_sections: + sections.append( + { + "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], + } + ) + + symbols: list[dict[str, int | str]] = [] + for section in sections: + if section["kind"] != SHT_SYMTAB: + continue + if section["entry_size"] != 16: + raise BoneError("S13 symbol-table entry-size drift") + string_section = sections[int(section["link"])] + strings = checked_slice(data, int(string_section["offset"]), int(string_section["size"])) + count = int(section["size"]) // int(section["entry_size"]) + for index in range(count): + base = int(section["offset"]) + index * int(section["entry_size"]) + symbols.append( + { + "name": string_at(strings, u32(data, base)), + "value": u32(data, base + 4), + "section_index": u16(data, base + 14), + } + ) + + return {"entry": entry, "segments": segments, "sections": sections, "symbols": symbols} + + +def unique_section(elf: dict[str, object], name: str) -> dict[str, int | str]: + matches = [section for section in elf["sections"] if section["name"] == name] # type: ignore[index] + if len(matches) != 1: + raise BoneError(f"S13 expected one section {name}, observed {len(matches)}") + return matches[0] + + +def load_segments(elf: dict[str, object]) -> list[dict[str, int]]: + segments = elf["segments"] # type: ignore[assignment] + 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[dict[str, int]]) -> None: + for segment in loads: + virtual = segment["virtual"] + physical = segment["physical"] + memory_size = segment["memory_size"] + if virtual >= SEA_PHYS: + raise BoneError(f"S13 absolute physical VMA survived: 0x{virtual:08x}") + if physical != SEA_PHYS + virtual: + raise BoneError( + f"S13 VMA/LMA translation drift virtual=0x{virtual:08x} physical=0x{physical:08x}" + ) + if virtual + memory_size > SEA_BYTES or physical + memory_size > SEA_END: + raise BoneError("S13 segment exceeds local or physical domain") + + +def verify_image(data: bytes) -> tuple[bytes, dict[str, int | str]]: + elf = parse_elf(data) + if elf["entry"] != 0: + raise BoneError(f"S13 entry is not local zero: 0x{int(elf['entry']):08x}") + + allowed = {region[0] for region in REGIONS} + for section in elf["sections"]: # type: ignore[index] + name = str(section["name"]) + if name in FORBIDDEN_SECTIONS: + raise BoneError(f"S13 ELF contains forbidden section {name}") + if int(section["flags"]) & SHF_ALLOC and name not in allowed: + raise BoneError(f"S13 ELF contains unowned alloc section {name}") + + code = unique_section(elf, ".sea_code") + if ( + code["kind"] != SHT_PROGBITS + or code["address"] != 0 + or int(code["size"]) == 0 + or int(code["size"]) > CODE_BYTES_MAX + ): + raise BoneError("S13 code-section geometry failed") + code_bytes = int(code["size"]) + + for name, virtual, _physical, size, _flags, has_file in REGIONS: + section = unique_section(elf, name) + if int(section["address"]) != virtual: + raise BoneError(f"S13 section VMA drift: {name}") + if has_file: + if section["kind"] != SHT_PROGBITS or int(section["size"]) != code_bytes: + raise BoneError("S13 code section type or size drift") + elif section["kind"] != SHT_NOBITS or int(section["size"]) != size: + raise BoneError(f"S13 NOLOAD section geometry drift: {name}") + + undefined = [ + symbol + for symbol in elf["symbols"] # type: ignore[index] + if int(symbol["section_index"]) == 0 and str(symbol["name"]) + ] + if undefined: + names = ", ".join(str(symbol["name"]) for symbol in undefined) + raise BoneError(f"S13 ELF retains undefined symbols: {names}") + starts = [ + symbol + for symbol in elf["symbols"] # type: ignore[index] + if symbol["name"] == "_start" and int(symbol["section_index"]) != 0 + ] + if len(starts) != 1 or int(starts[0]["value"]) != 0: + raise BoneError("S13 _start symbol is not exact local zero") + + loads = load_segments(elf) + 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: + elf = parse_elf(data) + loads = load_segments(elf) + + vma_adversary = [dict(segment) for segment in loads] + vma_adversary[0]["virtual"] = SEA_PHYS + try: + verify_translation(vma_adversary) + except BoneError: + pass + else: + raise BoneError("S13 absolute-VMA adversary was accepted") + + lma_adversary = [dict(segment) for segment in loads] + lma_adversary[0]["physical"] += 512 + 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) + + first = temporary / "bone-sea-s13-a.elf" + second = temporary / "bone-sea-s13-b.elf" + compile_image(shinesea, linker, bone_sea, shine, first) + compile_image(shinesea, linker, bone_sea, shine, second) + + first_data = first.read_bytes() + second_data = second.read_bytes() + if first_data != second_data: + raise BoneError("S13 repeated ELF builds are not byte-identical") + + first_flat, first_metrics = verify_image(first_data) + 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, OSError, 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()) From 238d08e42d0c48a463c30b8a4b4cb16c9f391e62 Mon Sep 17 00:00:00 2001 From: DEADBYTE Date: Wed, 5 Aug 2026 06:52:29 +0700 Subject: [PATCH 4/9] add the S13 native contract and proof launcher --- tools/bone-sea/src/bin/bone-sea-s13.rs | 269 +++++++++++++++++++++++++ 1 file changed, 269 insertions(+) create mode 100644 tools/bone-sea/src/bin/bone-sea-s13.rs 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..ae42266 --- /dev/null +++ b/tools/bone-sea/src/bin/bone-sea-s13.rs @@ -0,0 +1,269 @@ +#![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("vma_adversary[0][\"virtual\"] = SEA_PHYS")); + assert!(PROOF_TEXT.contains("lma_adversary[0][\"physical\"] += 512")); + } + + #[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")); + } +} From 9eb81691370c02565a31ebff0acb5d1e22d76b6a Mon Sep 17 00:00:00 2001 From: DEADBYTE Date: Wed, 5 Aug 2026 06:53:15 +0700 Subject: [PATCH 5/9] document the S13 segment-local address correction --- docs/BONE_SEA_S13.md | 274 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 274 insertions(+) create mode 100644 docs/BONE_SEA_S13.md 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. From 4184ce24a46df83730dd2d128abd445d68738a01 Mon Sep 17 00:00:00 2001 From: DEADBYTE Date: Wed, 5 Aug 2026 06:53:26 +0700 Subject: [PATCH 6/9] add the S13 temporary artifact license notice --- tools/bone-sea/s13/LICENSE-NOTICE.txt | 15 +++++++++++++++ 1 file changed, 15 insertions(+) create mode 100644 tools/bone-sea/s13/LICENSE-NOTICE.txt 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. From c2f43f3d7724d22bd4ee3801203aacfeb13bd714 Mon Sep 17 00:00:00 2001 From: DEADBYTE Date: Wed, 5 Aug 2026 06:53:45 +0700 Subject: [PATCH 7/9] add the S13 exact address-model workflow --- .../bone-sea-s13-local-offset-image.yml | 71 +++++++++++++++++++ 1 file changed, 71 insertions(+) create mode 100644 .github/workflows/bone-sea-s13-local-offset-image.yml 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" From f5796a65a3c057e665ab0ecba0c36f8741f58f64 Mon Sep 17 00:00:00 2001 From: DEADBYTE Date: Wed, 5 Aug 2026 06:56:01 +0700 Subject: [PATCH 8/9] fix the S13 local VMA translation judge --- tools/bone-sea/s13/prove.py | 292 +++++++++++++++++++++--------------- 1 file changed, 171 insertions(+), 121 deletions(-) diff --git a/tools/bone-sea/s13/prove.py b/tools/bone-sea/s13/prove.py index 24636cb..ed99db9 100644 --- a/tools/bone-sea/s13/prove.py +++ b/tools/bone-sea/s13/prove.py @@ -10,6 +10,7 @@ import subprocess import sys import tempfile +from dataclasses import dataclass from pathlib import Path from typing import Sequence @@ -72,6 +73,37 @@ ) +@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) @@ -181,13 +213,7 @@ def compile_rlib(crate: str, source: Path, output: Path, cwd: Path) -> None: ) -def compile_image( - shinesea: Path, - linker: Path, - bone_sea: Path, - shine: Path, - output: Path, -) -> None: +def compile_image(linker: Path, bone_sea: Path, shine: Path, output: Path) -> None: run_checked( [ "rustc", @@ -225,13 +251,13 @@ def compile_image( "-o", output, ], - cwd=shinesea, + cwd=ROOT, ) def checked_slice(data: bytes, offset: int, size: int) -> bytes: end = offset + size - if offset < 0 or end < offset or end > len(data): + 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] @@ -254,7 +280,7 @@ def string_at(table: bytes, offset: int) -> str: return tail[:length].decode("utf-8") -def parse_elf(data: bytes) -> dict[str, object]: +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: @@ -275,21 +301,21 @@ def parse_elf(data: bytes) -> dict[str, object]: if phentsize != 32 or shentsize != 40 or shnum == 0 or shstrndx >= shnum: raise BoneError("S13 ELF table geometry drift") - segments: list[dict[str, int]] = [] + segments: list[Segment] = [] for index in range(phnum): base = phoff + index * phentsize checked_slice(data, base, phentsize) segments.append( - { - "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), - } + 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]] = [] @@ -311,150 +337,143 @@ def parse_elf(data: bytes) -> dict[str, object]: shstr = raw_sections[shstrndx] names = checked_slice(data, shstr[4], shstr[5]) - sections: list[dict[str, int | str]] = [] - for raw in raw_sections: - sections.append( - { - "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], - } + 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[dict[str, int | str]] = [] + symbols: list[Symbol] = [] for section in sections: - if section["kind"] != SHT_SYMTAB: + if section.kind != SHT_SYMTAB: continue - if section["entry_size"] != 16: - raise BoneError("S13 symbol-table entry-size drift") - string_section = sections[int(section["link"])] - strings = checked_slice(data, int(string_section["offset"]), int(string_section["size"])) - count = int(section["size"]) // int(section["entry_size"]) + 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 = int(section["offset"]) + index * int(section["entry_size"]) + base = section.offset + index * section.entry_size + checked_slice(data, base, section.entry_size) symbols.append( - { - "name": string_at(strings, u32(data, base)), - "value": u32(data, base + 4), - "section_index": u16(data, base + 14), - } + Symbol( + name=string_at(strings, u32(data, base)), + value=u32(data, base + 4), + section_index=u16(data, base + 14), + ) ) - return {"entry": entry, "segments": segments, "sections": sections, "symbols": symbols} + return entry, segments, sections, symbols -def unique_section(elf: dict[str, object], name: str) -> dict[str, int | str]: - matches = [section for section in elf["sections"] if section["name"] == name] # type: ignore[index] +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(elf: dict[str, object]) -> list[dict[str, int]]: - segments = elf["segments"] # type: ignore[assignment] - if any(segment["kind"] in (PT_DYNAMIC, PT_INTERP) for segment in segments): +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] + 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[dict[str, int]]) -> None: +def verify_translation(loads: Sequence[Segment]) -> None: for segment in loads: - virtual = segment["virtual"] - physical = segment["physical"] - memory_size = segment["memory_size"] - if virtual >= SEA_PHYS: - raise BoneError(f"S13 absolute physical VMA survived: 0x{virtual:08x}") + 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 + memory_size > SEA_BYTES or physical + memory_size > SEA_END: - raise BoneError("S13 segment exceeds local or physical domain") + 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]]: - elf = parse_elf(data) - if elf["entry"] != 0: - raise BoneError(f"S13 entry is not local zero: 0x{int(elf['entry']):08x}") + 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 elf["sections"]: # type: ignore[index] - name = str(section["name"]) - if name in FORBIDDEN_SECTIONS: - raise BoneError(f"S13 ELF contains forbidden section {name}") - if int(section["flags"]) & SHF_ALLOC and name not in allowed: - raise BoneError(f"S13 ELF contains unowned alloc section {name}") - - code = unique_section(elf, ".sea_code") + 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 int(code["size"]) == 0 - or int(code["size"]) > CODE_BYTES_MAX + 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 = int(code["size"]) + code_bytes = code.size for name, virtual, _physical, size, _flags, has_file in REGIONS: - section = unique_section(elf, name) - if int(section["address"]) != virtual: + 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 int(section["size"]) != code_bytes: + 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 int(section["size"]) != size: + elif section.kind != SHT_NOBITS or section.size != size: raise BoneError(f"S13 NOLOAD section geometry drift: {name}") - undefined = [ - symbol - for symbol in elf["symbols"] # type: ignore[index] - if int(symbol["section_index"]) == 0 and str(symbol["name"]) - ] + undefined = [symbol for symbol in symbols if symbol.section_index == 0 and symbol.name] if undefined: - names = ", ".join(str(symbol["name"]) for symbol in undefined) + names = ", ".join(symbol.name for symbol in undefined) raise BoneError(f"S13 ELF retains undefined symbols: {names}") - starts = [ - symbol - for symbol in elf["symbols"] # type: ignore[index] - if symbol["name"] == "_start" and int(symbol["section_index"]) != 0 - ] - if len(starts) != 1 or int(starts[0]["value"]) != 0: + 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(elf) + 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] + 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 + 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: + if segment.file_size == 0 or segment.file_size > expected_size: raise BoneError("S13 code-segment file-size drift") - elif segment["file_size"] != 0: + 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"]) + 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") @@ -475,11 +494,23 @@ def verify_image(data: bytes) -> tuple[bytes, dict[str, int | str]]: def require_adversaries(data: bytes) -> None: - elf = parse_elf(data) - loads = load_segments(elf) - - vma_adversary = [dict(segment) for segment in loads] - vma_adversary[0]["virtual"] = SEA_PHYS + _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: @@ -487,8 +518,19 @@ def require_adversaries(data: bytes) -> None: else: raise BoneError("S13 absolute-VMA adversary was accepted") - lma_adversary = [dict(segment) for segment in loads] - lma_adversary[0]["physical"] += 512 + 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: @@ -524,20 +566,20 @@ def prove(args: argparse.Namespace) -> None: compile_rlib("bone_sea", ROOT / "tools/bone-sea/src/lib.rs", bone_sea, ROOT) compile_rlib("shinesea", shinesea / "src/lib.rs", shine, shinesea) - first = temporary / "bone-sea-s13-a.elf" - second = temporary / "bone-sea-s13-b.elf" - compile_image(shinesea, linker, bone_sea, shine, first) - compile_image(shinesea, linker, bone_sea, shine, second) + 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) - first_data = first.read_bytes() - second_data = second.read_bytes() + 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") - - first_flat, first_metrics = verify_image(first_data) 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 @@ -581,7 +623,15 @@ def main(argv: Sequence[str] | None = None) -> int: try: prove(args) return 0 - except (BoneError, OSError, ValueError, struct.error, subprocess.SubprocessError) as error: + except ( + BoneError, + IndexError, + OSError, + UnicodeError, + ValueError, + struct.error, + subprocess.SubprocessError, + ) as error: print(f"BONE/SEA S13 ERROR: {error}", file=sys.stderr) return 1 From 0213d2368da7c49555e62555b17496a91cea6f2b Mon Sep 17 00:00:00 2001 From: DEADBYTE Date: Wed, 5 Aug 2026 06:56:43 +0700 Subject: [PATCH 9/9] align the S13 native gate with the corrected adversaries --- tools/bone-sea/src/bin/bone-sea-s13.rs | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/tools/bone-sea/src/bin/bone-sea-s13.rs b/tools/bone-sea/src/bin/bone-sea-s13.rs index ae42266..91dbcfd 100644 --- a/tools/bone-sea/src/bin/bone-sea-s13.rs +++ b/tools/bone-sea/src/bin/bone-sea-s13.rs @@ -255,8 +255,10 @@ mod tests { #[test] fn deterministic_and_adversarial_gates_are_frozen() { assert!(PROOF_TEXT.contains("first_data != second_data")); - assert!(PROOF_TEXT.contains("vma_adversary[0][\"virtual\"] = SEA_PHYS")); - assert!(PROOF_TEXT.contains("lma_adversary[0][\"physical\"] += 512")); + 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]