BONE/SEA S13: relink the SEA image with segment-local VMAs

.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"

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
+  }
+}