Move retrieval and integrations to Lean with checked contracts

.github/workflows/adapters.yml

@@ -0,0 +1,38 @@
+name: Adapter contracts
+
+on:
+  push:
+    branches: [main]
+    paths:
+      - 'adapters/**'
+      - 'Eggshell/**'
+      - 'adapters/native/Tests.lean'
+      - 'tests/test_opencode_adapter.mjs'
+      - '.github/workflows/adapters.yml'
+      - 'lean-toolchain'
+      - 'lakefile.lean'
+  pull_request:
+
+permissions:
+  contents: read
+
+jobs:
+  adapters:
+    strategy:
+      fail-fast: false
+      matrix:
+        os: [ubuntu-latest, macos-15]
+    runs-on: ${{ matrix.os }}
+    steps:
+      - uses: actions/checkout@v5
+      - uses: leanprover/lean-action@v1
+        with:
+          auto-config: false
+      - name: Build independent adapter companion
+        working-directory: adapters/native
+        run: lake build eggshell_bridge adapter_tests
+      - name: Engine integration contracts
+        working-directory: adapters/native
+        run: .lake/build/bin/adapter_tests
+      - name: OpenCode output contracts
+        run: node --test tests/test_opencode_adapter.mjs

.github/workflows/ci.yml

@@ -22,16 +22,17 @@ jobs:
         with:
           auto-config: false
       - name: Build
-        run: lake build eggshell eggshell_tests
+        run: lake build eggshell eggshell_tests lifecycle_tests eggshell_package setup_package_tests
       - name: Test
         run: EGGSHELL_DATA_ROOT="$PWD/.lake/eggshell-tests-data" .lake/build/bin/eggshell_tests
       - name: Hook lifecycle regressions
-        run: python3 tests/test_hook_lifecycle.py -v
+        run: .lake/build/bin/lifecycle_tests
       - name: Check plugin package
-        run: python3 tests/test_plugin_package.py
+        run: .lake/build/bin/setup_package_tests
       - name: Check installer syntax
         run: |
           sh -n install.sh
           sh -n plugins/eggshell/bin/egg
+          sh -n plugins/eggshell/scripts/setup.sh
       - name: Check two-chat sample
         run: python3 -m unittest discover -s examples/two-chats -v

.github/workflows/plugin-package.yml

@@ -28,10 +28,10 @@ jobs:
           auto-config: false
       - name: Build and test
         run: |
-          lake build eggshell eggshell_tests
+          lake build eggshell eggshell_tests lifecycle_tests eggshell_package setup_package_tests
           EGGSHELL_DATA_ROOT="$PWD/.lake/eggshell-tests-data" .lake/build/bin/eggshell_tests
-          python3 tests/test_hook_lifecycle.py -v
-          python3 tests/test_plugin_package.py
+          .lake/build/bin/lifecycle_tests
+          .lake/build/bin/setup_package_tests
       - name: Package runtime
         run: |
           mkdir -p dist
@@ -48,20 +48,24 @@ jobs:
       contents: write
     steps:
       - uses: actions/checkout@v5
+      - uses: leanprover/lean-action@v1
+        with:
+          auto-config: false
       - uses: actions/download-artifact@v4
         with:
           pattern: runtime-*
           merge-multiple: true
           path: dist/runtimes
       - name: Assemble plugin
         run: |
-          version="$(python3 -c 'import json; print(json.load(open("plugins/eggshell/.codex-plugin/plugin.json"))["version"])')"
-          python3 scripts/package_plugin.py --runtime-dir dist/runtimes --output dist/publish --release "v$version"
+          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
         env:
           GH_TOKEN: ${{ github.token }}
         run: |
-          version="$(python3 -c 'import json; print(json.load(open("plugins/eggshell/.codex-plugin/plugin.json"))["version"])')"
+          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"
       - uses: actions/upload-artifact@v4

.github/workflows/release.yml

@@ -54,10 +54,10 @@ jobs:
           auto-config: false
       - name: Build and test
         run: |
-          lake build eggshell eggshell_tests
+          lake build eggshell eggshell_tests lifecycle_tests eggshell_package setup_package_tests
           EGGSHELL_DATA_ROOT="$PWD/.lake/eggshell-tests-data" .lake/build/bin/eggshell_tests
-          python3 tests/test_hook_lifecycle.py -v
-          python3 tests/test_plugin_package.py
+          .lake/build/bin/lifecycle_tests
+          .lake/build/bin/setup_package_tests
       - name: Package
         shell: bash
         run: |
