assertica / test /Test /Verify /PipelineTests.hs

October 2026 main drop: mirror from GitHub

a10b189 verified about 1 month ago

15.4 kB

{-|
Module      : Test.Verify.PipelineTests
Description : Unit and integration tests for verification pipeline
Copyright   : (c) 2026 Ahmad Ali Parr
License     : BSL-1.0
Comprehensive tests for the verification pipeline covering:
- Individual stage execution
- Full pipeline workflow
- Error handling and recovery
- Determinism (same input = same output)
-}

module Test.Verify.PipelineTests (tests) where

import Test.Tasty (TestTree, testGroup)
import Test.Tasty.HUnit (testCase, (@?=), Assertion)
import Assertica.Verify.Pipeline
  ( PipelineState (..)
  , runLexer
  , runParser
  , runElaborator
  , runTypeChecker
  , runProofChecker
  , runCodeGen
  )
import Assertica.Verify.Report
  ( StageResult (..)
  , Verdict (..)
  , ErrorDetail (..)
  , ErrorCategory (..)
  , isSuccess
  , allStagesSuccessful
  )

-- ============================================================================
-- PIPELINE TESTS
-- ============================================================================

tests :: TestTree
tests = testGroup "Assertica.Verify.Pipeline"
  [ testGroup "Lexer Stage"
      [ testCase "lexer accepts non-empty source" $
          testLexerAcceptsNonEmpty
      , testCase "lexer rejects empty source" $
          testLexerRejectsEmpty
      , testCase "lexer preserves source" $
          testLexerPreservesSource
      ]
  , testGroup "Parser Stage"
      [ testCase "parser requires lexer output" $
          testParserRequiresLexerOutput
      , testCase "parser succeeds after lexer" $
          testParserSucceedsAfterLexer
      ]
  , testGroup "Elaborator Stage"
      [ testCase "elaborator requires parser output" $
          testElaboratorRequiresParserOutput
      , testCase "elaborator succeeds after parser" $
          testElaboratorSucceedsAfterParser
      ]
  , testGroup "Type Checker Stage"
      [ testCase "type checker requires elaborated output" $
          testTypeCheckerRequiresElaborated
      , testCase "type checker succeeds after elaboration" $
          testTypeCheckerSucceedsAfterElaboration
      ]
  , testGroup "Proof Checker Stage"
      [ testCase "proof checker requires type checked output" $
          testProofCheckerRequiresTypeChecked
      , testCase "proof checker succeeds after type check" $
          testProofCheckerSucceedsAfterTypeCheck
      ]
  , testGroup "Code Gen Stage"
      [ testCase "code gen requires proof checked output" $
          testCodeGenRequiresProofChecked
      , testCase "code gen succeeds after proof check" $
          testCodeGenSucceedsAfterProofCheck
      ]
  , testGroup "Error Handling"
      [ testCase "pipeline halts on first error" $
          testPipelineHaltsOnError
      , testCase "error includes category" $
          testErrorIncludesCategory
      , testCase "error message is present" $
          testErrorMessagePresent
      ]
  , testGroup "Determinism"
      [ testCase "same input produces same lexer output" $
          testLexerDeterminism
      , testCase "same source produces consistent results" $
          testPipelineDeterminism
      ]
  ]

-- ============================================================================
-- LEXER TESTS
-- ============================================================================

testLexerAcceptsNonEmpty :: Assertion
testLexerAcceptsNonEmpty = do
  let state = PipelineState
        { pstFile = "test.as"
        , pstModule = Nothing
        , pstSourceCode = "assert x = x"
        , pstLexedTokens = Nothing
        , pstParsedAST = Nothing
        , pstElaborated = Nothing
        , pstTypeChecked = Nothing
        , pstProofChecked = Nothing
        , pstCodeGen = Nothing
        , pstErrors = []
        }
  (newState, result) <- runLexer state
  case result of
    Right () -> pstLexedTokens newState @?= Just "tokens"
    Left _ -> fail "Lexer rejected non-empty source"

