merge: resolve conflicts in bet-wasm

Author: hyperpolymath

.github/workflows/scorecard-enforcer.yml

@@ -17,17 +17,24 @@ concurrency:
   group: ${{ github.workflow }}-${{ github.ref }}
   cancel-in-progress: true
 
-permissions: read-all
+permissions:
+  contents: read
 
 jobs:
+  # Publish job. The OSSF attestation flow requires that a job invoking
+  # ossf/scorecard-action with publish_results: true contain ONLY `uses:`
+  # steps (no `run:`). A `run:` step in this job makes the OSSF publish
+  # endpoint reject the upload with HTTP 400 ("scorecard job must only have
+  # steps with `uses`"), failing the whole workflow. Score enforcement is
+  # therefore split into the separate unprivileged `score-gate` job below.
   scorecard:
     runs-on: ubuntu-latest
-    timeout-minutes: 30
+    timeout-minutes: 15
     permissions:
       security-events: write
       id-token: write  # For OIDC
     steps:
-      - uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v4
+      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
         with:
           persist-credentials: false
 
@@ -39,14 +46,39 @@ jobs:
           publish_results: true
 
       - name: Upload SARIF
-        uses: github/codeql-action/upload-sarif@8aad20d150bbac5944a9f9d289da16a4b0d87c1e # v3
+        uses: github/codeql-action/upload-sarif@c6f931105cb2c34c8f901cc885ba1e2e259cf745 # v4
         with:
           sarif_file: results.sarif
 
+  # Unprivileged enforcement gate. Re-derives the score read-only (no
+  # publish, no id-token), so it may legally contain a `run:` step.
+  # NOTE: uses JSON output deliberately. The SARIF format does NOT carry the
+  # aggregate score at .runs[0].tool.driver.properties.score (it is absent
+  # there, so a SARIF-based gate reads the `// 0` fallback and ALWAYS fails
+  # the < MIN_SCORE check); the JSON format exposes the aggregate at the
+  # top-level `.score`. publish_results is false here and does not affect the
+  # computed score, so enforcement behaviour is unchanged.
+  score-gate:
+    runs-on: ubuntu-latest
+    timeout-minutes: 15
+    permissions:
+      contents: read
+    steps:
+      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+        with:
+          persist-credentials: false
+
+      - name: Run Scorecard (analysis only)
+        uses: ossf/scorecard-action@4eaacf0543bb3f2c246792bd56e8cdeffafb205a # v2.4.3
+        with:
+          results_file: results.json
+          results_format: json
+          publish_results: false
+
       - name: Check minimum score
         run: |
-          # Parse score from results
-          SCORE=$(jq -r '.runs[0].tool.driver.properties.score // 0' results.sarif 2>/dev/null || echo "0")
+          # JSON output carries the aggregate score at the top-level `.score`.
+          SCORE=$(jq -r '.score // 0' results.json 2>/dev/null || echo "0")
 
           echo "OpenSSF Scorecard Score: $SCORE"
 
@@ -61,9 +93,9 @@ jobs:
   # Check specific high-priority items
   check-critical:
     runs-on: ubuntu-latest
-    timeout-minutes: 30
+    timeout-minutes: 15
     steps:
-      - uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v4
+      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
 
       - name: Check SECURITY.md exists
         run: |

Justfile

@@ -1,5 +1,5 @@
-// SPDX-License-Identifier: MPL-2.0
-// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 # betlang - Development Tasks
 # AUTHORITY: AUTHORITY_STACK.mustfile-nickel.scm
 # All operations MUST be invoked via `just <recipe>`.
@@ -84,6 +84,34 @@ test-tooling:
 clean-tooling:
     cargo clean
 
