Hugging Face's logo

Snapkitty
/
sovereign-forge

snapkitty
formal-verification
c
lean4
Model card Files
xet
 Community
sovereign-forge / spec /type-rules.md
SNAPKITTYWEST's picture
SNAPKITTYWEST
Sync with GitHub, license metadata from LICENSE files, commercial license notice
4cba1a6 verified
preview code
|
Raw History Blame Contribute Delete
6.05 kB

Sovereign Stack Machine: Type Rules (Formal)

Version: 1.0.0

Judgment Forms 

Ξ“ ⊒ p ↓ (Ο„, O, Ξ“')

where:
  Ξ“ = input stack type
  p = program (instruction sequence)
  Ο„ = type of computed value (if any)
  O = generated obligations
  Ξ“' = output stack type

Forward Type Inference (Deterministic) 

Algorithm: infer(p: List Instr, Ξ“β‚€: StackType) β†’ (Ξ“_out: StackType, O: List Obligation) βˆͺ Error

Base Case: Empty program

Ξ“ ⊒ [] ↓ (unit, [], Ξ“)

Inductive Step:

Ξ“ ⊒ i ↓ (Ο„, O_i, Ξ“')    Ξ“' ⊒ p ↓ (Ο„', O_p, Ξ“'')
β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”
  Ξ“ ⊒ (i :: p) ↓ (Ο„', O_i ++ O_p, Ξ“'')

Individual Instruction Rules

Push x 

Ξ“ ⊒ Push x ↓ (int64_t, [], Scalar :: Ξ“)

Dup 

h ∈ Ξ“    Ξ“ = h :: t
β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”
Ξ“ ⊒ Dup ↓ (unit, [], h :: h :: t)

Error: Stack empty

Swap 

Ξ“ = h₁ :: hβ‚‚ :: t
β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”
Ξ“ ⊒ Swap ↓ (unit, [], hβ‚‚ :: h₁ :: t)

Error: Fewer than 2 elements

Add 

Case 1: Scalar + Scalar
Ξ“ = Scalar :: Scalar :: t
β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”
Ξ“ ⊒ Add ↓ (unit, [AddBounds], Scalar :: t)

Case 2: Vec n + Vec n
Ξ“ = Vec n :: Vec n :: t
β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”
Ξ“ ⊒ Add ↓ (unit, [VecAddBounds n], Vec n :: t)

Case 3: Mat m n + Mat m n
Ξ“ = Mat m n :: Mat m n :: t
β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”
Ξ“ ⊒ Add ↓ (unit, [MatAddBounds m n], Mat m n :: t)

Error: Shape mismatch

MatPush m n 

β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”
Ξ“ ⊒ MatPush m n ↓ (unit, [], Mat m n :: Ξ“)

MatFill 

Ξ“ = Mat m n :: Scalar :: ... :: Scalar :: t    (m*n scalars)
β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”
Ξ“ ⊒ MatFill ↓ (unit, [MatFillBounds m n], Mat m n :: t)

Error: Insufficient scalars, or shape mismatch

MatMul 

Ξ“ = Mat m n :: Mat n k :: t
β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”
Ξ“ ⊒ MatMul ↓ (unit, [MatMulShape m n k, MatMulBounds m n k], Mat m k :: t)

Obligations:

  • MatMulShape m n k: Assert n values match (compile-time, runtime check)
  • MatMulBounds m n k: No overflow in any element

Error: Shape mismatch

MatTrans 

Ξ“ = Mat m n :: t
β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”
Ξ“ ⊒ MatTrans ↓ (unit, [], Mat n m :: t)

MatAug 

Ξ“ = Mat m nβ‚‚ :: Mat m n₁ :: t
β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”
Ξ“ ⊒ MatAug ↓ (unit, [MatAugShape m n₁ nβ‚‚], Mat m (n₁ + nβ‚‚) :: t)

Error: Row mismatch

Inv 

Ξ“ = Proof("Invertible") :: Mat n n :: t
β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”
Ξ“ ⊒ Inv ↓ (unit, [InvBounds n], Mat n n :: t)

Obligation: InvBounds n β€” check no overflow in Gauss-Jordan steps

Error: Non-square, or missing proof

Solve 

Ξ“ = Proof("Invertible") :: Mat n 1 :: Mat n n :: t
β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”
Ξ“ ⊒ Solve ↓ (unit, [SolveBounds n], Mat n 1 :: t)

Lstsq 

Ξ“ = Proof("FullColumnRank") :: Mat m 1 :: Mat m n :: t    (m β‰₯ n)
β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”
Ξ“ ⊒ Lstsq ↓ (unit, [LstsqBounds m n], Mat n 1 :: t)

VerifyInv 

Ξ“ = Mat n n :: Mat n n :: t
β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”
Ξ“ ⊒ VerifyInv ↓ (unit, [VerifyInvObligation n], Proof("InvOK") :: t)

Obligation: VerifyInvObligation n β€” verify A*X == I

VerifySol 

Ξ“ = Mat n 1 :: Mat n n :: Mat n 1 :: t
β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”
Ξ“ ⊒ VerifySol ↓ (unit, [VerifySolObligation n], Proof("SolOK") :: t)

VerifyLstsq 

Ξ“ = Mat n 1 :: Mat m n :: Mat m 1 :: t    (m β‰₯ n)
β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”
Ξ“ ⊒ VerifyLstsq ↓ (unit, [VerifyLstsqObligation m n], Proof("LstsqOK") :: t)

Unification Algorithm

For symbolic dimensions in branching code (not in core ISA):

unify(τ₁: ValType, Ο„β‚‚: ValType) β†’ (Substitution βˆͺ Conflict)

Base cases:
  unify(Scalar, Scalar) = {}
  unify(Vec n₁, Vec nβ‚‚) = if n₁ == nβ‚‚ then {} else Conflict("Vec dimension mismatch")
  unify(Mat m₁ n₁, Mat mβ‚‚ nβ‚‚) = if m₁==mβ‚‚ && n₁==nβ‚‚ then {} else Conflict(...)
  unify(τ₁, Ο„β‚‚) when τ₁ β‰  Ο„β‚‚ = Conflict("Type mismatch")

Apply substitution:

apply(Οƒ: Substitution, Ξ“: StackType) : StackType

Completeness & Soundness

Completeness: If a program is valid (no underflow, correct shapes), infer succeeds and produces Ξ“'.

Soundness: If infer(p, Ξ“) succeeds with (Ξ“', O), then execution of p starting with stack type Ξ“ produces stack type Ξ“' and only generates obligations in O.

Proof: By induction on program length and instruction structure. Each instruction rule preserves type safety and obligation correctness.

END TYPE RULES