diff --git a/benchmarks/scripts/criterion-drop-in-replacement/README.md b/benchmarks/scripts/criterion-drop-in-replacement/README.md
new file mode 100644
index 0000000..bcb1d84
--- /dev/null
+++ b/benchmarks/scripts/criterion-drop-in-replacement/README.md
@@ -0,0 +1,44 @@
+## Purpose
+
+This directory contains a Python re-implementation of the Haskell Criterion methodology to run executables (instead of Haskell functions, like Criterion normally does).
+One could call it "benchrunner-runner" because the purpose is to run `benchrunner` many times and calculate the appropriate run time statistics.
+
+We take as input a path to some program `prog` (meant to be the `benchrunner`) with the following interface:
+
+- `prog` takes `iters` as a command-line argument,
+- `prog` measures run time of a function of interest in a tight loop that repeats `iters` many times, and finally
+- `prog` prints to stdout the batchtime (total loop time) and selftimed (total loop time divided by `iters`).
+
+The ultimate goal is then to sweep `iters` and perform a linear regression against `iters` and `batchtime`.
+The slope is the mean and the y-intercept represents some notion of shared overhead, insensitive to `iters`.
+
+## Run
+
+This package contains two scripts:
+
+- `sweep_seq.py` (top level)
+- `criterionmethodology.py` (called by `sweep_seq.py`)
+
+Both can be ran directly, i.e.:
+
+```shellsession
+criterionmethodology benchrunner Quicksort Seq 2000
+```
+
+will call `benchrunner iters Quicksort Seq 2000` for various `iters`.
+
+`sweep_seq` performs a logarithmic sweep over different array sizes, invoking `criterionmethdology.py` at each point.
+
+## Arithmetic vs geometric mean
+
+Since performance data is non-negative and judged multiplicatively (twice as good means numbers are half, twice has bad means numbers are doubled; these are all *factors*), the geomean and geo-standard-deviation may make more sense theoretically.
+However, from some testing, the geomean seems to vary wildly for programs with fleeting execution times, even between repeated runs with the same parameters.
+
+In particular, to compute the geomean, we:
+
+- take the logarithm of all the `x` and `y` values,
+- compute linear regression over that, then 
+- exponentiate the y-intercept.
+
+The other dependent portion, which is the slope, becomes a power (the equation is `y = e^b x^m`), which represents *geometric overhead*, e.g. how much overhead is being added per iteration.
+This may do well to model any slowdowns, e.g. ones arising from pre-allocating arrays.
diff --git a/benchmarks/scripts/criterion-drop-in-replacement/criterionmethodology.py b/benchmarks/scripts/criterion-drop-in-replacement/criterionmethodology.py
new file mode 100755
index 0000000..71a7197
--- /dev/null
+++ b/benchmarks/scripts/criterion-drop-in-replacement/criterionmethodology.py
@@ -0,0 +1,144 @@
+#!/usr/bin/env python
+
+#
+# The script determines the cost of one iteration of a function (in seconds) using an executable that
+#
+# - runs `iters` iterations of that function in a tight loop and
+# - prints out the time it took to run them.
+#
+# Example call:
+#
+#    ./criterionmethodology.py $(cabal list-bin benchrunner) Quicksort Seq 2000
+#
+# In particular, we
+#
+# - run given executable (the first and only relevant argument) with 'iters' argument varied from 1 to N;
+#   N and the step size are dynamially determined based on the time it takes to run the binary;
+# - fetch timing results from binary's stdout and do linear regression over them;
+# - plot the regression (see the `plot` function) in `plot.png`.
+#
+# Growing the `iters` parameter is the main ingenuity of the script. It follows the Criterion methodology:
+# running the given binary for small number of iterations doubling them every time, and upon reaching
+# a certain threshold (FIRST_ITER_THRESHOLD), increasing them linearly until the overall execution time
+# reaches another threshold (TOTAL_TIME_THRESHOLD) seconds.
+#
+# - The `converge` function runs the whole process, starting with a small number of iterations.
+# - The `iter` function encodes the methodology for increasing 'iters'.
+# - The `do_bench` function runs the binary and scrapes the output, so the expected binary's interface is encoded in it.
+#
+
+import numpy as np
+from sys import argv
+import subprocess
+from time import time
+import math
+
+from matplotlib import pyplot as plt
+
+LOG=True
+MAKE_PLOT = False
+FIRST_ITER_THRESHOLD = 3e-6 # 0.65
+TOTAL_TIME_THRESHOLD = 1    # 3.5
+                            # ^^ Joseph's original values, but they are too high for my machine.
+
+# Poor-man logging
+def log(format, **xs):
+    if LOG:
+        print(format, **xs)
+
+def linear_regression_with_std(x, y):
+    x = np.array(x)
+    y = np.array(y)
+    x_mean = np.mean(x)
+    y_mean = np.mean(y)
+    numerator = np.sum((x - x_mean) * (y - y_mean))
+    denominator = np.sum((x - x_mean) ** 2)
+    slope = numerator / denominator
+    intercept = y_mean - slope * x_mean
+    y_pred = slope * x + intercept
+    residuals = y - y_pred
+    std_dev = np.std(residuals)
+    return slope, intercept, std_dev
+
+# Do one trial: run the binary with given arguments, including the given `iters`, and return the batch time.
+def do_bench(cliargs, iters):
+    out = str(subprocess.check_output([cliargs[0], str(iters)] + cliargs[1:]))
+    s1 = out[out.find("SELFTIMED")+11:]
+    s2 = float(s1[:s1.find("\n")-4])
+    selftimed = s2
+
+    b1 = out[out.find("BATCHTIME")+11:]
+    b2 = float(b1[:b1.find("SELFTIMED")-2])
+    batchtime = b2
+
+    #log(f"ITERS: {iters}, BATCHTIME: {batchtime}, SELFTIMED: {selftimed}")
+    return batchtime
+
+# Increase 'iters' and do one trial with that. Store results in xs and ys. Return new iters.
+def iter(iters, cliargs, start_time, xs, ys):
+    if time() - start_time < TOTAL_TIME_THRESHOLD:
+        iters = int(math.trunc(float(iters) * 1.2) + 1)
+    else:
+        iters += 1 + iters // 20
+    log(str(iters) + " ", end="", flush=True)
+    st = do_bench(cliargs, iters)
+    xs.append(iters)
+    ys.append(st)
+    return iters
+
+def plot(xs, ys, b, c, m, p):
+    plotfile = "plot.png"
+    os.remove(plotfile) if os.path.exists(plotfile) else None
+    plt.plot(xs, ys, 'rx')
+    plt.plot([xs[0], xs[-1]], [m*xs[0]+b, m*xs[-1]+b], color="blue")
+    plt.plot(xs, [c*x**p for x in xs], color="green")
+    plt.savefig(plotfile)
+
+# Main function to run the iteration experiment.
+# - cliargs is a list of command line arguments WIHTOUT the current script's name (argv[0]), in particular:
+#   - the first argument is the path to the binary, and
+#   - the rest is simply the arguments to pass to the binary.
+def converge(cliargs):
+    bin = cliargs[0].rsplit('/', 1)[-1] # Get the binary name from the path
+    log("Converge on: " + str([bin] + cliargs[1:]))
+    log("iters: ", end="")
+    xs = []
+    ys = []
+    iters = 1
+    t = time()
+
+    # First find a starting point for `iters` where the time is at least FIRST_ITER_THRESHOLD seconds
+    while len(xs) == 0:
+        log(str(iters) + " ", end="", flush=True)
+        st = do_bench(cliargs, iters)
+        if st < FIRST_ITER_THRESHOLD: # Artem: Joseph had `st * iters < ...` here but I think it's a typo
+            iters *= 2
+            continue
+        xs.append(iters)
+        ys.append(st)
+
+    log(" | ", end="", flush=True)
+    # Do two more trials increasing iters regardless of time
+    for _ in range(2):
+        iters = iter(iters, cliargs, t, xs, ys)
+
+    log(" | ", end="", flush=True)
+    # Keep increasing iters until we reach TOTAL_TIME_THRESHOLD seconds of execution in total
+    while time() - t < TOTAL_TIME_THRESHOLD:
+        iters = iter(iters, cliargs, t, xs, ys)
+    log("done!")
+
+    m, b, sig = linear_regression_with_std(xs, ys)
+    p, lnc, lngsd = linear_regression_with_std([math.log(x) for x in xs], [math.log(y) for y in ys])
+    c, gsd = math.exp(lnc), math.exp(lngsd)
+
+    log(f"Slope (Mean):     {m:.2e}, Stdev:    {sig:.2e}, Intercept (Overhead): {b:.2e}")
+    log(f"Factor (Geomean): {c:.2e}, GeoStdev: {gsd:.2e}, Power (Distortion):   {p:.2e}")
+
+    if MAKE_PLOT:
+        plot(xs, ys, b, c, m, p)
+
+    return m, sig, c, gsd
+
+if __name__ == "__main__":
+    converge(argv[1:])
diff --git a/benchmarks/scripts/criterion-drop-in-replacement/sweep_seq.py b/benchmarks/scripts/criterion-drop-in-replacement/sweep_seq.py
new file mode 100755
index 0000000..0014800
--- /dev/null
+++ b/benchmarks/scripts/criterion-drop-in-replacement/sweep_seq.py
@@ -0,0 +1,49 @@
+#!/usr/bin/env python3
+import os
+import numpy as np
+from criterionmethodology import converge
+import sys
+
+# names = ["Optsort", "Insertionsort", "Mergesort", "Quicksort"]
+# names = ["CopyArray", "Quicksort", "Insertionsort", "Mergesort"]
+names = ["Insertionsort"]
+
+# DENSITY = 4
+DENSITY = 12
+def bounds(name):
+    match name:
+        case "Insertionsort":
+            lo = 3  # 2**n ...
+            hi = 12 # for local testing; initially: 16
+        case "Quicksort":
+            lo = 3
+            hi = 22
+        case "Mergesort":
+            # lo = 12
+            lo = 3
+            hi = 24
+        case "Cilksort":
+            # lo = 12
+            lo = 3
+            hi = 16#24
+        case "Optsort":
+            lo = 3
+            hi = 16#24
+        case _:
+            lo = 3
+            hi = 20
+    return lo, hi, (hi-lo)*DENSITY+1
+
+def dotrial(exe, name, size):
+    return converge([exe, name, "Seq", str(int(size))])
+
+if __name__ == "__main__":
+    exe = sys.argv[1]
+    print("Running with executable:", exe)
+    for name in names:
+        lo, hi, pts = bounds(name)
+        with open("%s_out3.csv" % name, "w") as f:
+            f.write("# size\tmean\tstddev\tgeomean\tgeostdev\n")
+        for i in np.unique(np.logspace(lo, hi, pts, base=2).astype(int)):  # Artem: I don't understand this and I must
+            with open("%s_out3.csv" % name, "a") as f:
+                f.write("%d" % int(i) + "\t%f\t%f\t%f\t%f\n" % dotrial(exe, name, i))
diff --git a/benchmarks/scripts/c-sorting-benchmarks/readme b/benchmarks/scripts/old-criterion/c-sorting-benchmarks/readme
similarity index 100%
rename from benchmarks/scripts/c-sorting-benchmarks/readme
rename to benchmarks/scripts/old-criterion/c-sorting-benchmarks/readme
diff --git a/benchmarks/scripts/c-sorting-benchmarks/sort_insertion_out.csv b/benchmarks/scripts/old-criterion/c-sorting-benchmarks/sort_insertion_out.csv
similarity index 100%
rename from benchmarks/scripts/c-sorting-benchmarks/sort_insertion_out.csv
rename to benchmarks/scripts/old-criterion/c-sorting-benchmarks/sort_insertion_out.csv
diff --git a/benchmarks/scripts/c-sorting-benchmarks/sort_merge_seq_out.csv b/benchmarks/scripts/old-criterion/c-sorting-benchmarks/sort_merge_seq_out.csv
similarity index 100%
rename from benchmarks/scripts/c-sorting-benchmarks/sort_merge_seq_out.csv
rename to benchmarks/scripts/old-criterion/c-sorting-benchmarks/sort_merge_seq_out.csv
diff --git a/benchmarks/scripts/c-sorting-benchmarks/sort_quick_out.csv b/benchmarks/scripts/old-criterion/c-sorting-benchmarks/sort_quick_out.csv
similarity index 100%
rename from benchmarks/scripts/c-sorting-benchmarks/sort_quick_out.csv
rename to benchmarks/scripts/old-criterion/c-sorting-benchmarks/sort_quick_out.csv
diff --git a/benchmarks/scripts/plot.py b/benchmarks/scripts/old-criterion/plot.py
similarity index 100%
rename from benchmarks/scripts/plot.py
rename to benchmarks/scripts/old-criterion/plot.py
diff --git a/benchmarks/scripts/plot_relative_speedup.py b/benchmarks/scripts/old-criterion/plot_relative_speedup.py
similarity index 100%
rename from benchmarks/scripts/plot_relative_speedup.py
rename to benchmarks/scripts/old-criterion/plot_relative_speedup.py
diff --git a/benchmarks/scripts/readme b/benchmarks/scripts/old-criterion/readme
similarity index 100%
rename from benchmarks/scripts/readme
rename to benchmarks/scripts/old-criterion/readme
diff --git a/benchmarks/scripts/sweep_seq.py b/benchmarks/scripts/old-criterion/sweep_seq.py
similarity index 100%
rename from benchmarks/scripts/sweep_seq.py
rename to benchmarks/scripts/old-criterion/sweep_seq.py
diff --git a/src/Array.hs b/src/Array.hs
index 562c4e6..7c09b82 100644
--- a/src/Array.hs
+++ b/src/Array.hs
@@ -14,7 +14,8 @@ module Array
     Array
 
     -- * Construction and querying
