Fix Heapster type-checking bugs for Rust

[eddywestbrook]

This PR fixes some bugs and adds some features in order to progress Heapster type-checking for Rust programs. The changes include:

• changed how memblock permisisons with variable shapes are proved, so that they look for permissions on the left that contain the offsets on the right, not just those that precisely line up with them

• performance enhancement: changed a number of fmaps and mbMap2s in Implication.hs to use mbMapCl, to avoid the performance overhead of changing fresh pairs to fresh functions

• added support for proving sub-byte-sized fields using a truncation rule

• switched the pretty-printer to use layoutPretty instead of layoutSmart to avoid exponential behavior; also switched ppCommaSep to use the built-in library function punctuate

• changed SImpl_SplitLLVMWordField, SImpl_TruncateLLVMWordField, and SImpl_ConcatLLVMWordFields to PermImpl1 rules that generate fresh variables for the splitting, truncation, and concatenation of bitvector values, respectively, in order to handle symbolic values in these rules

[m-yac]

Looks good to me, though I can't say I reviewed most of the changes in Implication.hs much beyond just Haskell style, both due to the large number of changes and and due to my unfamiliarity with that part of the codebase. But since all the existing and new tests pass that gives me a good amount of confidence this all works.