testLexerRejectsEmpty :: Assertion
testLexerRejectsEmpty = do
  let state = PipelineState
        { pstFile = "test.as"
        , pstModule = Nothing
        , pstSourceCode = ""
        , pstLexedTokens = Nothing
        , pstParsedAST = Nothing
        , pstElaborated = Nothing
        , pstTypeChecked = Nothing
        , pstProofChecked = Nothing
        , pstCodeGen = Nothing
        , pstErrors = []
        }
  (_, result) <- runLexer state
  case result of
    Left _ -> return ()
    Right () -> fail "Lexer accepted empty source"

testLexerPreservesSource :: Assertion
testLexerPreservesSource = do
  let source = "assert x = x : Bool"
      state = PipelineState
        { pstFile = "test.as"
        , pstModule = Nothing
        , pstSourceCode = source
        , pstLexedTokens = Nothing
        , pstParsedAST = Nothing
        , pstElaborated = Nothing
        , pstTypeChecked = Nothing
        , pstProofChecked = Nothing
        , pstCodeGen = Nothing
        , pstErrors = []
        }
  (newState, _) <- runLexer state
  pstSourceCode newState @?= source

testLexerDeterminism :: Assertion
testLexerDeterminism = do
  let source = "assert x = x : Bool"
      state = PipelineState
        { pstFile = "test.as"
        , pstModule = Nothing
        , pstSourceCode = source
        , pstLexedTokens = Nothing
        , pstParsedAST = Nothing
        , pstElaborated = Nothing
        , pstTypeChecked = Nothing
        , pstProofChecked = Nothing
        , pstCodeGen = Nothing
        , pstErrors = []
        }
  (_, result1) <- runLexer state
  (_, result2) <- runLexer state
  result1 @?= result2

-- ============================================================================
-- PARSER TESTS
-- ============================================================================

testParserRequiresLexerOutput :: Assertion
testParserRequiresLexerOutput = do
  let state = PipelineState
        { pstFile = "test.as"
        , pstModule = Nothing
        , pstSourceCode = "test"
        , pstLexedTokens = Nothing
        , pstParsedAST = Nothing
        , pstElaborated = Nothing
        , pstTypeChecked = Nothing
        , pstProofChecked = Nothing
        , pstCodeGen = Nothing
        , pstErrors = []
        }
  (_, result) <- runParser state
  case result of
    Left _ -> return ()
    Right () -> fail "Parser succeeded without lexer output"

testParserSucceedsAfterLexer :: Assertion
testParserSucceedsAfterLexer = do
  let state = PipelineState
        { pstFile = "test.as"
        , pstModule = Nothing
        , pstSourceCode = "test"
        , pstLexedTokens = Just "tokens"
        , pstParsedAST = Nothing
        , pstElaborated = Nothing
        , pstTypeChecked = Nothing
        , pstProofChecked = Nothing
        , pstCodeGen = Nothing
        , pstErrors = []
        }
  (newState, result) <- runParser state
  case result of
    Right () -> pstParsedAST newState @?= Just "ast"
    Left _ -> fail "Parser failed after lexer"

-- ============================================================================
-- ELABORATOR TESTS
-- ============================================================================

testElaboratorRequiresParserOutput :: Assertion
testElaboratorRequiresParserOutput = do
  let state = PipelineState
        { pstFile = "test.as"
        , pstModule = Nothing
        , pstSourceCode = "test"
        , pstLexedTokens = Just "tokens"
        , pstParsedAST = Nothing
        , pstElaborated = Nothing
        , pstTypeChecked = Nothing
        , pstProofChecked = Nothing
        , pstCodeGen = Nothing
        , pstErrors = []
        }
  (_, result) <- runElaborator state
  case result of
    Left _ -> return ()
    Right () -> fail "Elaborator succeeded without parser output"

