Module kinduction 

k-Induction for Unbounded Safety Verification

BMC proves a property holds for k cycles. k-Induction proves it holds forever.

Algorithm:

1. For k = 1, 2, …, max_k: a. Base case: init AND T^k AND NOT(P) at each step. If UNSAT → base passes. b. Inductive step: P holds for k consecutive steps AND T AND NOT(P) at step k+1. If UNSAT → proven.
2. If base fails → Counterexample. If induction fails for all k → InductionFailed.

Structs

SignalDecl

Signal declaration for k-induction.

Enums

KInductionResult

Result of k-induction verification.

Functions

encode_expr_bool

Simple recursive Bool encoder for k-induction formulas.

encode_expr_int

Try to encode an expression as a Z3 Int. Returns None if not integer-typed.

instantiate_at

Instantiate an expression at a specific timestep by replacing @t with @{step}.

instantiate_transition

Instantiate a transition relation: replace @t with @{step} and @t’ with @{step+1}.

k_induction

Run k-induction on a safety property.