-- ========================================================================
--            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-rr-sr {
ex(ABP-INV-3 + GENst + CONST-LITL) pr(SS + RS + 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-ss-rs-rr-sr .
pr(IINV) pr(FACTtbu)
-- (iinv1 iinv2) = (st ft sr rs)
eq pre = iinv1 iinv2 . eq post = iinv1 iinv2 .
red check(sst) .
-- q.e.d.
close

-- ========================================================================
mod! ABP-INV-3-genCheck-srdr-srdu-rsdr-rsdu {
ex(ABP-INV-3 + GENst + CONST-LITL) pr(SRdr + SRdu + RSdr + RSdu)
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),
                (g("rsCh_")[empB;(g("rs___")[rsc1,(t;f),rsc2])])]),
 SS:PreState,BB:Bool] .
}
open ABP-INV-3-genCheck-srdr-srdu-rsdr-rsdu .
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

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