@@ -84,14 +84,18 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v5
+      - uses: leanprover/lean-action@v1
+        with:
+          auto-config: false
       - uses: actions/download-artifact@v4
         with:
           pattern: release-*
           merge-multiple: true
           path: dist/runtimes
       - name: Assemble plugin from tested runtimes
         run: |
-          python3 scripts/package_plugin.py --runtime-dir dist/runtimes --output dist/publish --release "$GITHUB_REF_NAME"
+          lake build eggshell_package
+          .lake/build/bin/eggshell_package --runtime-dir dist/runtimes --output dist/publish --release "$GITHUB_REF_NAME"
       - name: Publish runtime assets and plugin together
         env:
           GH_TOKEN: ${{ github.token }}

CONTRIBUTING.md

@@ -17,9 +17,9 @@ EGGSHELL_DATA_ROOT="$PWD/.lake/eggshell-tests-data" \
 
 Tests must use an isolated absolute `EGGSHELL_DATA_ROOT`; they refuse the normal
 user data directory. Keep public claims tied to completed, reproducible measurements.
-The shipped local search provider is also exercised with its installed MiniLM
-Python environment: `python tests/test_search_provider.py`. The model must already
-be cached; the test uses offline mode and makes no generative model requests.
+Build `search_tests` and run `.lake/build/bin/search_tests` to exercise the shipped
+local search provider. Its MiniLM numerical runtime and model must already be
+cached; the test uses offline mode and makes no generative model requests.
 For performance work, total tokens mean input plus reasoning output plus final
 output. Quality non-regression and `.egg` growth are constraints; tool count and
 elapsed time are diagnostics.
@@ -37,13 +37,13 @@ private benchmark transcripts.
 launcher. The standalone installer embeds its manifest and hooks in
 `Eggshell/Install.lean`; the existing test enforces that those definitions match.
 
-Run `python3 tests/test_plugin_package.py` after building the executable when
-changing package setup or runtime installation. These checks exercise checksum
-rejection, archive validation, missing-runtime hooks, and preservation of
-existing plugin registration and memory during runtime-only installation.
+Build `eggshell`, `eggshell_package`, and `setup_package_tests`, then run
+`.lake/build/bin/setup_package_tests` when changing setup or packaging.
+These native tests check configuration preservation, read-only inspection,
+runtime checksums, ZIP readability, and deterministic packaging.
 
 The manually dispatched **Plugin package** workflow builds and tests all four
-platform runtimes, then runs `scripts/package_plugin.py`. It publishes a small
+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

Eggshell/ContractAudit.lean

@@ -0,0 +1,31 @@
+module
+
+import Eggshell.SearchRank
+import Eggshell.SearchProvider
+import Eggshell.Setup
+public meta import Lean
+
+open Lean
+
+/- This module is imported by the test executable, not the product executable.
+   Reject admissions and any new axiom outside Lean's standard logical basis. -/
+run_meta do
+  let contracts := #[
+    ``Eggshell.SearchRank.unique_indices,
+    ``Eggshell.SearchRank.selected_no_duplicates,
+    ``Eggshell.SearchRank.selected_within_budget,
+    ``Eggshell.SearchRank.selected_is_existing,
+    ``Eggshell.SearchRank.selected_was_ranked,
+    ``Eggshell.SearchRank.zero_budget_is_empty,
+    ``Eggshell.Setup.configured_is_preserved,
+    ``Eggshell.Setup.check_never_initializes,
+    ``Eggshell.Setup.initialize_only_when_missing,
+    ``Eggshell.SearchProvider.accepted_cache_identity,
+    ``Eggshell.SearchProvider.changed_cache_text_rejected,
+    ``Eggshell.SearchProvider.changed_cache_model_rejected]
+  for contract in contracts do
+    let axioms ← Lean.collectAxioms contract
+    for dependency in axioms do
+      unless #[``propext, ``Quot.sound, ``Classical.choice].contains dependency do
+        throwError "{contract} depends on unapproved axiom {dependency}"
+    logInfo m!"Audited {contract}: {axioms}"

Eggshell/Install.lean

@@ -47,34 +47,44 @@ def initCommand : IO UInt32 := do
 def pluginManifest : String := r##"{
   "name": "eggshell",
   "version": "0.1.0",
-  "description": "Carry useful work across Codex chats with local memory you control",
+  "description": "Local memory that helps AI agents reuse work and spend fewer tokens",
   "author": {
     "name": "momonpya",
     "url": "https://github.com/momonpya"
   },
   "homepage": "https://github.com/momonpya/eggshell",
   "repository": "https://github.com/momonpya/eggshell",
   "license": "Apache-2.0",