-  , alloc, make, generate, generate_par, generate_par_m, makeArray
+  , alloc, make, allocScratch
+  , generate, generate_par, generate_par_m, makeArray
   , copy, copy_par, copy_par_m
   , size, get, set, slice, append
   , splitAt
@@ -95,9 +96,25 @@ makeArray = make
 #endif
 
 {-# INLINE free #-}
-free :: HasPrim a => Array a -. ()
+free :: Array a -. ()
 free = Unsafe.toLinear (\_ -> ())
 
+{-# INLINE allocScratch #-} -- todo: are we linear in the use of the algorithm?
+{-@ allocScratch :: forall <p :: Array dsts -> Bool>. n:Nat -> x:_ 
+      -> f:({xs:_ | size xs == n } -> { ys:_ | size ys == n } 
+              -> { tup:(Array<p> dsts, Array tmpdsts) | 
+                      token (fst tup) == token xs & token (snd tup) == token ys &
+                      size (fst tup) == size xs & size (snd tup) == size ys &
+                      left (fst tup) == left xs & left (snd tup) == left ys &
+                      right (fst tup) == right xs & right (snd tup) == right ys })
+      -> { src:_ | size src == n } -> { dst:Array<p> dsts | token src == token dsts } @-}
+allocScratch :: HasPrim tmps => Int -> tmps -> (Array srcs -. Array tmps -. (Array dsts, Array tmpdsts)) 
+                  -. Array srcs -. Array dsts
+allocScratch i a f arr =
+  let
+    !(dst, tmp) = f arr (makeArray i a)
+  in case free tmp of !() -> dst
+
 --------------------------------------------------------------------------------
 -- Parallel operations
 --------------------------------------------------------------------------------
diff --git a/src/DpsMergeSort.hs b/src/DpsMergeSort.hs
deleted file mode 100644
index 5f35b4b..0000000
--- a/src/DpsMergeSort.hs
+++ /dev/null
@@ -1,102 +0,0 @@
-
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE BangPatterns #-}
-
-
-module DpsMergeSort where
-
-import qualified Unsafe.Linear as Unsafe
-import qualified Language.Haskell.Liquid.Bag as B
-import           Language.Haskell.Liquid.ProofCombinators hiding ((?))
-import           ProofCombinators
-import           Array as A
-import           ArrayOperations
-import           DpsMerge
-import Properties.Equivalence
-import Properties.Order
-
-#ifdef MUTABLE_ARRAYS
-import           Array.Mutable as A
-#else
-import           Array.List as A
-#endif
-
--- DPS mergesort
-{-@ msortSwap :: xs:Array a
-      -> { ys:(Array a ) | A.size ys  == A.size xs   && left xs == left ys &&
-                           right xs == right ys }
-      -> (Array a, Array a)<{\zs ts -> toBag xs == toBag ts && isSorted' ts &&
-                                       token xs == token zs && token ys == token ts &&
-                                       A.size xs == A.size zs && A.size ys == A.size ts &&
-                                       left zs == left xs && right zs == right xs &&
-                                       left ts == left ys && right ts == right ys }>
-       / [A.size xs] @-}
-msortSwap :: (Show a, HasPrimOrd a) => A.Array a -> A.Array a -> (A.Array a, A.Array a)
-msortSwap !src !tmp =
-  let !(len, src') = A.size2 src in
-  if len <= 1
-  then let !(src'', tmp'') = copy2 src' 0 tmp 0 len in
-       (src'', tmp'')  ? lem_equal_slice_bag' src' tmp'' 0 len 0 (len
-                           ? lem_copy_equal_slice src' 0 tmp 0 len)
-                       ? lem_isSorted_copy    src' 0 tmp 0 len
-  else
-    let (src1, src2) = splitMid src'
-        (tmp1, tmp2) = splitMid tmp
-        (src1', tmp1') = msortInplace src1 tmp1
-        (src2', tmp2') = msortInplace src2 tmp2
-        !tmp3' = A.append tmp1' tmp2'
-        !(src'', tmp4) = merge src1' src2' tmp3'
-    in (src'', tmp4)   ? lem_toBag_splitMid src -- tmp4 holds the sorted data
-                       ? lem_toBag_splitMid tmp
-
-{-@ msortInplace :: xs:Array a
-      -> { ys:(Array a ) | A.size ys  == A.size xs   && left xs == left ys &&
-                      right xs == right ys }
-      -> { out:(Array a, Array a) | toBag xs == toBag (fst out) && isSorted' (fst out) &&
-                                    token xs == token (fst out) && token ys == token (snd out) &&
-                                    A.size xs == A.size (fst out) && A.size ys == A.size (snd out) &&
-                                    left (fst out) == left xs && right (fst out) == right xs &&
-                                    left (snd out) == left ys && right (snd out) == right ys }
-       / [A.size xs] @-}
-msortInplace :: (Show a, HasPrimOrd a) => A.Array a -> A.Array a -> (A.Array a, A.Array a)
-msortInplace !src !tmp =
-  let !(len, src') = A.size2 src in
-  if len <= 1
-  then (src', tmp)
-  else
-    let (src1, src2) = splitMid src'
-        (tmp1, tmp2) = splitMid tmp
-        (src1', tmp1') = msortSwap src1 tmp1
-        (src2', tmp2') = msortSwap src2 tmp2
-        !src3' = A.append src1' src2'
-        !(tmp'', src4') = merge tmp1' tmp2' src3'
-    in (src4', tmp'')  ? lem_toBag_splitMid src -- src4' holds the sorted data
-                       ? lem_toBag_splitMid tmp
-
-{-@ msort' :: { xs:(Array a) | A.size xs > 0 && left xs == 0 && right xs == size xs }
-           -> { y:a | y == A.get xs 0 }
-           -> { zs:(Array a) | toBag xs == toBag zs && isSorted' zs &&
-                               A.size xs == A.size zs && token xs == token zs } @-}
-msort' :: (Show a, HasPrimOrd a) => A.Array a -> a -> A.Array a
-msort' src anyVal =
-  let (n, src1) = A.size2 src
-      (src2, _tmp) = msortInplace src1 (A.makeArray n anyVal) in
-  _tmp `seq` src2
-
--- finally, the top-level merge sort function
-{-@ msort :: { xs:_ | left xs == 0 && right xs == size xs }
-                    -> { ys:_ | toBag xs == toBag ys && isSorted' ys &&
-                                A.size xs == A.size ys  } @-}
-{- # SPECIALISE msort :: A.Array Float -> A.Array Float #-}
-{- # SPECIALISE msort :: A.Array Int -> A.Array Int #-}
-msort :: (Show a, HasPrimOrd a) => A.Array a -> A.Array a
-msort src =
-  let (n, src1) = A.size2 src in
-      if n == 0 then src1
-      else let (x0, src2) = A.get2 src1 0
-               tmp = A.makeArray n x0
-               {-@ cpy :: { ys:(Array a) | size ys == n && left ys == 0 && right ys == n &&
-                                           toSlice ys 0 n == toSlice src2 0 n } @-}
-               cpy = A.copy src2 0 tmp 0 n
-                     ? lem_copy_equal_slice  src2 0 tmp 0 n
-            in msort' (cpy ? lem_equal_slice_bag   src2   cpy 0 n) x0
diff --git a/src/DpsMergeSort4.hs b/src/DpsMergeSort4.hs
index 129d49f..1022b08 100644
--- a/src/DpsMergeSort4.hs
+++ b/src/DpsMergeSort4.hs
@@ -76,9 +76,7 @@ msortInplace src tmp = go src tmp where
                                A.size xs == A.size zs && token xs == token zs } @-}
 msort' :: (Show a, HasPrimOrd a) => a -> A.Array a -. A.Array a
 msort' anyVal src =
-  let !(Ur len, src') = A.size2 src
-      !(src'', _tmp) = msortInplace src' (A.make len anyVal) in
-  case A.free _tmp of !() -> src''
+  let !(Ur len, src') = A.size2 src in allocScratch len anyVal msortInplace src'
 {-# INLINE msort' #-}
 
 -- finally, the top-level merge sort function -- TODO: use A.get2/A.size2 for linearity
diff --git a/src/DpsMergeSort4Par.hs b/src/DpsMergeSort4Par.hs
index 862eccf..d56c290 100644
--- a/src/DpsMergeSort4Par.hs
+++ b/src/DpsMergeSort4Par.hs
@@ -106,9 +106,7 @@ msort' :: (Show a, HasPrimOrd a) =>
 #endif
   a -> A.Array a -. A.Array a
 msort' anyVal src =
-  let !(Ur len, src') = A.size2 src
-      !(src'', _tmp) = msortInplace src' (A.make len anyVal) in
-  case A.free _tmp of !() -> src''
+  let !(Ur len, src') = A.size2 src in allocScratch len anyVal msortInplace src'
 {-# INLINE msort' #-}
 
 -- finally, the top-level merge sort function
diff --git a/src/DpsMergeSortPar.hs b/src/DpsMergeSortPar.hs
deleted file mode 100644
index d3f2997..0000000
--- a/src/DpsMergeSortPar.hs
+++ /dev/null
@@ -1,123 +0,0 @@
-
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE BangPatterns #-}
-
-
-module DpsMergeSortPar where
-
-import qualified Unsafe.Linear as Unsafe
-import qualified Language.Haskell.Liquid.Bag as B
-import           Language.Haskell.Liquid.ProofCombinators hiding ((?))
-import           ProofCombinators
-import           Array as A
-import           ArrayOperations
-import           DpsMergePar
-import qualified DpsMergeSort as Seq
---import qualified DpsMerge as Seq
-import Properties.Equivalence
-import Properties.Order
-import           Par
-import           Control.DeepSeq ( NFData(..) )
-
-#ifdef MUTABLE_ARRAYS
-import           Array.Mutable as A
-#else
-import           Array.List as A
-#endif
-
-#define KILO     1024
-#define SEQSIZE  4096
-
---------------------------------------------------------------------------------
-
--- DPS mergesort
-{-@ msortSwap :: xs:Array a
-      -> { ys:(Array a ) | A.size ys  == A.size xs   && left xs == left ys &&
-                           right xs == right ys }
-      -> (Array a, Array a)<{\zs ts -> toBag xs == toBag ts && isSorted' ts &&
-                                       token xs == token zs && token ys == token ts &&
-                                       A.size xs == A.size zs && A.size ys == A.size ts &&
-                                       left zs == left xs && right zs == right xs &&
-                                       left ts == left ys && right ts == right ys }>
-       / [A.size xs] @-}
-msortSwap :: (Show a, HasPrimOrd a, NFData a) => A.Array a -> A.Array a -> (A.Array a, A.Array a)
-msortSwap src tmp =
-  let (len, src') = A.size2 src in
---  if len <= 1
---  then let !(src'', tmp'') = copy2_par src' 0 tmp 0 len in
---       (src'', tmp'')
-  if len <= SEQSIZE
-  then Seq.msortSwap src' tmp
-  else
-    let (src1, src2)  = splitMid src'
-        (tmp1, tmp2)  = splitMid tmp
-        ((src1', tmp1'), (src2', tmp2'))
---                      = tuple2 (msortInplace src1) tmp1 (msortInplace src2) tmp2
-                      = msortInplace src1 tmp1 .||. msortInplace src2 tmp2
-        !tmp3' = A.append tmp1' tmp2'
-        !(src'', tmp4) = merge_par src1' src2' tmp3'
-    in  (src'', tmp4)  ? lem_toBag_splitMid src -- tmp4 holds the sorted data
-                       ? lem_toBag_splitMid tmp
-
-{-@ msortInplace :: xs:Array a
-      -> { ys:(Array a ) | A.size ys  == A.size xs   && left xs == left ys &&
-                      right xs == right ys }
-      -> { out:(Array a, Array a) | toBag xs == toBag (fst out) && isSorted' (fst out) &&
-                                    token xs == token (fst out) && token ys == token (snd out) &&
-                                    A.size xs == A.size (fst out) && A.size ys == A.size (snd out) &&
-                                    left (fst out) == left xs && right (fst out) == right xs &&
-                                    left (snd out) == left ys && right (snd out) == right ys }
-       / [A.size xs] @-}
-msortInplace :: (Show a, HasPrimOrd a, NFData a) => A.Array a -> A.Array a -> (A.Array a, A.Array a)
-msortInplace src tmp =
-  let (len, src') = A.size2 src in
-  if len <= SEQSIZE
-  then Seq.msortInplace src' tmp
-  else
-    let (src1, src2)   = splitMid src'
-        (tmp1, tmp2)   = splitMid tmp
-        ((src1', tmp1'), (src2', tmp2'))
---                       = tuple2 (msortSwap src1) tmp1 (msortSwap src2) tmp2
-                       = msortSwap src1 tmp1 .||. msortSwap src2 tmp2
-        !src3' = A.append src1' src2'
-        !(tmp'', src4') = merge_par tmp1' tmp2' src3'
-    in  (src4', tmp'')  ? lem_toBag_splitMid src -- src4' holds the sorted data
-                        ? lem_toBag_splitMid tmp
-
-{-@ msort' :: { xs:(Array a) | A.size xs > 0 && left xs == 0 && right xs == size xs }
-           -> { y:a | y == A.get xs 0 }
-           -> { zs:(Array a) | toBag xs == toBag zs && isSorted' zs &&
-                               A.size xs == A.size zs && token xs == token zs } @-}
-msort' :: (Show a, HasPrimOrd a, NFData a) => A.Array a -> a -> A.Array a
-msort' src anyVal =
-  let (n, src1) = A.size2 src
-      {-@ promise :: { tmp:(Array a) | size tmp == n && left tmp == 0 && right tmp == n }
-              -> { out:(Ur (Array a, Array a)) | toBag src == toBag (fst (unur out)) &&
-                                                 isSorted' (fst (unur out)) &&
-                    token src == token (fst (unur out)) && token tmp == token (snd (unur out)) &&
-                    size (fst (unur out)) == n && size (snd (unur out)) == n } @-}
-      promise tmp = Ur (msortInplace src1 tmp)
-      Ur (src2, _tmp) = A.alloc n anyVal (Unsafe.toLinear promise) in
-  _tmp `seq` src2
-
--- finally, the top-level merge sort function
-{-@ msort :: { xs:(A.Array a) | left xs == 0 && right xs == size xs }
-                    -> { ys:_ | toBag xs == toBag ys && isSorted' ys &&
-                                A.size xs == A.size ys  } @-}
-{- # SPECIALISE msort :: A.Array Float -> A.Array Float #-}
-{- # SPECIALISE msort :: A.Array Int -> A.Array Int #-}
-msort :: (Show a, HasPrimOrd a, NFData a) => A.Array a -> A.Array a
-msort src =
-  let (n, src1) = A.size2 src in
-      if n == 0 then src1
-      else let (x0, src2) = A.get2 src1 0
-               {-@ promise :: { tmp:(Array a) | size tmp == n && left tmp == 0 && right tmp == n }
-                           -> { out:(Ur (Array a)) | size (unur out) == n &&
-                                                     left (unur out) == 0 && right (unur out) == n &&
-                                                     toSlice (unur out) 0 n == toSlice src2 0 n} @-}
-               promise tmp = Ur (A.copy src2 0 tmp 0 n)
-                           ? lem_copy_equal_slice  src2 0 tmp 0 n
-               {-@ cpy :: { ys:(Array a) | size ys == n && left ys == 0 && right ys == n &&
-                                           toSlice ys 0 n == toSlice src2 0 n } @-}
-               Ur cpy = A.alloc n x0 (Unsafe.toLinear promise)
-           in msort' (cpy ? lem_equal_slice_bag   src2   cpy 0 n) x0
diff --git a/src/Insertion.hs b/src/Insertion.hs
index 55db8a4..24cbf9f 100644
--- a/src/Insertion.hs
+++ b/src/Insertion.hs
@@ -187,6 +187,18 @@ isort_top' :: HasPrimOrd a => A.Array a -. A.Array a
 isort_top' xs = isort 0 xs
 {-# INLINABLE isort_top' #-}
 
+
+-- | Sort the (possibly empty) input array. No allocation involved here.
+{-@ isort_top :: xs:_ -> { ys:_ | toBag xs == toBag ys &&  isSorted' ys &&
+                                  left xs == left ys && right xs == right ys &&
+                                  A.size xs == A.size ys && token xs == token ys } @-}
+isort_top :: forall a. HasPrimOrd a => A.Array a -. A.Array a
+isort_top xs0 =
+  let !(Ur n, xs1) = A.size2 xs0
+    in
+      if n <= 1 then xs1 else isort 0 xs
+
+{-
 -- | Sort a copy of the input array. Therefore token is not preserved.
 {-@ isort_top :: { xs:_ | A.size xs > 1 }
       -> { ys:_ | toBag xs  == toBag ys  && isSorted' ys &&
@@ -198,16 +210,13 @@ isort_top xs0 =
       if n <= 1 then xs1
       else
         let !(Ur hd, xs2) = A.get2 0 xs1
+            isort_tmp :: A.Array a -. A.Array a -. (A.Array a, A.Array a)
+            isort_tmp src tmp =
+              let !(old_arr, tmp_arr) = A.copy2 0 0 n src tmp
+                in (isort 0 (tmp_arr ? lem_equal_slice_bag src tmp 0 n), old_arr) 
+                      ? lem_copy_equal_slice  src 0 tmp 0 n  -- there's an issue with using !()
             {- @ promise :: { tmp:(Array a) | size tmp == n }
                         -> { out:(Ur (Array a)) | size (unur out) == n &&
                                                   toSlice (unur out) 0 n == toSlice xs2 0 n} @-}
-            promise :: A.Array a -. Ur (A.Array a)
-            --promise :: A.Array a -. (A.Array a -. Ur (A.Array a))
-            promise tmp =
-              let !(old_arr, tmp_arr) = A.copy2 0 0 n xs2 tmp
-                in case (A.free old_arr) of
-                    !() -> ur tmp_arr  -- let version doesn't linearlly check here, we suspect
-                            ? lem_copy_equal_slice  xs2 0 tmp 0 n  -- there's an issue with using !()
-            {-@ cpy :: { ys:(Array a) | size ys == n && toSlice ys 0 n == toSlice xs2 0 n } @-}
-            cpy = unur (A.alloc n hd promise)
-          in isort 0 (cpy ? lem_equal_slice_bag   xs2   cpy 0 n)
+          in allocScratch n hd isort_tmp xs2
+-}
\ No newline at end of file
diff --git a/src/PiecewiseFallbackSort.hs b/src/PiecewiseFallbackSort.hs
index 36a0b0e..abbd6c3 100644
--- a/src/PiecewiseFallbackSort.hs
+++ b/src/PiecewiseFallbackSort.hs
@@ -65,13 +65,15 @@ msortInplace cutoff src tmp =  -- cutoff > 0, though it may not be necessary to
                                A.size xs == A.size zs && token xs == token zs } @-}
 pfsort' :: (Show a, HasPrimOrd a) => a -> A.Array a -. A.Array a
 pfsort' anyVal src =
-  let !(Ur len, src') = A.size2 src  -- below expression is always in the interval [28, 708] (interval changed from meeting doc).
-      !(src'', _tmp) = msortInplace (if len <= 708 then 708  -- this can be any number >= 708 without affecting semantics, including `len`
-                                     else if len < 451776
-                                          -- this is the same as truncate (18820.2738 / sqrt (fromIntegral len)) per GHC.Float
-                                          then truncate((18820.2738 / (exp ((log (fromIntegral len)) * 0.5) )) :: Float)
-                                          else 28) src' (A.makeArray len anyVal) in
-  case A.free _tmp of !() -> src''
+  msort' :: (Show a, HasPrimOrd a) => a -> A.Array a -. A.Array a
+msort' anyVal src =
+  let !(Ur len, src') = A.size2 src -- below expression is always in the interval [28, 708] (interval changed from meeting doc).
+      cutoff          = if len <= 708 then 708  -- this can be any number >= 708 without affecting semantics, including `len`
+                        else if len < 451776
+                             -- this is the same as truncate (18820.2738 / sqrt (fromIntegral len)) per GHC.Float
+                             then truncate((18820.2738 / (exp ((log (fromIntegral len)) * 0.5) )) :: Float)
+                             else 28  
+   in allocScratch len anyVal (msortInplace cutoff) src'
 
 {-@ pfsort :: { xs:(A.Array a) | left xs == 0 && right xs == size xs }
                     -> { ys:_ | toBag xs == toBag ys && isSorted' ys &&
diff --git a/src/PiecewiseFallbackSortPar.hs b/src/PiecewiseFallbackSortPar.hs
index d31e5e2..b1a7e63 100644
--- a/src/PiecewiseFallbackSortPar.hs
+++ b/src/PiecewiseFallbackSortPar.hs
@@ -84,13 +84,13 @@ pfsort' :: (Show a, HasPrimOrd a) =>
 #endif
   a -> A.Array a -. A.Array a
 pfsort' anyVal src =
-  let !(Ur len, src') = A.size2 src
-      !(src'', _tmp) = msortInplace (if len <= 708 then 708  -- this can be any number >= 708 without affecting semantics, including `len`
-                                     else if len < 451776
-                                          -- this is the same as truncate (18820.2738 / sqrt (fromIntegral len)) per GHC.Float
-                                          then truncate((18820.2738 / (exp ((log (fromIntegral len)) * 0.5) )) :: Float)
-                                          else 28) src' (A.makeArray len anyVal) in
-  case A.free _tmp of !() -> src''
+  let !(Ur len, src') = A.size2 src -- below expression is always in the interval [28, 708] (interval changed from meeting doc).
+      cutoff          = if len <= 708 then 708  -- this can be any number >= 708 without affecting semantics, including `len`
+                        else if len < 451776
+                             -- this is the same as truncate (18820.2738 / sqrt (fromIntegral len)) per GHC.Float
+                             then truncate((18820.2738 / (exp ((log (fromIntegral len)) * 0.5) )) :: Float)
+                             else 28  
+   in allocScratch len anyVal (msortInplace cutoff) src'
 
 {-@ pfsort :: { xs:(A.Array a) | left xs == 0 && right xs == size xs }
                     -> { ys:_ | toBag xs == toBag ys && isSorted' ys &&
diff --git a/src/QuickSort.hs b/src/QuickSort.hs
index 3dac176..84502f7 100644
--- a/src/QuickSort.hs
+++ b/src/QuickSort.hs
@@ -32,6 +32,16 @@ import qualified Array as A
 
 --------------------------------------------------------------------------------
 
+{-@ quickSort :: xs:(Array a) -> { ys:(Array a) | isSorted' ys && A.size xs == A.size ys &&
+                                                                  toBag  xs == toBag  ys } @-}
+quickSort :: (HasPrimOrd a, Show a) => Array a -. Array a
+quickSort xs =
+  let (Ur n, xs1) = A.size2 xs in
+  if n == 0 then xs1
+  else quickSortBtw 0 n xs1
+{-# INLINABLE quickSort #-}
+
+{-
 {-@ quickSort :: xs:(Array a) -> { ys:(Array a) | isSorted' ys && A.size xs == A.size ys &&
                                                                   toBag  xs == toBag  ys } @-}
 -- quickSort :: (Ord a, Show a) => Array a -> Array a
@@ -45,6 +55,7 @@ quickSort xs =
                    (A.free(xs2'), cpy0) & \((), cpy) ->
                      quickSortBtw 0 n (cpy ? lem_equal_slice_bag   xs2   cpy 0 n)
 {-# INLINABLE quickSort #-}
+-}
 
 {-@ quickSort' :: xs:(Array a) -> { ys:(Array a) | isSorted' ys && A.size xs == A.size ys &&
                                                                   toBag  xs == toBag  ys } @-}
diff --git a/src/QuickSortCilk.hs b/src/QuickSortCilk.hs
index bffa939..6e57c91 100644
--- a/src/QuickSortCilk.hs
+++ b/src/QuickSortCilk.hs
@@ -38,6 +38,16 @@ import qualified Array as A
 -- | It's QuickSort, but this one falls back to insertion sort eventually
 --------------------------------------------------------------------------------
 
+{-@ quickSort :: xs:(Array a) -> { ys:(Array a) | isSorted' ys && A.size xs == A.size ys &&
+                                                                  toBag  xs == toBag  ys } @-}
+quickSort :: (HasPrimOrd a, Show a) => Array a -. Array a
+quickSort xs =
+  let (Ur n, xs1) = A.size2 xs in
+  if n == 0 then xs1
+  else quickSortBtw 0 n xs1
+{-# INLINABLE quickSort #-}
+
+{-
 {-@ quickSort :: xs:(Array a) -> { ys:(Array a) | isSorted' ys && A.size xs == A.size ys &&
                                                                   toBag  xs == toBag  ys } @-}
 -- quickSort :: (Ord a, Show a) => Array a -> Array a
@@ -54,6 +64,7 @@ quickSort xs =
                {- @ cpy :: { ys:(Array a) | size ys == n && toSlice ys 0 n == toSlice xs2 0 n } @-}
                Ur cpy = A.alloc n hd (Unsafe.toLinear promise)
             in quickSortBtw (cpy ? lem_equal_slice_bag   xs2   cpy 0 n) 0 n
+-}
 
 {-@ quickSortBtw :: xs:(Array a) -> { i:Int | 0 <= i } -> { j:Int | i <= j && j <= A.size xs }
                 -> { ys:(Array a) | isSortedBtw ys i j && A.size xs == A.size ys &&