Improve substitution to avoid eager composition and preserve sharing

.github/workflows/bench.yml

@@ -125,8 +125,8 @@ jobs:
       - name: Collect ramon files
         run: |
           mkdir -p ramon-files/base ramon-files/head
-          (cd fstar-base && find . -name '*.ramon' -exec cp --parents {} ../ramon-files/base/ \;) || true
-          (cd fstar-head && find . -name '*.ramon' -exec cp --parents {} ../ramon-files/head/ \;) || true
+          (cd fstar-base && find . \( -name '*.ramon' -o -name '*.fstarmem' \) -exec cp --parents {} ../ramon-files/base/ \;) || true
+          (cd fstar-head && find . \( -name '*.ramon' -o -name '*.fstarmem' \) -exec cp --parents {} ../ramon-files/head/ \;) || true
 
       - name: Upload artifacts
         uses: actions/upload-artifact@v4

.github/workflows/rebase.yml

@@ -0,0 +1,85 @@
+name: Rebase PR
+
+# Triggered by posting a comment containing "!rebase" on a pull request.
+# Rebases the PR branch onto its base branch and force-pushes the result.
+
+on:
+  issue_comment:
+    types: [created]
+
+defaults:
+  run:
+    shell: bash
+
+jobs:
+  rebase:
+    if: >
+      github.event.issue.pull_request &&
+      contains(github.event.comment.body, '!rebase') &&
+      contains(fromJSON('["OWNER","MEMBER","COLLABORATOR"]'), github.event.comment.author_association)
+    runs-on: ubuntu-latest
+    permissions:
+      pull-requests: write
+      contents: write
+
+    steps:
+      - name: React to comment
+        uses: actions/github-script@v7
+        with:
+          script: |
+            await github.rest.reactions.createForIssueComment({
+              owner: context.repo.owner,
+              repo: context.repo.repo,
+              comment_id: context.payload.comment.id,
+              content: 'eyes'
+            });
+
+      - name: Get PR info
+        id: pr
+        uses: actions/github-script@v7
+        with:
+          script: |
+            const pr = await github.rest.pulls.get({
+              owner: context.repo.owner,
+              repo: context.repo.repo,
+              pull_number: context.issue.number,
+            });
+            core.setOutput('head_ref', pr.data.head.ref);
+            core.setOutput('base_ref', pr.data.base.ref);
+            core.setOutput('head_repo_full_name', pr.data.head.repo.full_name);
+            core.setOutput('is_fork', pr.data.head.repo.full_name !== pr.data.base.repo.full_name);
+
+      - name: Check if fork
+        if: steps.pr.outputs.is_fork == 'true'
+        run: |
+          echo "::error::Cannot rebase PRs from forks (no push access to ${{ steps.pr.outputs.head_repo_full_name }})"
+          exit 1
+
+      - name: Checkout PR branch
+        uses: actions/checkout@v4
+        with:
+          ref: ${{ steps.pr.outputs.head_ref }}
+          fetch-depth: 0
+          token: ${{ secrets.GITHUB_TOKEN }}
+
+      - name: Rebase onto base
+        run: |
+          git config user.name "${{ github.event.comment.user.login }}"
+          git config user.email "${{ github.event.comment.user.id }}+${{ github.event.comment.user.login }}@users.noreply.github.com"
+          git fetch origin ${{ steps.pr.outputs.base_ref }}
+          git rebase origin/${{ steps.pr.outputs.base_ref }}
+
+      - name: Force-push
+        run: git push --force-with-lease
+
+      - name: React with result
+        if: always()
+        uses: actions/github-script@v7
+        with:
+          script: |
+            await github.rest.reactions.createForIssueComment({
+              owner: context.repo.owner,
+              repo: context.repo.repo,
+              comment_id: context.payload.comment.id,
+              content: '${{ job.status }}' === 'success' ? 'rocket' : '-1'
+            });

.scripts/ramon-report.py

@@ -69,6 +69,19 @@ def load_ramon_file(fn):
         return None
     if "rc" not in ret or "time" not in ret or "mem" not in ret:
         return None
