[CN] require closed enums / expose enum validity as a predicate (feature request)

[septract]

In C, enums are not closed - an enum is more or less just an alias for an integer type large enough to hold all enumerated values. However, in most cases I would guess we want to enforce closedness. It'd be nice for CN to either:

1. Implicitly enforce closedness, or
2. Add a predicate which enforces this property.

Current State

The function enum_test() is not statically safe in arbitrary calling contexts, and CN correctly complains if we try to verify it:

#include <stdbool.h>

enum my_enum {
  CASE1, 
  CASE2, 
}; 

void enum_test(enum my_enum in)
{
  switch (in) {
    case CASE1: 
      return;
    case CASE2: 
      return; 
    default: 
      assert(false); // Reachable, generates an error
  }
}

To solve this in CN as it is today, we need to write a predicate that enforces the enumeration is in bounds, and then thread this predicate wherever we need it in the program. This generates boilerplate and honestly is a bit confusing given this property seems 'obvious'. For example, here is one I wrote for the MKM code:

/*@ 
function (boolean) ValidState (u32 state) {
   ((state == (u32) CS_RECV_KEY_ID) || 
    (state == (u32) CS_SEND_CHALLENGE) || 
    (state == (u32) CS_RECV_RESPONSE) || 
    (state == (u32) CS_SEND_KEY) || 
    (state == (u32) CS_DONE) )
}
@*/ 

Proposal

Since this predicate is totally schematic, it might be nice to just define it automatically. We could either make it available to the programmer, or enforce it implicitly (with an escape hatch for when we want to break the enum discipline).

... 
void enum_test(enum my_enum in)
/*@
requires 
  enum_valid(in); 
@*/
{
  switch (in) {
    case CASE1: 
...