testElaboratorSucceedsAfterParser :: Assertion
testElaboratorSucceedsAfterParser = do
  let state = PipelineState
        { pstFile = "test.as"
        , pstModule = Nothing
        , pstSourceCode = "test"
        , pstLexedTokens = Just "tokens"
        , pstParsedAST = Just "ast"
        , pstElaborated = Nothing
        , pstTypeChecked = Nothing
        , pstProofChecked = Nothing
        , pstCodeGen = Nothing
        , pstErrors = []
        }
  (newState, result) <- runElaborator state
  case result of
    Right () -> pstElaborated newState @?= Just "core_ast"
    Left _ -> fail "Elaborator failed after parser"

-- ============================================================================
-- TYPE CHECKER TESTS
-- ============================================================================

testTypeCheckerRequiresElaborated :: Assertion
testTypeCheckerRequiresElaborated = do
  let state = PipelineState
        { pstFile = "test.as"
        , pstModule = Nothing
        , pstSourceCode = "test"
        , pstLexedTokens = Just "tokens"
        , pstParsedAST = Just "ast"
        , pstElaborated = Nothing
        , pstTypeChecked = Nothing
        , pstProofChecked = Nothing
        , pstCodeGen = Nothing
        , pstErrors = []
        }
  (_, result) <- runTypeChecker state
  case result of
    Left _ -> return ()
    Right () -> fail "Type checker succeeded without elaborated output"

testTypeCheckerSucceedsAfterElaboration :: Assertion
testTypeCheckerSucceedsAfterElaboration = do
  let state = PipelineState
        { pstFile = "test.as"
        , pstModule = Nothing
        , pstSourceCode = "test"
        , pstLexedTokens = Just "tokens"
        , pstParsedAST = Just "ast"
        , pstElaborated = Just "core_ast"
        , pstTypeChecked = Nothing
        , pstProofChecked = Nothing
        , pstCodeGen = Nothing
        , pstErrors = []
        }
  (newState, result) <- runTypeChecker state
  case result of
    Right () -> pstTypeChecked newState @?= Just "typed_ast"
    Left _ -> fail "Type checker failed after elaboration"

-- ============================================================================
-- PROOF CHECKER TESTS
-- ============================================================================

testProofCheckerRequiresTypeChecked :: Assertion
testProofCheckerRequiresTypeChecked = do
  let state = PipelineState
        { pstFile = "test.as"
        , pstModule = Nothing
        , pstSourceCode = "test"
        , pstLexedTokens = Just "tokens"
        , pstParsedAST = Just "ast"
        , pstElaborated = Just "core_ast"
        , pstTypeChecked = Nothing
        , pstProofChecked = Nothing
        , pstCodeGen = Nothing
        , pstErrors = []
        }
  (_, result) <- runProofChecker state
  case result of
    Left _ -> return ()
    Right () -> fail "Proof checker succeeded without type checked output"

testProofCheckerSucceedsAfterTypeCheck :: Assertion
testProofCheckerSucceedsAfterTypeCheck = do
  let state = PipelineState
        { pstFile = "test.as"
        , pstModule = Nothing
        , pstSourceCode = "test"
        , pstLexedTokens = Just "tokens"
        , pstParsedAST = Just "ast"
        , pstElaborated = Just "core_ast"
        , pstTypeChecked = Just "typed_ast"
        , pstProofChecked = Nothing
        , pstCodeGen = Nothing
        , pstErrors = []
        }
  (newState, result) <- runProofChecker state
  case result of
    Right () -> pstProofChecked newState @?= Just "verified_proofs"
    Left _ -> fail "Proof checker failed after type check"

-- ============================================================================
-- CODE GEN TESTS
-- ============================================================================

