Merge remote-tracking branch 'origin/develop' into work/desktop-stdlib

Author: b-re-w

.github/workflows/typedpython.yml

@@ -0,0 +1,77 @@
+name: TypedPython CI
+
+# The TypedPython gate and compiler are Python (python-multiplatform-ksp/src/{main,test}/python).
+# Gradle does not run them; this workflow does.
+on:
+  push:
+    branches: [ "develop", "main" ]
+    paths: [ "python-multiplatform-ksp/**", ".github/workflows/typedpython.yml" ]
+  pull_request:
+    branches: [ "develop", "main" ]
+    paths: [ "python-multiplatform-ksp/**", ".github/workflows/typedpython.yml" ]
+
+jobs:
+  test:
+    name: TypedPython tests (${{ matrix.os }})
+    runs-on: ${{ matrix.os }}
+    strategy:
+      fail-fast: false
+      matrix:
+        os: [ubuntu-latest, macos-latest]
+    defaults:
+      run:
+        working-directory: python-multiplatform-ksp
+    steps:
+      - uses: actions/checkout@v4
+
+      - uses: astral-sh/setup-uv@v5
+
+      - name: Create the environment
+        # pyrefly is pinned exactly: the gate reads its versioned type-report format.
+        run: |
+          uv venv .venv --python 3.13
+          uv pip install --python .venv/bin/python "pyrefly==1.3.2" pytest
+
+      - name: Behaviour tests
+        run: .venv/bin/python -m pytest -q -m "not measurement"
+
+      - name: Measurements (recorded, sanity bounds only)
+        # A shared runner is not an idle machine (AGENTS.md §8): read ratios, not absolute times.
+        run: .venv/bin/python -m pytest -q -s -m measurement
+
+  sanitizers:
+    # SPEC N-8: ASan/UBSan runs are the safety net outside the proof. Every extension TypedPython
+    # builds in these tests is compiled with -fsanitize=address,undefined (TP_SANITIZE=1, see
+    # conftest.py) and the interpreter runs with the ASan runtime preloaded; any report fails the run.
+    # Linux only: macOS refuses to load the ASan runtime into the framework Python (the cgen
+    # sanitizer test has a launcher-based macOS path of its own).
+    name: TypedPython tests under ASan + UBSan (ubuntu-latest)
+    runs-on: ubuntu-latest
+    defaults:
+      run:
+        working-directory: python-multiplatform-ksp
+    steps:
+      - uses: actions/checkout@v4
+
+      - uses: astral-sh/setup-uv@v5
+
+      - name: Create the environment
+        run: |
+          uv venv .venv --python 3.13
+          uv pip install --python .venv/bin/python "pyrefly==1.3.2" pytest
+
+      - name: Relax ASLR entropy (ASan shadow mapping on newer kernels)
+        run: sudo sysctl -w vm.mmap_rnd_bits=28 || true
+
+      - name: Self-check, the sanitizers must catch planted faults
+        # Builds a deliberately faulty extension (heap out-of-bounds read, signed overflow) and
+        # REQUIRES both reports. If this step passes, the setup below can detect faults.
+        run: .venv/bin/python tools/sanitizers.py selfcheck
+
+      - name: cgen, runtime and pipeline tests, sanitized
+        # detect_leaks=0: CPython itself leaks at exit. LD_PRELOAD is applied to this one command
+        # only (tools/sanitizers.py env prints it); the gate's pyrefly runs without it.
+        run: |
+          env $(.venv/bin/python tools/sanitizers.py env) \
+            .venv/bin/python -m pytest -q -m "not measurement" \
+              src/test/python/test_cgen.py src/test/python/test_runtime.py src/test/python/test_pipeline.py

benchmarks/typedpython/.gitignore

@@ -0,0 +1,5 @@
+target/
+java-out/
+__pycache__/
+*.class
+tp-build/

benchmarks/typedpython/java/BinaryTrees.java

