File size: 5,997 Bytes
9425aed | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 | -- Sovereign Event Bus (SEB) - Kernel Interface
-- Ada 2012 / SPARK Level 4
--
-- This file defines the verified kernel interface with all L0 invariants
-- encoded as preconditions and postconditions.
--
-- Invariants:
-- 1. Plasma Gate: Ed25519 signature valid
-- 2. Hash Chain: Prev_Hash == current tip hash
-- 3. Offset Monotonic: Event offset > prior offset
-- 4. Payload Hash: blake3(header || payload) matches footer.event_hash
-- 5. Segment Chain: Prev_Seg_Hash links to prior segment
pragma SPARK_Mode (On);
with SEB_Types;
use SEB_Types;
package SEB_Kernel is
-- Kernel Abstract State (SPARK Global_Input/Output)
type Kernel_Handle is private;
-- Initialization
procedure Initialize_Kernel
(Handle : out Kernel_Handle;
Initial_Segment_Id : Unsigned_64;
Initial_Segment_Sequence : Unsigned_64)
with Global => null;
-- Core Operation: Append Event
--
-- Preconditions (Level 4 verification):
-- 1. signature_valid: Ed25519.Verify(event.footer.signature, event.footer.event_hash)
-- 2. hash_chain_valid: event.footer.prev_hash == current_state.tip_hash
-- 3. offset_monotonic: event.header.prev_offset < proposed_offset
-- 4. payload_hash_valid: blake3(header || payload) == event.footer.event_hash
--
-- Postconditions:
-- 1. current_tip_hash == event.footer.event_hash
-- 2. current_tip_offset == new_offset
-- 3. event is WORM-sealed (msync called)
-- 4. events_sealed count incremented
procedure Append_Event
(Handle : in out Kernel_Handle;
Header : Event_Header;
Payload : Unsigned_8_Array;
Footer : Event_Footer;
Committed_Offset : out Segment_Offset)
with Global => null,
Pre => (
Is_Valid_Header (Header) and
Payload'Length = Natural (Header.Payload_Size) and
Payload'Length <= Natural (Payload_Max_Size)
),
Post => (
Committed_Offset >= Min_Offset and
Committed_Offset <= Max_Offset
);
-- Signature Verification (Plasma Gate)
--
-- Verifies Ed25519 signature on event hash.
-- Postcondition: result = Valid iff signature is correct
function Verify_Signature
(Hash : Hash_Type;
Signature : Signature_Type;
Public_Key : Public_Key_Type)
return Verification_Status
with Global => null,
Post => (
Verify_Signature'Result = Valid or
Verify_Signature'Result = Invalid_Signature
);
-- Hash Verification (Hash Chain Validation)
--
-- Verifies BLAKE3 hash of event data.
-- Postcondition: result = Valid iff hash matches expected
function Verify_Hash
(Header : Event_Header;
Payload : Unsigned_8_Array;
Expected_Hash : Hash_Type)
return Verification_Status
with Global => null,
Pre => Payload'Length = Natural (Header.Payload_Size),
Post => (
Verify_Hash'Result = Valid or
Verify_Hash'Result = Invalid_Hash
);
-- Chain Validation (History Integrity)
--
-- Verifies entire event chain from tip to genesis.
-- Returns status and number of events validated.
procedure Verify_Chain
(Handle : Kernel_Handle;
Valid : out Boolean;
Events_Checked : out Unsigned_64)
with Global => null,
Post => (
Valid = False or
Events_Checked > 0
);
-- Segment Rotation (WORM Boundary)
--
-- Rotates to new segment when current segment is full.
-- Creates segment chain link via prev_seg_hash.
--
-- Preconditions:
-- 1. current_segment_size + new_event_size > Segment_Size
-- 2. new_segment_sequence > current_segment_sequence
--
-- Postconditions:
-- 1. new segment created with unique ID
-- 2. prev_seg_hash == hash(prior segment)
-- 3. segment_sequence incremented
-- 4. offset reset to 0 in new segment
procedure Rotate_Segment
(Handle : in out Kernel_Handle;
New_Segment_Id : Unsigned_64;
New_Segment_Sequence : Unsigned_64;
Segment_Rotation_Offset : out Segment_Offset)
with Global => null,
Pre => New_Segment_Sequence > 0,
Post => Segment_Rotation_Offset = 0;
-- Query Operations
function Get_Current_Segment_Id (Handle : Kernel_Handle) return Unsigned_64
with Global => null;
function Get_Current_Sequence (Handle : Kernel_Handle) return Unsigned_64
with Global => null;
function Get_Current_Tip_Hash (Handle : Kernel_Handle) return Hash_Type
with Global => null;
function Get_Current_Tip_Offset (Handle : Kernel_Handle) return Segment_Offset
with Global => null;
function Get_Events_Sealed_Count (Handle : Kernel_Handle) return Unsigned_64
with Global => null;
function Get_Segments_Rotated_Count (Handle : Kernel_Handle) return Unsigned_64
with Global => null;
-- Offset Type for Array Bounds
type Unsigned_8_Array is array (Natural range <>) of Unsigned_8;
-- WORM Flush Operation
--
-- Ensures all pending writes are synchronized to persistent storage.
-- (mmap msync equivalent)
--
-- Postcondition: all prior Append_Event calls are durable
procedure WORM_Flush (Handle : in out Kernel_Handle)
with Global => null;
-- Exception Handling
Kernel_Error : exception;
Integrity_Error : exception;
Offset_Overflow : exception;
Segment_Full_Error : exception;
private
type Kernel_Handle is record
Current_Segment_Id : Unsigned_64 := 0;
Current_Sequence : Unsigned_64 := 0;
Tip_Hash : Hash_Type := (others => 0);
Tip_Offset : Segment_Offset := 0;
Events_Sealed : Unsigned_64 := 0;
Segments_Rotated : Unsigned_64 := 0;
end record;
end SEB_Kernel;
|