This module contains the verification of the bitblaster for BitVec.signExtend from
Impl.Operations.SignExtend.
@[irreducible]
theorem
Std.Tactic.BVDecide.BVExpr.bitblast.blastSignExtend.go_get_aux
{α : Type}
[Hashable α]
[DecidableEq α]
(aig : Std.Sat.AIG α)
(w : Nat)
(hw : 0 < w)
(input : aig.RefVec w)
(newWidth : Nat)
(curr : Nat)
(hcurr : curr ≤ newWidth)
(s : aig.RefVec curr)
(idx : Nat)
(hidx1 : idx < curr)
:
(Std.Tactic.BVDecide.BVExpr.bitblast.blastSignExtend.go w hw input newWidth curr hcurr s).get idx ⋯ = s.get idx hidx1
@[irreducible]
theorem
Std.Tactic.BVDecide.BVExpr.bitblast.blastSignExtend.go_get
{α : Type}
[Hashable α]
[DecidableEq α]
(aig : Std.Sat.AIG α)
(w : Nat)
(hw : 0 < w)
(input : aig.RefVec w)
(newWidth : Nat)
(curr : Nat)
(hcurr : curr ≤ newWidth)
(s : aig.RefVec curr)
(idx : Nat)
(hidx1 : idx < newWidth)
:
curr ≤ idx →
(Std.Tactic.BVDecide.BVExpr.bitblast.blastSignExtend.go w hw input newWidth curr hcurr s).get idx hidx1 = if hidx2 : idx < w then input.get idx ⋯ else input.get (w - 1) ⋯
theorem
Std.Tactic.BVDecide.BVExpr.bitblast.blastSignExtend_empty_eq_zeroExtend
{α : Type}
[Hashable α]
[DecidableEq α]
{newWidth : Nat}
(aig : Std.Sat.AIG α)
(target : aig.ExtendTarget newWidth)
(htarget : target.w = 0)
:
theorem
Std.Tactic.BVDecide.BVExpr.bitblast.denote_blastSignExtend
{α : Type}
[Hashable α]
[DecidableEq α]
{newWidth : Nat}
(aig : Std.Sat.AIG α)
(target : aig.ExtendTarget newWidth)
(assign : α → Bool)
(htarget : 0 < target.w)
(idx : Nat)
(hidx : idx < newWidth)
:
⟦assign,
{ aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastSignExtend aig target).aig,
ref := (Std.Tactic.BVDecide.BVExpr.bitblast.blastSignExtend aig target).vec.get idx hidx }⟧ = if hidx : idx < target.w then ⟦assign, { aig := aig, ref := target.vec.get idx hidx }⟧
else ⟦assign, { aig := aig, ref := target.vec.get (target.w - 1) ⋯ }⟧