@@ -0,0 +1,33 @@
+public class BinaryTrees {
+    static final class Node {
+        final Node left, right;
+        Node(Node left, Node right) { this.left = left; this.right = right; }
+    }
+
+    static Node make(int depth) {
+        if (depth > 0) return new Node(make(depth - 1), make(depth - 1));
+        return new Node(null, null);
+    }
+
+    static int check(Node node) {
+        Node left = node.left, right = node.right;
+        if (left == null || right == null) return 1;
+        return 1 + check(left) + check(right);
+    }
+
+    public static void main(String[] args) {
+        int n = Integer.parseInt(args[0]);
+        int minDepth = 4;
+        int maxDepth = Math.max(minDepth + 2, n);
+        int stretch = check(make(maxDepth + 1));
+        Node longLived = make(maxDepth);
+        long total = 0;
+        for (int depth = minDepth; depth <= maxDepth; depth += 2) {
+            int iterations = 1 << (maxDepth - depth + minDepth);
+            long chk = 0;
+            for (int i = 0; i < iterations; i++) chk += check(make(depth));
+            total += chk;
+        }
+        System.out.println(stretch + " " + total + " " + check(longLived));
+    }
+}

benchmarks/typedpython/java/Fannkuch.java

@@ -0,0 +1,39 @@
+public class Fannkuch {
+    public static void main(String[] args) {
+        int n = Integer.parseInt(args[0]);
+        int[] perm1 = new int[n];
+        for (int i = 0; i < n; i++) perm1[i] = i;
+        int[] count = new int[n];
+        int maxFlips = 0, checksum = 0, permCount = 0, r = n;
+        while (true) {
+            while (r != 1) { count[r - 1] = r; r--; }
+            int[] perm = perm1.clone();
+            int flips = 0;
+            int k = perm[0];
+            while (k != 0) {
+                int lo = 0, hi = k;
+                while (lo < hi) {
+                    int t = perm[lo]; perm[lo] = perm[hi]; perm[hi] = t;
+                    lo++; hi--;
+                }
+                flips++;
+                k = perm[0];
+            }
+            if (flips > maxFlips) maxFlips = flips;
+            if (permCount % 2 == 0) checksum += flips; else checksum -= flips;
+            boolean done = false;
+            while (true) {
+                if (r == n) { done = true; break; }
+                int p0 = perm1[0];
+                for (int i = 0; i < r; i++) perm1[i] = perm1[i + 1];
+                perm1[r] = p0;
+                count[r]--;
+                if (count[r] > 0) break;
+                r++;
+            }
+            if (done) break;
+            permCount++;
+        }
+        System.out.println(checksum + " " + maxFlips);
+    }
+}

benchmarks/typedpython/java/Nbody.java

