Install with Codex or Claude Copy this prompt, paste it into Codex, Claude, or another assistant, and let it review the skill page and install it for you.
A direct command skips the review prompt. Inspect the source before running it.
"""
{P ∧ B} C₁ {Q} {P ∧ ¬B} C₂ {Q}
───────────────────────────────────
{P} if B then C₁ else C₂ {Q}
"""
# Verify both branches
def
P_and_B
state
return
and
def
P_and_not_B
state
return
and
not
# Would need to verify {P ∧ B} C₁ {Q} and {P ∧ ¬B} C₂ {Q}
return
True
# Simplified
def
hoare_while
I: Assertion, B, C: Command
bool
"""
{I ∧ B} C {I}
────────────────────────
{I} while B do C {I ∧ ¬B}
I: loop invariant
Must prove:
1. I preserved by loop body when B true
2. After loop, I ∧ ¬B holds
"""
# Verify loop invariant preservation
def
I_and_B
state
return
and
# Would verify {I ∧ B} C {I}
return
True
# Simplified
def
eval_expr
expr, state: dict
"""Evaluate expression in state"""
# Simplified evaluation
return
# Example: Prove {x = 5} x := x + 1 {x = 6}
def
example_assign
# Postcondition: x = 6
lambda
'x'
6
# Precondition: Q[x := x+1] = (x+1 = 6) = (x = 5)
lambda
'x'
1
6
# Verify
'x'
5
assert
# Execute x := x + 1
'x'
'x'
1
assert
print
"Verified: {x = 5} x := x + 1 {x = 6}"
Weakest Precondition
wp(C, Q): Weakest precondition - most general P such that {P} C {Q}
defweakest_precondition(cmd: Command, Q: Assertion) -> Assertion:
"""
Compute wp(C, Q) - weakest precondition
"""match cmd:
case Skip():
# wp(skip, Q) = Qreturn Q
case Assign(var, expr):
# wp(x := e, Q) = Q[x := e]returnlambda state: Q(state | {var: eval_expr(expr, state)})
case Seq(C1, C2):
# wp(C₁; C₂, Q) = wp(C₁, wp(C₂, Q))
wp_C2 = weakest_precondition(C2, Q)
return weakest_precondition(C1, wp_C2)
case If(B, C1, C2):
# wp(if B then C₁ else C₂, Q) = (B ⟹ wp(C₁, Q)) ∧ (¬B ⟹ wp(C₂, Q))
wp_C1 = weakest_precondition(C1, Q)
wp_C2 = weakest_precondition(C2, Q)
returnlambda state: (
(eval_expr(B, state) and wp_C1(state)) or
(not eval_expr(B, state) and wp_C2(state))
)
case While(B, body):
# wp(while B do C, Q) requires loop invariant# For now, return Q (simplified)return Q
# Example: wp(x := x + 1; y := x * 2, y = 12)
C1 = Assign('x', lambda s: s['x'] + 1)
C2 = Assign('y', lambda s: s['x'] * 2)
program = Seq(C1, C2)
postcondition = lambda s: s['y'] == 12
wp = weakest_precondition(program, postcondition)
# wp should be: x + 1 * 2 = 12, i.e., x = 5
state = {'x': 5, 'y': 0}
print(f"wp holds for x=5: {wp(state)}")
Refinement Types
Refinement type: {x:τ | P(x)} - type τ refined by predicate P
@dataclassclassRefinementType:
"""Refinement type: {x:τ | P(x)}"""
base_type: type
predicate: Callable[[any], bool]
defcheck(self, value):
"""Check if value satisfies refinement"""ifnotisinstance(value, self.base_type):
returnFalsereturnself.predicate(value)
# Examples
Pos = RefinementType(int, lambda x: x > 0)
Nat = RefinementType(int, lambda x: x >= 0)
NonZero = RefinementType(int, lambda x: x != 0)
defsafe_div(a: int, b: int) -> int:
"""
Type: (a:int) → (b:int) → {b ≠ 0} → int
Requires proof that b ≠ 0
"""assert NonZero.check(b), "Division by zero"return a // b
# Usage
result = safe_div(10, 2) # OKprint(f"10 / 2 = {result}")
try:
result = safe_div(10, 0) # Error: assertion failsexcept AssertionError as e:
print(f"Error: {e}")
# In Liquid Haskell:"""
{-@ type Pos = {v:Int | v > 0} @-}
{-@ type NonZero = {v:Int | v /= 0} @-}
{-@ div :: Int -> NonZero -> Int @-}
div :: Int -> Int -> Int
div x y = x `div` y
-- Type checker ensures y ≠ 0 at call sites
"""
SMT-Based Verification
Using Z3 for verification:
try:
from z3 import Int, Solver, sat, And, Or, Not
defverify_program_z3():
"""
Verify: {x ≥ 0} if x < 10 then y := x else y := 10 {y < 11}
Using Z3 SMT solver
"""
x, y, y_out = Int('x'), Int('y'), Int('y_out')
# Precondition: x ≥ 0
P = x >= 0# Program semantics
branch1 = And(x < 10, y_out == x) # Then: y := x
branch2 = And(x >= 10, y_out == 10) # Else: y := 10
program = Or(branch1, branch2)
# Postcondition: y < 11
Q = y_out < 11# Verify: ¬(P ∧ program ⟹ Q)# If unsatisfiable, then {P} program {Q} is valid
solver = Solver()
solver.add(P)
solver.add(program)
solver.add(Not(Q))
if solver.check() == sat:
print(f"Counterexample: {solver.model()}")
returnFalseelse:
print("Verified: {x ≥ 0} program {y < 11}")
returnTrue
verify_program_z3()
except ImportError:
print("Z3 not available, skipping SMT verification example")
Separation Logic
Heap assertions: P * Q (P and Q hold on disjoint heap parts)
@dataclassclassPointsTo:
"""x ↦ v - heap location x contains value v"""
location: str
value: any@dataclassclassSeparatingConjunction:
"""P * Q - P and Q hold on disjoint heaps"""
left: 'HeapAssertion'
right: 'HeapAssertion'@dataclassclassEmp:
"""emp - empty heap"""pass
HeapAssertion = Union[PointsTo, SeparatingConjunction, Emp]
# Frame rule (key rule in separation logic):"""
{P} C {Q}
─────────────────── (Frame)
{P * R} C {Q * R}
If R describes heap C doesn't touch, it's preserved
"""defframe_rule_example():
"""
Example: {x ↦ 5} *p := 10 {x ↦ 5}
where p and x are different locations
Frame rule:
{emp} *p := 10 {p ↦ 10}
─────────────────────────────── (Frame)
{emp * x ↦ 5} *p := 10 {p ↦ 10 * x ↦ 5}
"""print("Frame rule: Unmodified heap portions preserved")
frame_rule_example()
Patterns
Pattern 1: Loop Invariants
defverify_loop_invariant():
"""
Verify: {n ≥ 0} i := 0; s := 0; while i < n do (s := s + i; i := i + 1) {s = n*(n-1)/2}
Loop invariant: s = i*(i-1)/2 ∧ i ≤ n
"""# Precondition: n ≥ 0# After i := 0; s := 0: s = 0 ∧ i = 0 (implies invariant)# Invariant: s = i*(i-1)/2 ∧ i ≤ n# Body preserves invariant when i < n# After loop: i = n ∧ s = i*(i-1)/2 = n*(n-1)/2print("Loop invariant: s = i*(i-1)/2 ∧ i ≤ n")
verify_loop_invariant()
Pattern 2: Verification Conditions
defgenerate_verification_conditions(cmd: Command, Q: Assertion) -> list:
"""
Generate verification conditions (VCs) for program
VCs are formulas to prove for correctness
"""
vcs = []
# Example: for loop, generate:# 1. Invariant initially true# 2. Invariant preserved by body# 3. Invariant + ¬condition implies postconditionmatch cmd:
case While(cond, body):
# Would generate 3 VCs abovepassreturn vcs
Quick Reference
Hoare Logic Rules
{P} skip {P} (Skip)
{P[x := e]} x := e {P} (Assign)
{P} C₁ {R} {R} C₂ {Q}
──────────────────────── (Seq)
{P} C₁; C₂ {Q}
{P ∧ B} C₁ {Q} {P ∧ ¬B} C₂ {Q}
────────────────────────────────── (If)
{P} if B then C₁ else C₂ {Q}
{I ∧ B} C {I}
──────────────────────── (While)
{I} while B do C {I ∧ ¬B}
