Publish indexed evidence memory and current LLVM measurements

.github/workflows/ci.yml

@@ -16,13 +16,20 @@ jobs:
       matrix:
         os: [ubuntu-latest, macos-15]
     runs-on: ${{ matrix.os }}
+    env:
+      EGGSHELL_PREFIX: ${{ github.workspace }}/.lake/ci-runtime
     steps:
       - uses: actions/checkout@v5
+      - uses: actions/setup-python@v6
+        with:
+          python-version: "3.12"
       - uses: leanprover/lean-action@v1
         with:
           auto-config: false
       - name: Build
         run: lake build eggshell eggshell_tests lifecycle_tests eggshell_package setup_package_tests
+      - name: Prepare numerical runtime and model
+        run: .lake/build/bin/eggshell install runtime
       - name: Test
         run: EGGSHELL_DATA_ROOT="$PWD/.lake/eggshell-tests-data" .lake/build/bin/eggshell_tests
       - name: Hook lifecycle regressions

.github/workflows/plugin-package.yml

@@ -21,25 +21,41 @@ jobs:
           - os: macos-15-intel
             target: macos-x86_64
     runs-on: ${{ matrix.os }}
+    env:
+      EGGSHELL_PREFIX: ${{ github.workspace }}/.lake/ci-runtime
     steps:
       - uses: actions/checkout@v5
+      - uses: actions/setup-python@v6
+        with:
+          python-version: "3.12"
       - uses: leanprover/lean-action@v1
         with:
           auto-config: false
       - name: Build and test
         run: |
           lake build eggshell eggshell_tests lifecycle_tests eggshell_package setup_package_tests
+          .lake/build/bin/eggshell install runtime
           EGGSHELL_DATA_ROOT="$PWD/.lake/eggshell-tests-data" .lake/build/bin/eggshell_tests
           .lake/build/bin/lifecycle_tests
           .lake/build/bin/setup_package_tests
       - name: Package runtime
+        shell: bash
         run: |
+          set -euo pipefail
           mkdir -p dist
-          tar -czf "dist/eggshell-${{ matrix.target }}.tar.gz" -C .lake/build/bin eggshell
+          archive="dist/eggshell-${{ matrix.target }}.tar.gz"
+          tar -czf "$archive" -C .lake/build/bin eggshell
+          if command -v shasum >/dev/null 2>&1; then
+            shasum -a 256 "$archive" | awk '{print $1}' > "$archive.sha256"
+          else
+            sha256sum "$archive" | awk '{print $1}' > "$archive.sha256"
+          fi
       - uses: actions/upload-artifact@v4
         with:
           name: runtime-${{ matrix.target }}