+# --- Rust toolchain recipes (the working compiler/interpreter pipeline) ------
+# These drive the real multi-crate Rust implementation under compiler/, runtime/
+# and tools/. (The Racket recipes above target the historical core/*.rkt tree.)
+
+# Build the entire Rust workspace (all crates)
+build-rust:
+    cargo build --workspace
+
+# Test the entire Rust workspace
+test-rust:
+    cargo test --workspace
+
+# Type-check a betlang source file with the Rust checker
+check FILE:
+    cargo run -q -p bet -- check {{FILE}}
+
+# Run a betlang source file with the Rust interpreter
+run FILE:
+    cargo run -q -p bet -- run {{FILE}}
+
+# Compile a betlang source file to a backend (TARGET = js | llvm | beam)
+compile FILE TARGET="js":
+    cargo run -q -p bet -- compile {{FILE}} --target {{TARGET}}
+
+# Start the Rust REPL
+repl-rust:
+    cargo run -q -p bet -- repl
+
 # ============================================================================
 # PROOFS (formal verification — see docs/AFFINESCRIPT-ALIGNMENT.adoc)
 # ============================================================================

bindings/chapel/Cargo.toml

@@ -18,6 +18,7 @@ libc = "0.2"
 # Core
 rand.workspace = true
 rand_distr.workspace = true
+rand_pcg.workspace = true   # seedable PCG generator for `bet_seed`
 
 [build-dependencies]
 cbindgen = "0.28"

bindings/chapel/build.rs

@@ -10,6 +10,15 @@ fn main() {
         .with_language(cbindgen::Language::C)
         .with_include_guard("BET_CHAPEL_H")
         .with_documentation(true)
+        // Preserve the SPDX/copyright header on the generated file. cbindgen
+        // overwrites include/betlang.h wholesale on every build; without this
+        // the licence header is silently stripped each time (an automated
+        // licence edit, which estate policy forbids — keep it manual & stable).
+        .with_header(
+            "// SPDX-License-Identifier: MPL-2.0\n\
+             // Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>\n\
+             // GENERATED by cbindgen (build.rs) — do not edit by hand.",
+        )
         .generate()
         .expect("Unable to generate bindings")
         .write_to_file("include/betlang.h");

bindings/chapel/include/betlang.h

@@ -1,5 +1,7 @@
 // SPDX-License-Identifier: MPL-2.0
 // Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+// GENERATED by cbindgen (build.rs) — do not edit by hand.
+
 #ifndef BET_CHAPEL_H
 #define BET_CHAPEL_H
 
@@ -143,4 +145,4 @@ void bet_seed(uint64_t seed);
  */
 const char *bet_version(void);
 
-#endif /* BET_CHAPEL_H */
+#endif  /* BET_CHAPEL_H */

compiler/bet-check/src/lib.rs

@@ -837,7 +837,10 @@ fn check_bet(bet: &BetExpr, env: &mut CheckEnv, span: Span) -> CompileResult<Typ
 
     env.unify(&t0, &t1, Some(span))?;
     env.unify(&t0, &t2, Some(span))?;
-    Ok(env.resolve(&t0))
+    // A `bet` introduces probabilistic choice: it has type `Dist T`, not `T`.
+    // (Matches the mechanised rule `tBet : … → HasType … (Ty.dist T)` in
+    // proofs/BetLang.lean; eliminate with `sample : Dist 'a -> 'a`.)
+    Ok(Type::Dist(Box::new(env.resolve(&t0))))
 }
 
 /// Check a weighted bet: branches unify, weights must be numeric.
@@ -863,7 +866,8 @@ fn check_weighted_bet(
     for i in 1..branch_types.len() {
         env.unify(&branch_types[0], &branch_types[i], Some(span))?;
     }
-    Ok(env.resolve(&branch_types[0]))
+    // Weighted bet, like uniform bet, is a distribution: `Dist T`.
+    Ok(Type::Dist(Box::new(env.resolve(&branch_types[0]))))
 }
 
 /// Check a conditional bet: condition is Bool/Ternary, all branches unify.
@@ -892,7 +896,9 @@ fn check_conditional_bet(
     env.unify(&true_ty, &f0, Some(span))?;
     env.unify(&true_ty, &f1, Some(span))?;
     env.unify(&true_ty, &f2, Some(span))?;
-    Ok(env.resolve(&true_ty))
+    // Conditional bet also yields a distribution over `T`: point-mass on the
+    // `if_true` value when the condition holds, else the ternary distribution.
+    Ok(Type::Dist(Box::new(env.resolve(&true_ty))))
 }
 
 // ============================================
