added definition of params
introduce fork soundness and change transform lemma names
added soundness of methods and chalice