-          path: dist/*.tar.gz
+          path: |
+            dist/*.tar.gz
+            dist/*.sha256
           retention-days: 7
   bundle:
     needs: runtime
@@ -61,13 +77,17 @@ jobs:
           lake build eggshell_package
           version="$(.lake/build/bin/eggshell_package --version)"
           .lake/build/bin/eggshell_package --runtime-dir dist/runtimes --output dist/publish --release "v$version"
-      - name: Publish pinned runtime assets and plugin ZIP
+      - name: Publish tested runtimes, checksums and plugin together
         env:
           GH_TOKEN: ${{ github.token }}
         run: |
+          set -euo pipefail
           version="$(.lake/build/bin/eggshell_package --version)"
           gh release view "v$version" --repo "$GITHUB_REPOSITORY"
-          gh release upload "v$version" dist/publish/*.tar.gz dist/publish/eggshell-codex-plugin.zip --clobber --repo "$GITHUB_REPOSITORY"
+          gh release upload "v$version" \
+            dist/runtimes/*.tar.gz dist/runtimes/*.sha256 \
+            dist/publish/*.tar.gz dist/publish/eggshell-codex-plugin.zip dist/publish/runtime.json \
+            --clobber --repo "$GITHUB_REPOSITORY"
       - uses: actions/upload-artifact@v4
         with:
           name: eggshell-directory-package

.github/workflows/release.yml

@@ -47,14 +47,20 @@ jobs:
           - os: macos-15-intel
             target: macos-x86_64
     runs-on: ${{ matrix.os }}
+    env:
+      EGGSHELL_PREFIX: ${{ github.workspace }}/.lake/ci-runtime
     steps:
       - uses: actions/checkout@v5
+      - uses: actions/setup-python@v6
+        with:
+          python-version: "3.12"
       - uses: leanprover/lean-action@v1
         with:
           auto-config: false
       - name: Build and test
         run: |
           lake build eggshell eggshell_tests lifecycle_tests eggshell_package setup_package_tests
+          .lake/build/bin/eggshell install runtime
           EGGSHELL_DATA_ROOT="$PWD/.lake/eggshell-tests-data" .lake/build/bin/eggshell_tests
           .lake/build/bin/lifecycle_tests
           .lake/build/bin/setup_package_tests

CONTRIBUTING.md

@@ -45,8 +45,10 @@ runtime checksums, ZIP readability, and deterministic packaging.
 The manually dispatched **Plugin package** workflow builds and tests all four
 platform runtimes, then runs the Lean `eggshell_package` executable. It publishes a small
 `eggshell-codex-plugin.zip` and runtime archives whose names include their content
-hashes on the release matching the plugin version. Existing standalone release
-archives and the release tag are preserved. The ZIP pins the exact runtime
+hashes on the release matching the plugin version. The same tested archives also
+replace the standalone downloads and their SHA-256 files; `runtime.json` records
+the source commit and archive checksums. The version and release tag stay unchanged.
+The ZIP pins the exact runtime
 URLs and SHA-256 values; hooks never download dependencies.
 
 A package build is separate from OpenAI directory submission and approval.

Eggshell/AdvisoryFrontier.lean

@@ -0,0 +1,69 @@
+module
+
+public import Eggshell.PluginModel
+
+@[expose] public section
+
+namespace Eggshell.Plugin
+open Lean
+
+/-- Stable DB identity and its append-only root insertion frontier. This is
+publication metadata, never a claim that an omitted body was delivered. -/
+structure AdvisoryFrontier where
+  identity : String
+  nextRoot : Nat
+  deriving ToJson, FromJson, BEq
+
+/-- A position checked against the exact pinned source that supplies it. -/
+structure AdvisoryPosition where
+  frontier : AdvisoryFrontier
+  ordinal : Nat
+  published : ordinal < frontier.nextRoot
+
+def advisoryFrontierKey (question : String) (frontier : AdvisoryFrontier) : String :=
+  "a:" ++ (toJson (question, frontier)).compress
+
+def acceptedAdvisoryFrontier (question identity : String) (receipts : List String) : Option Nat :=
+  (receipts.filterMap fun receipt => do
+    if !receipt.startsWith "a:" then none else do
+      let json ← (Json.parse (receipt.drop 2).toString).toOption
+      let (recorded, frontier) ← (fromJson? json : Except String (String × AdvisoryFrontier)).toOption
+      if recorded == question && frontier.identity == identity then some frontier.nextRoot else none).head?
+
+/-- Reranking is not a new request. After the first accepted packet, old
+advisory owners stay closed. New publications, another question/source and
+independently grounded native operations remain eligible. -/
+def advisoryPositionAllowed (accepted : Option Nat) (ordinal : Nat) : Bool :=
+  accepted.all (fun limit => decide (limit ≤ ordinal))
+
+theorem old_advisory_position_closed (ordinal limit : Nat) (old : ordinal < limit) :
+    advisoryPositionAllowed (some limit) ordinal = false := by
+  simp [advisoryPositionAllowed, Nat.not_le.mpr old]
+
+theorem new_advisory_position_retained (ordinal limit : Nat) (fresh : limit ≤ ordinal) :
+    advisoryPositionAllowed (some limit) ordinal = true := by
+  simp [advisoryPositionAllowed, fresh]
+
+theorem unaccepted_advisory_position_retained (ordinal : Nat) :
+    advisoryPositionAllowed none ordinal = true := rfl
+
+def advisoryOwnerAllowed (question : String) (receipts : List String)
+    (positions : List AdvisoryPosition) : Bool :=
+  positions.isEmpty || positions.any (fun position => advisoryPositionAllowed
+    (acceptedAdvisoryFrontier question position.frontier.identity receipts) position.ordinal)
+
+def advisoryTransportAllowed (grounded : Bool) (excluded : List Value) (owner : Value) : Bool :=
+  grounded || !excluded.contains owner
+
+theorem grounded_transport_retained (excluded : List Value) (owner : Value) :
+    advisoryTransportAllowed true excluded owner = true := by
+  simp [advisoryTransportAllowed]
+
+theorem excluded_advisory_transport_closed (excluded : List Value) (owner : Value)
+    (present : excluded.contains owner = true) :
+    advisoryTransportAllowed false excluded owner = false := by
+  unfold advisoryTransportAllowed
+  rw [present]
+  rfl
+
+end Eggshell.Plugin