// A function over a list of byte sequences 
fn tokens: [List(Bytes)] -> [List(Bytes)] {
    tokens(nil) := nil;
    (tokens(?x:Bytes :: rest) :=  (check? {
                (is_self_token(?x)) ==> ?x :: tokens(rest)
                | else ==> tokens(rest)
    });
}


fn balance: [Bytes] -> Nat {
    balance(?b:Bytes) := (check? {
        (length(?b:Bytes) >= 16) ==> uint128_le(?b[0..16]))
        | else ==> 0
    });
}

// a function over a list of byte sequences that returns a list of tuples of (hash_string, number)
// such for each token, hash_string is a lock_hash of a bag of tokens and number is the total sum of the balances
// of the bags in the list owned by that lock_hash

fn balances: [List(Bytes)] -> [(Bytes, Nat)] {
    
}

Spec {
    mint {
        (forall ?p:Prev ?n:Next .   sum(balance(?p)) < sum(balance(?n)) ==> exists ?o:Bytes . 
            and( 
                in(?o, ?p),
                lock_hash(?0) = slice(args(), 0, 32) 
            )
        )
    }

    transfer {
        (forall ?p:Prev ?n:Next .  
            and(
                balances(tokens(?p)) =/= balances(tokens(?n)),
                len(balances(tokens(?p))) = len(balances(tokens(?n))) 
            ) ==> sum(balance(?p)) = sum(balance(?n))
        )
    }

    burn {
        (forall ?p:Prev ?n:Next .  
            len(balances(tokens(?p))) < len(balances(tokens(?n))) ==> sum(balance(?p)) < sum(balance(?n))
        )
    }
}



Contract {

// Case analysis over Spec...
// When case analysis is performed over the Spec, the axioms of each operation (mint, transfer and burn in this case)
// are already added to the assumption base.
// The antecedent of each clause (i.e., the guard clause) must be assumed. Then, the stated conclusion must be proven from the
// assumption of each guard clause


// The below proof states that for any state change, the sum of the balances in the prev state is less than or equal to the sum of the
// balances in the next state. I.e., that a single step preserves this property.
// It does *not* prove that this is true for a possibly infinite *sequence* of state changes (many steps) preserves this property.
// Such a safety property can be proved by induction over a list of (Prev, Next) tuples 

    conclude conservation_of_tokens_in_single_step := (forall ?p:Prev ?n:Next . sum(balance(?p)) <= sum(balance(?n))) {
        pick-any ?p:Prev, ?n:Next {
            (!cases Spec
                (!chain [
                        (sum(balance(?p)) < sum(balance(?n))) 
                    ==> (sum(balance(?p)) <= sum(balance(?n)))                          [(forall ?n:Nat ?m:Nat . ?n < ?m ==> ?n <= ?m)]
                ]),

                (!chain [
                        (and
                            (balances(tokens(?p)) =/= balances(tokens(?n)), 
                            (len(balances(tokens(?p))) = len(balances(tokens(?n))))
                        ) 
                    ==> sum(balance(?p)) = sum(balance(?n))                             [transfer]
                    ==> sum(balance(?p)) <= sum(balance(?n))                            [(forall ?n:Nat ?m:Nat . ?n = ?m ==> ?n <= ?m)]
                ]),

                (!chain [
                        (len(balances(tokens(?p))) < len(balances(tokens(?n))))
                    ==> sum(balance(?p)) < sum(balance(?n))                             [burn]
                    ==> (sum(balance(?p)) <= sum(balance(?n)))                          [(forall ?n:Nat ?m:Nat . ?n < ?m ==> ?n <= ?m)]
                ])
                
            )
        } 
    }
    
}