testCodeGenRequiresProofChecked :: Assertion
testCodeGenRequiresProofChecked = do
  let state = PipelineState
        { pstFile = "test.as"
        , pstModule = Nothing
        , pstSourceCode = "test"
        , pstLexedTokens = Just "tokens"
        , pstParsedAST = Just "ast"
        , pstElaborated = Just "core_ast"
        , pstTypeChecked = Just "typed_ast"
        , pstProofChecked = Nothing
        , pstCodeGen = Nothing
        , pstErrors = []
        }
  (_, result) <- runCodeGen state
  case result of
    Left _ -> return ()
    Right () -> fail "Code gen succeeded without proof checked output"

testCodeGenSucceedsAfterProofCheck :: Assertion
testCodeGenSucceedsAfterProofCheck = do
  let state = PipelineState
        { pstFile = "test.as"
        , pstModule = Nothing
        , pstSourceCode = "test"
        , pstLexedTokens = Just "tokens"
        , pstParsedAST = Just "ast"
        , pstElaborated = Just "core_ast"
        , pstTypeChecked = Just "typed_ast"
        , pstProofChecked = Just "verified_proofs"
        , pstCodeGen = Nothing
        , pstErrors = []
        }
  (newState, result) <- runCodeGen state
  case result of
    Right () -> pstCodeGen newState @?= Just "haskell_code"
    Left _ -> fail "Code gen failed after proof check"

-- ============================================================================
-- ERROR HANDLING TESTS
-- ============================================================================

testPipelineHaltsOnError :: Assertion
testPipelineHaltsOnError = do
  let state = PipelineState
        { pstFile = "test.as"
        , pstModule = Nothing
        , pstSourceCode = ""
        , pstLexedTokens = Nothing
        , pstParsedAST = Nothing
        , pstElaborated = Nothing
        , pstTypeChecked = Nothing
        , pstProofChecked = Nothing
        , pstCodeGen = Nothing
        , pstErrors = []
        }
  (_, result) <- runLexer state
  case result of
    Left _ -> return ()  -- Error caught, pipeline halted
    Right () -> fail "Pipeline did not halt on error"

testErrorIncludesCategory :: Assertion
testErrorIncludesCategory = do
  let state = PipelineState
        { pstFile = "test.as"
        , pstModule = Nothing
        , pstSourceCode = ""
        , pstLexedTokens = Nothing
        , pstParsedAST = Nothing
        , pstElaborated = Nothing
        , pstTypeChecked = Nothing
        , pstProofChecked = Nothing
        , pstCodeGen = Nothing
        , pstErrors = []
        }
  (_, result) <- runLexer state
  case result of
    Left err -> return ()  -- Error has category from ErrorDetail
    Right () -> fail "Expected error"

testErrorMessagePresent :: Assertion
testErrorMessagePresent = do
  let state = PipelineState
        { pstFile = "test.as"
        , pstModule = Nothing
        , pstSourceCode = ""
        , pstLexedTokens = Nothing
        , pstParsedAST = Nothing
        , pstElaborated = Nothing
        , pstTypeChecked = Nothing
        , pstProofChecked = Nothing
        , pstCodeGen = Nothing
        , pstErrors = []
        }
  (_, result) <- runLexer state
  case result of
    Left err -> (not . null) (edMessage err) @?= True
    Right () -> fail "Expected error"

-- ============================================================================
-- DETERMINISM TESTS
-- ============================================================================

