[CN] Consolidate `trusted` and `spec` keywords

[septract]

There are two keywords for introducing unverified functions to CN - trusted and spec. We should only have one keyword for both cases and make the usage consistent.

// Function declaration uses `trusted`
int unverified_trusted(int x, int y)
/*@ 
  trusted; // <-- no prototype needed here 
  requires x > 7i32; 
  ensures return == 0i32; 
@*/
{
  ; // unverified code here ... 
} 

// Prototype uses `spec`
int unverified_spec(int x, int y); 
/*@ 
  spec unverified_spec(i32 x, i32 y); // <-- specification-level prototype needed here
  requires x > 7i32; 
  ensures return == 0i32; 
@*/

This duplication makes the language more difficult to learn, in my opinion. The two keywords do similar but slightly different things, which makes for a more 'noisy' / confusing language design. It also causes specific incompatible behavior - eg. spec and trusted are parsed differently so we can't easily switch between them (see this ticket: #371).

It also seems anomalous that spec needs an additional function declaration, and trusted doesn't. Is the 'spec-level prototype' taken by spec ever not determined by the function arguments? (See @peterohanley making this same point here: https://github.com/rems-project/cerberus/issues/304#issuecomment-2225994635)

Proposed resolution:

Ideally, we only use one keyword in both situations. To me, trusted is the more appropriate choice (but I don't feel strongly about this - spec is also fine). So I propose:

• Parse spec as an alias for trusted, and deprecate spec (Or vice versa)
• Remove the requirement to give a spec type declaration

(CN version: git-7ca5f6c3d [2024-08-05 18:31:25 +0100])

[septract]

@cp526 I imagine there is / was some rationale for this design. Is there some use-case I don't know about that requires the spec / trusted distinction?

[cp526]

spec and trusted have a different purpose.

trusted instructs CN not to verify the annotated function (CN only checks wellformedness of the specification).

spec is for giving a specification to function prototypes. Because function prototypes don't necessarily assign names to their arguments, CN needs syntax such as spec unverified_spec(i32 x, i32 y); ... to give names to the arguments so later specifications can refer to them.

Both of these are needed. That said, spec was added in a rush and there are a couple of deficiencies: (1), as you mention, spec does not accept the same syntax as specifications attached to function definitions (e.g. accesses), (2) probably nothing in CN currently prevents using spec for function definitions, but then, AIUI, these are not verified against that spec (so here we have to either forbid spec for defined functions or allow it but do the proof), (3) currently the spec argument list is not even compared for compatibility with the C-types in the function prototype (that's quite bad and we already have a ticket for that).