Skip to content

Commit bc25fad

Browse files
hyperpolymathclaude
andcommitted
fix(uppaal): https for the UPPAAL flat-DTD URI; STATE.a2ml session log
Closes the InsecureProtocol Medium finding from today's chunked panic-attack sweep. uu.se 301-redirects http→https for the DTD URI and the https endpoint returns 200, so flipping the protocol matches upstream's own migration without breaking UPPAAL's reader. STATE.a2ml gains [session-2026-04-25-evening] recording the rest-crate fix + panic-attack chunked sweep + this uppaal fix, plus the deferred follow-ups (echidnabi.ipkg ProofDrift detector miss, 26 prover-wrapper UnboundedAllocation aggregations, Chapel detector gap) and the /api/v1/consult deployment-validation status (code merged, e2e exercise pending a separate session). Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
1 parent 4dbe74f commit bc25fad

2 files changed

Lines changed: 18 additions & 1 deletion

File tree

.machine_readable/6a2/STATE.a2ml

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -811,6 +811,23 @@ pkg-4-open-followups = [
811811
"cargo check --all-targets reveals pre-existing type_info field gap in 4 test binaries (neural_property_tests, aspect_tests, e2e_prover_test, security_aspect_tests): echidna::core::{Hypothesis,Definition,Variable} gained a type_info field but test fixtures were not updated. Independent of Package 4. Needs a separate fix pass.",
812812
]
813813

814+
# ─── Session 2026-04-25 evening: rest-crate fix + chunked panic-attack sweep ─
815+
[session-2026-04-25-evening]
816+
summary = "Two follow-ups closed at end of long session: echidna-rest pre-existing 37 errors fixed (unblocks /api/v1/consult), and the panic-attack full-repo run that had timed out at 180s replaced with a 14-chunk per-subdir sweep."
817+
commits = [
818+
"6c878a1 fix(rest): unblock /api/v1/consult — 37 pre-existing rest-crate errors",
819+
"4dbe74f chore(reports): chunked panic-attack sweep — replaces 180s-timeout single-run",
820+
"<pending> fix(uppaal): https for the UPPAAL flat-DTD URI",
821+
]
822+
rest-crate-fix = "models::ProverKind gains 13 variants (FStar, Dafny, Why3, TLAPS, Twelf, Nuprl, Minlog, Imandra, GLPK, SCIP, MiniZinc, Chuffed, ORTools) so the FFI ordinal table 17..29 round-trips through the REST schema. core_kind_to_rest / rest_kind_to_core wired both ways; drops the '_ => Vampire' mistargeting fallback for ord ≤ 29. FfiProverBackend now implements search_theorems (empty-vec stub), config / set_config (stores ProverConfig). apply_tactic returns CoreTacticResult::Success(state.clone()) (no Box). ProofState::new wrapping in Term::Var to match the new Term-typed core API. c_char ↔ u8 raw-pointer casts at the Zig FFI boundary. 637 lib tests still passing."
823+
panic-attack-sweep = "14 per-subdir chunks (src/rust, src/interfaces, src/julia, src/abi, src/zig, src/zig_ffi, src/idris, src/ada, src/ui, src/rescript, crates/echidna-{core,mcp,wire}, crates/typed_wasm). Combined wall time ~60s; previously single-run timed out at 180s. 44 findings — 41 are in existing memory-rule classes (file-level UnboundedAllocation in 26 prover wrappers, legitimate-FFI UnsafeCode/UnsafeFFI in interface ffi_wrappers + zig bridges, ProofDrift on .ipkg). 3 actionable: SupplyChain on echidna-mcp Cargo.toml (false-positive — workspace Cargo.lock is at root, panic-attack scans crate in isolation), PanicPath on z3.rs (false-positive — the 'expect calls' are parser-helper self.expect(...)? ; the one panic! is a #[test] assertion), InsecureProtocol on uppaal.rs (real, fixed: UPPAAL flat-DTD URI flipped http:// → https://; uu.se 301-redirects already, https returns 200). Reports retained at reports/panic-attack-chunks/*.json + SUMMARY.md."
824+
panic-attack-followups = [
825+
"echidnaabi.ipkg ProofDrift is a detector miss on a config file — worth a panic-attack memory entry to skip .ipkg for ProofDrift class.",
826+
"26 prover-wrapper UnboundedAllocation flags are file-level aggregations per the existing memory rule — per-backend audit pass is its own multi-session work, not a one-shot.",
827+
"src/chapel returned 'Could not detect language' — panic-attack has no Chapel detector. Track separately if Chapel hardening becomes a goal.",
828+
]
829+
consult-deployment-status = "/api/v1/consult code-merged (1195cb0 + 6c878a1). End-to-end exercise against a running echidna server has NOT been done — needs a separate session with podman + boj-server + echidna stood up, then `curl POST /api/v1/consult` with a real question. Branch protection allowed the push through; the 6 required CI checks are presumably running in the background as of this session close."
830+
814831
# ─── Migration roadmap audit 2026-04-25 ─────────────────────────────────────
815832
[migration-roadmap]
816833
date = "2026-04-25"

src/rust/provers/uppaal.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -54,7 +54,7 @@ impl UppaalBackend {
5454

5555
xml.push_str("<?xml version=\"1.0\" encoding=\"utf-8\"?>\n");
5656
xml.push_str("<!DOCTYPE nta PUBLIC '-//Uppaal Team//DTD Flat System 1.1//EN'\n");
57-
xml.push_str(" 'http://www.it.uu.se/research/group/darts/uppaal/flat-1_2.dtd'>\n");
57+
xml.push_str(" 'https://www.it.uu.se/research/group/darts/uppaal/flat-1_2.dtd'>\n");
5858
xml.push_str("<!-- ECHIDNA UPPAAL Export -->\n");
5959
xml.push_str("<nta>\n");
6060

0 commit comments

Comments
 (0)