mirror of
https://github.com/allaunthefox/Research-Stack.git
synced 2026-08-12 00:00:35 +00:00
allaun
b6ab3e5f22
SilverSight modules moved from Semantics/Semantics/SilverSight/ to SilverSight/SilverSight/ (separate directory, same lake project). Changes: - SilverSight Lean modules: Schema, WireFormat, ProductSchema, ProductWireFormat, Receipt, Bind → 0-Core-Formalism/lean/SilverSight/ - Imports updated: Semantics.SilverSight.* → SilverSight.* - Namespace updated: Semantics.SilverSight → SilverSight - Cross-project imports preserved: Semantics.FixedPoint, open Semantics.FixedPoint - lakefile.toml: SilverSight lean_lib now uses srcDir = ../SilverSight - AGENTS.md: READ-ONLY notice added — Research Stack is archived, all new formal work goes to SilverSight - SilverSight/AGENTS.md: clean-slate operating contract Build: SilverSight 3307 jobs, 0 errors Build: Compiler 3314 jobs, 0 errors
77 lines
4.7 KiB
Text
77 lines
4.7 KiB
Text
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
|