-  "keywords": ["codex", "agent-memory", "work-graph", "productivity"],
+  "keywords": [
+    "codex",
+    "agent-memory",
+    "work-graph",
+    "productivity"
+  ],
   "interface": {
     "displayName": "Eggshell",
-    "shortDescription": "Local memory for Codex",
-    "longDescription": "Eggshell saves requests, tool results, and conclusions in local .egg files. Related Codex chats receive selected prior work and instructions to reuse supported findings, check changed facts, and report what remains unverified. Memory is organized locally without additional LLM calls. Requires macOS or Linux, Python 3, and Codex command hooks.",
+    "shortDescription": "Token-saving local memory",
+    "longDescription": "Eggshell helps AI agents reuse prior work and spend fewer tokens. The current integration supports Codex with local command hooks on macOS or Linux.\n\nRequests, tool results, and conclusions stay in local .egg files. Related chats receive selected findings and instructions to check changed facts and report what remains unverified. Memory organization and retrieval run locally without generative LLM calls. Ordinary task and handoff tokens still count toward model usage. There is no hosted memory service or telemetry.\n\nAfter installing, ask Codex: Set up Eggshell for this project. Setup downloads a checksummed runtime, Python dependencies, and a search model, then initializes missing project settings while preserving existing configuration. Review and enable the hooks in /hooks and start a new chat. Installation alone does not activate memory.\n\nA startup notice identifies missing setup or confirms that the session hook ran. Use !egg doctor to check configuration without changing settings. Complete an investigation and a related follow-up in a separate chat, then use !egg graph to inspect the memory actually delivered. Once configured and enabled, saving and relevant handoffs happen automatically.\n\nThis integration does not provide automatic memory in ordinary ChatGPT Chat. Other agent harnesses are not yet supported. Use !egg off to disable memory; !egg drop clears the active turn but retains saved observations and queued commits.",
     "developerName": "momonpya",
     "category": "Productivity",
     "capabilities": [],
     "websiteURL": "https://github.com/momonpya/eggshell",
     "brandColor": "#6B6256",
     "defaultPrompt": [
-      "Continue this task from relevant prior work without repeating completed investigation."
+      "Set up Eggshell for this project.",
+      "Check whether Eggshell memory is working in this project.",
+      "Show what Eggshell handed to this task and why it was selected."
     ]
   }
 }"##
 
 def hooksManifest : String := r#"{
   "description": "Record native results and deliver relevant prior work.",
   "hooks": {
-    "SessionStart": [{"hooks": [{"type": "command", "command": "\"${PLUGIN_ROOT}/bin/egg\" codex-hook", "timeout": 30}]}],
+    "SessionStart": [
+      {"matcher": "^(startup|resume|clear)$", "hooks": [{"type": "command", "command": "\"${PLUGIN_ROOT}/bin/egg\" codex-start", "timeout": 30}]},
+      {"matcher": "^compact$", "hooks": [{"type": "command", "command": "\"${PLUGIN_ROOT}/bin/egg\" codex-hook", "timeout": 30}]}
+    ],
     "UserPromptSubmit": [{"hooks": [{"type": "command", "command": "\"${PLUGIN_ROOT}/bin/egg\" codex-hook", "additionalContextLimit": 48000, "timeout": 30}]}],
     "PreToolUse": [{"hooks": [{"type": "command", "command": "\"${PLUGIN_ROOT}/bin/egg\" codex-hook", "additionalContextLimit": 48000, "timeout": 30}]}],
     "PostToolUse": [{"hooks": [{"type": "command", "command": "\"${PLUGIN_ROOT}/bin/egg\" codex-hook", "additionalContextLimit": 48000, "timeout": 30}]}],
@@ -122,6 +132,7 @@ def pluginLauncher (root : System.FilePath) : String :=
   "#!/bin/sh\nset -eu\nEGGSHELL_PREFIX=" ++ shellQuote root.toString ++ r#"
 export EGGSHELL_PREFIX
 case "${1-}" in
+  codex-start) exec "$EGGSHELL_PREFIX/libexec/eggshell" codex-hook ;;
   codex-hook|codex-daemon|codex-worker|codex-rpc) exec "$EGGSHELL_PREFIX/libexec/eggshell" "$@" ;;
   *) exec "$EGGSHELL_PREFIX/libexec/eggshell" egg "$@" ;;
 esac