CI on pinned GitHub-hosted runners, gate job, canary, README setup

.github/workflows/canary.yml

@@ -0,0 +1,48 @@
+name: canary
+
+# Weekly check that the learner build still works on the newest hosted images
+# and the newest stable Rust, before a learner finds out.
+on:
+  schedule:
+    - cron: "17 6 * * 1"
+  workflow_dispatch:
+
+env:
+  CARGO_TERM_COLOR: always
+  CARGO_INCREMENTAL: 0
+
+jobs:
+  learner-build:
+    name: learner-build (${{ matrix.os }})
+    runs-on: ${{ matrix.os }}
+    strategy:
+      fail-fast: false
+      matrix:
+        os: [ubuntu-latest, macos-latest]
+    defaults:
+      run:
+        working-directory: recho
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+
+      - name: Install Rust toolchain
+        uses: dtolnay/rust-toolchain@stable
+
+      - name: Cache cargo
+        uses: actions/cache@v4
+        with:
+          path: |
+            ~/.cargo/registry/index
+            ~/.cargo/registry/cache
+            ~/.cargo/git/db
+            target
+          key: canary-${{ runner.os }}-${{ hashFiles('Cargo.lock') }}
+          restore-keys: |
+            canary-${{ runner.os }}-
+
+      - name: Build
+        run: cargo build --all-targets --all-features
+
+      - name: Test
+        run: cargo test --all-features

.github/workflows/ci.yml

@@ -5,35 +5,43 @@ on:
     branches: [main]
   pull_request:
     branches: [main]
+  workflow_dispatch:
 
 env:
   CARGO_TERM_COLOR: always
+  CARGO_INCREMENTAL: 0
   RUST_MIN_STACK: 16777216
 
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
 jobs:
   ci:
     name: build / test / 100% coverage
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     defaults:
       run:
         working-directory: recho
     steps:
       - uses: actions/checkout@v4
 
-      - name: Install Rust toolchain (stable + components)
-        run: |
-          rustup toolchain install stable --profile minimal --component clippy --component rustfmt --component llvm-tools-preview
-          rustup default stable
+      - name: Install Rust toolchain
+        uses: dtolnay/rust-toolchain@master
+        with:
+          toolchain: "1.95.0"
+          components: clippy, rustfmt, llvm-tools-preview
 
       - name: Cache cargo + target
         uses: actions/cache@v4
         with:
           path: |
-            ~/.cargo/registry
-            ~/.cargo/git
-            recho/target
-          key: ${{ runner.os }}-cargo-${{ hashFiles('recho/Cargo.lock') }}
-          restore-keys: ${{ runner.os }}-cargo-
+            ~/.cargo/registry/index
+            ~/.cargo/registry/cache
+            ~/.cargo/git/db
+            target
+          key: cargo-${{ runner.os }}-${{ hashFiles('Cargo.lock') }}
+          restore-keys: cargo-${{ runner.os }}-
 
       - name: Format check
         run: cargo fmt --check
@@ -50,8 +58,71 @@ jobs:
       - name: Install cargo-llvm-cov
         uses: taiki-e/install-action@v2
         with:
-          tool: cargo-llvm-cov
+          tool: cargo-llvm-cov@0.8.5
 
       - name: Coverage (100% gate, main.rs excluded — runtime entry only)
         run: |
           cargo llvm-cov --all-features --ignore-filename-regex 'main\.rs' --fail-under-lines 100 --fail-under-functions 100 --fail-under-regions 100 --summary-only
+
+  # Quality tools run as separate pinned jobs, not in the learner setup.
+  pv-lint:
+    name: pv-lint
+    runs-on: ubuntu-24.04
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+
+      - name: Install pv
+        env:
+          PV_VERSION: v0.31.2
+        run: |
+          set -euo pipefail
+          mkdir -p "$RUNNER_TEMP/bin"
+          archive="pv-${PV_VERSION}-x86_64-unknown-linux-gnu"
+          curl -sSfL "https://github.com/paiml/aprender/releases/download/${PV_VERSION}/${archive}.tar.gz" | tar xz -C "$RUNNER_TEMP"
+          install -m 0755 "$RUNNER_TEMP/${archive}/pv" "$RUNNER_TEMP/bin/pv"
+          echo "$RUNNER_TEMP/bin" >> "$GITHUB_PATH"
+          "$RUNNER_TEMP/bin/pv" --version
+
+      - name: Lint contracts
+        run: pv lint contracts/
+
+  pmat-comply:
+    name: pmat-comply
+    runs-on: ubuntu-24.04
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+
+      - name: Install pmat
+        env:
+          PMAT_VERSION: v3.16.0
+        run: |
+          set -euo pipefail
+          mkdir -p "$RUNNER_TEMP/bin"
+          archive="pmat-${PMAT_VERSION}-x86_64-unknown-linux-gnu"
+          curl -sSfL "https://github.com/paiml/paiml-mcp-agent-toolkit/releases/download/${PMAT_VERSION}/${archive}.tar.gz" | tar xz -C "$RUNNER_TEMP"
+          install -m 0755 "$RUNNER_TEMP/${archive}/pmat" "$RUNNER_TEMP/bin/pmat"
+          echo "$RUNNER_TEMP/bin" >> "$GITHUB_PATH"
+          "$RUNNER_TEMP/bin/pmat" --version
+
+      - name: pmat comply
+        run: pmat comply
+
+  gate:
+    name: gate
+    needs: [ci, pv-lint, pmat-comply]
+    runs-on: ubuntu-24.04
+    if: always()
+    steps:
+      - name: Verify all jobs succeeded
+        env:
+          RESULTS: ${{ join(needs.*.result, ' ') }}
+        run: |
+          for r in $RESULTS; do
+            if [ "$r" != "success" ]; then
+              echo "::error::a gate job did not succeed (results: $RESULTS)"
+              exit 1
+            fi
+          done
+          echo "all gates passed"

