feat(sap): wire real-SAP E2E into CI via a self-hosted runner

.github/workflows/sap-e2e.yml

@@ -0,0 +1,67 @@
+name: SAP E2E (real GUI)
+
+# Tier 3 of the SAP testing ladder (see #32): the fake engine (sap_pipeline)
+# and the COM simulator (sap_sim_e2e) run on every push via ci.yml. This
+# workflow is the one that talks to an actual SAP GUI session, so it needs
+# the self-hosted `sap` runner and stays out of the pull_request path —
+# fork PRs must never reach a real SAP system.
+on:
+  workflow_dispatch:
+  schedule:
+    - cron: "0 3 * * *"
+
+# Only one physical SAP GUI session exists on the runner; a second run
+# stepping on it mid-navigation is worse than making the next one wait.
+concurrency:
+  group: sap-e2e
+  cancel-in-progress: false
+
+env:
+  CARGO_TERM_COLOR: always
+
+jobs:
+  sap-e2e:
+    name: sap_e2e (real SAP GUI)
+    runs-on: [self-hosted, sap]
+    timeout-minutes: 20
+    steps:
+      - uses: actions/checkout@v4
+
+      # Nightly runs have nobody at the keyboard: make sure SAP Logon is up
+      # and clear the handful of modal dialogs known to block scripting
+      # (multiple-logon prompts, license info) before they can stall the job.
+      - name: session bootstrap
+        shell: pwsh
+        run: ./scripts/sap-session-bootstrap.ps1
+        env:
+          SAP_CONNECTION: ${{ secrets.SAP_CONNECTION }}
+
+      - name: cargo test sap_e2e (real COM engine, live SAP GUI)
+        run: cargo test -p flowproof-cli --test sap_e2e -- --nocapture
+        env:
+          FLOWPROOF_E2E_SAP: "1"
+          # ${VAR} indirection: FlowSpec.connection carries this literally
+          # and resolves it at launch time, so the value never reaches a
+          # trace file or a log line.
+          SAP_CONNECTION: ${{ secrets.SAP_CONNECTION }}
+
+      # Broader coverage than the one hardcoded correctness check above:
+      # replays every committed example flow as a suite (zero AI, each
+      # trace already recorded against this same reference SAP system).
+      # view-order.flow.yaml and stock-overview.flow.yaml assume order 314
+      # and material MZ-FG-C900 exist on whichever system this runner
+      # points at — real data on the reference system this was recorded
+      # against, not guaranteed elsewhere.
+      - name: replay SAP example flows (live SAP GUI)
+        run: cargo run -p flowproof-cli --bin flowproof -- run examples/sap/
+        env:
+          SAP_CONNECTION: ${{ secrets.SAP_CONNECTION }}
+
+      # Leave the session clean for whichever run is next, whether that's
+      # tonight's schedule or a manual dispatch during the working day.
+      - name: session reset
+        if: always()
+        shell: pwsh
+        run: ./scripts/sap-session-bootstrap.ps1
+        env:
+          SAP_CONNECTION: ${{ secrets.SAP_CONNECTION }}

crates/flowproof-cli/tests/sap_e2e.rs

@@ -1,6 +1,7 @@
-//! End-to-end against a REAL SAP GUI session. No CI runner has one, so
-//! this is maintainer-run: Windows, SAP GUI installed, logged in, scripting
-//! enabled (`sapgui/user_scripting = TRUE`), and FLOWPROOF_E2E_SAP=1.
+//! End-to-end against a REAL SAP GUI session: on the self-hosted `sap`
+//! runner via .github/workflows/sap-e2e.yml (see #32), or maintainer-run
+//! locally with Windows, SAP GUI installed, logged in, scripting enabled
+//! (`sapgui/user_scripting = TRUE`), and FLOWPROOF_E2E_SAP=1.
 //!
 //! The flow only navigates and reads — it types a transaction code and
 //! asserts on the status/title, touching no business data.
@@ -10,13 +11,19 @@
 use flowproof_adapters::sap_com::SapAppDriver;
 use flowproof_agent::FlowSpec;
 
-const SPEC: &str = "\
-name: Navigate to session status
-app: sap
-steps:
-  - Go to /nSESSION_MANAGER
-  - assert: page shows Session
-";
+/// A logged-in session already exists on every machine this test runs on
+/// today (attach-only, `connection` omitted). SAP_CONNECTION lets an
+/// unattended nightly run open one instead, should the runner ever come up
+/// without one — the value is carried as `${VAR}` and resolved at launch
+/// time, so it never reaches the trace.
+fn spec_yaml() -> String {
+    let mut spec = String::from("name: Navigate to session status\napp: sap\n");
+    if std::env::var("SAP_CONNECTION").is_ok() {
+        spec.push_str("connection: ${SAP_CONNECTION}\n");
+    }
+    spec.push_str("steps:\n  - Go to /nSESSION_MANAGER\n  - assert: page shows Session\n");
+    spec
+}
 
 #[test]
 fn navigates_a_real_sap_session() {
@@ -31,7 +38,7 @@ fn navigates_a_real_sap_session() {
     std::fs::create_dir_all(&dir).expect("temp dir");
     let trace_path = dir.join("session.trace.jsonl");
 
-    let spec = FlowSpec::parse(SPEC).expect("spec parses");
+    let spec = FlowSpec::parse(&spec_yaml()).expect("spec parses");
 
     let mut driver = SapAppDriver::new().expect("COM engine");
     flowproof_agent::record(&spec, &mut driver, &trace_path).expect("records against live SAP");

scripts/sap-session-bootstrap.ps1

@@ -0,0 +1,41 @@
+<#
+  Run before and after sap_e2e on the self-hosted `sap` runner. Unattended
+  (nightly) runs have nobody at the keyboard, so this closes the small set
+  of modal dialogs known to block SAP GUI Scripting - a multiple-logon
+  prompt or a license-information notice left open stalls FindById forever
+  otherwise - and makes sure SAP Logon itself is running.
+
+  Best-effort: the dialog titles below are the common English ones seen in
+  practice, not an exhaustive list. If a future dialog isn't covered, add
+  its title here rather than reworking the loop.
+#>
+
+$ErrorActionPreference = 'Stop'
+
+$blockingTitles = @(
+    'License Information for Multiple Logon',
+    'Information'
+)
+
+$shell = New-Object -ComObject WScript.Shell
+
+foreach ($title in $blockingTitles) {
+    Get-Process | Where-Object { $_.MainWindowTitle -eq $title } | ForEach-Object {
+        if ($shell.AppActivate($_.Id)) {
+            Start-Sleep -Milliseconds 300
+            $shell.SendKeys('~')  # Enter - accept the dialog's default button
+            Write-Host "Dismissed blocking dialog: $title"
+        }
+    }
+}
+
+if (-not (Get-Process -Name saplogon -ErrorAction SilentlyContinue)) {
+    if (-not $env:SAP_CONNECTION) {
+        Write-Error "saplogon.exe is not running and SAP_CONNECTION is not set - cannot open a session unattended."
+    }
+    Write-Host "SAP Logon is not running - starting it."
+    Start-Process 'saplogon.exe'
+    Start-Sleep -Seconds 5
+}
+
+Write-Host 'SAP session bootstrap complete.'