@@ -0,0 +1,74 @@
+import java.util.Locale;
+
+public class Nbody {
+    static final double PI = 3.141592653589793;
+    static final double SOLAR_MASS = 4 * PI * PI;
+    static final double DAYS = 365.24;
+    static final double[] x = {0.0, 4.84143144246472090e+00, 8.34336671824457987e+00, 1.28943695621391310e+01, 1.53796971148509165e+01};
+    static final double[] y = {0.0, -1.16032004402742839e+00, 4.12479856412430479e+00, -1.51111514016986312e+01, -2.59193146099879641e+01};
+    static final double[] z = {0.0, -1.03622044471123109e-01, -4.03523417114321381e-01, -2.23307578892655734e-01, 1.79258772950371181e-01};
+    static final double[] vx = {0.0, 1.66007664274403694e-03 * DAYS, -2.76742510726862411e-03 * DAYS, 2.96460137564761618e-03 * DAYS, 2.68067772490389322e-03 * DAYS};
+    static final double[] vy = {0.0, 7.69901118419740425e-03 * DAYS, 4.99852801234917238e-03 * DAYS, 2.37847173959480950e-03 * DAYS, 1.62824170038242295e-03 * DAYS};
+    static final double[] vz = {0.0, -6.90460016972063023e-05 * DAYS, 2.30417297573763929e-05 * DAYS, -2.96589568540237556e-05 * DAYS, -9.51592254519715870e-05 * DAYS};
+    static final double[] mass = {SOLAR_MASS, 9.54791938424326609e-04 * SOLAR_MASS, 2.85885980666130812e-04 * SOLAR_MASS, 4.36624404335156298e-05 * SOLAR_MASS, 5.15138902046611451e-05 * SOLAR_MASS};
+
+    static void offsetMomentum() {
+        double px = 0.0, py = 0.0, pz = 0.0;
+        for (int i = 0; i < 5; i++) {
+            px += vx[i] * mass[i];
+            py += vy[i] * mass[i];
+            pz += vz[i] * mass[i];
+        }
+        vx[0] = -px / SOLAR_MASS;
+        vy[0] = -py / SOLAR_MASS;
+        vz[0] = -pz / SOLAR_MASS;
+    }
+
+    static void advance(double dt, int steps) {
+        for (int s = 0; s < steps; s++) {
+            for (int i = 0; i < 5; i++) {
+                for (int j = i + 1; j < 5; j++) {
+                    double dx = x[i] - x[j];
+                    double dy = y[i] - y[j];
+                    double dz = z[i] - z[j];
+                    double d2 = dx * dx + dy * dy + dz * dz;
+                    double mag = dt / (d2 * Math.sqrt(d2));
+                    vx[i] -= dx * mass[j] * mag;
+                    vy[i] -= dy * mass[j] * mag;
+                    vz[i] -= dz * mass[j] * mag;
+                    vx[j] += dx * mass[i] * mag;
+                    vy[j] += dy * mass[i] * mag;
+                    vz[j] += dz * mass[i] * mag;
+                }
+            }
+            for (int i = 0; i < 5; i++) {
+                x[i] += dt * vx[i];
+                y[i] += dt * vy[i];
+                z[i] += dt * vz[i];
+            }
+        }
+    }
+
+    static double energy() {
+        double e = 0.0;
+        for (int i = 0; i < 5; i++) {
+            e += 0.5 * mass[i] * (vx[i] * vx[i] + vy[i] * vy[i] + vz[i] * vz[i]);
+            for (int j = i + 1; j < 5; j++) {
+                double dx = x[i] - x[j];
+                double dy = y[i] - y[j];
+                double dz = z[i] - z[j];
+                e -= mass[i] * mass[j] / Math.sqrt(dx * dx + dy * dy + dz * dz);
+            }
+        }
+        return e;
+    }
+
+    public static void main(String[] args) {
+        int n = Integer.parseInt(args[0]);
+        offsetMomentum();
+        double before = energy();
+        advance(0.01, n);
+        double after = energy();
+        System.out.println(String.format(Locale.ROOT, "%.9f %.9f", before, after));
+    }
+}

benchmarks/typedpython/java/SpectralNorm.java

@@ -0,0 +1,46 @@
+import java.util.Locale;
+
+public class SpectralNorm {
+    static double evalA(int i, int j) {
+        return 1.0 / ((i + j) * (i + j + 1) / 2 + i + 1);
+    }
+
+    static void mulAv(int n, double[] v, double[] out) {
+        for (int i = 0; i < n; i++) {
+            double s = 0.0;
+            for (int j = 0; j < n; j++) s += evalA(i, j) * v[j];
+            out[i] = s;
+        }
+    }
+
+    static void mulAtv(int n, double[] v, double[] out) {
+        for (int i = 0; i < n; i++) {
+            double s = 0.0;
+            for (int j = 0; j < n; j++) s += evalA(j, i) * v[j];
+            out[i] = s;
+        }
+    }
+
+    static void mulAtAv(int n, double[] v, double[] out, double[] tmp) {
+        mulAv(n, v, tmp);
+        mulAtv(n, tmp, out);
+    }
+
+    public static void main(String[] args) {
+        int n = Integer.parseInt(args[0]);
+        double[] u = new double[n];
+        double[] v = new double[n];
+        double[] tmp = new double[n];
+        java.util.Arrays.fill(u, 1.0);
+        for (int k = 0; k < 10; k++) {
+            mulAtAv(n, u, v, tmp);
+            mulAtAv(n, v, u, tmp);
+        }
+        double vbv = 0.0, vv = 0.0;
+        for (int i = 0; i < n; i++) {
+            vbv += u[i] * v[i];
+            vv += v[i] * v[i];
+        }
+        System.out.println(String.format(Locale.ROOT, "%.9f", Math.sqrt(vbv / vv)));
+    }
+}

benchmarks/typedpython/java/Wordfreq.java

