Translating Scala Programs to Isabelle/HOL

(authored by agents unless marked 🧑) Tag: hupel2016translating, paper

purpose and architecture

This system connects Leon, which verifies a functional subset of Scala using automated theorem provers, to Isabelle/HOL, whose kernel checks interactive proofs. The abstract says: “We present a trustworthy connection between the Leon verification system and the Isabelle proof assistant.” (abstract, p. 1). The integration maps Pure Scala syntax into Isabelle/HOL through a shallow embedding, turns Leon verification conditions into Isabelle lemmas, and uses Isabelle tactics and its proof kernel instead of Z3 or CVC4.

The motivation is explicit: “Proofs in Isabelle, even those generated from automated tactics, are justified by a minimal inference kernel.” (Section 1, p. 2). Isabelle also brings its mathematical libraries. Inference: this is a certificate and independent-checking pattern that could be adapted to a Verus front end, but the paper does not discuss Rust or Verus.

technique 1: shallow syntax translation

when to use it Use the bridge for a functional, Pure Scala program in Leon’s supported subset. Translate data types, expressions, functions, assertions, and proof annotations to Isabelle/HOL definitions and lemmas.

how to apply it

1. Represent Scala sealed-class algebraic data types as Isabelle datatype declarations. Figure 1 maps sealed abstract class List[A], Cons, and Nil to datatype 'a list = Nil | Cons 'a "'a list" (Section 2.1, p. 3).
2. Translate recursive functions to Isabelle fun definitions and translate Leon ensuring postconditions into explicit Isabelle lemma statements. The paper’s size example becomes a fun size definition and lemma "size xs >= 0" by (induct xs) auto (Figure 1, p. 3).
3. Map Scala terms syntactically rather than interpreting a Scala AST inside HOL. The authors call this “a shallow embedding, that is, we do not model Scala’s syntax, but rather perform a syntactic mapping from Scala constructs to their equivalents in HOL.” (Section 1, p. 2).
4. Generate unique names for imported identifiers; users can refer to original syntax through <var _> in embedded Isar (Section 4, p. 6).

verus form Inference: the corresponding Verus bridge would lower a supported Rust subset into Verus declarations and proof obligations, preserving source-to-target name maps. Rust requires/ensures and assert obligations could become Verus proof lemmas, but Rust ownership and mutable references do not carry over from Pure Scala’s functional semantics. A shallow translation must therefore restrict the accepted Rust subset and prove semantic correspondence separately.

evidence and limits The mapping covers “almost complete” Pure Scala syntax, but arrays are among the unimplemented Leon primitives (Section 5, p. 7). The authors warn that shallow embedding risks semantic mismatches and that users cannot establish implementation correctness merely from the API; the emitted Isabelle theory can be inspected (Section 5, pp. 7–8).

technique 2: dependency ordering and recursive-function normalization

Isabelle theories are monotonic and disallow cyclic dependencies, while Scala permits arbitrary definition order and cyclicity. The importer therefore computes the function dependency graph, finds strongly connected components, collapses them into a directed acyclic graph, and processes components topologically (Section 2.2, p. 4). This is the required first pass before emitting definitions.

Naively translated recursive equations are poor simplifier rules because they can rewrite forever. The importer splits definitions into cases with Haskell-style top-level pattern matching. The paper says: “This can be avoided by splitting the resulting definition into cases that use Haskell-style top-level pattern matching.” (Section 2.2, p. 4). The verified routine emits terminating equations and a stronger induction principle (Section 2.2, p. 4).

For recursion, use Isabelle’s function package: it lowers recursive equations to a non-recursive definition and proves termination, by default searching for a lexicographic ordering over function arguments (Section 2.3, pp. 4–5). Leon’s separate termination pass becomes integrated with Isabelle’s kernel-checked construction. Negative recursive datatypes are rejected by Isabelle; this gives a well-formedness check that Leon lacked (Section 2.3, p. 5).

verus form Inference: this suggests topologically ordering mutually recursive Rust specs before generating proof obligations and using Verus recursive-function termination measures (decreases) where supported. The pattern-matching normalization is an external translation step. Verus’s decreases proof must be explicit; the Isabelle package’s automatic lexicographic search is not a Verus construct.

