[FEATURE] Syntax sugar for CN

[podhrmic]

Summary

As I am going through the tutorial (very well done btw!), I am realizing that some syntax sugar in CN would go a long way in terms of increasing productivity, and making specs writing much faster. If possible, focusing on CN syntax sugar first would be a great result.

For example:

• explicitly stating types for 0,1 and other small numbers - this should be automatic
• array ownership (e.g. the second loop example in the tutorial) - this should be much easier to write, maybe just specify the array type and length?
• automatic completion - lots of possibilities here, including type hints and such (but likely more complex to implement)

[podhrmic]

@peterohanley might have other recommendations as well

[peterohanley]

• sugar for read-only use of values. 6 expressions here are just to lifting the current value at the end of two pointers to the spec level. It would be nice if it was just 2 terms.

function (u8) Generate_Sensor_Trips(map<u64,u32> vals, map<u64,u32> setpoints) {
  let t = Trip(vals, setpoints, (u64)T());
  let p = Trip(vals, setpoints, (u64)P());
  let s = Trip(vals, setpoints, (u64)S());
  (t ? 1u8 : 0u8) + (p ? 2u8 : 0u8) + (s ? 4u8 : 0u8)
}

uint8_t Generate_Sensor_Trips(uint32_t vals[3], uint32_t setpoints[3]);
/*$ spec Generate_Sensor_Trips(pointer vals, pointer setpoints);
    requires
      take vin = each(u64 i; i < (u64)NTRIP()) {Owned<uint32_t>(array_shift(vals,i))};
      take sin = each(u64 j; j < (u64)NTRIP()) {Owned<uint32_t>(array_shift(setpoints,j))};
    ensures return == Generate_Sensor_Trips(vin, sin);
      take vout = each(u64 k; k < (u64)NTRIP()) {Owned<uint32_t>(array_shift(vals,k))};
      take sout = each(u64 l; l < (u64)NTRIP()) {Owned<uint32_t>(array_shift(setpoints,l))};
      vin == vout;
      sin == sout;
$*/

[peterohanley]

• A convenient way to refer to an Owned object that also has various constraints on it.

This would be helpful for structures that need to be well-formed, not just legal memory. Predicates can do this but I haven't gotten them to be convenient about it. This may just be a matter of writing a few helpers.