SilverSight/REBASE_RULES.md
allaun 7a973a06f6 feat(core): harden SilverSightCore and port canonical FixedPoint
- Remove Float from Core/SilverSightCore.lean (Receipt.pathCost is now Option Nat)
- Prove TIC theorems tic_never_decreases and computation_generates_time
- Add lakefile.lean, lean-toolchain, and .gitignore for .lake/
- Port Research-Stack Semantics.FixedPoint.lean to formal/CoreFormalism/FixedPoint.lean
- Delete thin Q16_16_Spec.lean; update Python/QUBO comments and docs
- Create AGENTS.md distilled from Research Stack core bindings
- Update REBASE_RULES.md to strip legacy hacks and reference AGENTS.md

Build: 2978 jobs, 0 errors (lake build)
2026-06-21 06:30:12 -05:00

11 KiB

REBASE RULES — SilverSight Agent / Rules Manifest

Purpose: This file is a rebase seed. When starting a fresh project map, copy only the files and rules listed here. Do not migrate runtime state, stale audits, completed assignment boards, or legacy deployment hacks.

Principle: Port the contracts and the rituals, not the state.

Status: Research Stack contained many legacy hacks (Hermes ports, Headroom proxy endpoints, old benchmark tables, repo-specific paths). Those have been stripped. The core conceptual bindings — Lean authority, no-Float compute, receipt boundaries, programming-choice flow, and the post-interaction ritual — are preserved here and in AGENTS.md.


1. Core Operating Contracts (MUST PORT)

These files are the source of truth for every agent, skill, and editor hook. They are actively maintained and cross-referenced throughout the stack.

File Scope
AGENTS.md (this repo) SilverSight master operating contract. Distilled from Research Stack; strips legacy deployment details and adapts rules to the library-method architecture.
0-Core-Formalism/lean/Semantics/AGENTS.md Lean/Semantics local contract: blessed Compiler surface, build baselines, quarantine boundaries, proof-tactic lessons, current solidification anchors. ADAPT to formal/AGENTS.md in SilverSight.
4-Infrastructure/AGENTS.md Infrastructure and shim contract: storage stack, hardware-witness boundaries, ENE schema, compute dispatch pattern. PORT ONLY IF infrastructure work continues; otherwise drop.
6-Documentation/docs/AGENTS.md Strict LLM operating rules: anti-drift evidence standards, bind primitive, naming conventions, sigma levels, SI units, deletion criteria, PQC policy. ADAPT to docs/AGENTS.md if strict doc rules are needed.
5-Applications/text-to-cad/AGENTS.md CAD harness contract: generated CAD/URDF source-of-truth, viewer handoff, repo policies. PORT ONLY IF CAD work continues.
scripts/qc-flag/AGENTS.md Lean QC protocol: 7-check inspection protocol. ADAPT to tests/qc-flag/AGENTS.md if the protocol is adopted.
shared-data/artifacts/lean_expert_agent/AGENTS.md Lean expert agent /inspect protocol and output format. ADAPT if a formal reviewer agent is wired up.
.github/RRC_OPERATING_CONTRACT.md Rainbow Raccoon Compiler gate definition: ACCEPT / HOLD / QUARANTINE. ADAPT to SilverSight's receipt gate if RRC work continues.