@@ -0,0 +1,51 @@
+import java.util.ArrayList;
+import java.util.HashMap;
+import java.util.List;
+import java.util.Map;
+
+public class Wordfreq {
+    static final long VOCAB = 50000;
+    static final long MOD = 2147483647L;
+
+    static long nextState(long s) { return (s * 48271) % MOD; }
+
+    static String wordOf(long id) {
+        long x = id + 17576;
+        StringBuilder sb = new StringBuilder();
+        while (x > 0) {
+            sb.append((char) (97 + x % 26));
+            x /= 26;
+        }
+        return sb.reverse().toString();
+    }
+
+    public static void main(String[] args) {
+        int n = Integer.parseInt(args[0]);
+        Map<String, Integer> counts = new HashMap<>();
+        long s = 12345;
+        for (int i = 0; i < n; i++) {
+            s = nextState(s);
+            long a = s % VOCAB;
+            s = nextState(s);
+            long b = s % VOCAB;
+            counts.merge(wordOf(a * b / VOCAB), 1, Integer::sum);
+        }
+        long weighted = 0;
+        for (int c : counts.values()) weighted += (long) c * c;
+        List<String> taken = new ArrayList<>();
+        List<String> parts = new ArrayList<>();
+        for (int k = 0; k < 5; k++) {
+            String bestWord = "";
+            int bestCount = -1;
+            for (Map.Entry<String, Integer> e : counts.entrySet()) {
+                String w = e.getKey();
+                int c = e.getValue();
+                if (taken.contains(w)) continue;
+                if (c > bestCount || (c == bestCount && w.compareTo(bestWord) < 0)) { bestWord = w; bestCount = c; }
+            }
+            taken.add(bestWord);
+            parts.add(bestWord + ":" + bestCount);
+        }
+        System.out.println(counts.size() + " " + weighted + " " + String.join(",", parts));
+    }
+}

benchmarks/typedpython/js/binary_trees.mjs

@@ -0,0 +1,25 @@
+class Node {
+  constructor(left, right) { this.left = left; this.right = right; }
+}
+function make(depth) {
+  if (depth > 0) return new Node(make(depth - 1), make(depth - 1));
+  return new Node(null, null);
+}
+function check(node) {
+  const left = node.left, right = node.right;
+  if (left === null || right === null) return 1;
+  return 1 + check(left) + check(right);
+}
+const n = parseInt(process.argv[2], 10);
+const minDepth = 4;
+const maxDepth = Math.max(minDepth + 2, n);
+const stretch = check(make(maxDepth + 1));
+const longLived = make(maxDepth);
+let total = 0;
+for (let depth = minDepth; depth <= maxDepth; depth += 2) {
+  const iterations = 1 << (maxDepth - depth + minDepth);
+  let chk = 0;
+  for (let i = 0; i < iterations; i++) chk += check(make(depth));
+  total += chk;
+}
+console.log(`${stretch} ${total} ${check(longLived)}`);

benchmarks/typedpython/js/fannkuch.mjs

@@ -0,0 +1,34 @@
+function fannkuch(n) {
+  const perm1 = Array.from({ length: n }, (_, i) => i);
+  const count = new Array(n).fill(0);
+  let maxFlips = 0, checksum = 0, permCount = 0, r = n;
+  for (;;) {
+    while (r !== 1) { count[r - 1] = r; r--; }
+    const perm = perm1.slice();
+    let flips = 0;
+    let k = perm[0];
+    while (k !== 0) {
+      let lo = 0, hi = k;
+      while (lo < hi) {
+        const t = perm[lo]; perm[lo] = perm[hi]; perm[hi] = t;
+        lo++; hi--;
+      }
+      flips++;
+      k = perm[0];
+    }
+    if (flips > maxFlips) maxFlips = flips;
+    if (permCount % 2 === 0) checksum += flips; else checksum -= flips;
+    for (;;) {
+      if (r === n) return [checksum, maxFlips];
+      const p0 = perm1[0];
+      for (let i = 0; i < r; i++) perm1[i] = perm1[i + 1];
+      perm1[r] = p0;
+      count[r]--;
+      if (count[r] > 0) break;
+      r++;
+    }
+    permCount++;
+  }
+}
+const [checksum, maxFlips] = fannkuch(parseInt(process.argv[2], 10));
+console.log(`${checksum} ${maxFlips}`);