mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-08-06 10:25:45 +00:00
allaun
8fd4638240
Schema.lean and Receipt.lean now import SilverSight.FixedPoint instead of Semantics.FixedPoint. SilverSight builds standalone. Build: 3307 jobs, 0 errors.
77 lines
4.7 KiB
Text
77 lines
4.7 KiB
Text
import SilverSight.FixedPoint
|
|
|
|
namespace SilverSight
|
|
|
|
open SilverSight.FixedPoint
|
|
open SilverSight.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
|