Newbie: proving cryptol code (and llvm equivalence) for the block cipher

[mojoman]

Hello,

I am trying to prove various things about my Cryptol implementation of Russian standart 128-bit block cipher ("Grasshopper"). This is my first code in Cryptol, so it is most certainly neither effective nor good-looking. It does not look more complex than the relevant code for AES in cryptol-specs to me -- however I am not able to prove anything non-trivial about it.
Decryption(Encryption) lemma takes days and does not finish with any type of prover, trying to llvm_verify equivalence with official openssl engine C implementation also takes days and does not finish with any prover.
I suspect that something is inherently wrong with my Cryptol spec code and its symbolic representation is too large, but I just cannot understand what exactly -- after all, AES spec is proving its properties in seconds on my laptop with trivial prover :( Any ideas would be very welcome, thanks!

My repository with the spec and relevant saw script:
https://github.com/mojoman/cryptol-grasshopper