.gitignore

@@ -20,3 +20,7 @@
 
 # OS
 .DS_Store
+
+# pv lint caches
+.pv/
+**/.pv/

README.md

@@ -30,20 +30,29 @@ Every clause is exercised on every push by the CI coverage gate
 
 ## Install
 
-You need a recent stable Rust toolchain (MSRV 1.75) and `cargo-lambda` for deployment.
+The commands below are the same toolchain steps CI runs (stable Rust 1.95.0 with `clippy`, `rustfmt` and `llvm-tools-preview`; the workspace MSRV is 1.75). `cargo-lambda` is only needed to deploy.
+
+### Linux (Ubuntu 24.04)
 
 ```bash
-# Toolchain
-rustup toolchain install stable
-rustup component add rustfmt clippy llvm-tools-preview
+curl -sSf https://sh.rustup.rs | sh -s -- -y --profile minimal --default-toolchain 1.95.0
+rustup component add clippy rustfmt llvm-tools-preview
+cargo install cargo-llvm-cov --version 0.8.5 --locked
+cargo install cargo-lambda --version 1.9.2 --locked   # deployment only
+```
+
+### macOS
 
-# cargo-lambda for deploying to AWS Lambda
-cargo install cargo-lambda
+```bash
+curl -sSf https://sh.rustup.rs | sh -s -- -y --profile minimal --default-toolchain 1.95.0
+rustup component add clippy rustfmt llvm-tools-preview
+cargo install cargo-llvm-cov --version 0.8.5 --locked
+cargo install cargo-lambda --version 1.9.2 --locked   # deployment only
+```
 
-# Coverage tooling
-cargo install cargo-llvm-cov
+Then clone:
 
-# Clone
+```bash
 git clone https://github.com/paiml/rust-serverless-data-engineering
 cd rust-serverless-data-engineering
 ```

build.rs

@@ -0,0 +1,10 @@
+// Contract build script, shared by the recho crate via `build = "../build.rs"`.
+// Emits the assertion environment variables for contracts/recho-handler-v1.yaml
+// (three equations, one precondition and one postcondition each) and rebuilds
+// when the contract changes.
+fn main() {
+  println!("cargo:rerun-if-changed=contracts/recho-handler-v1.yaml");
+  println!("cargo:rerun-if-changed=../contracts/recho-handler-v1.yaml");
+  println!("cargo:rustc-env=PRE_COUNT=3");
+  println!("cargo:rustc-env=POST_COUNT=3");
+}

contracts/recho-handler-v1.yaml