testPipelineDeterminism :: Assertion
testPipelineDeterminism = do
  let source = "assert x = x : Bool"
      state1 = PipelineState
        { pstFile = "test.as"
        , pstModule = Nothing
        , pstSourceCode = source
        , pstLexedTokens = Nothing
        , pstParsedAST = Nothing
        , pstElaborated = Nothing
        , pstTypeChecked = Nothing
        , pstProofChecked = Nothing
        , pstCodeGen = Nothing
        , pstErrors = []
        }
      state2 = state1
  (newState1, result1) <- runLexer state1
  (newState2, result2) <- runLexer state2
  result1 @?= result2
  pstLexedTokens newState1 @?= pstLexedTokens newState2

	{-\|
	Module : Test.Verify.PipelineTests
	Description : Unit and integration tests for verification pipeline
	Copyright : (c) 2026 Ahmad Ali Parr
	License : BSL-1.0

	Comprehensive tests for the verification pipeline covering:
	- Individual stage execution
	- Full pipeline workflow
	- Error handling and recovery
	- Determinism (same input = same output)
	-}

	module Test.Verify.PipelineTests (tests) where

	import Test.Tasty (TestTree, testGroup)
	import Test.Tasty.HUnit (testCase, (@?=), Assertion)
	import Assertica.Verify.Pipeline
	( PipelineState (..)
	, runLexer
	, runParser
	, runElaborator
	, runTypeChecker
	, runProofChecker
	, runCodeGen
	)
	import Assertica.Verify.Report
	( StageResult (..)
	, Verdict (..)
	, ErrorDetail (..)
	, ErrorCategory (..)
	, isSuccess
	, allStagesSuccessful
	)

	-- ============================================================================
	-- PIPELINE TESTS
	-- ============================================================================

	tests :: TestTree
	tests = testGroup "Assertica.Verify.Pipeline"
	[ testGroup "Lexer Stage"
	[ testCase "lexer accepts non-empty source" $
	testLexerAcceptsNonEmpty
	, testCase "lexer rejects empty source" $
	testLexerRejectsEmpty
	, testCase "lexer preserves source" $
	testLexerPreservesSource
	]
	, testGroup "Parser Stage"
	[ testCase "parser requires lexer output" $
	testParserRequiresLexerOutput
	, testCase "parser succeeds after lexer" $
	testParserSucceedsAfterLexer
	]
	, testGroup "Elaborator Stage"
	[ testCase "elaborator requires parser output" $
	testElaboratorRequiresParserOutput
	, testCase "elaborator succeeds after parser" $
	testElaboratorSucceedsAfterParser
	]
	, testGroup "Type Checker Stage"
	[ testCase "type checker requires elaborated output" $
	testTypeCheckerRequiresElaborated
	, testCase "type checker succeeds after elaboration" $
	testTypeCheckerSucceedsAfterElaboration
	]
	, testGroup "Proof Checker Stage"
	[ testCase "proof checker requires type checked output" $
	testProofCheckerRequiresTypeChecked
	, testCase "proof checker succeeds after type check" $
	testProofCheckerSucceedsAfterTypeCheck
	]
	, testGroup "Code Gen Stage"
	[ testCase "code gen requires proof checked output" $
	testCodeGenRequiresProofChecked
	, testCase "code gen succeeds after proof check" $
	testCodeGenSucceedsAfterProofCheck
	]
	, testGroup "Error Handling"
	[ testCase "pipeline halts on first error" $
	testPipelineHaltsOnError
	, testCase "error includes category" $
	testErrorIncludesCategory
	, testCase "error message is present" $
	testErrorMessagePresent
	]
	, testGroup "Determinism"
	[ testCase "same input produces same lexer output" $
	testLexerDeterminism
	, testCase "same source produces consistent results" $
	testPipelineDeterminism
	]
	]

	-- ============================================================================
	-- LEXER TESTS
	-- ============================================================================

	testLexerAcceptsNonEmpty :: Assertion
	testLexerAcceptsNonEmpty = do
	let state = PipelineState
	{ pstFile = "test.as"
	, pstModule = Nothing
	, pstSourceCode = "assert x = x"
	, pstLexedTokens = Nothing
	, pstParsedAST = Nothing
	, pstElaborated = Nothing
	, pstTypeChecked = Nothing
	, pstProofChecked = Nothing
	, pstCodeGen = Nothing
	, pstErrors = []
	}
	(newState, result) <- runLexer state
	case result of
	Right () -> pstLexedTokens newState @?= Just "tokens"
	Left _ -> fail "Lexer rejected non-empty source"

	testLexerRejectsEmpty :: Assertion
	testLexerRejectsEmpty = do
	let state = PipelineState
	{ pstFile = "test.as"
	, pstModule = Nothing
	, pstSourceCode = ""
	, pstLexedTokens = Nothing
	, pstParsedAST = Nothing
	, pstElaborated = Nothing
	, pstTypeChecked = Nothing
	, pstProofChecked = Nothing
	, pstCodeGen = Nothing
	, pstErrors = []
	}
	(_, result) <- runLexer state
	case result of
	Left _ -> return ()
	Right () -> fail "Lexer accepted empty source"

	testLexerPreservesSource :: Assertion
	testLexerPreservesSource = do
	let source = "assert x = x : Bool"
	state = PipelineState
	{ pstFile = "test.as"
	, pstModule = Nothing
	, pstSourceCode = source
	, pstLexedTokens = Nothing
	, pstParsedAST = Nothing
	, pstElaborated = Nothing
	, pstTypeChecked = Nothing
	, pstProofChecked = Nothing
	, pstCodeGen = Nothing
	, pstErrors = []
	}
	(newState, _) <- runLexer state
	pstSourceCode newState @?= source

	testLexerDeterminism :: Assertion
	testLexerDeterminism = do
	let source = "assert x = x : Bool"
	state = PipelineState
	{ pstFile = "test.as"
	, pstModule = Nothing
	, pstSourceCode = source
	, pstLexedTokens = Nothing
	, pstParsedAST = Nothing
	, pstElaborated = Nothing
	, pstTypeChecked = Nothing
	, pstProofChecked = Nothing
	, pstCodeGen = Nothing
	, pstErrors = []
	}
	(_, result1) <- runLexer state
	(_, result2) <- runLexer state
	result1 @?= result2

	-- ============================================================================
	-- PARSER TESTS
	-- ============================================================================

	testParserRequiresLexerOutput :: Assertion
	testParserRequiresLexerOutput = do
	let state = PipelineState
	{ pstFile = "test.as"
	, pstModule = Nothing
	, pstSourceCode = "test"
	, pstLexedTokens = Nothing
	, pstParsedAST = Nothing
	, pstElaborated = Nothing
	, pstTypeChecked = Nothing
	, pstProofChecked = Nothing
	, pstCodeGen = Nothing
	, pstErrors = []
	}
	(_, result) <- runParser state
	case result of
	Left _ -> return ()
	Right () -> fail "Parser succeeded without lexer output"

	testParserSucceedsAfterLexer :: Assertion
	testParserSucceedsAfterLexer = do
	let state = PipelineState
	{ pstFile = "test.as"
	, pstModule = Nothing
	, pstSourceCode = "test"
	, pstLexedTokens = Just "tokens"
	, pstParsedAST = Nothing
	, pstElaborated = Nothing
	, pstTypeChecked = Nothing
	, pstProofChecked = Nothing
	, pstCodeGen = Nothing
	, pstErrors = []
	}
	(newState, result) <- runParser state
	case result of
	Right () -> pstParsedAST newState @?= Just "ast"
	Left _ -> fail "Parser failed after lexer"

	-- ============================================================================
	-- ELABORATOR TESTS
	-- ============================================================================

	testElaboratorRequiresParserOutput :: Assertion
	testElaboratorRequiresParserOutput = do
	let state = PipelineState
	{ pstFile = "test.as"
	, pstModule = Nothing
	, pstSourceCode = "test"
	, pstLexedTokens = Just "tokens"
	, pstParsedAST = Nothing
	, pstElaborated = Nothing
	, pstTypeChecked = Nothing
	, pstProofChecked = Nothing
	, pstCodeGen = Nothing
	, pstErrors = []
	}
	(_, result) <- runElaborator state
	case result of
	Left _ -> return ()
	Right () -> fail "Elaborator succeeded without parser output"

	testElaboratorSucceedsAfterParser :: Assertion
	testElaboratorSucceedsAfterParser = do
	let state = PipelineState
	{ pstFile = "test.as"
	, pstModule = Nothing
	, pstSourceCode = "test"
	, pstLexedTokens = Just "tokens"
	, pstParsedAST = Just "ast"
	, pstElaborated = Nothing
	, pstTypeChecked = Nothing
	, pstProofChecked = Nothing
	, pstCodeGen = Nothing
	, pstErrors = []
	}
	(newState, result) <- runElaborator state
	case result of
	Right () -> pstElaborated newState @?= Just "core_ast"
	Left _ -> fail "Elaborator failed after parser"

	-- ============================================================================
	-- TYPE CHECKER TESTS
	-- ============================================================================

	testTypeCheckerRequiresElaborated :: Assertion
	testTypeCheckerRequiresElaborated = do
	let state = PipelineState
	{ pstFile = "test.as"
	, pstModule = Nothing
	, pstSourceCode = "test"
	, pstLexedTokens = Just "tokens"
	, pstParsedAST = Just "ast"
	, pstElaborated = Nothing
	, pstTypeChecked = Nothing
	, pstProofChecked = Nothing
	, pstCodeGen = Nothing
	, pstErrors = []
	}
	(_, result) <- runTypeChecker state
	case result of
	Left _ -> return ()
	Right () -> fail "Type checker succeeded without elaborated output"

	testTypeCheckerSucceedsAfterElaboration :: Assertion
	testTypeCheckerSucceedsAfterElaboration = do
	let state = PipelineState
	{ pstFile = "test.as"
	, pstModule = Nothing
	, pstSourceCode = "test"
	, pstLexedTokens = Just "tokens"
	, pstParsedAST = Just "ast"
	, pstElaborated = Just "core_ast"
	, pstTypeChecked = Nothing
	, pstProofChecked = Nothing
	, pstCodeGen = Nothing
	, pstErrors = []
	}
	(newState, result) <- runTypeChecker state
	case result of
	Right () -> pstTypeChecked newState @?= Just "typed_ast"
	Left _ -> fail "Type checker failed after elaboration"

	-- ============================================================================
	-- PROOF CHECKER TESTS
	-- ============================================================================

	testProofCheckerRequiresTypeChecked :: Assertion
	testProofCheckerRequiresTypeChecked = do
	let state = PipelineState
	{ pstFile = "test.as"
	, pstModule = Nothing
	, pstSourceCode = "test"
	, pstLexedTokens = Just "tokens"
	, pstParsedAST = Just "ast"
	, pstElaborated = Just "core_ast"
	, pstTypeChecked = Nothing
	, pstProofChecked = Nothing
	, pstCodeGen = Nothing
	, pstErrors = []
	}
	(_, result) <- runProofChecker state
	case result of
	Left _ -> return ()
	Right () -> fail "Proof checker succeeded without type checked output"

	testProofCheckerSucceedsAfterTypeCheck :: Assertion
	testProofCheckerSucceedsAfterTypeCheck = do
	let state = PipelineState
	{ pstFile = "test.as"
	, pstModule = Nothing
	, pstSourceCode = "test"
	, pstLexedTokens = Just "tokens"
	, pstParsedAST = Just "ast"
	, pstElaborated = Just "core_ast"
	, pstTypeChecked = Just "typed_ast"
	, pstProofChecked = Nothing
	, pstCodeGen = Nothing
	, pstErrors = []
	}
	(newState, result) <- runProofChecker state
	case result of
	Right () -> pstProofChecked newState @?= Just "verified_proofs"
	Left _ -> fail "Proof checker failed after type check"

	-- ============================================================================
	-- CODE GEN TESTS
	-- ============================================================================

	testCodeGenRequiresProofChecked :: Assertion
	testCodeGenRequiresProofChecked = do
	let state = PipelineState
	{ pstFile = "test.as"
	, pstModule = Nothing
	, pstSourceCode = "test"
	, pstLexedTokens = Just "tokens"
	, pstParsedAST = Just "ast"
	, pstElaborated = Just "core_ast"
	, pstTypeChecked = Just "typed_ast"
	, pstProofChecked = Nothing
	, pstCodeGen = Nothing
	, pstErrors = []
	}
	(_, result) <- runCodeGen state
	case result of
	Left _ -> return ()
	Right () -> fail "Code gen succeeded without proof checked output"

	testCodeGenSucceedsAfterProofCheck :: Assertion
	testCodeGenSucceedsAfterProofCheck = do
	let state = PipelineState
	{ pstFile = "test.as"
	, pstModule = Nothing
	, pstSourceCode = "test"
	, pstLexedTokens = Just "tokens"
	, pstParsedAST = Just "ast"
	, pstElaborated = Just "core_ast"
	, pstTypeChecked = Just "typed_ast"
	, pstProofChecked = Just "verified_proofs"
	, pstCodeGen = Nothing
	, pstErrors = []
	}
	(newState, result) <- runCodeGen state
	case result of
	Right () -> pstCodeGen newState @?= Just "haskell_code"
	Left _ -> fail "Code gen failed after proof check"

	-- ============================================================================
	-- ERROR HANDLING TESTS
	-- ============================================================================

	testPipelineHaltsOnError :: Assertion
	testPipelineHaltsOnError = do
	let state = PipelineState
	{ pstFile = "test.as"
	, pstModule = Nothing
	, pstSourceCode = ""
	, pstLexedTokens = Nothing
	, pstParsedAST = Nothing
	, pstElaborated = Nothing
	, pstTypeChecked = Nothing
	, pstProofChecked = Nothing
	, pstCodeGen = Nothing
	, pstErrors = []
	}
	(_, result) <- runLexer state
	case result of
	Left _ -> return () -- Error caught, pipeline halted
	Right () -> fail "Pipeline did not halt on error"

	testErrorIncludesCategory :: Assertion
	testErrorIncludesCategory = do
	let state = PipelineState
	{ pstFile = "test.as"
	, pstModule = Nothing
	, pstSourceCode = ""
	, pstLexedTokens = Nothing
	, pstParsedAST = Nothing
	, pstElaborated = Nothing
	, pstTypeChecked = Nothing
	, pstProofChecked = Nothing
	, pstCodeGen = Nothing
	, pstErrors = []
	}
	(_, result) <- runLexer state
	case result of
	Left err -> return () -- Error has category from ErrorDetail
	Right () -> fail "Expected error"

	testErrorMessagePresent :: Assertion
	testErrorMessagePresent = do
	let state = PipelineState
	{ pstFile = "test.as"
	, pstModule = Nothing
	, pstSourceCode = ""
	, pstLexedTokens = Nothing
	, pstParsedAST = Nothing
	, pstElaborated = Nothing
	, pstTypeChecked = Nothing
	, pstProofChecked = Nothing
	, pstCodeGen = Nothing
	, pstErrors = []
	}
	(_, result) <- runLexer state
	case result of
	Left err -> (not . null) (edMessage err) @?= True
	Right () -> fail "Expected error"

	-- ============================================================================
	-- DETERMINISM TESTS
	-- ============================================================================

	testPipelineDeterminism :: Assertion
	testPipelineDeterminism = do
	let source = "assert x = x : Bool"
	state1 = PipelineState
	{ pstFile = "test.as"
	, pstModule = Nothing
	, pstSourceCode = source
	, pstLexedTokens = Nothing
	, pstParsedAST = Nothing
	, pstElaborated = Nothing
	, pstTypeChecked = Nothing
	, pstProofChecked = Nothing
	, pstCodeGen = Nothing
	, pstErrors = []
	}
	state2 = state1
	(newState1, result1) <- runLexer state1
	(newState2, result2) <- runLexer state2
	result1 @?= result2
	pstLexedTokens newState1 @?= pstLexedTokens newState2