Technical Solutions

A deep dive into Fanal's architecture, language design, type system, and automation pipeline for verified quantum programming.

1Architecture — Five-Layer Design

Parsing Syntax

User-facing Lean macros

Supportive

AI-generated

Syntax (AST)

Term constructors

Typing (Relations)

Deterministic & decidable

Semantics (Matrices)

Denotational interpretation

Descriptive

Human-maintained

Automation (Tactics)

Certified rewriting & decision

Supportive

AI-generated

2Module Dependencies

Dependency Graph

Module	Purpose	Components
CExpr	Classical expressions, data types, arithmetic	Syntax, Typing, Semantics
Label	Register labels for quantum register annotation	Syntax, Typing, Semantics
Set	Summation domains (e.g., univ)	Syntax, Typing, Semantics
Dirac	Plain Dirac notation	Syntax, Typing, Semantics, EqDef
LDirac	Register-annotated Dirac notation	Syntax, Typing, Semantics, EqDef

3Language Design

DataType — Foundation for Register Dimensions

\texttt{fin}\;n

— Finite {0, ..., n-1}

\texttt{tuple}\;[t_1, \ldots, t_k]

— Product type

\texttt{array}\;n\;t

— Fixed-size array

\llbracket \texttt{fin}\;n \rrbracket = \text{Fin}\;n

\llbracket \texttt{tuple}\;[t_1, \ldots] \rrbracket = \llbracket t_1 \rrbracket \times \cdots

\llbracket \texttt{array}\;n\;t \rrbracket = \text{Fin}\;n \to \llbracket t \rrbracket

DiracTerm — 16 Constructors

Primitives

$|t\rangle$ ket, $\langle t|$ bra
$\delta[i,j]$ Kronecker delta
Complex scalar, zero, identity

Operations

Addition, negation, scalar multiplication
Matrix multiplication, tensor product
Adjoint, big sum, big tensor product

DiracSort — (ketType, braType)

Every Dirac term has a sort $(\alpha, \beta)$ describing its matrix dimensions:

scalar

(\texttt{unit}, \texttt{unit})

ket \alpha

(\alpha, \texttt{unit})

bra \alpha

(\texttt{unit}, \alpha)

op \;\alpha\;\beta

(\alpha, \beta)

\llbracket \text{sort}\;(\alpha, \beta) \rrbracket = \text{Matrix}\;\llbracket\alpha\rrbracket\;\llbracket\beta\rrbracket\;\mathbb{C}

4Labelled Dirac Notation

Why Labels?

Plain Dirac notation does not track which registers an operator acts on. Labelled Dirac extends each term with register patterns (ket label, bra label), enabling compositional reasoning about multi-register quantum systems.

Access Path Model

Labels resolve to register atoms via root + path of AccessSteps, reaching leaf dimensions that determine matrix indices.

q : tuple [array 3 (fin 2), fin 4]

tupleProj 0

array 3 (fin 2)

arrayElem 1

fin 2

tupleProj 1

fin 4

Atom: <q, [tupleProj 0, arrayElem 1]> resolves to

\texttt{fin}\;2

LDirac Operations

labelAttach register annotations to a plain Dirac term

⊗ₗTensor — requires disjoint atoms

+ₗAddition — requires matching dims/atoms

·ₗMultiply — requires contraction compatible

Design principle: Typing is decidable. Undecidable premises (disjointness, dimension matching) are deferred to evaluation time, returning Option.

5Type System

Three Variable Categories, One Unified Context

ctype dt

Classical variable

x : Fin n, index, flag

dtype (α,β)

Dirac variable

A : Hα → Hβ

qtype dt

q : quantum register

Key Typing Principles

(1) Deterministic(2) Decidable(3) Deferred checks

Sort Operations

(\alpha_1, \beta_1) \otimes (\alpha_2, \beta_2) = (\texttt{tuple}[\alpha_1, \alpha_2],\; \texttt{tuple}[\beta_1, \beta_2])

(\alpha, \beta)^\dagger = (\beta, \alpha)

(\alpha, \gamma) \cdot (\gamma, \beta) = (\alpha, \beta) \quad \text{(contraction on } \gamma \text{)}

6Automation Pipeline

Pipeline Overview

Goal

t₁ ≈ t₂

→

Phase 1

Normalization (rewrite rules on AST)

→

Phase 2

Comparison (syntactic equality)

→

Phase 3

Close goal (rfl or native_decide)

→

QED

Proof complete

`dirac_eq` Tactic — 7-Strategy Fallback

1Untyped norm → rfl~90% of goals

1bUntyped norm → native_decide

1eExpanded untyped (BKB, congr, id) → rfl

1ebExpanded untyped → native_decide

2Typed normalizer → rfl

3Typed + proof irrelevance → rfl

3bTyped + proof irrel → native_decidelast resort

`ldirac_eq` — Labelled Dirac Automation

Reduces labelled Dirac goals to plain Dirac, then reuses dirac_eq. Key reduction rules:

Absorption: same labels → mergeTensor combine: disjoint → fuse

Lean 4

example : gateX ⫍ k0 ≈ₕ k1 := by dirac_eq

example : ⟦ A ⟧_(a,a) ·ₗ ⟦ B ⟧_(a,a) ≈ₗ ⟦ A·B ⟧_(a,a) := by ldirac_eq

7Challenges & Solutions

Challenge	Solution
ℂ lacks DecidableEq — blocks native_decide	Conservative BEq: fails (never unsound) on non-concrete values
Register disjointness undecidable at type level	Deferred evaluation: typing stays decidable; disjointness checked at eval time via Option
Heterogeneous equality (different sorts)	HSemEq (≈ₕ) with SortIso: reindex matrices along isomorphisms
Lean 4 kernel timeout on large normalizations	Multi-strategy fallback: try rfl first, escalate to native_decide
Descriptive code readability vs proof complexity	Physical separation: Descriptive/ (human) vs Supportive/ (AI)