dfunction.ath

load "dpair.ath"
load "function.ath"
define lAlive := Location.alive 


module DFunction {
    open Function
    assert (theory-axioms Function.theory)
    # Declarations
    declare alive: (D,R) [(DPr (fn D R) (fn D R))] -> Boolean

    declare apply: (D,R) [(DPr (fn D R) (fn D R)) D] -> (Option R) 

    declare functionReplica: (D,R) [(fn D R) Location Location] 
                                   -> (DPr (fn D R) (fn D R))

    declare replicaComposition: (A, B, C) [(DPr (fn A B) (fn A B)) (DPr (fn B C) (fn B C))] 
                                          -> (DPr (fn A C) (fn A C))

    # Definitions

    define [f g x l1 l0 lg lg0 lg1 lf0 lf1] := 
           [?f:(fn 'D 'R) ?g:(fn 'R 'O) ?x:'D ?l1:Location ?l0:Location
            ?lg:Location ?lg0:Location ?lg1:Location ?lf0:Location ?lf1:Location]

    define rComp := 
            (replicaComposition (functionReplica f lf0 lf1) (functionReplica g lg0 lg1))
            # g(f(x))

    # Asserts

    assert* alive_axiom := (iff (alive (dpr l1 f l0 f)) ((lAlive l1) or (lAlive l0)))

    assert* function_replica_axiom := ((functionReplica f l1 l0) = (dpr l1 f l0 f))

    assert apply_axioms :=
    (fun [
        (apply (functionReplica f l1 l0) x) = 
            [
                (SOME (f at x)) when (alive (functionReplica f l1 l0))
                NONE            when (~(alive (functionReplica f l1 l0)))
            ]

    ])

    # NOTE: both guards must name the SAME replica, `(functionReplica f lf0 lf1)`
    # — the one that actually occurs in `rComp`. An earlier version wrote the
    # negative guard over `(functionReplica f l1 l0)`, and since `l1`/`l0` are
    # pattern variables distinct from `lf0`/`lf1`, `fun` quantified them
    # independently of the composition's own sites. That let the NONE clause be
    # instantiated at an unrelated dead pair while the composition's own sites
    # were alive, so the same term was provably both `NONE` and
    # `(SOME (g at (f at x)))` — an inconsistent assumption base, and with it a
    # vacuous `fault_tolerance_correctness`.
    assert apply_composition_axiom :=
    (fun [
        (apply rComp x) =
            [
                (apply (functionReplica g lg0 lg1 ) (f at x))  when (alive (functionReplica f lf0 lf1))
                NONE                         when (~(alive (functionReplica f lf0 lf1)))
            ]
    ])


    # Theorem Definitions

    define fault_tolerance_correctness :=
    (forall x f l1 l0 .
        (if
            ((lAlive l1) or (lAlive l0))
            ((apply (functionReplica f l1 l0) x) = (SOME (f at x)))
        )
    )

    define fault_tolerance_correctness_composition :=
    (forall x f g lg0 lg1 lf0 lf1 .
        (if
            (((lAlive lf0) or (lAlive lf1)) and ((lAlive lg0) or (lAlive lg1)))
            ((apply rComp x) = (SOME (g o f) at x))
            # g(f(x))
        )
    )

    # Theorem Proofs

    conclude fault_tolerance_correctness
        pick-any x:'D f:(fn 'D 'R) l1:Location l0:Location
            assume((lAlive l1) or (lAlive l0))
                let {
                    _ := 
                        (!chain<- [
                            (alive (functionReplica f l1 l0))
                            <== (alive (dpr l1 f l0 f))           [function_replica_axiom]
                            <== ((lAlive l1) or (lAlive l0))                 [alive_axiom]
                        ])
                }
                (!chain [
                    (apply (functionReplica f l1 l0) x) 
                    = (SOME (f at x))                                       [apply_axioms]
                ])

    conclude fault_tolerance_correctness_composition
        pick-any x:'D f:(fn 'D 'R) g:(fn 'R 'O) lg0:Location lg1:Location lf0:Location lf1:Location
            assume hyp := (((lAlive lf0) or (lAlive lf1)) and ((lAlive lg0) or (lAlive lg1)))
                let {
                    alive_functionReplica_f :=
                        (!chain<- [
                            (alive (functionReplica f lf0 lf1))
                            <== (alive (dpr lf0 f lf1 f))         [function_replica_axiom]
                            <== ((lAlive lf0) or (lAlive lf1))               [alive_axiom]
                        ]);
                    alive_functionReplica_g :=
                        (!chain<- [
                            (alive (functionReplica g lg0 lg1))
                            <== (alive (dpr lg0 g lg1 g))         [function_replica_axiom]
                            <== ((lAlive lg0) or (lAlive lg1))               [alive_axiom]
                        ])
                }
                (!chain [
                    (apply (replicaComposition (functionReplica f lf0 lf1) (functionReplica g lg0 lg1)) x)
                    =
                    (apply (functionReplica g lg0 lg1) (f at x))           [apply_composition_axiom]
                    =
                    (SOME (g at (f at x)))                                            [apply_axioms]
                    =
                    (SOME ((g o f) at x))                                       [compose-definition]
                ])

}