Skip to main content

lower_bool_within

logicaffeine_compile::codegen_sva::bitblast

Function lower_bool_within 

Source 
pub fn lower_bool_within(
    e: &BoundedExpr,
    budget: u128,
) -> Result<ProofExpr, BlastRefusal>
Expand description

lower_bool_bounded against an EXPLICIT ceiling. The production ceiling is BLAST_BUDGET_NODES; a caller passing its own is how a lock proves the guard is live code — shrink the ceiling and an obligation that certifies must come back Budget, with the same arithmetic, not a special case.