Immediate values on ARM

[vbgl]

A few things do not work yet, although they should.

• 32-bit immediate assigned to a register (workaround: halve into 16-bit parts and use #MOVT)

export
fn big() -> reg u32 {
  reg u32 r;
  r = 0x12345678;
  return r;
}

• Immediate arguments whose decoding clobbers the carry flag

export
fn mask(reg u32 x) -> reg u32 {
  x &= 0xff00;
  return x;
}

[sarranz]

Note that for the first part, we could reuse arm_cmd_load_large_imm from arm_params, that is already proven to have the appropriate semantics. But it's done for fexprs, se we could maybe parameterize these definitions on the type of expressions and lvals? I don't know if it's worth it for the proofs, though.