dlls_simple.ath

### dlls_simple.ath — SUPERSEDED DRAFT. Do not load this file.
###
### This is an early, stripped-down draft of the distributed list of buckets. The
### development actually used by `dhtable_mateo.ath` and `sensor_app.ath` is
### `dlls.ath`. Nothing in the tree loads this file, and nothing should: it
### declares the SAME module name `DL_L_S` as `dlls.ath`, so loading both would
### give one module two conflicting definitions of `in`.
###
### It is kept only as a record of the earlier design. Two known defects remain
### in its `in` predicate, both fixed in `dlls.ath` and deliberately left here so
### the draft still reads as what it was:
###
###   * the walk does not wrap when `bucket` and `rv` have both reached zero at
###     the `dempty` terminus, so a value in a wrapped replica reads as absent; and
###   * the last clause, `(in (S bucket) rv dlls o_dlls htv) <==> (in bucket rv
###     dlls o_dlls htv)`, decrements the bucket index without advancing `dlls`,
###     so the index has no effect on which bucket is inspected.
###
### What has been repaired is the one defect that was not merely wrong but
### unsound: the leading catch-all clause used to make the assumption base
### inconsistent. See the note on `in_axioms` below.

load "lst-in"
load "lst-toset"
load "dlist.ath"
load "function.ath"
open Function
module DL_L_S {
    define [f]     := [?f:(fn 'S N)]
    define [lsts]  := [?lsts:(Lst 'S)]
    define [s htv v head]          := [?s:'S ?htv:'S ?v:'S ?head:(Lst 'S)]
    define [n rv rv0 bucket]  := [?n:N ?rv:N ?rv0:N ?bucket:N]
    define [dlls tail_dlls o_dlls]  := 
           [?dlls:(DLst (Lst 'S)) ?tail_dlls:(DLst (Lst 'S)) ?o_dlls:(DLst (Lst 'S))]
    define [l l0 lh htl htl0 ll tail_l tail_l0] := 
           [?l:Location ?l0:Location ?lh:Location ?htl:Location ?htl0:Location
            ?ll:(Lst Location) ?tail_l:(Lst Location) ?tail_l0:(Lst Location)]

    ### initDPrList
    ### Purpose:
    ###     Initialize a distributed list of buckets, one bucket per input location. Each
    ###     bucket is initialize as an empty list. You might notice that f is never use,
    ###     the reason being that is the way to have information about 'S in the parameter
    ###     input list.
    ###
    ### Parameters:
    ###     f::(fn S N)         : A hash function
    ###     htl0::Location      : default tail location (for dempty)
    ###     lsts:(Lst Location) : list of locations to initialize
    ###
    ### Returns:
    ###     A (DLst (Lst S)) where every location in lsts
    ###     corresponds to an empty bucket (list).
    declare initDPrList: (S) [(fn S N) Location (Lst Location)] -> (DLst (Lst S))
    assert  initDPrList_axioms := 
         (fun [ 
            (initDPrList f htl0 empty) = (dempty htl0)
            (initDPrList f htl0 (lst l tail_l)) = (dlst l empty (initDPrList f htl0 tail_l))
        ])

    # TODO: need a proof for this.. should be easy
    assert initDPrList_characterization :=
    (forall f htl lsts . (
                          ((initDPrList f htl lsts) = (dempty htl)) 
                        | (exists l tail_l . (initDPrList f htl lsts) = (dlst l empty (initDPrList f htl tail_l) ))))
    
    ### in
    ### Purpose:
    ###     Replication aware membership predicate for distributed bucket lists.
    ###     Determines whether a value `v` is stored in the bucket indexed by `bucket`,
    ###     or in any of the next `rv` replica buckets, with a wrap around semantics.
    ###
    ### Parameters:
    ###     bucket::N              : primary bucket index to inspect
    ###     rv::N                  : replication factor, number of successor buckets to check
    ###     dlls::(DLst (Lst S))   : current suffix of the distributed list to traverse
    ###     o_dlls::(DLst (Lst S)) : original distributed list (used when wrap-around is required)
    ###     v::S                   : value to search for
    ###
    ### Returns:
    ###     Boolean indicating whether `v` appears in the bucket at position `bucket` or 
    ###      within the next `rv` buckets modulo the length of the list.
    declare in: (S) [N N (DLst (Lst S)) (DLst (Lst S)) S] -> Boolean
    # SOUNDNESS NOTE. `fun` does not match its clauses in order: each becomes an
    # independent universally quantified biconditional, so two clauses whose
    # patterns unify equate one atom with two right-hand sides and contradict each
    # other. This clause used to read
    #     (in bucket rv dlls (dempty htl) htv) <==> false
    # with an unrestricted `dlls`, which unified with the `dlst` clause below at
    # `o_dlls = (dempty htl)` and proved `(forall x l . ~ (Lst.in x l))` — no
    # element belongs to any list. `dlls` is always a suffix of `o_dlls`, so an
    # empty `o_dlls` forces an empty `dlls`; spelling that out restores
    # consistency and still covers the cases the other clauses leave open.
    assert in_axioms := (fun [
        (in bucket rv (dempty htl0) (dempty htl) htv) <==> false
        (in zero zero (dempty htl) o_dlls htv) <==> false
        (in zero zero (dlst lh lsts tail_dlls) o_dlls htv) <==> (Lst.in htv lsts)
        (in zero (S rv) (dlst lh lsts tail_dlls) o_dlls htv) <==>
            [
                true 
                    when (Lst.in htv lsts)
                (in zero rv tail_dlls o_dlls htv) 
                    when (~ Lst.in htv lsts)
            ]
        (in zero (S rv) (dempty htl) o_dlls htv) <==> (in zero (S rv) o_dlls o_dlls htv)
        (in (S bucket) rv dlls o_dlls htv) <==> (in bucket rv dlls o_dlls htv) 
    ])
    
    define in_init_false_lsts := 
        (forall  lsts f v htl . 
            (~ in zero zero (initDPrList f htl lsts) (initDPrList f htl lsts) v ))
    by-induction in_init_false_lsts {
        empty =>
        pick-any f v htl
            let {
                predicate := (in zero zero (initDPrList f htl empty) (initDPrList f htl empty) v);
                init_empty_case := (!chain [ (initDPrList f htl empty) 
                                            = (dempty htl) [initDPrList_axioms] ]) ;
                in_false :=
                    (!chain [ 
                        predicate
                        # Both slots hold the same init-list, so rewrite both and
                        # appeal to the (dempty _) (dempty _) clause.
                        ==> (in zero zero (dempty htl) (initDPrList f htl empty) v)    [init_empty_case]
                        ==> (in zero zero (dempty htl) (dempty htl) v)                 [init_empty_case]
                        ==> false                                                      [in_axioms]
                    ])
            }
            (!by-contradiction (~ predicate) in_false)
        | (lst l0 tail_l) =>
        # TODO: In this case I do not use the IH... this means that this proof can be done
        # without by-induction?... I think that no, rather it should be done with
        # datatype-cases
        pick-any f v htl
        let { 
            predicate   := (in zero zero (initDPrList f htl (lst l0 tail_l)) (initDPrList f htl (lst l0 tail_l)) v);
            init_lsts   := (!chain [ (initDPrList f htl (lst l0 tail_l)) 
                                    = (dlst l0 empty (initDPrList f htl tail_l)) [initDPrList_axioms] ]);
            in_false    := (!chain [
                   predicate
                ==> (in zero zero (dlst l0 empty (initDPrList f htl tail_l)) (dlst l0 empty (initDPrList f htl tail_l)) v) [init_lsts]
                ==> (Lst.in v empty)                   [in_axioms]
                ==> false                              [Lst.in_axioms]
            ])}
        (!by-contradiction (~predicate) in_false)
    }

    define in_init_false_rv := 
        (forall rv lsts f v htl . 
            (~ in zero rv (initDPrList f htl lsts) (initDPrList f htl lsts) v ))
    by-induction in_init_false_rv {
        zero =>
        pick-any lsts f v htl
            (!chain<- [
                (~ in zero zero (initDPrList f htl lsts) (initDPrList f htl lsts) v )
                <== true [in_init_false_lsts]
            ])
        | (S rv0) =>
        let {
        IH := (forall lsts f v htl .  (~ in zero rv0 (initDPrList f htl lsts) (initDPrList f htl lsts) v ))
        }
        pick-any lsts f:(fn 'S N) v:'S htl
        (!cases (!uspec* initDPrList_characterization [f htl lsts])
            assume  empty_dlst := ((initDPrList f htl lsts) = (dempty htl)) 
            (!by-contradiction
                (~ in zero (S rv0) (initDPrList f htl lsts) (initDPrList f htl lsts) v)
                (!chain [ 
                        (in zero (S rv0) (initDPrList f htl lsts) (initDPrList f htl lsts) v)
                    # Both slots hold the same init-list, so rewrite both and
                    # appeal to the (dempty _) (dempty _) clause.
                    ==> (in zero (S rv0) (dempty htl) (initDPrList f htl lsts) v) [empty_dlst]
                    ==> (in zero (S rv0) (dempty htl) (dempty htl) v)             [empty_dlst]
                    ==> false                                                     [in_axioms]
                ]))
            assume no_empty_dlst := 
                (exists l tail_l . 
                    (initDPrList f htl lsts) = (dlst l empty (initDPrList f htl tail_l)))
            pick-witnesses l0 tail_l0 for no_empty_dlst init_characterization
            let {
                ih := (!uspec* IH [tail_l0 f v htl]);
                _ := (write ih)}
            (!by-contradiction
                (~ in zero (S rv0) (initDPrList f htl lsts) (initDPrList f htl lsts) v)
                (!chain [
                        (in zero (S rv0) (initDPrList f htl lsts) (initDPrList f htl lsts) v)
                    ==> (in zero (S rv0) (dlst l0 empty (initDPrList f htl tail_l0)) (initDPrList f htl lsts) v) [init_characterization]
                    # This step is force... but the justification should be in_axioms,
                    # just do not know at first glance how to make it work, this step does
                    # not worry me
                    ==> (in zero rv0 (initDPrList f htl tail_l0) (initDPrList f htl tail_l0) v) [force]
                    ==> ((~in zero rv0 (initDPrList f htl tail_l0) (initDPrList f htl tail_l0) v) and (in zero rv0 (initDPrList f htl tail_l0) (initDPrList f htl tail_l0) v)) [augment]

                    # This is the step that really worries me, in theory the justification
                    # should be ih (Line 141) but that is not quiet the ih for this
                    # induction. Thus, is there a way to make this work? or what should I do?
                    ==> false                                                                [prop-taut]
                ])
            )
        )
    }

}