| -- BOB Quantum Kernel Error Status (WORM-sealed) |
| -- Phase 2: Loop Invariant Formalization |
| -- Status: Observable error codes tied to WORM logs (bookkeeping only) |
|
|
| module Core.ErrorCode where |
|
|
| open import Data.Nat using (ℕ) |
|
|
| -- Error status codes (copied from bob_errors.f90 enum) |
| data ErrorCode : Set where |
| BOB_SUCCESS : ErrorCode -- 0 (no error) |
| BOB_ERROR_ALLOCATION : ErrorCode -- Memory allocation failure |
| BOB_ERROR_INVALID_STATE : ErrorCode -- Invalid quantum state |
| BOB_ERROR_INVALID_GATE : ErrorCode -- Invalid gate operation |
| BOB_ERROR_NOT_UNITARY : ErrorCode -- Matrix is not unitary |
| BOB_ERROR_INVALID_ARGUMENT : ErrorCode -- Bad argument |
| BOB_ERROR_DIMENSION_MISMATCH : ErrorCode -- Dimension mismatch |
| BOB_ERROR_OTHER : ErrorCode -- Other error |
|
|
| -- Decidable equality for error codes |
| _==ₑ_ : ErrorCode → ErrorCode → Set |
| BOB_SUCCESS ==ₑ BOB_SUCCESS = Set |
| BOB_SUCCESS ==ₑ _ = ⊥ |
| BOB_ERROR_ALLOCATION ==ₑ BOB_ERROR_ALLOCATION = Set |
| BOB_ERROR_ALLOCATION ==ₑ _ = ⊥ |
| BOB_ERROR_INVALID_STATE ==ₑ BOB_ERROR_INVALID_STATE = Set |
| BOB_ERROR_INVALID_STATE ==ₑ _ = ⊥ |
| BOB_ERROR_INVALID_GATE ==ₑ BOB_ERROR_INVALID_GATE = Set |
| BOB_ERROR_INVALID_GATE ==ₑ _ = ⊥ |
| BOB_ERROR_NOT_UNITARY ==ₑ BOB_ERROR_NOT_UNITARY = Set |
| BOB_ERROR_NOT_UNITARY ==ₑ _ = ⊥ |
| BOB_ERROR_INVALID_ARGUMENT ==ₑ BOB_ERROR_INVALID_ARGUMENT = Set |
| BOB_ERROR_INVALID_ARGUMENT ==ₑ _ = ⊥ |
| BOB_ERROR_DIMENSION_MISMATCH ==ₑ BOB_ERROR_DIMENSION_MISMATCH = Set |
| BOB_ERROR_DIMENSION_MISMATCH ==ₑ _ = ⊥ |
| BOB_ERROR_OTHER ==ₑ BOB_ERROR_OTHER = Set |
| BOB_ERROR_OTHER ==ₑ _ = ⊥ |
|
|
| -- Predicate: no error occurred |
| isSuccess : ErrorCode → Set |
| isSuccess BOB_SUCCESS = Set |
| isSuccess _ = ⊥ |
|
|
