SLOP

`choir.cfg.predecessor-mirror`

Reference tiny.choir Verification choir.cfg.predecessor-mirror

Connection

Lean proves selected CFG model invariants. A bounded Zig property exercises the related public block-mutation API.

Relationship: Executable property. This record does not imply whole-program verification.

Scope. A generated state machine exercises attach, successor replacement, detach, move, and remove actions. After each action it checks parent links, the Boolean predecessor mirror, predecessor counts, and verifyBlock.

Public API	Binding	Canonical implementation
`tiny.choir.Block.addOperation`	`lib/choir/src/core/block.zig`	`lib/choir/src/core/block.zig`
`tiny.choir.Operation.setSuccessors`	`lib/choir/src/core/operation/model.zig`	`lib/choir/src/core/operation/model.zig`
`tiny.choir.Block.detachOperation`	`lib/choir/src/core/block.zig`	`lib/choir/src/core/block.zig`
`tiny.choir.Operation.moveToEnd`	`lib/choir/src/core/operation/model.zig`	`lib/choir/src/core/operation/model.zig`
`tiny.choir.Block.removeOperation`	`lib/choir/src/core/block.zig`	`lib/choir/src/core/block.zig`
`tiny.choir.Block.hasPredecessor`	`lib/choir/src/core/block.zig`	`lib/choir/src/core/block.zig`
`tiny.choir.Block.getNumPredecessors`	`lib/choir/src/core/block.zig`	`lib/choir/src/core/block.zig`
`tiny.choir.ir.verifyBlock`	`lib/choir/src/core/root.zig`	`lib/choir/src/core/verify.zig`

Lean audit

These theorem declarations describe the Lean model. Their recorded axioms are shown explicitly; the claims do not by themselves establish refinement by the Zig implementation.

Theorem	Module	Axioms
`verification/choir/Choir/IR/CFG/Transition.lean` `Choir.IR.CFG.Reachable.preserves_consistency`	`Choir.IR.CFG.Transition`	None recorded
`verification/choir/Choir/IR/CFG/Verification.lean` `Choir.IR.CFG.exact_check_eq_true_iff_runtime_consistent`	`Choir.IR.CFG.Verification`	`propext` `Quot.sound`
`verification/choir/Choir/IR/CFG/Preservation.lean` `Choir.IR.CFG.empty_predecessors_license_erasure`	`Choir.IR.CFG.Preservation`	None recorded
`verification/choir/Choir/IR/CFG/Necessity.lean` `Choir.IR.CFG.Necessity.guarded_erase_keeps_duplicate_support`	`Choir.IR.CFG.Necessity`	None recorded
`verification/choir/Choir/IR/CFG/Necessity.lean` `Choir.IR.CFG.Necessity.unguarded_erase_breaks_runtime_consistency`	`Choir.IR.CFG.Necessity`	None recorded

Executable evidence

`choir.cfg.predecessor-mirror.property`

Recorded outcome: passed.

Producer. choir-cfg-evidence/v1

Command. zig build choir-cfg-evidence

Sources.

Bounds

Fact	Value
`actions_per_example_max`	64
`actions_per_example_min`	1
`blocks`	4
`examples`	200
`operations`	6
`seed`	0xc6f020260728
`successors_per_operation_max`	3

Coverage

Fact	Value
`tiny.choir.Block.addOperation`	1015
`tiny.choir.Block.detachOperation`	327
`tiny.choir.Block.removeOperation`	321
`tiny.choir.Operation.moveToEnd`	354
`tiny.choir.Operation.setSuccessors`	1262

Checks

Fact	Value
`model.operation.parent`	19674
`tiny.choir.Block.getNumPredecessors`	13116
`tiny.choir.Block.hasPredecessor`	52464
`tiny.choir.ir.verifyBlock`	13116

Recorded nonclaims

Zig-to-Lean refinement proof or Zig source correctness proof
allocation and out-of-memory rollback
arbitrary block, operation, successor, or trace sizes
concurrency
dominance
nested regions
operation-order cache repair
pointer identity
traits and interfaces
use-def chains

Freshness

Publication-qualified. The catalog records a clean tree at the exact revision used for this publication: daab053ee43316e1809a84551d573ddd1e5bf3d2.

Limitations

The property does not prove that production Zig refines the Lean CFG model.
The recorded property run covers the build host, not every supported target.
The property covers a bounded generated state space, not arbitrary programs.
Allocation failure, concurrency, nested regions, dominance, use-def chains, operation-order repair, and pointer behavior are outside this capability.

Audit

Capability	`choir.cfg.predecessor-mirror`
Relationship	Executable property
Public APIs	8
Lean claims	5
Evidence records	1
Catalog schema	`tiny.verification.catalog/v1`
Source revision	`daab053ee43316e1809a84551d573ddd1e5bf3d2`