some x86_64 stack lemmas
added bignum-to-decimal-string function
bug fix