pub exec fn u128_from_le_bytes(s: &[u8]) -> x : u128
s@.len() == 16,
x == spec_u128_from_le_bytes(s@),