Verify code refines Z specification via abstraction function and commutativity checks
From z-spec-devnpx claudepluginhub punt-labs/claude-plugins --plugin z-spec[spec.tex] [language: swift|typescript|python|kotlin] [--lean] [--generate-abstraction] [--impl file]/refineRefines existing CLI harness for software at <software-path> by analyzing gaps in coverage and adding new commands/tests, optionally focusing on specific features.
/refineRefines existing cli-anything-web CLI: performs gap analysis, records new traffic with Playwright or DevTools, implements missing endpoints, updates tests and REPL help.
/refineRefines an existing writer skill by analyzing additional writing samples and updating the voice profile. Provide path to skill directory.
/refineAnalyzes existing PRD for gaps using a section checklist, generates markdown gap analysis, and refines via targeted interactive questions.
/refineRefines raw ideas and todos into structured, actionable software engineering plans by proactively asking questions to uncover hidden requirements and applying design patterns.
Verify that implementation code correctly refines a Z specification by defining an abstraction function and generating commutativity tests (and optionally Lean 4 proofs) for every operation.
The key correctness property for each operation:
abstract(concreteOp(concreteState)) = abstractOp(abstract(concreteState))
If this holds for every operation, the code is a provably correct refinement of the specification.
Arguments: $ARGUMENTS
Parse arguments:
docs/*.tex)--lean - also generate Lean 4 commutativity proofs in proofs/--generate-abstraction - auto-generate abstraction function scaffold
(otherwise walk the user through defining it interactively)--impl <file> - path to implementation file (default: auto-detect from project)Verify the specification has been type-checked:
which fuzz >/dev/null 2>&1 || echo "FUZZ_NOT_FOUND"
If fuzz is not found: Warn but do not block. The refinement
process can proceed without type-checking, but recommend running
/z-spec:check first.
If --lean is specified, verify Lean 4 and Lake are installed:
which lean >/dev/null 2>&1 || echo "LEAN_NOT_FOUND"
which lake >/dev/null 2>&1 || echo "LAKE_NOT_FOUND"
If lean or lake not found: Stop and tell the user:
Lean 4 is not installed. Run
/z-spec:setup leanto install the Lean 4 toolchain via elan. Or omit--leanto generate commutativity tests only.
The Z specification should already exist. Implementation code
should also exist (from /z-spec:model2code or hand-written).
If a file path is provided, use it directly.
If no file specified:
docs/ for .tex files containing Z specificationsRead the specification file.
Scan the specification and extract the following constructs.
Look for given set declarations in \begin{zed} blocks:
\begin{zed}
[USERID, SESSIONID]
\end{zed}
Record each name. These are abstract types in the specification.
Look for free type definitions in \begin{zed} blocks:
\begin{zed}
Status ::= pending | active | suspended | closed
\end{zed}
Record the type name and all constructors.
Look for \begin{axdef} blocks with global constants:
\begin{axdef}
MAX\_BALANCE : \nat
\where
MAX\_BALANCE = 1000000
\end{axdef}
Record each constant name, type, and defining predicate.
Look for state schemas -- schemas that are not operations
(no \Delta, \Xi, or primed-only variables):
\begin{schema}{Account}
balance : \num \\
status : Status
\where
balance \geq 0 \lor status = suspended \\
status = closed \implies balance = 0
\end{schema}
Record:
\where blockLook for schemas that initialize the state:
\begin{schema}{InitAccount}
Account'
\where
balance' = 0 \\
status' = pending
\end{schema}
Record:
Look for schemas containing \Delta or \Xi:
\begin{schema}{Deposit}
\Delta Account \\
amount? : \nat_1
\where
status = active \\
balance' = balance + amount? \\
status' = status
\end{schema}
For each operation, record:
\Delta (state-changing) or \Xi (query/observation)? with their types! with their typesx')x' = xIf a language is specified, use it.
Otherwise auto-detect from project files:
| File Present | Language |
|---|---|
Package.swift, *.xcodeproj | Swift |
package.json, tsconfig.json | TypeScript |
pyproject.toml, setup.py, requirements.txt | Python |
build.gradle.kts, pom.xml | Kotlin |
Search for classes or structs matching the state schema name:
struct <Name> or class <Name> in Sources/
or src/interface <Name> or class <Name> in
src/ or lib/class <Name> in src/ or the project rootdata class <Name> or class <Name> in
src/main/If not found, ask the user to specify the implementation file path.
Read the implementation file and extract:
Build a mapping table:
| Abstract (Z spec) | Concrete (code) | Notes |
|--------------------|-----------------|-------|
| balance : Nat | balance: number | Direct mapping |
| status : Status | statusCode: string | Needs translation |
| - | lastModified: Date | Implementation detail (no abstract counterpart) |
If --generate-abstraction is specified, analyze both the abstract
spec and the concrete code to produce a starter abstraction function.
For each abstract state variable, attempt to find a matching concrete field using these heuristics:
| Heuristic | Example |
|---|---|
| Exact name match | balance -> balance |
| Case-insensitive match | Status -> status |
| Prefix/suffix match | balance -> accountBalance, balanceAmount |
| Type-compatible match | Nat -> number, Int, int |
For fields that cannot be auto-matched, emit a TODO comment.
For each Z free type used in the abstract state, detect how the concrete code represents it and generate a mapping function:
/**
* Maps concrete status code to abstract Status type.
*
* Abstract: Status ::= pending | active | suspended | closed
* Concrete: string codes "P", "A", "S", "C"
*
* VERIFY: confirm these mappings match your code conventions.
*/
function mapStatusCode(code: string): Status {
const mapping: Record<string, Status> = {
'P': Status.Pending,
'A': Status.Active,
'S': Status.Suspended,
'C': Status.Closed,
};
const result = mapping[code];
if (result === undefined) {
throw new Error(`Unknown status code: ${code}`);
}
return result;
}
If the concrete code uses an enum that directly matches the Z free type (same constructors, possibly different casing), generate a direct mapping comment instead.
Produce the function combining all field mappings:
TypeScript:
/**
* Abstraction function: maps concrete state to abstract Z spec state.
*
* Abstract state (from Z spec):
* balance : Nat
* status : Status (pending | active | suspended | closed)
*
* Concrete state (from code):
* balance: number
* statusCode: string // "P", "A", "S", "C"
* lastModified: Date
*
* YOU MUST VERIFY AND CUSTOMIZE THIS FUNCTION.
*/
export function abstract(concrete: ConcreteAccount): AbstractAccount {
return {
balance: concrete.balance,
status: mapStatusCode(concrete.statusCode),
// NOTE: lastModified has no abstract counterpart (implementation detail)
};
}
Swift:
/// Abstraction function: maps concrete state to abstract Z spec state.
///
/// Abstract state (from Z spec):
/// balance : Nat
/// status : Status
///
/// Concrete state (from code):
/// balance: Int
/// statusCode: String
/// lastModified: Date
///
/// YOU MUST VERIFY AND CUSTOMIZE THIS FUNCTION.
func abstract(_ concrete: ConcreteAccount) -> AbstractAccount {
AbstractAccount(
balance: concrete.balance,
status: mapStatusCode(concrete.statusCode)
// NOTE: lastModified has no abstract counterpart
)
}
Python:
def abstract(concrete: ConcreteAccount) -> AbstractAccount:
"""
Abstraction function: maps concrete state to abstract Z spec state.
Abstract state (from Z spec):
balance : Nat
status : Status (pending | active | suspended | closed)
Concrete state (from code):
balance: int
status_code: str # "P", "A", "S", "C"
last_modified: datetime
YOU MUST VERIFY AND CUSTOMIZE THIS FUNCTION.
"""
return AbstractAccount(
balance=concrete.balance,
status=map_status_code(concrete.status_code),
# NOTE: last_modified has no abstract counterpart
)
Kotlin:
/**
* Abstraction function: maps concrete state to abstract Z spec state.
*
* Abstract state (from Z spec):
* balance : Nat
* status : Status (pending | active | suspended | closed)
*
* Concrete state (from code):
* balance: Int
* statusCode: String
* lastModified: Instant
*
* YOU MUST VERIFY AND CUSTOMIZE THIS FUNCTION.
*/
fun abstract(concrete: ConcreteAccount): AbstractAccount =
AbstractAccount(
balance = concrete.balance,
status = mapStatusCode(concrete.statusCode),
// NOTE: lastModified has no abstract counterpart
)
Mark every mapping with a comment indicating:
// Direct mapping -- same name, compatible type// Translated mapping -- VERIFY -- type or name differs// TODO: no matching concrete field found -- needs manual work// NOTE: no abstract counterpart (implementation detail) --
concrete field with no Z equivalentIf the user does not specify --generate-abstraction, walk them
through defining the abstraction function interactively.
Display the abstract state extracted from the Z specification:
## Abstract State (from Z spec)
| Variable | Type | Invariant constraints |
|----------|------|-----------------------|
| balance | Nat | balance >= 0 OR status = suspended |
| status | Status | status = closed IMPLIES balance = 0 |
Display the concrete state extracted from the implementation:
## Concrete State (from code)
| Field | Type | Default |
|-------|------|---------|
| balance | number | 0 |
| statusCode | string | "P" |
| lastModified | Date | new Date() |
For each abstract variable, ask the user:
balance : Nat?"For each Z free type, ask:
Status ::= pending | active | suspended | closed? (enum, string codes, numeric constants)"For concrete fields with no obvious abstract counterpart, ask:
lastModified: Date has no apparent Z counterpart. Is this
an implementation detail to ignore, or does it correspond to
an abstract variable I missed?"After collecting all mappings, generate the abstraction function using the same patterns as step 4c.
Before generating commutativity tests, ensure abstract operation functions exist. These mirror the Z spec semantics:
TypeScript:
/**
* Abstract Deposit operation (from Z spec).
* Precondition: status = active
* Effect: balance' = balance + amount
* Frame: status' = status
*/
function abstractDeposit(
state: AbstractAccount,
input: { amount: number }
): AbstractAccount {
return {
balance: state.balance + input.amount,
status: state.status,
};
}
function depositPrecondition(
state: AbstractAccount,
amount: number
): boolean {
return state.status === Status.Active && amount > 0;
}
Generate one abstract operation function per Z operation schema. These serve as the specification oracle for commutativity tests.
Verify that the initial concrete state abstracts to the initial abstract state. This is the base case for refinement correctness.
TypeScript:
describe('Refinement: Init', () => {
it('concrete init abstracts to abstract init', () => {
// Concrete initialization
const concrete = new ConcreteAccount();
// Abstract initialization
const abstractInit: AbstractAccount = {
balance: 0,
status: Status.Pending,
};
// Verify: abstract(init_concrete) = init_abstract
expect(abstract(concrete)).toEqual(abstractInit);
});
});
Swift:
final class RefinementInitTests: XCTestCase {
// Init commutativity: abstract(init_concrete) = init_abstract
func testConcreteInitAbstractsToAbstractInit() {
let concrete = ConcreteAccount()
let abstractInit = AbstractAccount(balance: 0, status: .pending)
XCTAssertEqual(abstract(concrete), abstractInit)
}
}
Python:
class TestRefinementInit:
def test_concrete_init_abstracts_to_abstract_init(self):
"""Init commutativity: abstract(init_concrete) = init_abstract"""
concrete = ConcreteAccount()
abstract_init = AbstractAccount(balance=0, status=Status.PENDING)
assert abstract(concrete) == abstract_init
Kotlin:
class RefinementInitTest {
@Test
fun `concrete init abstracts to abstract init`() {
val concrete = ConcreteAccount()
val abstractInit = AbstractAccount(balance = 0, status = Status.Pending)
assertEquals(abstractInit, abstract(concrete))
}
}
For each Delta operation, generate tests verifying:
abstract(concreteOp(concreteState)) = abstractOp(abstract(concreteState))
For each Xi operation, generate tests verifying:
concreteQuery(concreteState) = abstractQuery(abstract(concreteState))
For each operation, generate concrete test cases using values
from the partition table (if /z-spec:partition has been run)
or representative values from the type domain.
TypeScript:
describe('Refinement: Deposit', () => {
it('concrete deposit commutes with abstract deposit', () => {
// Setup concrete state
const concrete = createConcreteState({
balance: 100,
statusCode: 'A',
});
// Capture abstract before
const abstractBefore = abstract(concrete);
// Run concrete operation
concreteDeposit(concrete, { amount: 50 });
// Run abstract operation on the abstract-before state
const abstractAfter = abstractDeposit(abstractBefore, {
amount: 50,
});
// Verify commutativity: abstract . concrete = abstract . abstract
expect(abstract(concrete)).toEqual(abstractAfter);
});
it('commutes at boundary: zero balance', () => {
const concrete = createConcreteState({
balance: 0,
statusCode: 'A',
});
const abstractBefore = abstract(concrete);
concreteDeposit(concrete, { amount: 1 });
const abstractAfter = abstractDeposit(abstractBefore, {
amount: 1,
});
expect(abstract(concrete)).toEqual(abstractAfter);
});
it('commutes at boundary: large amount', () => {
const concrete = createConcreteState({
balance: 500,
statusCode: 'A',
});
const abstractBefore = abstract(concrete);
concreteDeposit(concrete, { amount: 999500 });
const abstractAfter = abstractDeposit(abstractBefore, {
amount: 999500,
});
expect(abstract(concrete)).toEqual(abstractAfter);
});
});
Swift:
final class RefinementDepositTests: XCTestCase {
func testDeposit_commutesWithAbstractDeposit() {
var concrete = ConcreteAccount(balance: 100, statusCode: "A")
let abstractBefore = abstract(concrete)
concrete.deposit(amount: 50)
let abstractAfter = abstractDeposit(abstractBefore, amount: 50)
XCTAssertEqual(abstract(concrete), abstractAfter)
}
func testDeposit_commutesAtBoundary_zeroBalance() {
var concrete = ConcreteAccount(balance: 0, statusCode: "A")
let abstractBefore = abstract(concrete)
concrete.deposit(amount: 1)
let abstractAfter = abstractDeposit(abstractBefore, amount: 1)
XCTAssertEqual(abstract(concrete), abstractAfter)
}
}
Python:
class TestRefinementDeposit:
def test_deposit_commutes_with_abstract_deposit(self):
"""Commutativity: abstract(deposit(c)) = absDeposit(abstract(c))"""
concrete = ConcreteAccount(balance=100, status_code="A")
abstract_before = abstract(concrete)
concrete.deposit(amount=50)
abstract_after = abstract_deposit(abstract_before, amount=50)
assert abstract(concrete) == abstract_after
def test_deposit_commutes_at_boundary_zero_balance(self):
"""Commutativity at boundary: balance=0"""
concrete = ConcreteAccount(balance=0, status_code="A")
abstract_before = abstract(concrete)
concrete.deposit(amount=1)
abstract_after = abstract_deposit(abstract_before, amount=1)
assert abstract(concrete) == abstract_after
Kotlin:
class RefinementDepositTest {
@Test
fun `deposit commutes with abstract deposit`() {
val concrete = ConcreteAccount(balance = 100, statusCode = "A")
val abstractBefore = abstract(concrete)
concrete.deposit(amount = 50)
val abstractAfter = abstractDeposit(abstractBefore, amount = 50)
assertEquals(abstractAfter, abstract(concrete))
}
@Test
fun `deposit commutes at boundary - zero balance`() {
val concrete = ConcreteAccount(balance = 0, statusCode = "A")
val abstractBefore = abstract(concrete)
concrete.deposit(amount = 1)
val abstractAfter = abstractDeposit(abstractBefore, amount = 1)
assertEquals(abstractAfter, abstract(concrete))
}
}
For each operation, also generate a property-based test using the language's property testing library. This provides much stronger coverage than example-based tests alone.
TypeScript (fast-check):
import fc from 'fast-check';
describe('Refinement: Deposit (property-based)', () => {
it('commutes for all valid inputs', () => {
fc.assert(
fc.property(
validConcreteStateArb,
fc.integer({ min: 1, max: 1000000 }),
(concreteState, amount) => {
const absBefore = abstract(concreteState);
// Only test when precondition holds
fc.pre(depositPrecondition(absBefore, amount));
const concreteCopy = structuredClone(concreteState);
concreteDeposit(concreteCopy, { amount });
const absAfter = abstractDeposit(absBefore, { amount });
expect(abstract(concreteCopy)).toEqual(absAfter);
},
),
);
});
});
Swift (SwiftCheck or custom):
func testDeposit_commutesForAllValidInputs() {
// Property-based: test with random valid states and amounts
for _ in 0..<100 {
let balance = Int.random(in: 0...1000000)
let amount = Int.random(in: 1...100000)
var concrete = ConcreteAccount(balance: balance, statusCode: "A")
let abstractBefore = abstract(concrete)
guard depositPrecondition(abstractBefore, amount: amount) else {
continue
}
concrete.deposit(amount: amount)
let abstractAfter = abstractDeposit(abstractBefore, amount: amount)
XCTAssertEqual(abstract(concrete), abstractAfter,
"Failed for balance=\(balance), amount=\(amount)")
}
}
Python (Hypothesis):
from hypothesis import given, assume
import hypothesis.strategies as st
class TestRefinementDepositProperty:
@given(
balance=st.integers(min_value=0, max_value=1000000),
amount=st.integers(min_value=1, max_value=1000000),
)
def test_deposit_commutes_for_all_valid_inputs(
self, balance: int, amount: int
):
concrete = ConcreteAccount(balance=balance, status_code="A")
abstract_before = abstract(concrete)
assume(deposit_precondition(abstract_before, amount))
concrete.deposit(amount=amount)
abstract_after = abstract_deposit(abstract_before, amount=amount)
assert abstract(concrete) == abstract_after
Kotlin (kotest-property):
class RefinementDepositPropertyTest : FunSpec({
test("deposit commutes for all valid inputs") {
checkAll(
Arb.int(0..1_000_000),
Arb.int(1..1_000_000),
) { balance, amount ->
val concrete = ConcreteAccount(balance = balance, statusCode = "A")
val abstractBefore = abstract(concrete)
assume(depositPrecondition(abstractBefore, amount))
concrete.deposit(amount = amount)
val abstractAfter = abstractDeposit(abstractBefore, amount = amount)
abstract(concrete) shouldBe abstractAfter
}
}
})
When generating example-based tests, select values that exercise:
| Category | Strategy |
|---|---|
| Happy path | Typical mid-range values |
| Boundary: lower | Minimum valid input/state values |
| Boundary: upper | Maximum or near-maximum values |
| Boundary: invariant | Values near invariant limits |
| Multiple operations | Compose two operations and check |
Use partition data from /z-spec:partition if available.
If --lean is specified and proofs/ exists, generate formal
commutativity proofs in addition to tests.
If proofs/ exists with lakefile.toml, reuse it. Otherwise
create the project structure (same as /z-spec:prove).
Define the abstraction function as a Lean function mapping concrete state to abstract state:
/-
ZSpec.Refinement
Generated from: <spec-file-name>
Abstraction function and commutativity proofs for data refinement.
-/
import ZSpec.State
import ZSpec.Operations
-- Concrete state (mirrors implementation)
structure ConcreteAccount where
balance : Nat
statusCode : String
lastModified : Nat -- simplified from Date
deriving Repr
-- Abstraction function
def abstract (c : ConcreteAccount) : Account := {
balance := c.balance,
status := mapStatusCode c.statusCode
}
-- Status code mapping
def mapStatusCode (code : String) : Status :=
match code with
| "P" => Status.pending
| "A" => Status.active
| "S" => Status.suspended
| "C" => Status.closed
| _ => Status.pending -- fallback
Mirror the implementation's operations in Lean:
-- Concrete deposit (mirrors implementation)
def concreteDeposit (c : ConcreteAccount) (amount : Nat) :
ConcreteAccount :=
{ c with balance := c.balance + amount }
-- Concrete init
def concreteInit : ConcreteAccount :=
{ balance := 0, statusCode := "P", lastModified := 0 }
/-- Init commutativity: abstract(init_concrete) = init_abstract -/
theorem init_commutes :
abstract concreteInit = initAccount := by
sorry
For each Delta operation:
/-- Deposit commutativity:
abstract(concreteDeposit c amount) = deposit (abstract c) amount -/
theorem deposit_commutes (c : ConcreteAccount) (amount : Nat)
(h_pre : deposit_precondition (abstract c) amount) :
abstract (concreteDeposit c amount) =
deposit (abstract c) amount := by
sorry
For each Xi operation:
/-- GetBalance commutativity:
concreteGetBalance c = getBalance (abstract c) -/
theorem getBalance_commutes (c : ConcreteAccount) :
concreteGetBalance c = getBalance (abstract c) := by
sorry
Try the following tactics in order for each sorry:
| Tactic | When It Works |
|---|---|
rfl | When both sides reduce to the same term |
simp [abstract, concreteOp, abstractOp] | Definition unfolding |
unfold abstract concreteOp abstractOp; rfl | Direct unfolding |
unfold abstract concreteOp abstractOp; simp | Unfolding with simplification |
unfold abstract concreteOp abstractOp; omega | Arithmetic after unfolding |
ext <;> simp [abstract, concreteOp, abstractOp] | Structure extensionality |
aesop | Automated reasoning (Mathlib, slower) |
Follow the same batch discharge process as /z-spec:prove:
rfl and simp for all obligationsunfold; omega for remainingext or aesop for remainingcd proofs && timeout 120 lake build 2>&1
Generate these files in the existing proofs/ project:
proofs/
ZSpec/
Refinement/
Concrete.lean -- Concrete state and operations
Abstraction.lean -- Abstraction function
Commutativity.lean -- Commutativity theorems
Write the generated commutativity tests to a file following project conventions:
| Language | File Name | Location |
|---|---|---|
| Swift | <Name>RefinementTests.swift | Test target directory |
| TypeScript | <name>.refinement.test.ts | Alongside existing tests |
| Python | test_<name>_refinement.py | Test directory |
| Kotlin | <Name>RefinementTest.kt | Test source directory |
Do not overwrite existing test files. Use the Refinement
suffix to distinguish from hand-written, model2code-generated,
or partition-generated tests.
Write the abstraction function and abstract operation functions to a separate file:
| Language | File Name |
|---|---|
| Swift | <Name>Abstraction.swift |
| TypeScript | <name>.abstraction.ts |
| Python | <name>_abstraction.py |
| Kotlin | <Name>Abstraction.kt |
After generating all artifacts, report a summary.
## Abstraction Function
**Abstract state**: Account (balance, status)
**Concrete state**: ConcreteAccount (balance, statusCode, lastModified)
| Abstract Field | Concrete Field | Mapping |
|----------------|----------------|---------|
| balance : Nat | balance: number | Direct (identity) |
| status : Status | statusCode: string | Translated via mapStatusCode |
| - | lastModified: Date | Ignored (implementation detail) |
## Commutativity Tests
**Specification**: docs/account.tex
**Implementation**: src/account.ts
**Test file**: src/account.refinement.test.ts
| # | Operation | Kind | Example tests | Property tests | Status |
|---|-----------|------|---------------|----------------|--------|
| 1 | Init | init | 1 | - | generated |
| 2 | Deposit | Delta | 3 | 1 | generated |
| 3 | Withdraw | Delta | 4 | 1 | generated |
| 4 | GetBalance | Xi | 2 | 1 | generated |
| 5 | CloseAccount | Delta | 2 | 1 | generated |
### Summary
- **Operations covered**: 5
- **Example-based tests**: 12
- **Property-based tests**: 4
- **Total test cases**: 16
## Lean Commutativity Proofs
**Lean project**: proofs/
| # | Theorem | Status | Tactic |
|---|---------|--------|--------|
| 1 | init_commutes | proved | rfl |
| 2 | deposit_commutes | sorry | - |
| 3 | withdraw_commutes | proved | simp; omega |
| 4 | getBalance_commutes | proved | rfl |
| 5 | closeAccount_commutes | sorry | - |
### Summary
- **Total obligations**: 5
- **Proved**: 3
- **Remaining (sorry)**: 2
- **Proof coverage**: 60%
Suggest concrete next steps based on the results:
npm test / swift test /
pytest / gradle test"--lean was used with remaining sorry markers: "To
discharge remaining proofs, open proofs/ZSpec/Refinement/ Commutativity.lean in VS Code with the Lean 4 extension."/z-spec:partition to derive
systematic test inputs, then use those values in the
commutativity tests."When re-running refinement for a specification that already has refinement artifacts:
.new
file and show a diff.sorry replaced
with real proofs. Check each theorem: if the body is not
sorry, preserve it.| Error | Response |
|---|---|
| Specification not found | "No Z specification found. Specify path or create one with /z-spec:code2model." |
| No state schemas | "No state schemas found in the specification. Cannot define refinement without abstract state." |
| No operation schemas | "No operation schemas found. Generating only init commutativity test." |
| Implementation not found | "Could not locate implementation code for {StateName}. Specify the file path: /z-spec:refine spec.tex typescript --impl src/account.ts" |
| Language not detected | "Could not detect target language. Specify explicitly: /z-spec:refine spec.tex typescript" |
| Lean not installed (with --lean) | "Lean 4 is not installed. Run /z-spec:setup lean to install via elan, or omit --lean." |
| Lake not installed (with --lean) | "Lake not found. It should be included with Lean 4. Run elan toolchain install leanprover/lean4:v4.16.0." |
lake build fails | Show errors, suggest fixes, keep sorry markers. |
lake build timeout | "Build timed out after 120s. Try cd proofs && lake build manually." |
| Parse error in schema | "Could not parse schema {name}. Skipping." (continue with others) |
| No matching concrete field | "Could not match abstract field {field} to any concrete field. Mark as TODO in abstraction function." |
| Abstraction file already exists | "Abstraction function file already exists. Generating {name}.abstraction.new.ts for comparison." |
| Property testing library not found | "Property testing library not found. Install fast-check / hypothesis / SwiftCheck / kotest-property. Generating example-based tests only." |
Given this Z specification (docs/account.tex):
\begin{zed}
Status ::= pending | active | suspended | closed
\end{zed}
\begin{schema}{Account}
balance : \nat \\
status : Status
\where
balance \geq 0 \\
status = closed \implies balance = 0
\end{schema}
\begin{schema}{InitAccount}
Account'
\where
balance' = 0 \\
status' = pending
\end{schema}
\begin{schema}{Deposit}
\Delta Account \\
amount? : \nat_1
\where
status = active \\
balance' = balance + amount? \\
status' = status
\end{schema}
\begin{schema}{Withdraw}
\Delta Account \\
amount? : \nat_1
\where
status = active \\
amount? \leq balance \\
balance' = balance - amount? \\
status' = status
\end{schema}
\begin{schema}{GetBalance}
\Xi Account \\
result! : \nat
\where
result! = balance
\end{schema}
And this implementation (src/account.ts):
export enum StatusCode {
Pending = 'P',
Active = 'A',
Suspended = 'S',
Closed = 'C',
}
export class BankAccount {
balance: number;
statusCode: StatusCode;
lastModified: Date;
constructor() {
this.balance = 0;
this.statusCode = StatusCode.Pending;
this.lastModified = new Date();
}
deposit(amount: number): void {
if (amount <= 0) throw new Error('Amount must be positive');
if (this.statusCode !== StatusCode.Active) return;
this.balance += amount;
this.lastModified = new Date();
}
withdraw(amount: number): void {
if (amount <= 0) throw new Error('Amount must be positive');
if (this.statusCode !== StatusCode.Active) return;
if (amount > this.balance) return;
this.balance -= amount;
this.lastModified = new Date();
}
getBalance(): number {
return this.balance;
}
}
Running /z-spec:refine docs/account.tex typescript --generate-abstraction
produces:
src/account.abstraction.ts:
import { BankAccount, StatusCode } from './account';
// --- Abstract types (from Z spec) ---
export enum Status {
Pending = 'pending',
Active = 'active',
Suspended = 'suspended',
Closed = 'closed',
}
export interface AbstractAccount {
balance: number;
status: Status;
}
// --- Status code mapping ---
function mapStatusCode(code: StatusCode): Status {
const mapping: Record<StatusCode, Status> = {
[StatusCode.Pending]: Status.Pending,
[StatusCode.Active]: Status.Active,
[StatusCode.Suspended]: Status.Suspended,
[StatusCode.Closed]: Status.Closed,
};
return mapping[code];
}
// --- Abstraction function ---
/**
* Maps concrete BankAccount to abstract Account from Z spec.
*
* Abstract state: balance : Nat, status : Status
* Concrete state: balance, statusCode, lastModified
*
* VERIFY: confirm all mappings are correct.
*/
export function abstract(concrete: BankAccount): AbstractAccount {
return {
balance: concrete.balance, // Direct mapping
status: mapStatusCode(concrete.statusCode), // Translated
// NOTE: lastModified has no abstract counterpart
};
}
// --- Abstract operations (from Z spec) ---
export function abstractInit(): AbstractAccount {
return { balance: 0, status: Status.Pending };
}
export function depositPrecondition(
state: AbstractAccount,
amount: number,
): boolean {
return state.status === Status.Active && amount > 0;
}
export function abstractDeposit(
state: AbstractAccount,
amount: number,
): AbstractAccount {
return { balance: state.balance + amount, status: state.status };
}
export function withdrawPrecondition(
state: AbstractAccount,
amount: number,
): boolean {
return (
state.status === Status.Active &&
amount > 0 &&
amount <= state.balance
);
}
export function abstractWithdraw(
state: AbstractAccount,
amount: number,
): AbstractAccount {
return { balance: state.balance - amount, status: state.status };
}
export function abstractGetBalance(state: AbstractAccount): number {
return state.balance;
}
src/account.refinement.test.ts:
import { BankAccount, StatusCode } from './account';
import {
abstract,
abstractInit,
abstractDeposit,
abstractWithdraw,
abstractGetBalance,
depositPrecondition,
withdrawPrecondition,
} from './account.abstraction';
import fc from 'fast-check';
function createAccount(
balance: number,
statusCode: StatusCode,
): BankAccount {
const acct = new BankAccount();
acct.balance = balance;
acct.statusCode = statusCode;
return acct;
}
// --- Init commutativity ---
describe('Refinement: Init', () => {
it('concrete init abstracts to abstract init', () => {
const concrete = new BankAccount();
expect(abstract(concrete)).toEqual(abstractInit());
});
});
// --- Deposit commutativity ---
describe('Refinement: Deposit', () => {
it('commutes for typical deposit', () => {
const concrete = createAccount(100, StatusCode.Active);
const absBefore = abstract(concrete);
concrete.deposit(50);
expect(abstract(concrete)).toEqual(abstractDeposit(absBefore, 50));
});
it('commutes at boundary: zero balance', () => {
const concrete = createAccount(0, StatusCode.Active);
const absBefore = abstract(concrete);
concrete.deposit(1);
expect(abstract(concrete)).toEqual(abstractDeposit(absBefore, 1));
});
it('commutes at boundary: minimum amount', () => {
const concrete = createAccount(500, StatusCode.Active);
const absBefore = abstract(concrete);
concrete.deposit(1);
expect(abstract(concrete)).toEqual(abstractDeposit(absBefore, 1));
});
it('commutes for all valid inputs (property)', () => {
fc.assert(
fc.property(
fc.integer({ min: 0, max: 1000000 }),
fc.integer({ min: 1, max: 1000000 }),
(balance, amount) => {
const concrete = createAccount(balance, StatusCode.Active);
const absBefore = abstract(concrete);
fc.pre(depositPrecondition(absBefore, amount));
concrete.deposit(amount);
const absAfter = abstractDeposit(absBefore, amount);
expect(abstract(concrete)).toEqual(absAfter);
},
),
);
});
});
// --- Withdraw commutativity ---
describe('Refinement: Withdraw', () => {
it('commutes for typical withdrawal', () => {
const concrete = createAccount(200, StatusCode.Active);
const absBefore = abstract(concrete);
concrete.withdraw(50);
expect(abstract(concrete)).toEqual(
abstractWithdraw(absBefore, 50),
);
});
it('commutes at boundary: withdraw entire balance', () => {
const concrete = createAccount(100, StatusCode.Active);
const absBefore = abstract(concrete);
concrete.withdraw(100);
expect(abstract(concrete)).toEqual(
abstractWithdraw(absBefore, 100),
);
});
it('commutes at boundary: minimum withdrawal', () => {
const concrete = createAccount(100, StatusCode.Active);
const absBefore = abstract(concrete);
concrete.withdraw(1);
expect(abstract(concrete)).toEqual(
abstractWithdraw(absBefore, 1),
);
});
it('commutes for all valid inputs (property)', () => {
fc.assert(
fc.property(
fc.integer({ min: 1, max: 1000000 }),
fc.integer({ min: 1, max: 1000000 }),
(balance, amount) => {
const concrete = createAccount(balance, StatusCode.Active);
const absBefore = abstract(concrete);
fc.pre(withdrawPrecondition(absBefore, amount));
concrete.withdraw(amount);
const absAfter = abstractWithdraw(absBefore, amount);
expect(abstract(concrete)).toEqual(absAfter);
},
),
);
});
});
// --- GetBalance commutativity ---
describe('Refinement: GetBalance', () => {
it('concrete query matches abstract query', () => {
const concrete = createAccount(350, StatusCode.Active);
expect(concrete.getBalance()).toBe(
abstractGetBalance(abstract(concrete)),
);
});
it('matches for all valid states (property)', () => {
fc.assert(
fc.property(
fc.integer({ min: 0, max: 1000000 }),
fc.constantFrom(
StatusCode.Pending,
StatusCode.Active,
StatusCode.Suspended,
StatusCode.Closed,
),
(balance, statusCode) => {
const concrete = createAccount(balance, statusCode);
expect(concrete.getBalance()).toBe(
abstractGetBalance(abstract(concrete)),
);
},
),
);
});
});
Report:
## Abstraction Function
**Abstract state**: Account (balance, status)
**Concrete state**: BankAccount (balance, statusCode, lastModified)
| Abstract Field | Concrete Field | Mapping |
|----------------|----------------|---------|
| balance : Nat | balance: number | Direct (identity) |
| status : Status | statusCode: StatusCode | Translated via mapStatusCode |
| - | lastModified: Date | Ignored (implementation detail) |
## Commutativity Tests
**Specification**: docs/account.tex
**Implementation**: src/account.ts
| # | Operation | Kind | Example tests | Property tests | Status |
|---|-----------|------|---------------|----------------|--------|
| 1 | Init | init | 1 | - | generated |
| 2 | Deposit | Delta | 3 | 1 | generated |
| 3 | Withdraw | Delta | 3 | 1 | generated |
| 4 | GetBalance | Xi | 1 | 1 | generated |
### Summary
- **Operations covered**: 4
- **Example-based tests**: 8
- **Property-based tests**: 3
- **Total test cases**: 11
### Generated Files
- `src/account.abstraction.ts` (abstraction function + abstract operations)
- `src/account.refinement.test.ts` (commutativity tests)
### Next Steps
1. **Review the abstraction function** in `src/account.abstraction.ts`.
This is the critical piece -- an incorrect mapping will make tests
pass even when the implementation is wrong.
2. Run `npm test` to execute the commutativity tests.
3. If any test fails, check (in order): abstraction function,
implementation code, abstract operation function.
4. For systematic test inputs, run `/z-spec:partition docs/account.tex`
and incorporate the partition values.
Always type-check the specification before running refinement.
/z-spec:check validates Z syntax; /z-spec:refine verifies
that the implementation correctly refines the spec.
/z-spec:model2code generates implementation code from the spec.
/z-spec:refine then verifies that the generated (or modified)
code still correctly refines the spec. They form a natural
workflow: generate, customize, then verify.
/z-spec:prove generates invariant preservation proofs about
the specification itself. /z-spec:refine --lean generates
commutativity proofs that the implementation refines the spec.
Together they provide two layers: the spec is internally
consistent (prove), and the code implements the spec (refine).
/z-spec:partition derives systematic test inputs via TTF tactics.
These partition values are excellent inputs for commutativity
tests. Run partition first, then use those values in refinement
tests for maximum coverage.
/z-spec:test uses random operation sequences to check the
implementation against the spec via ProB animation. /z-spec:refine
proves commutativity per-operation with an explicit abstraction
function. Oracle testing finds bugs through exploration; refinement
provides a structured correctness argument. This command provides
the strongest correctness guarantee available in the plugin.
reference/z-notation.mdreference/schema-patterns.mdreference/lean4-patterns.mdreference/test-patterns.md