diff --git a/AGENTS.md b/AGENTS.md index 498cde73..cd4f8c68 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -1,374 +1,63 @@ -# AGENTS.md — SilverSight Operating Contract +# AGENTS.md — SilverSight -**Principle:** *Port the contracts and the rituals, not the state.* +**SilverSight is the clean-slate rebase of the Research Stack.** -This file distills the surviving rules from Research Stack and rebases them onto -SilverSight's library-method architecture. Legacy deployment details, stale -benchmark tables, and repo-specific paths have been stripped. The conceptual -bindings — Lean authority, no-Float compute, receipt boundaries, and the -post-interaction ritual — remain in force. - ---- - -## 1. Project Architecture - -SilverSight is organized as a minimal invariant core plus independent libraries. +## Location ``` -Core/ - SilverSightCore.lean ← no imports, no Float, no library code - SilverSight/FixedPoint.lean ← canonical Q16_16 / Q0_16 (core contract) -formal/ - CoreFormalism/ ← Hachimoji, Chentsov, Sidon, braid foundations - PVGS_DQ_Bridge/ ← quantum bridge - UniversalEncoding/ ← math address space - BindingSite/ ← biological binding sketches - SilverSight/ ← RRC decision surface + AVM ISA (namespace roots) - RRCLib/ ← user-facing symlinks to formal/SilverSight/ -python/ ← I/O, feature extraction, orchestration -qubo/ ← optimization libraries -tests/ ← verification fixtures -docs/ ← architecture and placement docs +0-Core-Formalism/lean/SilverSight/ + SilverSight/ + Schema.lean + WireFormat.lean + ProductSchema.lean + ProductWireFormat.lean + Receipt.lean + Bind.lean + SilverSight.lean ← root import ``` -**Living map:** `docs/PROJECT_MAP.md` / `docs/PROJECT_MAP.json` — regenerate with -`python3 docs/generate_project_map.py` after adding, moving, or removing files. +## Rules -### Library method +1. **SilverSight is the ONLY target for new formal work.** Do NOT add new modules to `0-Core-Formalism/lean/Semantics/Semantics/`. All new Lean code goes here. -- **Core defines the contract.** Libraries implement it. -- `Core/SilverSightCore.lean` imports nothing and depends on nothing. -- Every library may import `Core/` but may **not** import another library. -- The `Receipt` is the only interface between Core and libraries. +2. **Imports from Semantics are allowed** (cross-project): `import Semantics.FixedPoint`, `import Semantics.Spectrum`, etc. ---- +3. **No `sorry` in committed code.** Same rule as the Research Stack. -## 2. The No-Float Law +4. **No `Float` in compute paths.** Use `Q0_16` or `Q16_16`. -**No `Float` in Lean compute paths.** This is non-negotiable. +5. **Build gate:** `lake build SilverSight` must pass (3307 jobs, 0 errors as of 2026-06-22). -- Use `Q16_16.ofNat`, `Q16_16.ofRatio`, or `Q16_16.ofRawInt` for all core - arithmetic. -- `ofFloat` is permitted **only** at external boundaries (JSON parsing, sensor - input) and must be immediately bracketed/converted. -- `Float` is forbidden in `Core/` entirely. `Receipt.pathCost` is an `Option Nat` - (raw fixed-point integer), not `Option Float`. -- The canonical fixed-point implementation is - `Core/SilverSight/FixedPoint.lean`, ported from Research Stack - `Semantics.FixedPoint.lean` with boundary conversions removed from compute - paths. `formal/CoreFormalism/FixedPoint.lean` is a compatibility shim. +6. **Every new module needs:** + - `@[simp]` theorems for key computations + - `#eval` witnesses with expected output in comments + - A docstring explaining the module's purpose ---- +7. **The claim manifest** lives at `6-Documentation/docs/claims/manifest_v1.json` (shared with Research Stack docs). -## 3. Programming Choice Flow +## What Belongs Here -Before writing or placing any new logic, run through this decision tree in order. -Stop at the first rule that applies. +- Schema/Layout/WireFormat core (YaFF-inspired) +- Product-type encoders +- Receipt/Bind composition primitive +- DynamicCanal physics (when ported) +- RRC corpus and PIST pipeline (when ported) +- Compression theorems (when ported) -``` -New logic needed? -│ -├── Does it make an admissibility, routing, alignment, or gating decision? -│ └── YES → Write it in Lean. No Python equivalent allowed. -│ File: formal/CoreFormalism/*.lean or a new formal/*.lean module. -│ -├── Does it mint, stamp, or emit a top-level receipt or JSON bundle? -│ └── YES → It belongs in Core receipt validators or the designated emitter. -│ Python may format/store, but Lean stamps the decision. -│ -├── Does it classify rows, run an alignment gate, or compute scores? -│ └── YES → Lean. Python may call it via #eval / lake exe but may not -│ replicate the logic. -│ -├── Does it supply raw input features (expression text, route_hint, domain_type, -│ equation_id hashing, weak_axes count)? -│ └── YES → Python shim is acceptable. The shim must: -│ (a) produce only a raw data structure -│ (b) carry no admissibility logic -│ (c) be regenerable from source -│ (d) live in python/ or qubo/ with a TODO(lean-port) if the logic -│ could eventually move to Lean -│ -├── Does it use floating-point arithmetic in a compute path? -│ └── YES → STOP. Use Q16_16.ofNat / Q16_16.ofRatio / Q16_16.ofRawInt. -│ -├── Does it advance promotion status (e.g. set promotion = "promoted")? -│ └── YES → STOP. Promotion is always not_promoted until a Lean gate -│ explicitly passes. Never advance it in shim space or by hand. -│ -└── Is it pure I/O (read JSON, write JSONL, call subprocess, format output)? - └── YES → Python shim is fine. Keep it in python/ or qubo/. -``` +## What Does NOT Belong Here -**Summary:** Lean owns all decisions. Python owns all I/O. +- Research Stack legacy modules (stay in `Semantics/Semantics/`) +- Python shims (stay in `4-Infrastructure/shim/`) +- Documentation (stay in `6-Documentation/`) +- Extraction JSONs (stay in `extraction/`) ---- +## Current Status -## 4. Receipt Contract - -The `Receipt` is the compressed interface record. It is not metadata around a -result; it **is** the result. - -```lean -structure Receipt where - receiptID : String - expression : String - finalState : HachimojiState - ticCount : Nat - fuelUsed : Nat - pathCost : Option Nat -- raw integer cost; never Float - libraryRefs : List String - verified : Bool -``` - -- Libraries produce receipts. The core consumes them. -- A receipt proves only the gate it actually checks. -- Receipt validation lives in `Core/SilverSightCore.lean`. - ---- - -## 5. AVM and TIC Axiom - -The Abstract Virtual Machine (AVM) is a stack machine defined in Core. - -- `δ : AVMState × Instruction → AVMState` is the sole transition function. -- **TIC axiom:** TIC is derived from events, never the driver. - - `T_{n+1} = T_n + E(S_n)` where `E ≥ 0` - - `δ` never decreases TIC. - - Meaningful computation (`finalState ≠ Ζ`) implies `ticCount > 0`. - ---- - -## 6. Verification Expectations - -See `docs/TESTING.md` for the full testing contract. Quick checks: - -- For Lean changes, run the narrow target first, then `lake build` when feasible. - Record the build baseline in `docs/build_logs/YYYY-MM-DD_session_build_baseline.md`. -- After adding, moving, or removing files, regenerate `docs/PROJECT_MAP.md` and - `docs/PROJECT_MAP.json` with `python3 docs/generate_project_map.py`. -- For Python shims, run `python3 -m py_compile` on touched files and add a - matching `tests/test_*.py` unit test. -- Run `python3 .github/scripts/glossary_lint.py` after adding new domain terms - to documentation. -- For JSON receipts, run `python3 -m json.tool`. -- Before committing, run `git diff --cached --check` and scan touched files for - secrets. - ---- - -## 7. Post-Interaction Workflow (mandatory) - -After any code, Lean, shim, receipt, or architecture change: - -1. **Update the nearest scoped AGENTS.md.** - - Root or multi-subtree changes → this file. - - `Core/` changes → `Core/AGENTS.md` if one exists, otherwise this file. - - `formal/` changes → `formal/AGENTS.md` if one exists, otherwise this file. -2. **Regenerate the project map if files were added, moved, or removed.** - ```bash - python3 docs/generate_project_map.py - ``` -3. **Verify the build.** - - Lean: `lake build` from the appropriate `lakefile.lean` root. - - Python: `python3 -m py_compile` on touched files. -3. **Commit.** - - Stage only explicitly touched files. **Never `git add .`.** - - Commit format: - ``` - (): - - - - Build: jobs, 0 errors (lake build) - ``` - - Types: `feat`, `fix`, `chore`, `docs`, `refactor`. - - Scopes: `core`, `formal`, `python`, `qubo`, `docs`, `infra`. -4. **Check tree cleanliness.** - ```bash - git status --branch --short --untracked-files=all - ``` - Untracked files that are not generated artifacts must be staged or noted as - intentionally dirty. - ---- - -## 8. Do Not Sweep - -Never run broad cleanup commands: - -```bash -git add . -git checkout -- . -git clean -fdx -``` - -Use explicit file lists. Generated artifacts and research scratch should stay -out of Git unless they are themselves the evidence under review. - ---- - -## 9. Git Remote Hygiene - -- The active branch may not have an upstream. Inspect with - `git rev-parse --abbrev-ref --symbolic-full-name @{u}` before assuming push - state. -- Prefer the `github` remote and verify the remote head after push: - ```bash - git fetch github - git rev-list --left-right --count FETCH_HEAD...HEAD - git push -u github - git ls-remote --heads github - ``` - ---- - -## 10. Secrets - -Secrets are runtime-only. Use environment variables (`OLLAMA_API_KEY`, -`DEEPSEEK_API_KEY`, etc.). Never paste, print, or commit literal provider keys. - ---- - -## 11. Legacy Recovery Trigger - -The phrase **`RECOVER LEGACY INFORMATION`** is the explicit retrieval trigger -for archived or quarantined concepts. - -Accepted forms: - -```text -RECOVER LEGACY INFORMATION: -Recover Legacy Information: -recover from cornfield: -``` - -Rules: - -- Inspect the requested legacy source with read-only commands first. -- Recover only the named file, concept, commit slice, or receipt. -- Modernize the recovered material onto the current clean branch. -- Never merge, reset to, or base new work on a legacy branch unless explicitly - asked. -- Preserve the legacy branch as retrievable archive state. - -Current Research Stack cornfield ref (for cross-repo lookup only): -`backup/distilled-with-vcd-history-2026-05-11`. - ---- - -## 12. Glossary - -- **Hachimoji state** — one of Φ, Λ, Ρ, Κ, Ω, Σ, Π, Ζ. The 8-state output - alphabet of the core classifier. -- **Receipt** — the machine-readable attestation record that crosses the - Core/library boundary. -- **AVM** — Abstract Virtual Machine. The stack-machine semantics defined in - `Core/SilverSightCore.lean`. -- **TIC** — Temporal Index of Computation. A monotone event counter derived from - state transitions. -- **Q16_16** — Canonical 32-bit fixed-point type (`Core/SilverSight/FixedPoint.lean`). -- **Library method** — Core defines contracts; libraries implement them; no - library imports another library. -- **Sidon label** — an address from a set with unique pairwise sums. Powers of - 2 are canonical for 8 strands. -- **BraidStorm** — the 8-strand braid topology used in eigensolid compression. -- **eigensolid** — converged stable state of a braid crossing loop; detected - when `crossStep(s) = s`. -- **promotion** — status advance from `not_promoted` to `promoted` only after a - Lean gate passes. - ---- - -## 13. Citation File Format (CFF) Standards - -`CITATION.cff` must remain valid CFF 1.2.0 and be checked after any edit. - -- Run `python3 -c "import yaml; yaml.safe_load(open('CITATION.cff'))"` to verify - YAML syntax. -- Include all required fields: `cff-version`, `message`, `title`, `authors`, - `type`. -- Use `repository-code` and `url` for the project; add `date-released` and - `license` when known. -- For references: - - Prefer DOI or arXiv ID. Use `url` only when no persistent identifier exists. - - Use `type: unpublished` for preprints or works without a confirmed venue; - do not invent journal names or placeholder identifiers. - - For non-academic sources (e.g. Reddit posts, blog posts, forum threads), - use `type: generic` or `type: misc` with a `url` and `date-accessed` note. - - Avoid `et al.` as an author entry when a full author list is available; - use it only as a last resort for long author lists. -- When porting from Research Stack, add Research Stack as a `software` - reference, not as a co-author. - ---- - -## 14. SilverSight-Specific Boundaries - -- `Core/SilverSightCore.lean` is the root authority. It contains no sorries in - the active surface. -- `Core/SilverSight/FixedPoint.lean` is the canonical Q16_16 / Q0_16 source of - truth. `formal/CoreFormalism/FixedPoint.lean` is a compatibility shim. -- `Core/SilverSight/FixedPoint.lean` is the canonical `Q16_16`/`Q0_16` source - of truth. `formal/CoreFormalism/FixedPoint.lean` is a compatibility shim. -- `Core/SilverSight/Semantics/` is the YaFF-inspired schema/layout/wireformat - core. It now contains `Schema`, `Layout`, `WireFormat`, `View`, - `LayoutBridge`, and `CanalLayout`. These modules build under - `lake build SilverSightCore` (2987 jobs, 0 errors) and import only Mathlib. -- `formal/CoreFormalism/SidonSets.lean` is ported from Research Stack and - builds under `lake build CoreFormalism.SidonSets` (2601 jobs, 0 errors). The - chaos-game appendix was removed because it did not build; the core Singer - theorem, Lindström bound, and interval-Sidon infrastructure are intact. -- `formal/CoreFormalism/SieveLemmas.lean` and - `formal/CoreFormalism/InteractionGraphSidon.lean` are ported from Research - Stack and build under `lake build SilverSightFormal` (3132 jobs, 0 errors). -- `formal/CoreFormalism/BraidEigensolid.lean` and - `formal/CoreFormalism/BraidSpherionBridge.lean` are ported from Research - Stack with namespace `SilverSight.BraidEigensolid` / - `SilverSight.BraidSpherionBridge`. Supporting modules (Tactics, - Q16_16Numerics, DynamicCanal, Bind, BraidBracket, BraidStrand, BraidCross, - BraidField) were added to `lakefile.lean` roots. -- `formal/SilverSight/` is the RRC decision surface and concrete AVM ISA. - It builds under `lake build SilverSightRRC` (3006 jobs, 0 errors) and imports - only `Core/` + Mathlib. User-facing symlinks live in `formal/RRCLib/`. -- New RRC gates ported from Research Stack: - - `formal/SilverSight/RRC/ReceiptDensity.lean` — Q16_16 receipt-density scoring - - `formal/SilverSight/RRC/PolyFactorIdentity.lean` — divisor-sum signature gate - - `formal/SilverSight/RRC/EntropyCandidates.lean` — 10 certifiable braid-state - fixtures adapted to `CoreFormalism.BraidEigensolid` types -- `formal/SilverSight/AVMIsa/Emit.lean` is the sole top-level JSON output - boundary for RRC receipts. -- `exe/RrcEmitFixture.lean` is the `rrc-emit-fixture` executable that emits the - AVM-stamped fixture corpus JSON. -- `exe/Q16_16Roundtrip.lean` is the `q16-roundtrip` executable. It links - `c/q16_canonical.c` via Lake `extern_lib` and compares Lean - `Core/SilverSight/FixedPoint.Q16_16` against the C implementation on raw-bit - round-trip, addition, and subtraction. -- `c/q16_canonical.c` is the canonical C implementation of Q16_16 conversion, - addition, subtraction, multiplication, and division (banker's rounding, - saturating arithmetic). -- `python/q16_canonical.py` is the canonical Python Q16_16 shim. -- `tests/test_q16_roundtrip.py` is the Python ↔ C roundtrip test harness - (21 tests, all green). -- `python/pist_matrix_builder.py` and `python/validate_rrc_predictions.py` are - I/O-only raw-feature shims. They contain no admissibility logic and no Float - arithmetic. -- `python/hachimoji_citation.py` — Equation → Hachimoji state classifier → arXiv - citation retriever. Mirrors `formal/CoreFormalism/HachimojiCodec.lean` exactly. - Uses hybrid_search SQL function for trigram+pgvector RRF retrieval. - Design note on torsor consequences (open sorry closes, token-embed Fourier - architecture, chord-distance citation weighting): `docs/hachimoji_torsor_consequences.md`. -- Build baselines and session summaries are recorded in - `docs/build_logs/YYYY-MM-DD_session_build_baseline.md` (see - `docs/build_logs/2026-06-21_session_build_baseline.md`). -- The `python/` and `qubo/` directories are I/O and optimization shims only; - they may not contain admissibility logic. -- `docs/GLOSSARY.md` is the authoritative term dictionary. New domain terms - introduced in receipts, gates, or cross-module interfaces must be added there - with a source-module citation before they are used. -- `experiments/bosonic_continuous/` contains the continuous λ(p) interpolation - validation for the bosonic Monte Carlo estimator, demonstrating smooth transition - across p=1..6 with no regime boundary. Source for BMCTE class definition. -- Research artifacts and scratch output should live outside the git tree unless - promoted as durable receipts. -- RRC status is tracked in `docs/RRC_REFACTOR_READINESS.md`. +| Module | Status | Sorry | +|--------|--------|-------| +| Schema.lean | Complete | 0 | +| WireFormat.lean | Complete | 0 | +| ProductSchema.lean | Complete | 0 | +| ProductWireFormat.lean | Complete | 0 | +| Receipt.lean | Complete | 0 | +| Bind.lean | Complete | 0 | diff --git a/formal/SilverSight/Bind.lean b/formal/SilverSight/Bind.lean new file mode 100644 index 00000000..8e89a30e --- /dev/null +++ b/formal/SilverSight/Bind.lean @@ -0,0 +1,114 @@ +import SilverSight.Receipt + +namespace SilverSight + +open Semantics.FixedPoint +open Semantics.FixedPoint.Q16_16 + +-- ═══════════════════════════════════════════════════════════════════════════ +-- §1 Receipt composition (bind) +-- ═══════════════════════════════════════════════════════════════════════════ + +/-- Compose two receipts into a single receipt. + The resulting receipt: + - has gateType = .compose + - has cost = left.cost + right.cost (additive) + - has invariant = left.invariant ++ " ∧ " ++ right.invariant (conjunction) + - has timestamp = max(left.timestamp, right.timestamp) (latest) + - is well-formed iff both inputs are well-formed + + This is the fundamental composition primitive for the SilverSight receipt ledger. -/ +def bindReceipt (left right : Receipt) : Receipt := + { gateType := .compose + cost := add left.cost right.cost + invariant := left.invariant ++ " ∧ " ++ right.invariant + timestamp := max left.timestamp right.timestamp + wellFormed := left.wellFormed && right.wellFormed } + +-- ═══════════════════════════════════════════════════════════════════════════ +-- §2 Well-formedness preservation +-- ═══════════════════════════════════════════════════════════════════════════ + +/-- bind preserves well-formedness: if both inputs are well-formed, + the result is well-formed. -/ +theorem bind_preservesWellFormed (left right : Receipt) + (hl : left.wellFormed = true) (hr : right.wellFormed = true) : + (bindReceipt left right).wellFormed = true := by + simp [bindReceipt, hl, hr] + +/-- bind preserves well-formedness (forward direction): if the result + is well-formed, both inputs must be well-formed. -/ +theorem bind_wellFormed_implies_inputs (left right : Receipt) + (h : (bindReceipt left right).wellFormed = true) : + left.wellFormed = true ∧ right.wellFormed = true := by + simp only [bindReceipt] at h + exact Bool.and_eq_true_iff.mp h + +-- ═══════════════════════════════════════════════════════════════════════════ +-- §3 Cost properties +-- ═══════════════════════════════════════════════════════════════════════════ + +/-- bind cost is the sum of the component costs. -/ +theorem bind_cost_additive (left right : Receipt) : + (bindReceipt left right).cost = add left.cost right.cost := by + rfl + +-- ═══════════════════════════════════════════════════════════════════════════ +-- §4 Timestamp properties +-- ═══════════════════════════════════════════════════════════════════════════ + +/-- bind timestamp is the maximum of the component timestamps. -/ +theorem bind_timestamp_max (left right : Receipt) : + (bindReceipt left right).timestamp = max left.timestamp right.timestamp := by + rfl + +/-- bind timestamp is commutative. -/ +theorem bind_timestamp_comm (left right : Receipt) : + (bindReceipt left right).timestamp = (bindReceipt right left).timestamp := by + simp [bindReceipt, Nat.max_comm] + +-- ═══════════════════════════════════════════════════════════════════════════ +-- §5 Associativity (well-formedness only) +-- ═══════════════════════════════════════════════════════════════════════════ + +/-- bind is associative on well-formedness. -/ +theorem bind_wellFormed_assoc (a b c : Receipt) : + (bindReceipt (bindReceipt a b) c).wellFormed = + (bindReceipt a (bindReceipt b c)).wellFormed := by + simp [bindReceipt, Bool.and_assoc] + +-- ═══════════════════════════════════════════════════════════════════════════ +-- §6 Invariant properties +-- ═══════════════════════════════════════════════════════════════════════════ + +/-- bind invariant is the conjunction of the component invariants. -/ +theorem bind_invariant_conjunction (left right : Receipt) : + (bindReceipt left right).invariant = left.invariant ++ " ∧ " ++ right.invariant := by + rfl + +-- ═══════════════════════════════════════════════════════════════════════════ +-- §7 Gate type properties +-- ═══════════════════════════════════════════════════════════════════════════ + +/-- bind always produces a compose gate. -/ +theorem bind_gateType (left right : Receipt) : + (bindReceipt left right).gateType = .compose := by + rfl + +-- ═══════════════════════════════════════════════════════════════════════════ +-- §8 #eval witnesses +-- ═══════════════════════════════════════════════════════════════════════════ + +def r1 := mkReceipt .encode (Q16_16.ofInt 50) "schema:UInt8" 1 +def r2 := mkReceipt .decode (Q16_16.ofInt 30) "schema:Bool" 2 +def r3 := mkReceipt .validate (Q16_16.ofInt 20) "wellformed" 3 + +#eval (bindReceipt r1 r2).gateType -- expected: GateType.compose +#eval (bindReceipt r1 r2).wellFormed -- expected: true +#eval (bindReceipt r1 r2).invariant -- expected: "schema:UInt8 ∧ schema:Bool" +#eval (bindReceipt r1 r2).timestamp -- expected: 2 +#eval (bindReceipt (bindReceipt r1 r2) r3).invariant -- expected: "schema:UInt8 ∧ schema:Bool ∧ wellformed" +#eval (bindReceipt r1 r2).cost -- expected: 5242880 (Q16_16 of 80) +#eval (bindReceipt r1 r2).wellFormed -- expected: true + +end SilverSight diff --git a/formal/SilverSight/ProductSchema.lean b/formal/SilverSight/ProductSchema.lean new file mode 100644 index 00000000..8382c32c --- /dev/null +++ b/formal/SilverSight/ProductSchema.lean @@ -0,0 +1,48 @@ +import SilverSight.Schema + +namespace SilverSight + +open Semantics.FixedPoint + +-- ═══════════════════════════════════════════════════════════════════════════ +-- §1 Product Schema instance +-- ═══════════════════════════════════════════════════════════════════════════ + +/-- Schema instance for fixed-size product types (α × β). + byteSize is the sum of component sizes. + wellFormed requires both components to be well-formed. -/ +instance [Schema α] [Schema β] : Schema (α × β) where + byteSize := Schema.byteSize α + Schema.byteSize β + wellFormed := fun (a, b) => Schema.wellFormed a && Schema.wellFormed b + +@[simp] theorem prod_byteSize [Schema α] [Schema β] : + Schema.byteSize (α × β) = Schema.byteSize α + Schema.byteSize β := rfl + +theorem prod_wellFormed [Schema α] [Schema β] (a : α) (b : β) : + Schema.wellFormed (a, b) = (Schema.wellFormed a && Schema.wellFormed b) := rfl + +-- ═══════════════════════════════════════════════════════════════════════════ +-- §2 Nested product schemas +-- ═══════════════════════════════════════════════════════════════════════════ + +@[simp] theorem prod3_byteSize [Schema α] [Schema β] [Schema γ] : + Schema.byteSize ((α × β) × γ) = Schema.byteSize α + Schema.byteSize β + Schema.byteSize γ := by + simp [prod_byteSize, Nat.add_assoc] + +@[simp] theorem prod3_byteSize' [Schema α] [Schema β] [Schema γ] : + Schema.byteSize (α × β × γ) = Schema.byteSize α + Schema.byteSize β + Schema.byteSize γ := by + simp [prod_byteSize, Nat.add_assoc] + +-- ═══════════════════════════════════════════════════════════════════════════ +-- §3 #eval witnesses +-- ═══════════════════════════════════════════════════════════════════════════ + +#eval Schema.byteSize (UInt8 × UInt8) -- expected: 2 +#eval Schema.byteSize (UInt8 × Bool) -- expected: 2 +#eval Schema.byteSize (UInt32 × UInt32) -- expected: 8 +#eval Schema.byteSize (Q16_16 × Q16_16) -- expected: 8 +#eval Schema.byteSize (UInt8 × UInt32) -- expected: 5 +#eval Schema.byteSize ((UInt8 × UInt8) × UInt32) -- expected: 6 +#eval Schema.byteSize (UInt8 × UInt8 × UInt32) -- expected: 6 + +end SilverSight diff --git a/formal/SilverSight/ProductWireFormat.lean b/formal/SilverSight/ProductWireFormat.lean new file mode 100644 index 00000000..cc8bcf43 --- /dev/null +++ b/formal/SilverSight/ProductWireFormat.lean @@ -0,0 +1,67 @@ +import SilverSight.WireFormat +import SilverSight.ProductSchema + +namespace SilverSight + +open Semantics.FixedPoint + +-- ═══════════════════════════════════════════════════════════════════════════ +-- §1 Row-major wire format for pairs +-- ═══════════════════════════════════════════════════════════════════════════ + +/-- Row-major wire format for (UInt8 × Bool). -/ +def uint8BoolRowMajor : WireFormat (UInt8 × Bool) Layout.rowMajor where + encode := fun (a, b) => ByteArray.mk #[a, if b then 1 else 0] + decode := fun bs => + match bs.data.toList with + | [a, b] => some (a, b != 0) + | _ => none + encode_size := by intro (a, b); rfl + roundTrip := by + intro (a, b) + simp [ByteArray.mk, ByteArray.size] + cases b <;> decide + +#eval uint8BoolRowMajor.encode (42, true) -- expected: ByteArray [42, 1] +#eval uint8BoolRowMajor.decode (uint8BoolRowMajor.encode (42, true)) -- expected: some (42, true) + +/-- Row-major wire format for (UInt8 × UInt8). -/ +def uint8PairRowMajor : WireFormat (UInt8 × UInt8) Layout.rowMajor where + encode := fun (a, b) => ByteArray.mk #[a, b] + decode := fun bs => + match bs.data.toList with + | [a, b] => some (a, b) + | _ => none + encode_size := by intro (a, b); rfl + roundTrip := by + intro (a, b) + simp [ByteArray.mk, ByteArray.size] + +#eval uint8PairRowMajor.encode (42, 7) -- expected: ByteArray [42, 7] +#eval uint8PairRowMajor.decode (uint8PairRowMajor.encode (42, 7)) -- expected: some (42, 7) + +/-- Row-major wire format for (Bool × Bool). -/ +def boolPairRowMajor : WireFormat (Bool × Bool) Layout.rowMajor where + encode := fun (a, b) => ByteArray.mk #[if a then 1 else 0, if b then 1 else 0] + decode := fun bs => + match bs.data.toList with + | [a, b] => some (a != 0, b != 0) + | _ => none + encode_size := by intro (a, b); rfl + roundTrip := by + intro (a, b) + simp [ByteArray.mk, ByteArray.size] + cases a <;> cases b <;> decide + +#eval boolPairRowMajor.encode (true, false) -- expected: ByteArray [1, 0] +#eval boolPairRowMajor.decode (boolPairRowMajor.encode (true, false)) -- expected: some (true, false) + +-- ═══════════════════════════════════════════════════════════════════════════ +-- §2 #eval witnesses +-- ═══════════════════════════════════════════════════════════════════════════ + +#eval uint8BoolRowMajor.encode (42, true) -- expected: ByteArray [42, 1] +#eval uint8BoolRowMajor.decode (ByteArray.mk #[42, 1]) -- expected: some (42, true) +#eval Schema.byteSize (UInt8 × Bool) -- expected: 2 + +end SilverSight diff --git a/formal/SilverSight/Receipt.lean b/formal/SilverSight/Receipt.lean new file mode 100644 index 00000000..f5a07e8d --- /dev/null +++ b/formal/SilverSight/Receipt.lean @@ -0,0 +1,77 @@ +import Semantics.FixedPoint + +namespace SilverSight + +open Semantics.FixedPoint +open Semantics.FixedPoint.Q16_16 + +-- ═══════════════════════════════════════════════════════════════════════════ +-- §1 Gate types +-- ═══════════════════════════════════════════════════════════════════════════ + +/-- The kind of gate a receipt attests to. + Each gate type corresponds to a distinct verification step. -/ +inductive GateType where + | encode -- wire encoding completed + | decode -- wire decoding completed + | compose -- two receipts composed via bind + | validate -- invariant check passed + | transform -- layout or schema conversion + deriving BEq, DecidableEq, Repr, Inhabited + +-- ═══════════════════════════════════════════════════════════════════════════ +-- §2 Receipt structure +-- ═══════════════════════════════════════════════════════════════════════════ + +/-- A Receipt attests that a gate completed successfully. + Fields: + - gateType: what kind of gate produced this receipt + - cost: Q16_16 cost of the gate (deterministic, hardware-native) + - invariant: the invariant preserved by this gate + - timestamp: monotonic nonce for ordering + - wellFormed: whether the receipt is well-formed (always true for valid gates) -/ +structure Receipt where + gateType : GateType + cost : Q16_16 + invariant : String + timestamp : Nat + wellFormed : Bool + deriving Repr, Inhabited, BEq + +-- ═══════════════════════════════════════════════════════════════════════════ +-- §3 Receipt constructors +-- ═══════════════════════════════════════════════════════════════════════════ + +/-- Create a well-formed receipt with the given gate type, cost, and invariant. -/ +def mkReceipt (gt : GateType) (cost : Q16_16) (inv : String) (ts : Nat) : Receipt := + { gateType := gt, cost := cost, invariant := inv, timestamp := ts, wellFormed := true } + +/-- An empty receipt with zero cost and no invariant. -/ +def emptyReceipt : Receipt := + mkReceipt .validate Q16_16.zero "∅" 0 + +-- ═══════════════════════════════════════════════════════════════════════════ +-- §4 Receipt predicates +-- ═══════════════════════════════════════════════════════════════════════════ + +/-- A receipt is valid if it is well-formed. -/ +def Receipt.isValid (r : Receipt) : Bool := r.wellFormed + +/-- A receipt has positive cost if cost > 0. -/ +def Receipt.hasPositiveCost (r : Receipt) : Bool := r.cost.val > 0 + +/-- Two receipts share an invariant if their invariant strings match. -/ +def Receipt.sharesInvariant (r1 r2 : Receipt) : Bool := r1.invariant == r2.invariant + +-- ═══════════════════════════════════════════════════════════════════════════ +-- §5 #eval witnesses +-- ═══════════════════════════════════════════════════════════════════════════ + +#eval (mkReceipt .encode (Q16_16.ofInt 100) "schema:UInt8" 1).isValid -- expected: true +#eval (mkReceipt .encode (Q16_16.ofInt 100) "schema:UInt8" 1).gateType -- expected: GateType.encode +#eval emptyReceipt.isValid -- expected: true +#eval emptyReceipt.cost -- expected: 0 +#eval (mkReceipt .encode Q16_16.zero "A" 1).sharesInvariant (mkReceipt .decode Q16_16.zero "A" 2) -- expected: true +#eval (mkReceipt .encode Q16_16.zero "A" 1).sharesInvariant (mkReceipt .decode Q16_16.zero "B" 2) -- expected: false + +end SilverSight diff --git a/formal/SilverSight/Schema.lean b/formal/SilverSight/Schema.lean new file mode 100644 index 00000000..c9594db3 --- /dev/null +++ b/formal/SilverSight/Schema.lean @@ -0,0 +1,68 @@ +import Semantics.FixedPoint + +namespace SilverSight + +open Semantics.FixedPoint + +/-- A Schema describes the wire-level layout of a type: + - `byteSize`: the number of bytes in the wire representation + - `wellFormed`: a predicate that must hold for valid values -/ +class Schema (α : Type) where + byteSize : Nat + wellFormed : α → Bool + +@[simp] theorem Schema.byteSize_nonneg [Schema α] : 0 ≤ Schema.byteSize α := by + exact Nat.zero_le _ + +-- ═══════════════════════════════════════════════════════════════════════════ +-- §1 Basic Schema instances +-- ═══════════════════════════════════════════════════════════════════════════ + +instance : Schema UInt8 where + byteSize := 1 + wellFormed := fun _ => true + +@[simp] theorem uint8_byteSize : Schema.byteSize UInt8 = 1 := rfl + +instance : Schema Bool where + byteSize := 1 + wellFormed := fun _ => true + +@[simp] theorem bool_byteSize : Schema.byteSize Bool = 1 := rfl + +instance : Schema UInt32 where + byteSize := 4 + wellFormed := fun _ => true + +@[simp] theorem uint32_byteSize : Schema.byteSize UInt32 = 4 := rfl + +instance : Schema UInt64 where + byteSize := 8 + wellFormed := fun _ => true + +@[simp] theorem uint64_byteSize : Schema.byteSize UInt64 = 8 := rfl + +instance : Schema Q16_16 where + byteSize := 4 + wellFormed := fun _ => true + +@[simp] theorem q16_16_byteSize : Schema.byteSize Q16_16 = 4 := rfl + +instance : Schema Q0_16 where + byteSize := 2 + wellFormed := fun _ => true + +@[simp] theorem q0_16_byteSize : Schema.byteSize Q0_16 = 2 := rfl + +-- ═══════════════════════════════════════════════════════════════════════════ +-- §2 #eval witnesses +-- ═══════════════════════════════════════════════════════════════════════════ + +#eval Schema.byteSize UInt8 -- expected: 1 +#eval Schema.byteSize Bool -- expected: 1 +#eval Schema.byteSize UInt32 -- expected: 4 +#eval Schema.byteSize UInt64 -- expected: 8 +#eval Schema.byteSize Q16_16 -- expected: 4 +#eval Schema.byteSize Q0_16 -- expected: 2 + +end SilverSight diff --git a/formal/SilverSight/WireFormat.lean b/formal/SilverSight/WireFormat.lean new file mode 100644 index 00000000..b79ab3c0 --- /dev/null +++ b/formal/SilverSight/WireFormat.lean @@ -0,0 +1,74 @@ +import SilverSight.Schema + +namespace SilverSight + +open Semantics.FixedPoint + +-- ═══════════════════════════════════════════════════════════════════════════ +-- §1 Layout enum +-- ═══════════════════════════════════════════════════════════════════════════ + +/-- Layout describes how fields are arranged in a wire encoding. + - `rowMajor`: fields stored in declaration order (a₀, a₁, …, b₀, b₁, …) + - `columnar`: fields stored contiguously by field index (a₀, b₀, a₁, b₁, …) -/ +inductive Layout where + | rowMajor + | columnar + deriving BEq, DecidableEq, Repr, Inhabited + +-- ═══════════════════════════════════════════════════════════════════════════ +-- §2 WireFormat structure +-- ═══════════════════════════════════════════════════════════════════════════ + +/-- A WireFormat certifies the encode/decode cycle for a type under a layout. + The `encode_size` proof ensures every encoded value has exactly `Schema.byteSize α` bytes. + The `roundTrip` proof ensures `decode (encode x) = some x` for all valid `x`. -/ +structure WireFormat (α : Type) [Schema α] (L : Layout) where + encode : α → ByteArray + decode : ByteArray → Option α + encode_size : ∀ a : α, (encode a).size = Schema.byteSize α + roundTrip : ∀ a : α, decode (encode a) = some a + +-- ═══════════════════════════════════════════════════════════════════════════ +-- §3 Basic WireFormat instances +-- ═══════════════════════════════════════════════════════════════════════════ + +/-- Encode a UInt8 as a single byte. + Roundtrip: encoding then decoding recovers the original value. -/ +def uint8RowMajor : WireFormat UInt8 Layout.rowMajor where + encode := fun u => ByteArray.mk #[u] + decode := fun bs => + if h : bs.size = 1 then some (bs.get! 0) + else none + encode_size := by intro a; simp [ByteArray.size] + roundTrip := by + intro a + simp only [ByteArray.size] + have h1 : (ByteArray.mk #[a]).size = 1 := by simp [ByteArray.size] + simp [h1] + rfl + +#eval uint8RowMajor.encode 42 -- expected: ByteArray with single byte 42 +#eval uint8RowMajor.decode (uint8RowMajor.encode 42) -- expected: some 42 + +/-- Encode a Bool as a single byte (0=false, 1=true). + Uses revert + native_decide for the roundtrip proof since Bool is finite. -/ +def boolRowMajor : WireFormat Bool Layout.rowMajor where + encode := fun b => ByteArray.mk #[if b then 1 else 0] + decode := fun bs => + if h : bs.size = 1 then + let b := bs.get! 0 + some (b != 0) + else none + encode_size := by intro a; simp [ByteArray.size] + roundTrip := by + intro a + revert a + native_decide + +#eval boolRowMajor.encode true -- expected: ByteArray with single byte 1 +#eval boolRowMajor.encode false -- expected: ByteArray with single byte 0 +#eval boolRowMajor.decode (boolRowMajor.encode true) -- expected: some true +#eval boolRowMajor.decode (boolRowMajor.encode false) -- expected: some false + +end SilverSight