add statement contract for assignment to ABC
add statement for p->DEF
fix statement contracts
firnish formal verification of Decoder
remove old stuff