Using CInline to inline local letbindings

[mtzguido]

This is an alternative to #469. In FStarLang/FStar#3418 (which this depends on to really work), I am making F* interpret the CInline attribute for local definitions too, and setting a flag in the relevant binder in the extracted krml AST. This PR makes krml pick it up and trigger inlining.

For instance, this function:

let foo (x:UInt32.t) =
  [@@CInline] let y = x in
  [@@CInline] let z = x in
  y `add_underspec` z

Now extracts to

uint32_t Inline_foo(uint32_t x)
{
  return x + x;
}

Some questions:

0- Does it make sense to reinterpret CInline? I could add another attribute if not.

1- I think this may require bumping the krml ast version? I see the comment about adding constructors only at the end, but I suppose adding a field to a record is just a backwards-incompatible change...

2- Other than that I wonder if we should have a list of meta instead, like in the ML AST. That would make future extensions easier.

3- Also I would like to add an expected output test for this--- I wrote some makefiles to do it in F* (FStarLang/FStar#3417), but perhaps these tests are better located in this repo? We already have a bit of a circular dependency since we check krmllib in F*, so it wouldn't be crazy to keep them there.

[msprotz]

0- yes to reinterpreting CInline, this is natural
1- probably needs a format bump, yes
2- list of meta is probably a good idea, if you're up for it, I will 100% support this
3- happy to have this as a test in test/ -- just do something super simple like let main () = [@@CInline] let foobar = 0l in foobar followed by a custom additional test target (see e.g. check-useless-alias) that probably does ! grep -q foobar .output/.../MyTest.c

[mtzguido]

Updated! I bumped the version to 31, seems like we missed some previous bumps (https://github.com/FStarLang/FStar/pull/3418/files#diff-a5bd15a0626a7115aaa43df331610430cc7e149c594c3878fd880d3bfcdf02d8R34).

I used the meta list in the binary format / input AST, but kept a boolean field in the internal one.

[msprotz]

Looks great -- thanks so much! I'm happy for this to be merged. CC @R1kM that the uu_ hack for HACL-rs will no longer be necessary after this to force a local let-binding to be inlined