allaun/SilverSight
1
0
Fork 0
mirror of https://github.com/allaunthefox/SilverSight.git synced 2026-07-31 01:25:21 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

feat(core): add Phase 1 SilverSight core modules

Browse source 
New modules in formal/SilverSight/:
- Schema.lean: Schema class with 6 type instances
- WireFormat.lean: WireFormat structure + Layout enum
- ProductSchema.lean: Schema (α × β) instance
- ProductWireFormat.lean: Row-major pair encoders
- Receipt.lean: Receipt structure + GateType enum
- Bind.lean: bindReceipt composition primitive

Build: 3307 jobs, 0 errors (from Research Stack lake build SilverSight)
All modules use Semantics.FixedPoint cross-project import.
This commit is contained in:
allaun 2026-06-22 21:48:15 -05:00
parent 7327775e16
commit 4f7c554981
7 changed files with 492 additions and 355 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

399
AGENTS.md
View file

@ -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:
```
<type>(<scope>): <summary>
<body — what changed and why>
Build: <N> 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 <branch>
git rev-list --left-right --count FETCH_HEAD...HEAD
git push -u github <branch>
git ls-remote --heads github <branch>
```
---
## 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: <path, commit, concept, or artifact>
Recover Legacy Information: <path, commit, concept, or artifact>
recover from cornfield: <path, commit, concept, or artifact>
```
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 |

114
formal/SilverSight/Bind.lean Normal file
View file

@ -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

48
formal/SilverSight/ProductSchema.lean Normal file
View file

@ -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

67
formal/SilverSight/ProductWireFormat.lean Normal file
View file

@ -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

77
formal/SilverSight/Receipt.lean Normal file
View file

@ -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

68
formal/SilverSight/Schema.lean Normal file
View file

@ -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

74
formal/SilverSight/WireFormat.lean Normal file
View file

@ -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