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

[amosr]

hi @mtzguido, sorry for going dark on this one for so long. could you check if this test looks reasonable?

unfortunately I haven't been able to test it locally yet - I'm having trouble running the tests on MacOS at the moment, and trying to run make docker-ci gives me a permission error:

ERROR: failed to solve: fstar_ci_base: pull access denied, repository does not exist or may require authorization: server message: insufficient_scope: authorization failed

I was hoping to debug the test on ci, but it looks like it's still going after ten hours - how long is it expected to take? I'll keep poking around and see if I can find another way to run the tests inside a docker container.