Pancake array support

[JunmingZhao42]

As discussed it might be a good idea to support c-like arrays in pancake. For example

var arr_ptr = @base;
var offset = 4 * 8;
stw arr_ptr + offset, 42;
var x = lds 1 arr_ptr + offset;

can be written as

var arr_ptr = @base;
arr_ptr[4] = 42;
var x = arr_ptr[4];

That'll certainly make implementation easier and benefit code readability. And potentially also make it easier to translate to ATP intermediate language like silver.

[myreen]

This would be fine by me, as long as this feature doesn't invent or just hijack the name offset. Perhaps the example code could just expand to:

var arr_ptr = @base;
stw arr_ptr + 4 * 8, 42;
var x = lds 1 arr_ptr + 4 * 8;

One minor comment: the 8 in 4 * 8 is assuming this is code for a 64-bit architecture. I would like Pancake to have a @bytes_in_word (or @word_size) expression in the concrete syntax. This expression should expand to the value of the HOL constant bytes_in_word, which is 4 for 32-bit and 8 for 64-bit architectures. Having such a constant in Pancake concrete syntax makes it possible to write target-independent Pancake code.