+
+    # Prefer F*-only memory (excludes Z3) from companion .fstarmem file.
+    fstarmem_fn = fn.removesuffix(".ramon") + ".fstarmem"
+    try:
+        with open(fstarmem_fn) as f:
+            for line in f:
+                parts = line.split(None, 1)
+                if len(parts) >= 2 and parts[0] == "fstar.mempeak":
+                    ret["mem"] = int(parts[1].strip())
+                    break
+    except FileNotFoundError:
+        pass
+
     return ret
 
 def find_ramon_files(root):
@@ -299,8 +312,8 @@ def md_table(items, n=20):
 
     # ── Notes ──
     L.append("---\n")
-    L.append("> **Note:** Time measurements are from single runs and may be noisy, especially for fast tests. "
-             "Memory measurements are generally more deterministic. "
+    L.append("> **Note:** Memory values report the peak OCaml heap of the F\\* process (excluding Z3 subprocesses). "
+             "Time measurements are from single runs and may be noisy, especially for fast tests. "
              "Tests with baseline time < 0.1s are excluded from time statistics. "
              "The geometric mean (Geo Mean) of the patched/baseline ratio is the most robust summary "
              "statistic for performance comparisons (1.0× = no change, <1× = improvement).")
@@ -474,8 +487,9 @@ def stat_class(val, invert=False):
 </div>
 
 <div class="note">
-<strong>Note on measurement reliability:</strong> Time measurements are from single runs and may be noisy,
-especially for tests completing in under 5 seconds. Memory measurements are generally more deterministic.
+<strong>Note on measurement reliability:</strong> Memory values report the peak OCaml heap of the F* process,
+excluding Z3 subprocesses. Time measurements are from single runs and may be noisy,
+especially for tests completing in under 5 seconds.
 Tests with baseline time &lt; 0.1s are excluded from time statistics.
 The geometric mean (Geo Mean) of the patched/baseline ratio is the most robust summary statistic
 for performance comparisons (1.0× = no change, &lt;1× = improvement).

mk/common.mk

@@ -46,7 +46,9 @@ ifneq ($(RESOURCEMONITOR),)
 	ifneq ($(MONID),)
 		MONPREFIX=$(MONID).
 	endif
-	RAMON=ramon -o $@.$(MONPREFIX)ramon --
+	# NB: this sets the Make variable RAMON to the string "FSTAR_MEM_REPORT=... ramon ...".
+	# In the recipe, the shell interprets FSTAR_MEM_REPORT=... as an env var for ramon.
+	RAMON=FSTAR_MEM_REPORT=$@.$(MONPREFIX)fstarmem ramon -o $@.$(MONPREFIX)ramon --
 endif
 
 # Ensure that any failing rule will not create its target file.

src/ml/FStarC_MemReport.ml

@@ -0,0 +1,17 @@
+(* If FSTAR_MEM_REPORT is set, register an at_exit handler that writes
+   the peak OCaml heap size (in bytes) to the given file path. This
+   reports F*-only memory excluding Z3 subprocesses, which makes
+   memory benchmarks more deterministic. *)
+let setup () =
+  match Sys.getenv_opt "FSTAR_MEM_REPORT" with
+  | Some fn ->
+    at_exit (fun () ->
+      try
+        let stat = Gc.quick_stat () in
+        let peak_bytes = stat.Gc.top_heap_words * (Sys.word_size / 8) in
+        let oc = open_out fn in
+        Printf.fprintf oc "fstar.mempeak %d\n" peak_bytes;
+        close_out oc
+      with _ -> ()
+    )
+  | None -> ()

src/syntax/FStarC.Syntax.Subst.fst

@@ -64,18 +64,14 @@ let compose_subst (s1 s2 : subst_ts) : subst_ts =
                | _ -> snd s1 in
     (s, ropt)
 
-//apply a delayed substitution s to t,
-//composing it with any other delayed substitution that may already be there
+// Apply a delayed substitution s to t.
+// This may nest Tm_delayed nodes, that is fine. If we coalesce
+// them, that implies composing the substitutions and potentially breaking
+// sharing.
+let delay' (t:term) (s : subst_ts) rng : ML term =
+    mk_Tm_delayed (t, s) rng
 let delay (t:term) (s : subst_ts) : ML term =
- match t.n with
- | Tm_delayed {tm=t'; substs=s'} ->
-    //s' is the subsitution already associated with this node;
-    //s is the new subsitution to add to it
-    //compose substitutions by concatenating them
-    //the order of concatenation is important!
-    mk_Tm_delayed (t', compose_subst s' s) t.pos
- | _ ->
-    mk_Tm_delayed (t, s) t.pos
+    delay' t s t.pos
 
 (*
     force_uvar' (t:term) : term * bool
@@ -198,11 +194,11 @@ let rec subst' (s:subst_ts) (t:term) : ML term =
     | Tm_fvar _ -> tag_with_range t0 s   //fvars are never subject to substitution
 
     | Tm_delayed {tm=t';substs=s'} ->
-        //s' is the subsitution already associated with this node;
-        //s is the new subsitution to add to it
-        //compose substitutions by concatenating them
-        //the order of concatenation is important!
-        mk_Tm_delayed (t', compose_subst s' s) t.pos
+        (* I really just want this:
+           delay t s
+        Or to remove this completely and fall in the default case above.
+        But somehow, that's incredibly bad for ranges. *)
+        delay' t' (compose_subst s' s) t.pos
 
     | Tm_bvar a ->
         apply_until_some_then_map (subst_bv a) (fst s) subst_tail t0
@@ -214,10 +210,7 @@ let rec subst' (s:subst_ts) (t:term) : ML term =
         mk (Tm_type (subst_univ (fst s) u)) (mk_range t0.pos s)
 
     | _ ->
-      //NS: 04/12/2018
-      //    Substitutions on Tm_uvar just gets delayed
-      //    since its solution may eventually end up being an open term
-      mk_Tm_delayed (t0, s) (mk_range t.pos s)
+      delay' t0 s (mk_range t.pos s)
 
 let subst_dec_order' s = function
   | Decreases_lex l -> Decreases_lex (l |> List.map (subst' s))
@@ -367,16 +360,14 @@ let compose_uvar_subst (u:ctx_uvar) (s0:subst_ts) (s:subst_ts) : ML subst_ts =
     |  s' -> [s'], snd s
 
 //
-// If resolve_uvars is true, it will lookup the unionfind graph
-//   and use uvar solution, if it has already been solved
-//   see the Tm_uvar case in this function
-// Otherwise it will just compose s with the uvar subst
+// Push a substitution one level down.
 // 
-let rec push_subst_aux (resolve_uvars:bool) s t : ML _ =
+let rec push_subst (s : subst_ts) (t : term) : ML _ =
     //makes a syntax node, setting it's use range as appropriate from s
     let mk t' = Syntax.mk t' (mk_range t.pos s) in
     match t.n with
-    | Tm_delayed _ -> failwith "Impossible (delayed node in push_subst)"
+    | Tm_delayed _ ->
+      push_subst s (compress_subst t)
 
     | Tm_lazy i ->
         begin match i.lkind with
@@ -385,7 +376,7 @@ let rec push_subst_aux (resolve_uvars:bool) s t : ML _ =
              * The hope is that this does not occur often and so
              * we still get good performance. *)
           let t = Option.must !lazy_chooser i.lkind i in // Can't call Syntax.Util from here
-          push_subst_aux resolve_uvars s t
+          push_subst s t
         | _ ->
             (* All others must be closed, so don't bother *)
             tag_with_range t s
@@ -396,14 +387,7 @@ let rec push_subst_aux (resolve_uvars:bool) s t : ML _ =
     | Tm_unknown -> tag_with_range t s //these are always closed
 
     | Tm_uvar (uv, s0) ->
-      let fallback () =
-        tag_with_range ({t with n = Tm_uvar(uv, compose_uvar_subst uv s0 s)}) s
-      in
-      if not resolve_uvars
-      then fallback ()
-      else (match (Unionfind.find uv.ctx_uvar_head) with
-            | None -> fallback ()
-            | Some t -> push_subst_aux resolve_uvars (compose_subst s0 s) t)
+      tag_with_range ({t with n = Tm_uvar(uv, compose_subst s0 s)}) s
 
     | Tm_type _
     | Tm_bvar _
@@ -490,17 +474,14 @@ let rec push_subst_aux (resolve_uvars:bool) s t : ML _ =
     | Tm_meta {tm=t; meta=m} ->
         mk (Tm_meta {tm=subst' s t; meta=m})
 
-let push_subst s t : ML _ = push_subst_aux true s t
-
 //
 // Only push the pending substitution down,
 //   no resolving uvars
 //
-let compress_subst (t:term) : ML term =
+and compress_subst (t:term) : ML term =
   match t.n with
   | Tm_delayed {tm=t; substs=s} ->
-    let resolve_uvars = false in
-    push_subst_aux resolve_uvars s t
+    push_subst s t
   | _ -> t
 
 (* compress:
@@ -513,41 +494,21 @@ let compress_subst (t:term) : ML term =
          2. eliminate any top-level (Tm_uvar uv) node,
             when uv has been assigned a solution already
 
-      `compress` should will *not* memoize the result of uvar
-      solutions (since those could be reverted), nor the result
-      of `push_subst` (since it internally uses the unionfind
-      graph too).
-
-      The function is broken into a fast-path where the
-      result can be easily determined and a recursive slow
-      path.
-
-      Warning: if force_uvar changes to operate on inputs other than
-      Tm_uvar then the fastpath out match in compress will need to be
-      updated.
-
-      This function should NEVER return a Tm_delayed. If you do any
-      non-trivial change to it, it would be wise to uncomment the check
-      below and run a full regression build.
+      This function should NEVER return a Tm_delayed, nor a resolved uvar. If
+      you do any non-trivial change to it, it would be wise to uncomment the
+      check below and run a full regression build.
 *)
-let rec compress_slow (t:term) : ML _ =
+let rec compress (t:term) : ML term =
+  let r =
     let t = force_uvar t in
     match t.n with
     | Tm_delayed {tm=t'; substs=s} ->
-        compress (push_subst s t')
-    | _ ->
-        t
-and compress (t:term) : ML term =
-  match t.n with
-    | Tm_delayed _ | Tm_uvar _ ->
-        let r = compress_slow t in
-        (* begin match r.n with *)
-        (* | Tm_delayed _ -> failwith "compress attempting to return a Tm_delayed" *)
-        (* | _ -> () *)
-        (* end; *)
-        r
+      compress (push_subst s t')
     | _ ->
-        t
+      t
+  in
+  // compress_post_check r;
+  r
 
 let subst s t : ML _ = subst' ([s], NoUseRange) t
 let set_use_range r t : ML _ = subst' ([], SomeUseRange (Range.set_def_range r (Range.use_range r))) t

stage1/dune/main.ml

@@ -27,4 +27,7 @@ let x =
       (* Tweak garbage collector parameters. *)
       Gc.set { (Gc.get()) with Gc.minor_heap_size = 1048576; Gc.major_heap_increment = 4194304; Gc.space_overhead = 150; };
 
+      (* Set up peak heap memory reporting (for benchmarking). *)
+      Fstarcompiler.FStarC_MemReport.setup ();
+
       Fstarcompiler.FStarC_Main.main ()

stage2/dune/main.ml

@@ -27,4 +27,7 @@ let x =
       (* Tweak garbage collector parameters. *)
       Gc.set { (Gc.get()) with Gc.minor_heap_size = 1048576; Gc.major_heap_increment = 4194304; Gc.space_overhead = 150; };
 
+      (* Set up peak heap memory reporting (for benchmarking). *)
+      Fstarcompiler.FStarC_MemReport.setup ();
+
       Fstarcompiler.FStarC_Main.main ()

stage3/dune/main.ml

@@ -27,6 +27,9 @@ let x =
       (* Tweak garbage collector parameters. *)
       Gc.set { (Gc.get()) with Gc.minor_heap_size = 1048576; Gc.major_heap_increment = 4194304; Gc.space_overhead = 150; };
 
+      (* Set up peak heap memory reporting (for benchmarking). *)
+      Fstarcompiler.FStarC_MemReport.setup ();
+
       (* Only on stage3: we've baked Pulse into the compiler, which
          brings in the plugin library. Make sure F* knows this so it
          will not try to load it again. *)