Add [@@no_inline_let] annotation

[amosr]

This adds a [@@no_inline_let] annotation so that the norm tactic doesn't always unfold local lets.

I had to update the rlimit in some places. Some of these were necessary to get the current master building on MacOS even without the no_inline_let changes, but others were required by the no_inline_let. Perhaps the annotation should be hidden in a separate module to avoid polluting the pervasives namespace?

[mtzguido]

Hi Amos, sorry this dropped off the radar. If it's still useful I'd be fine with merging this as-is.

[amosr]

Hi Guido,

Yes, this is still useful to me - I haven't been able to find another good way to have precise control over inlining with norm

[amosr]

(Sorry - I actually accidentally pressed the 'merge from master' button. I'll get this building again in the next few days)

[mtzguido]

It was just some flaky failure. I pushed a fix to this PR. It would be good to get a test for this somewhere in the repo though.

[amosr]

Oh, thanks. Good idea - I'll try to make one soon. Do you have a preference whether I put it as a separate PR or modify this one?

[mtzguido]

Probably better to just append to this one... but no big deal either way!

[amosr]

Hi Guido, I just thought I'd check - can you think of a robust way to make an automated test that it's not inlining? I noticed that tests/tactics/Inlining.fst says to manually inspect the result - maybe that's the way to go here too.

I did think that maybe I could force an exponential blowup / OOM if the lets are inlined, something like this, but unfortunately it's blowing up regardless...:

module InliningNoInline

open FStar.Tactics.V2

// Dummy with multiple arguments to duplicate terms
let join4 a b c d = 0

// Inlining the local lets (without inlining join4) will create a very large term
let explode (i: int) =
  [@@no_inline_let]
  let i4 = join4 i i i i in
  [@@no_inline_let]
  let i16 = join4 i4 i4 i4 i4 in
  [@@no_inline_let]
  let i64 = join4 i16 i16 i16 i16 in
  [@@no_inline_let]
  let i256 = join4 i64 i64 i64 i64 in
  [@@no_inline_let]
  let i1024 = join4 i256 i256 i256 i256 in
  [@@no_inline_let]
  let i4096 = join4 i1024 i1024 i1024 i1024 in
  [@@no_inline_let]
  let i16384 = join4 i4096 i4096 i4096 i4096 in
  [@@no_inline_let]
  let ix8 = join4 i16384 i16384 i16384 i16384 in
  [@@no_inline_let]
  let ix9 = join4 ix8 ix8 ix8 ix8 in
  [@@no_inline_let]
  let ix10 = join4 ix9 ix9 ix9 ix9 in
  [@@no_inline_let]
  let ix11 = join4 ix10 ix10 ix10 ix10 in
  [@@no_inline_let]
  let ix12 = join4 ix11 ix11 ix11 ix11 in
  [@@no_inline_let]
  let ix13 = join4 ix12 ix12 ix12 ix12 in
  ix13

let test () =
  assert (explode 1 == 0)
    by (dump "PRE"; norm [delta_only [`%explode]]; norm [delta_only [`%join4]]; dump "POST")

[mtzguido]

Seems like they are getting inlined during SMT encoding... we encode pure lets by inlining, regardless of these normalization toggles. I wonder why... we could use SMT-LIB lets I think.

In any case, maybe a better test is to check that the extracted code (of a smaller example) matches what you expect? We already do this for a few files, see for instance the .ml-cmp rules in tests/micro-benchmarks