Non-negotiable rules extracted from the contracts

  1. Lean is the source of truth. Python and Verilog are extraction targets only.
  2. Programming choice flow — before writing new logic, check this decision tree in order:
    • Admissibility / routing / alignment / gating decision? → Lean only.
    • Minting/stamping a top-level receipt or JSON bundle? → Lean stamps; Python formats/stores only.
    • Classifying rows / computing alignment scores? → Lean (formal/CoreFormalism/ or a new formal/*.lean module).
    • Supplying raw input features (expression text, IDs, weak_axes)? → Python shim OK, no admissibility logic, regenerable from source.
    • Float arithmetic in a compute path? → STOP. Use Q16_16.ofNat, Q16_16.ofRatio, or Q16_16.ofRawInt.
    • Advancing promotion status in shim space? → STOP. not_promoted until a Lean gate passes.
    • Pure I/O (read/write JSON, subprocess, format output)? → Python shim OK. Receipt output is stamped in Lean and stored by Python.
  3. No Float in Lean compute paths. ofFloat is permitted only at JSON/sensor boundaries and must be immediately bracketed. Float is forbidden in Core/ entirely.
  4. Post-interaction workflow (mandatory after any code/receipt/architecture change):
    • Update the nearest scoped AGENTS.md for every touched subtree.
    • Run the narrow Lean target first, then full lake build if Lean files touched.
    • Commit with an explicit file list; never git add ..
    • Run git status --branch --short --untracked-files=all.
  5. Do Not Sweep: never run git add ., git checkout -- ., or git clean -fdx.
  6. Secrets are runtime-only: use environment variables (OLLAMA_API_KEY, DEEPSEEK_API_KEY, etc.); never commit literal keys.
  7. Legacy recovery is explicit: use RECOVER LEGACY INFORMATION: <path/commit/concept> only. Cross-repo cornfield ref: backup/distilled-with-vcd-history-2026-05-11.

2. Editor / Agent Configs (MUST PORT)

These files inject the contracts into editor/agent runtimes.

File Purpose
.cursorrules Cursor: ContextStream init()/context()/search() rules.
.devin/config.json Devin: programming-choice reminder hook.
.devin/hooks.json Devin: ContextStream hooks.
.devin/hooks/programming-choice-reminder.sh Injects programming-choice flow + post-interaction checklist before every user message.
.claude/settings.json Claude Code: ContextStream hooks.
.cursor/hooks.json Cursor: ContextStream hooks.
.roo/mcp.json Roo: MCP server definitions.
.mcp.json (root) Minimal MCP config: filesystem, git, fetch, contextstream, lean, remote-lean-proof, sympy, wolfram, aws, github, headroom.
.contextstream/config.json ContextStream workspace/project IDs.
.kilo/rules/contextstream.md Kilo Code manual ContextStream rules (no hooks available).
.roo/rules/contextstream.md Roo Code ContextStream rules.
.windsurf/rules/contextstream.md Windsurf ContextStream rules.

ContextStream-first workflow (enforced or self-enforced in every editor)

  • First message: init(folder_path=...)context(user_message=...).
  • Subsequent messages: context(user_message=...) FIRST.
  • Before any file search: search(mode="auto") BEFORE Glob/Grep/Read/Explore/Task/EnterPlanMode.
  • After edits: project(action="index") in editors without auto-indexing.
  • Save transcripts: save_exchange=true in editors without auto-saving.

3. Skills (MUST PORT)

Skill Path Purpose
lean-proof .devin/skills/lean-proof/SKILL.md Mandatory for all Lean work: proof quality, Q16_16 contract, #eval witnesses, promotion gate.
contextstream-workflow .github/skills/contextstream-workflow/SKILL.md Persistent memory: plans, tasks, decisions, lessons.
research-stack-workflow .github/skills/research-stack-workflow/SKILL.md Token-efficient proof workflow; local inference first on neon.
headroom .opencode/skills/headroom/SKILL.md Context compression and cross-agent memory.
cad 5-Applications/text-to-cad/skills/cad/SKILL.md Script-driven STEP/STL/DXF/GLB generation.
urdf 5-Applications/text-to-cad/skills/urdf/SKILL.md URDF generation and validation.
rrc-compile .claude/skills/rrc-compile/SKILL.md RRC pipeline orchestrator.
rrc-scale-analysis .claude/skills/rrc-scale-analysis/SKILL.md RRC pre-flight Q16_16 scale-band analysis.

4. MCP Servers (MUST PORT)

From .mcp.json / .roo/mcp.json:

Server Role
contextstream Persistent memory / context / search
filesystem Read/write proof artifacts and receipts
git History, blame, diff
fetch HTTP docs and RFCs
lean Lean 4 / Mathlib typecheck bridge
remote-lean-proof Hermes / OpenCode / Codex proof backend
sympy Symbolic arithmetic verification
wolfram-alpha Formula verification (needs WOLFRAM_APP_ID)
aws AWS API access
github PRs, issues, CI
headroom Token / context compression

5. Conditional Items (PORT ONLY IF DOMAIN REMAINS ACTIVE)

File Condition
.windsurf/lifeguard.yaml Keep only if genetics / GCCL / Mass Number abstraction work continues. Contains safety doctrine for biological-equivalence claims, reverse-collapse, bounded recursion, and claim-state hygiene.
.opencode/agents/*.md Keep only if the target sorry/theorem is still open in the new rebase. These are task-specific subagent prompts.
.claude/workflows/ground-disproved-theorems.js Keep only if Claude Code still uses this workflow.

6. DROP — Do Not Port

Item Reason
.consolidation-manifests/ Historical SHA256 manifests from 2026-05-04. Not load-bearing.
.headroom/*.db Runtime memory databases; regenerate on first use.
.agents/plugins/marketplace.json References a dormant ./plugins/substack-connector. Not load-bearing.
.github/copilot-instructions.md Core rules are valid, but the "Current Project State" block is stale (2026-05-28). Port rules separately, not this file as authority.
.windsurf/SORRY_AUDIT.md Stale audit (2026-05-28). Root AGENTS.md now reports 0 sorries in the active Compiler surface. Archive only.
.windsurf/ASSIGNMENTS.md Dated 2026-04-19; all assignments marked COMPLETE and references old paths. Historical residue.
Staging manifests (stack_solidification_staging_manifest_2026-05-09.md, etc.) Historical archives; referenced but not authoritative.
Cornfield / legacy branches Do not merge or base work on them. Use only via explicit recovery trigger.

7. Minimal Rebase Checklist

Use this when standing up the new project map.

  • Copy all files in Section 1 (Core Operating Contracts).
  • Copy all files in Section 2 (Editor / Agent Configs).
  • Copy all files in Section 3 (Skills).
  • Copy/adapt .mcp.json and .roo/mcp.json with current server paths.
  • Update .contextstream/config.json with new workspace/project IDs if they change.
  • Review Section 5 conditional items and keep only active-domain rules.
  • Verify Section 6 dropped items are not carried over.
  • Run lake build Compiler and confirm job count matches the new baseline.
  • Update build baseline and commit hash in 0-Core-Formalism/lean/Semantics/AGENTS.md.

8. Design Note for the New Map

When designing the new project layout, preserve these boundary rules:

  • Lean owns decisions; Python owns I/O.
  • Core/SilverSightCore.lean is the root authority and imports nothing.
  • The Receipt is the sole Core/library boundary. Lean stamps; libraries format/store.
  • python/ and qubo/ are I/O and optimization shims only. No admissibility logic in shim space.
  • Research artifacts go outside the git tree unless promoted as durable receipts.
  • Every new compression path needs two Lean theorems: eigensolid_convergence and receipt_invertible.
  • No library imports another library. Libraries import Core/ only.

Generated from active Research Stack agent rules and contracts, stripped of legacy hacks. Principle: port contracts and rituals, not state. SilverSight master contract: AGENTS.md.