[CN-Exec] Idiomatic encoding of constants not supported

[septract]

Summary

cn test doesn't support the style guide's recommended encoding of macro-defined constants. We need this for the OpenSUT MKM proof (target code here).

Problem

In order to support macro-defined constants, the CN style guide recommends the following idiom (see here, from which this example is taken):

#define CONST 1
    /*@ function (i32) CONST () @*/
    static int c_CONST() /*@ cn_function CONST; @*/ { return CONST; }

int foo (int x)
/*@
  requires true;
  ensures return == CONST();
@*/
{
  return CONST;
}

cn test doesn't support this idiom:

$ cn test --output=testgen cn-const-test.c               
cn-const-test.c:20:30: warning: experimental keyword 'cn_function' (use of experimental features is discouraged)
    static int c_CONST() /*@ cn_function CONST; @*/ { return CONST; }
                             ^~~~~~~~~~~ 
Uninterpreted CN functions not supported at runtime. Please provide a concrete function definition for:
'CONST() : i32' at <cn-const-test.c:19:8, cn-const-test.c:19:31>

CN version: git-140db7a8a [2024-12-26 17:38:30 +0000]

Analysis

We need this capability for the MKM proof. See the boilerplate code here which lifts the constants defined in policy.h into CN-level functions.

We could work around this limitation in MKM, but the obvious way to do it would be to concretize all these values - expensive to maintain and unnecessary for cn verify. This is a bit of an annoying problem to have, because the only reason we introduced these functions in the first place is to work around another CN limitation, the lack of support for macro constants.

Intuitively seems like this should be relatively easy limitation to lift, since the whole point is the CN-level function is something very simple, a constant value. But this fact isn't apparent from the code, it's just a consequence of the way we use the idiom.

We have separately talked about whether there should be a more developed facility / keyword for lifting constants into CN. See #378 and various backchannel discussions. To me this gives more evidence we should add a cn_const keyword, or just lift all constants by default.

cc: @yav since we talked recently about cn test and improving the way CN preprocesses files, @bcpierce00 since we want to eventually port the CN manual to a 'testing-first' style of exposition, and @podhrmic re the OpenSUT MKM code.

[rbanerjee20]

Thanks for highlighting this.

I know that uninterpreted CN functions are not supported at runtime in general, throwing the error shown above (no provided function body => no sensible translation into C). I believe there is no translation within the testing machinery for cn_functions, so it is safe to say they are not supported by runtime testing currently. This would explain why CONST() is translated as though its body is not known, even though, according to the style guide, this is expected to be inferred (?) from the cn_function annotation on c_CONST(). I am currently unsure as to how the link between the CN uninterpreted function CONST() and the C function cn_CONST() via the cn_function annotation is encoded within CN's internal AST (which is being used for the executable spec translation). All that is happening right now is that the tooling is trying to translate the uninterpreted function CONST() and then immediately giving up and throwing an error.

Would be useful to chat with @cp526 once he is back, firstly to understand how an example like this is encoded internally but also to discuss whether/how we should add constants to the CN language.

[septract]

Yes, that makes sense. This isn't an implementation bug as such. The runtime testing is doing a reasonable thing here, given that cn_function isn't supported yet. I more think of this as more a language design / documentation bug. This way of handling macro-defined constants is itself a bit of a hack which we should revisit. Definitely keen to discuss this further once @cp526 is back in 2025.