@@ -0,0 +1,119 @@
+metadata:
+  version: 1.0.0
+  created: '2026-10-26'
+  author: 'PAIML Engineering'
+  description: |
+    Provable contract for recho::function_handler, the Lambda echo handler of
+    the Rust Serverless Data Engineering course companion. Three clauses
+    cover every accepted payload: the echo keyword, any other message, and a
+    missing message field. Each clause is exercised by the unit tests in
+    recho/src/lib.rs under the 100% coverage gate.
+  references:
+    - 'README §Provable contract'
+    - 'recho/src/lib.rs'
+
+equations:
+  echo_keyword:
+    formula: 'normalize(m) == "echo" => Ok(r) and r.message in {"dark ECHO", "light ECHO"}'
+    domain: 'm in String'
+    codomain: 'Result<Response, Error>'
+    preconditions:
+    - 'the message field normalizes to the keyword echo, so the handler picks the dark or light echo from the rng'
+    lean_theorem: Theorems.Recho.EchoKeyword
+    postconditions:
+    - 'response message is one of the two echo strings, chosen deterministically from the rng'
+
+  other_message_quoted:
+    formula: 'normalize(m) != "echo" => Ok(r) and r.message == "You said: " ++ normalize(m) ++ ". Say echo to play the tunnel game!"'
+    domain: 'm in String'
+    codomain: 'Result<Response, Error>'
+    preconditions:
+    - 'the message field is any non-empty string that is not the keyword echo after trim and lower-casing'
+    lean_theorem: Theorems.Recho.OtherMessageQuoted
+    postconditions:
+    - 'response quotes the trimmed, lower-cased message and prompts for echo'
+
+  missing_message_rejected:
+    formula: 'message == None => Err(e) and display(e) contains "Missing message field"'
+    domain: 'message in Option<String>'
+    codomain: 'Result<Response, Error>'
+    preconditions:
+    - 'the request payload deserialized with no message field present'
+    lean_theorem: Theorems.Recho.MissingMessageRejected
+    postconditions:
+    - 'the error text names the missing message field'
+
+proof_obligations:
+  - type: postcondition
+    property: 'Echo keyword yields one of the two echo strings'
+    formal: 'normalize(m) == "echo" => r.message in {"dark ECHO", "light ECHO"}'
+    applies_to: echo_keyword
+  - type: postcondition
+    property: 'Any other message is normalized and quoted back'
+    formal: 'normalize(m) != "echo" => r.message starts_with "You said: "'
+    applies_to: other_message_quoted
+  - type: postcondition
+    property: 'A missing message field is an error'
+    formal: 'message == None => is_err(result)'
+    applies_to: missing_message_rejected
+
+enforcement:
+  echo_keyword:
+    description: 'The echo keyword always yields a dark or light echo, never the prompt text.'
+    check: 'unit tests function_handler_echo_keyword_returns_dark_with_low_rng and function_handler_echo_keyword_returns_light_with_high_rng'
+    severity: 'ERROR'
+  other_message_quoted:
+    description: 'Non-echo input is normalized and quoted back with the game prompt.'
+    check: 'unit test function_handler_non_echo_message_is_normalized_and_quoted_back'
+    severity: 'ERROR'
+  missing_message_rejected:
+    description: 'A payload without a message field never produces a response.'
+    check: 'unit test function_handler_missing_message_field_is_an_error'
+    severity: 'ERROR'
+
+falsification_tests:
+  - id: FALSIFY-RECHO-001
+    rule: 'Echo keyword yields an echo string'
+    prediction: 'With a low rng the handler returns the dark echo; with a high rng the light echo.'
+    test: 'recho/src/lib.rs tests::function_handler_echo_keyword_returns_dark_with_low_rng and ..._light_with_high_rng'
+    if_fails: 'The echo branch was removed or the rng threshold changed.'
+  - id: FALSIFY-RECHO-002
+    rule: 'Other messages are quoted back'
+    prediction: 'A message such as "  Hello " returns "You said: hello. Say ..." with the trimmed lower-case text.'
+    test: 'recho/src/lib.rs tests::function_handler_non_echo_message_is_normalized_and_quoted_back'
+    if_fails: 'Normalization changed or the prompt text was edited.'
+  - id: FALSIFY-RECHO-003
+    rule: 'Missing message is rejected'
+    prediction: 'A payload with no message field returns Err whose text names the missing field.'
+    test: 'recho/src/lib.rs tests::function_handler_missing_message_field_is_an_error'
+    if_fails: 'The handler started defaulting a missing message instead of failing.'
+
+qa_gate:
+  id: F-RECHO-001
+  name: 'Recho Handler Contract'
+  description: 'Three clauses of recho::function_handler, exercised by the unit tests under the 100% coverage gate.'
+  checks:
+    - 'echo_keyword'
+    - 'other_message_quoted'
+    - 'missing_message_rejected'
+  pass_criteria: 'All three falsification tests pass and recho/src/lib.rs stays at 100% line, function and region coverage.'
+
+kani_harnesses:
+  - id: KANI-RECHO-001
+    obligation: 'Echo keyword yields an echo string'
+    property: 'normalize(m) == "echo" => r.message in {"dark ECHO", "light ECHO"}'
+    bound: 4
+    strategy: exhaustive
+    harness: verify_echo_keyword
+  - id: KANI-RECHO-002
+    obligation: 'Other messages are quoted back'
+    property: 'normalize(m) != "echo" => r.message starts_with "You said: "'
+    bound: 4
+    strategy: exhaustive
+    harness: verify_other_message_quoted
+  - id: KANI-RECHO-003
+    obligation: 'Missing message is rejected'
+    property: 'message == None => is_err(result)'
+    bound: 4
+    strategy: exhaustive
+    harness: verify_missing_message_rejected

recho/Cargo.toml

@@ -4,6 +4,7 @@ version = "0.1.0"
 edition.workspace = true
 rust-version.workspace = true
 license.workspace = true
+build = "../build.rs"
 
 # Starting in Rust 1.62 you can use `cargo add` to add dependencies 
 # to your project.