program-to-model-extractor

Program-to-Model Extractor

Extract high-level mathematical models from functional code for formal reasoning in Isabelle/HOL.

Overview

This skill transforms functional programs (Haskell, OCaml, F#) into abstract mathematical models suitable for formal verification in Isabelle/HOL. The extraction focuses on the algorithm's mathematical essence—capturing core properties, invariants, and structural patterns while abstracting away language-specific implementation details.

Extraction Workflow

1. Analyze the Source Code

Identify key elements:

• Data structures: Algebraic types, lists, trees, custom types
• Core functions: Main computational logic
• Recursion patterns: Structural, tail, mutual recursion
• Properties: What should be true about inputs/outputs?

2. Extract Data Types

Convert source language types to Isabelle datatypes:

-- Haskell
data Tree a = Leaf | Node a (Tree a) (Tree a)

(* Isabelle *)
datatype 'a tree = Leaf | Node "'a" "'a tree" "'a tree"

3. Model Functions

Choose the appropriate Isabelle construct:

For primitive recursion (terminates obviously):

fun length :: "'a list ⇒ nat" where
  "length [] = 0" |
  "length (x # xs) = 1 + length xs"

For general recursion (needs termination proof):

function gcd :: "nat ⇒ nat ⇒ nat" where
  "gcd m n = (if n = 0 then m else gcd n (m mod n))"
by pat_completeness auto
termination by (relation "measure snd") auto

For non-recursive definitions:

definition compose :: "('b ⇒ 'c) ⇒ ('a ⇒ 'b) ⇒ ('a ⇒ 'c)" where
  "compose f g = (λx. f (g x))"

4. State Properties

Extract and formalize key properties as lemmas:

lemma length_append: "length (xs @ ys) = length xs + length ys"
lemma quicksort_permutes: "mset (quicksort xs) = mset xs"
lemma quicksort_sorted: "sorted (quicksort xs)"

5. Identify Invariants

For stateful or accumulator-based functions, state what holds during computation: