-- ========================================================================
--            ABP Proof score for invariant properties
--                the third verification condition 
-- ========================================================================

-- ========================================================================
require abp-genCheck
require abp-genSt
require abp-constLitl
require abp-factTbu

-- ========================================================================
mod! ABP-INV-3-genCheck-ss-rs {
ex(ABP-INV-3 + GENst + CONST-LITL) pr(SS + RS)
op sst : -> SqSqTr .
eq sst = 
[(g("[______]")[(g("sBit_")[t;f]),(sNn: n1),(g("srCh_")[src1]),
              (g("rBit_")[t;f]),(rNns: ns1),(g("rsCh_")[rsc1])]),
 SS:PreState,BB:Bool] .
}
open ABP-INV-3-genCheck-ss-rs .
pr(IINV)
eq pre = iinv1 iinv2 . eq post = iinv1 iinv2 .
red check(sst) .
close

-- ========================================================================
mod! ABP-INV-3-genCheck-rr-sr {
ex(ABP-INV-3 + GENst + CONST-LITL) pr(RR + SR)
op sst : -> SqSqTr .
-- n1 n2 are literals
eq sst = 
[(g("[______]")
   [(g("sBit_")[t;f]),(sNn: n1),
    (g("srCh_")[(g("_sr_")[src1,(g("bn__")[(t;f),(n1;n2)])])]),
    (g("rBit_")[t;f]),(rNns: ns1),
    (g("rsCh_")[(g("_rs_")[rsc1,(t;f)])])]),
 SS:PreState,BB:Bool] .
}
open ABP-INV-3-genCheck-rr-sr .
pr(IINV) pr(FACTtbu)
-- (iinv1 iinv2) = (st ft sr rs)
eq pre = iinv1 iinv2 . eq post = iinv1 iinv2 .
red check(sst) .
close

-- ========================================================================
mod! ABP-INV-3-genCheck-srdr-srdu {
ex(ABP-INV-3 + GENst + CONST-LITL) pr(SRdr + SRdu)
op sst : -> SqSqTr .
-- n1 n2 are Nn literals declared in CONST-LITL
eq sst = 
[(g("[______]")[(g("sBit_")[t;f]),(sNn: n1),
              (g("srCh_")[empBN;(g("sr___")
                                [src1,
                                 (g("bn__")[(t;f),(n1;n2)]),
                                 src2])]),
              (g("rBit_")[t;f]),(rNns: ns1),
              (rsCh: rsc1)]),
 SS:PreState,BB:Bool] .
}
open ABP-INV-3-genCheck-srdr-srdu .
pr(IINV) pr(FACTtbu)
eq pre = iinv1 iinv2 . eq post = iinv1 iinv2 .
:goal{eq check(sst) = $ .}
:ctf{eq n2 = p n1 .}
-- q.e.d.
close

-- ========================================================================
mod! ABP-INV-3-genCheck-rsdr-rsdu {
ex(ABP-INV-3 + GENst + CONST-LITL) pr(RSdr + RSdu)
op sst : -> SqSqTr .
eq sst = 
[(g("[______]")[(g("sBit_")[t;f]),(sNn: n1),(srCh: src1),
              (g("rBit_")[t;f]),(rNns: ns1),
              (g("rsCh_")[empB;(g("rs___")[rsc1,(t;f),rsc2])])]),
 SS:PreState,BB:Bool] .
}
open ABP-INV-3-genCheck-rsdr-rsdu .
pr(IINV) pr(FACTtbu)
eq pre = iinv1 iinv2 . eq post = iinv1 iinv2 .
red check(sst) .
close

-- ========================================================================
eof