This module contains the verification of the BitVec expressions (BVExpr) bitblaster from Impl.Expr.

@[reducible, inline]

abbrev Std.Tactic.BVDecide.BVExpr.Cache.Inv (assign : Assignment) (aig : Sat.AIG BVBit) (cache : Cache aig) : Prop

Equations

• One or more equations did not get rendered due to their size.

theorem Std.Tactic.BVDecide.BVExpr.Cache.Inv_empty {assign : Assignment} (aig : Sat.AIG BVBit) : Inv assign aig empty

theorem Std.Tactic.BVDecide.BVExpr.Cache.Inv_cast {aig1 : Sat.AIG BVBit} {assign : Assignment} {aig2 : Sat.AIG BVBit} (cache : Cache aig1) (hpref : Sat.AIG.IsPrefix aig1.decls aig2.decls) (hinv : Inv assign aig1 cache) : Inv assign aig2 (cache.cast ⋯)

theorem Std.Tactic.BVDecide.BVExpr.Cache.Inv_insert {aig : Sat.AIG BVBit} {w : Nat} {assign : Assignment} (cache : Cache aig) (expr : BVExpr w) (refs : aig.RefVec w) (hinv : Inv assign aig cache) (hrefs : ∀ (idx : Nat) (hidx : idx < w), ⟦assign.toAIGAssignment, { aig := aig, ref := refs.get idx hidx }⟧ = (eval assign expr).getLsbD idx) : Inv assign aig (cache.insert expr refs)

theorem Std.Tactic.BVDecide.BVExpr.Cache.get?_eq_some_iff {aig : Sat.AIG BVBit} {w : Nat} {refs : aig.RefVec w} (cache : Cache aig) (expr : BVExpr w) : cache.get? expr = some refs ↔ cache.map.get? { w := w, expr := expr } = some refs.refs

theorem Std.Tactic.BVDecide.BVExpr.Cache.denote_eq_eval_of_get?_eq_some_of_Inv {aig : Sat.AIG BVBit} {w : Nat} {assign : Assignment} (cache : Cache aig) (expr : BVExpr w) (refs : aig.RefVec w) (hsome : cache.get? expr = some refs) (hinv : Inv assign aig cache) (i : Nat) (h : i < w) : ⟦assign.toAIGAssignment, { aig := aig, ref := refs.get i h }⟧ = (eval assign expr).getLsbD i

theorem Std.Tactic.BVDecide.BVExpr.bitblast.goCache_val_eq_bitblast {w : Nat} (aig : Sat.AIG BVBit) (expr : BVExpr w) (cache : Cache aig) : goCache aig expr cache = bitblast aig { val := expr, cache := cache }

theorem Std.Tactic.BVDecide.BVExpr.bitblast.go_denote_mem_prefix {w : Nat} {inv : Bool} (aig : Sat.AIG BVBit) (expr : BVExpr w) (assign : Assignment) (cache : Cache aig) (start : Nat) (hstart : start < aig.decls.size) : ⟦assign.toAIGAssignment, { aig := (go aig expr cache).result.val.aig, ref := { gate := start, invert := inv, hgate := ⋯ } }⟧ = ⟦assign.toAIGAssignment, { aig := aig, ref := { gate := start, invert := inv, hgate := hstart } }⟧

theorem Std.Tactic.BVDecide.BVExpr.bitblast.goCache_denote_mem_prefix {w : Nat} {inv : Bool} (aig : Sat.AIG BVBit) (expr : BVExpr w) (assign : Assignment) (cache : Cache aig) (start : Nat) (hstart : start < aig.decls.size) : ⟦assign.toAIGAssignment, { aig := (goCache aig expr cache).result.val.aig, ref := { gate := start, invert := inv, hgate := ⋯ } }⟧ = ⟦assign.toAIGAssignment, { aig := aig, ref := { gate := start, invert := inv, hgate := hstart } }⟧

@[irreducible]

theorem Std.Tactic.BVDecide.BVExpr.bitblast.goCache_Inv_of_Inv {aig : Sat.AIG BVBit} {assign : Assignment} {w : Nat} (cache : Cache aig) (hinv : Cache.Inv assign aig cache) (expr : BVExpr w) : Cache.Inv assign (goCache aig expr cache).result.val.aig (goCache aig expr cache).cache

@[irreducible]

theorem Std.Tactic.BVDecide.BVExpr.bitblast.go_Inv_of_Inv {aig : Sat.AIG BVBit} {assign : Assignment} {w : Nat} (cache : Cache aig) (hinv : Cache.Inv assign aig cache) (expr : BVExpr w) : Cache.Inv assign (go aig expr cache).result.val.aig (go aig expr cache).cache

@[irreducible]

theorem Std.Tactic.BVDecide.BVExpr.bitblast.goCache_denote_eq {w : Nat} (aig : Sat.AIG BVBit) (expr : BVExpr w) (assign : Assignment) (cache : Cache aig) (hinv : Cache.Inv assign aig cache) (idx : Nat) (hidx : idx < w) : ⟦assign.toAIGAssignment, { aig := (goCache aig expr cache).result.val.aig, ref := (goCache aig expr cache).result.val.vec.get idx hidx }⟧ = (eval assign expr).getLsbD idx

@[irreducible]

theorem Std.Tactic.BVDecide.BVExpr.bitblast.go_denote_eq {w : Nat} (aig : Sat.AIG BVBit) (expr : BVExpr w) (assign : Assignment) (cache : Cache aig) (hinv : Cache.Inv assign aig cache) (idx : Nat) (hidx : idx < w) : ⟦assign.toAIGAssignment, { aig := (go aig expr cache).result.val.aig, ref := (go aig expr cache).result.val.vec.get idx hidx }⟧ = (eval assign expr).getLsbD idx

theorem Std.Tactic.BVDecide.BVExpr.bitblast_aig_IsPrefix {w : Nat} (aig : Sat.AIG BVBit) (input : WithCache (BVExpr w) aig) : Sat.AIG.IsPrefix aig.decls (bitblast aig input).result.val.aig.decls

theorem Std.Tactic.BVDecide.BVExpr.bitblast_denote_mem_prefix {w : Nat} {inv : Bool} (aig : Sat.AIG BVBit) (input : WithCache (BVExpr w) aig) (assign : Assignment) (start : Nat) (hstart : start < aig.decls.size) : ⟦assign.toAIGAssignment, { aig := (bitblast aig input).result.val.aig, ref := { gate := start, invert := inv, hgate := ⋯ } }⟧ = ⟦assign.toAIGAssignment, { aig := aig, ref := { gate := start, invert := inv, hgate := hstart } }⟧

theorem Std.Tactic.BVDecide.BVExpr.bitblast_Inv_of_Inv {w : Nat} {aig : Sat.AIG BVBit} {assign : Assignment} (input : WithCache (BVExpr w) aig) (hinv : Cache.Inv assign aig input.cache) : Cache.Inv assign (bitblast aig input).result.val.aig (bitblast aig input).cache

theorem Std.Tactic.BVDecide.BVExpr.denote_bitblast {w : Nat} (aig : Sat.AIG BVBit) (input : WithCache (BVExpr w) aig) (assign : Assignment) (hinv : Cache.Inv assign aig input.cache) (idx : Nat) (hidx : idx < w) : ⟦assign.toAIGAssignment, { aig := (bitblast aig input).result.val.aig, ref := (bitblast aig input).result.val.vec.get idx hidx }⟧ = (eval assign input.val).getLsbD idx