Verification Boundary Reporter

theory VerifiedSort
imports Main "HOL-Library.Multiset"
begin

fun insert :: "nat ⇒ nat list ⇒ nat list" where
  "insert x [] = [x]" |
  "insert x (y # ys) = (if x ≤ y then x # y # ys else y # insert x ys)"

fun insertion_sort :: "nat list ⇒ nat list" where
  "insertion_sort [] = []" |
  "insertion_sort (x # xs) = insert x (insertion_sort xs)"

lemma insert_sorted:
  "sorted xs ⟹ sorted (insert x xs)"
  by (induction xs) auto

lemma mset_insert:
  "mset (insert x xs) = {#x#} + mset xs"
  by (induction xs) (auto simp: ac_simps)

theorem insertion_sort_correct:
  "sorted (insertion_sort xs) ∧ mset (insertion_sort xs) = mset xs"
  by (induction xs) (auto simp: insert_sorted mset_insert)

export_code insertion_sort in SML file "sort.sml"

end

# Verification Boundary Report

**Project:** VerifiedSort
**Date:** 2026-02-17
**Verifier:** Isabelle/HOL
**Analyst:** Verification Boundary Reporter

## Executive Summary

The insertion sort implementation is fully verified with complete proofs of
correctness (sorting and permutation preservation). The verification relies
on Isabelle's standard library and kernel as the trusted computing base.
Code extraction to SML is part of the TCB.

## Verification Statistics

- Total components: 5
- Verified: 3 (60%)
- Assumed: 0 (0%)
- Unverified: 0 (0%)
- TCB elements: 2 (40%)

## Verified Components

### insert function
**Location:** VerifiedSort.thy:5-7
**Properties Proven:**
- Preserves sortedness (insert_sorted)
- Preserves multiset (mset_insert)
**Proof Status:** ✓ Complete
**Dependencies:** None (base case)

### insertion_sort function
**Location:** VerifiedSort.thy:9-11
**Properties Proven:**
- Produces sorted output
- Preserves all elements (permutation)
**Proof Status:** ✓ Complete
**Dependencies:** insert, insert_sorted, mset_insert

### Correctness theorem
**Location:** VerifiedSort.thy:18-19
**Statement:** sorted (insertion_sort xs) ∧ mset (insertion_sort xs) = mset xs
**Proof Status:** ✓ Complete
**Proof Method:** Induction with auto

## Assumptions and Axioms

None. All proofs are complete without axioms.

## Trusted Computing Base

### Isabelle/HOL Kernel
**Type:** Proof Assistant Kernel
**Description:** The Isabelle/HOL logical kernel that checks all proofs
**Justification:** Fundamental to all verification; cannot be verified within itself
**Mitigation:** Small, well-audited kernel; decades of use

### Isabelle Standard Library
**Type:** Library
**Description:** HOL-Library.Multiset for multiset operations
**Justification:** Used for permutation reasoning
**Mitigation:** Part of standard Isabelle distribution, widely used and tested

### Code Generation
**Type:** Tool
**Description:** export_code mechanism that generates SML
**Justification:** Translates verified Isabelle code to executable SML
**Mitigation:** Code generator is part of Isabelle, but translation correctness
is not formally verified. Generated code must be trusted to match semantics.

## Unverified Components

None. All algorithmic components are verified.

## Verification Gaps

None identified in the core algorithm.

## Limitations

1. **Code extraction trust:** The generated SML code is not verified to match
   the Isabelle semantics. The code generator is trusted.

2. **Termination:** While termination is proven by Isabelle's function package,
   the extracted code's termination depends on the SML runtime.

3. **I/O and side effects:** Any I/O operations in the extracted code are
   outside the verification boundary.

4. **Numeric representation:** The verification uses mathematical integers (nat),
   but extracted code uses machine integers which may overflow.

## Recommendations

1. **Consider verified extraction:** Use a verified code generator or
   certified compilation if higher assurance is needed.

2. **Add overflow checks:** If using extracted code with large inputs,
   add runtime checks for integer overflow.

3. **Document TCB:** Clearly communicate to users that code extraction
   is part of the trusted base.