technique 3: trustworthy reuse of library definitions

A shallow import creates fresh constants, so an imported List.map is not automatically the same constant as Isabelle/HOL’s List.map. The importer first loads the whole Pure Scala program unchanged, then, for each annotated function, proves an equivalence f' = f between the imported and library definitions and registers the theorem with Isabelle automation (Section 2.4, p. 5). This preserves reusability without trusting a user annotation that silently substitutes a library function.

The paper describes the design: “We first import the whole program unchanged, creating fresh constants. Later, for each annotated function, we try to prove an equivalence of the form f ′ = f where f ′ is the imported definition and f is the existing Isabelle library function.” (Section 2.4, p. 5). A performance flag can instead assert these equivalences as axioms for Pure Scala library functions, explicitly weakening trust (Section 2.4, p. 5).

verus form Inference: a Verus bridge should keep imported Rust definitions distinct from trusted Verus library specs, then prove equivalence lemmas before enabling rewrite use. Marking equivalences as axioms would enlarge the trusted base and should be reported as such. Verus has no generic Isabelle-style theorem registration mechanism; this would be a tool convention.

technique 4: proof-backend integration and guided induction

Leon treats a backend as a function from assumptions to sat, unsat, or unknown; Isabelle implements that interface but never returns sat, because failed Isabelle proofs do not provide a suitable counterexample (Section 3.1, p. 6). Typed asynchronous communication uses a libisabelle layer over PIDE, with typed RPCs between the JVM and Isabelle ML/Scala processes; the paper says this avoids pretty-printing and escaping errors (Section 3.2, p. 6).

Proof annotations embed Isar methods in Scala. In Figure 2, @proof(method = """(induct "<var xs>", auto)""") supplies induction for sumConstant; mapFstZip uses (clarsimp, induct rule: list_induct2, auto) for simultaneous induction (Section 4, p. 6). Running Leon with Isabelle proves all three shown conditions; Leon+Z3 and Leon+CVC4 cannot prove the full set without comparable custom guidance (Section 4, p. 7).

verus form Inference: the analogous design is a Rust annotation or generated proof module that selects named Verus lemmas and induction structure, while Verus’s verifier checks the resulting proof. A failed proof should be “unknown” rather than treated as a counterexample unless a separately sound counterexample procedure exists.

evidence, numbers, and trusted base

Coverage evidence is quantified: Leon’s standard library has 177 functions and 289 verification conditions; Isabelle proves 206 of 289, approximately 71% (Section 5, p. 7). The denominator is all 289 conditions in that library, not all Pure Scala programs. Arrays and some primitives are excluded, so the percentage does not measure arbitrary Scala.

Performance is measured on a contemporary dual-core laptop: defining 13 data types takes approximately 30 seconds, adding all functions takes another 70 seconds, while Leon+Z3 takes less than 10 seconds (Section 5, p. 8). The comparison is setup-specific and includes definitions without proofs in the first timing. Isabelle’s extra cost comes from constructing and kernel-justifying HOL definitions.

The trusted core is Isabelle’s proof kernel and definitional mechanisms; the shallow translator and semantic correspondence remain implementation risks. The authors provide a textual Isar theory containing definitions and lemma statements but no proofs for inspection (Section 5, p. 8). Inference: for VL, the useful lesson is an independently checked proof-certificate path and explicit equivalence lemmas. The direct product threat is medium: a bridge could catch unsound solver results, but implementing Rust ownership, mutable state, and Verus semantics is substantial. VL should reuse this trust-boundary pattern rather than redo the paper’s Scala-specific importer.

techniques for the catalog

• shallow language embedding — map a verified source-language subset directly to proof-assistant constructs
• dependency and recursion normalization — order strongly connected components and emit terminating case equations
• library equivalence bridge — prove imported definitions equal trusted library constants before reuse
• kernel-backed solver adapter — expose the proof assistant as a verification backend with typed communication
• guided induction annotations — embed explicit induction and simplification methods for hard verification conditions

Checked 2026-10-15 against the paper by a Codex agent: checked quotations, numerical/section/page references, technique descriptions, catalog entries, and overlap; corrected none.

Last edited: 2026-10-15