Add streaming B3 declaration-level SMT translation with dependency tracking

[MikaelMayer]

Context

Follow-up to #307 (B3 Verifier PR). Currently, processes complete B3 programs in batch. This issue proposes adding streaming translation at the declaration level to enable incremental verification and better support for language lifting.

Motivation

1. Streaming conversion: Process declarations one at a time as they arrive from other languages
2. Incremental verification: Verify procedures as soon as their dependencies are satisfied
3. Better modularity: Each declaration type has explicit handling
4. Memory efficiency: Avoid building entire B3 AST in memory before verification

Proposed Architecture

ProgramBuilder with Dependency Tracking

structure ProgramBuilder where
  verificationState : B3VerificationState  -- Emitted to SMT (axioms, functions)
  pendingDecls : List (B3AST.Decl SourceRange)  -- Waiting for dependencies
  reports : List ProcedureReport
  errors : List String

-- Core streaming API
def addDeclaration (builder : ProgramBuilder) (decl : B3AST.Decl SourceRange)
    : IO ProgramBuilder := do
  -- Try to emit this declaration
  -- If dependencies satisfied: emit to SMT, check if any pending can now be emitted
  -- If dependencies missing: add to pendingDecls
  ...

def endProgram (builder : ProgramBuilder) : IO (List ProcedureReport × List String) := do
  -- Report errors for any remaining pendingDecls with unfulfilled dependencies
  ...

-- Optional: Manual dependency override
def flushPending (builder : ProgramBuilder) (assumeDependenciesSatisfied : Bool := false)
    : IO ProgramBuilder := do
  -- If assumeDependenciesSatisfied: emit all pending declarations
  -- Otherwise: report errors
  ...

Key Features

1. Dependency tracking: Track what each declaration needs (function names, type names)
2. Eager emission: Emit to SMT as soon as dependencies are ready
3. Buffering: Hold back declarations with unmet dependencies
4. Cascade effect: When a declaration is emitted, check if it unblocks pending ones
5. Manual override: flushPending for cases where dependencies are known to be satisfied

Use Case: Language Lifting

When lifting from another language to B3:

-- Streaming: emit B3 declarations as you translate
let mut builder ← ProgramBuilder.init solver
for sourceDecl in sourceProgram do
  let b3Decl ← liftToB3Declaration sourceDecl
  builder ← builder.addDeclaration b3Decl
  -- Verification happens automatically when dependencies are met

let (reports, errors) ← builder.endProgram

This avoids building the entire B3 AST in memory before verification starts.

Implementation Notes

• Parameterless procedures are just statements wrapped in push/pop
• Need to track function dependencies (which functions does this declaration reference?)
• Need to track type dependencies (which types does this declaration use?)
• Consider using a dependency graph or topological sort for efficient resolution

Related

• PR Add B3 Verifier: SMT-based verification for B3 programs #307 - B3 Verifier implementation
• Current programToSMT works fine for complete programs, this is an enhancement for streaming use cases