@@ -1265,7 +1271,11 @@ mod tests {
             ],
         };
         let result = check_expr(&dummy(Expr::Bet(bet)), &mut env);
-        assert_eq!(result.expect("TODO: handle error"), Type::Int);
+        // `bet` introduces probabilistic choice, so its type is `Dist Int`.
+        assert_eq!(
+            result.expect("TODO: handle error"),
+            Type::Dist(Box::new(Type::Int))
+        );
     }
 
     #[test]
@@ -1699,9 +1709,11 @@ mod tests {
         );
     }
 
-    /// The core primitive bridges to Echo by composition at the type level:
-    /// `echo(bet a b c) : Echo T`. (Runtime branch-tag retention — `bet_echo` —
-    /// remains deferred; the *type* story needs no new primitive.)
+    /// The core primitive bridges to Echo by composition at the type level.
+    /// Since `bet a b c : Dist T`, the composite is `echo(bet a b c) : Echo (Dist T)`
+    /// — the retained-loss residue over the *distribution*. (Runtime branch-tag
+    /// retention — `bet_echo` — remains deferred; the *type* story needs no new
+    /// primitive.)
     #[test]
     fn test_bet_echo_bridge_by_composition() {
         let mut env = CheckEnv::new();
@@ -1714,8 +1726,8 @@ mod tests {
         };
         let e = call("echo", vec![dummy(Expr::Bet(bet))]);
         assert_eq!(
-            check_expr(&e, &mut env).expect("echo (bet 1 2 3) : Echo Int"),
-            Type::Echo(Box::new(Type::Int))
+            check_expr(&e, &mut env).expect("echo (bet 1 2 3) : Echo (Dist Int)"),
+            Type::Echo(Box::new(Type::Dist(Box::new(Type::Int))))
         );
     }
 

compiler/bet-codegen/src/lib.rs

@@ -102,24 +102,36 @@ pub fn codegen_module(module: &Module, target: Target) -> CompileResult<CodeOutp
 fn js_preamble() -> &'static str {
     r#"// === Betlang Runtime Preamble ===
 
-// Uniform ternary choice among exactly 3 alternatives
+// Uniform ternary choice among exactly 3 alternatives.
+// `bet` has type `Dist T`: it returns a *distribution object* (sample with
+// `__bet_sample`), not an eager draw — consistent with the checker/interpreter.
 function __bet_uniform(a, b, c) {
-  const r = Math.random();
-  if (r < 1/3) return a;
-  if (r < 2/3) return b;
-  return c;
+  return {
+    name: 'bet',
+    sample() {
+      const r = Math.random();
+      if (r < 1/3) return a;
+      if (r < 2/3) return b;
+      return c;
+    },
+  };
 }
 
-// Weighted ternary choice (weights normalised internally)
+// Weighted ternary choice (weights normalised internally). Returns a Dist.
 function __bet_weighted(alts, weights) {
-  const total = weights.reduce((s, w) => s + w, 0);
-  const r = Math.random() * total;
-  let cumul = 0;
-  for (let i = 0; i < alts.length; i++) {
-    cumul += weights[i];
-    if (r < cumul) return alts[i];
-  }
-  return alts[alts.length - 1];
+  return {
+    name: 'weighted_bet',
+    sample() {
+      const total = weights.reduce((s, w) => s + w, 0);
+      const r = Math.random() * total;
+      let cumul = 0;
+      for (let i = 0; i < alts.length; i++) {
+        cumul += weights[i];
+        if (r < cumul) return alts[i];
+      }
+      return alts[alts.length - 1];
+    },
+  };
 }
 
 // --- Distribution objects ---

compiler/bet-eval/Cargo.toml

@@ -8,6 +8,9 @@ license.workspace = true
 [dependencies]
 bet-syntax = { path = "../bet-syntax" }
 bet-core = { path = "../bet-core" }
+bet-rt = { path = "../../runtime/bet-rt" }       # the unified runtime Value (Dist, …)
+bet-rand = { path = "../../runtime/bet-rand" }   # centralised ternary/weighted RNG
+im.workspace = true                              # bet_rt::Value::List is im::Vector
 rand.workspace = true
 rand_distr.workspace = true
 thiserror.workspace = true