From 3ce885c5d0a4a5344eb5df862dfcf7a4ec3996fc Mon Sep 17 00:00:00 2001 From: Mario Yaksetig Costa Date: Mon, 22 Jun 2026 19:52:28 -0500 Subject: [PATCH] Fix production readiness gates --- .github/scripts/check_checker_differential.py | 22 +- .github/workflows/ci.yml | 12 +- .../workflows/live-adapter-conformance.yml | 9 + Cargo.lock | 4 +- benchmarks/bymc/Dockerfile | 31 +- crates/tarsier-certcheck/src/tests.rs | 17 +- .../tarsier-cli/src/commands/proof_export.rs | 101 ++++-- crates/tarsier-dsl/src/grammar.pest | 1 - crates/tarsier-dsl/src/parser/tests.rs | 37 +++ fuzz/Cargo.lock | 297 +----------------- fuzz/fuzz_targets/fuzz_encode.rs | 3 +- scripts/cometbft-conformance-active-smoke.sh | 12 +- scripts/cometbft-live-harness.sh | 11 +- scripts/etcd-raft-live-harness.sh | 12 +- 14 files changed, 209 insertions(+), 360 deletions(-) diff --git a/.github/scripts/check_checker_differential.py b/.github/scripts/check_checker_differential.py index d58dfe6..bbe7918 100644 --- a/.github/scripts/check_checker_differential.py +++ b/.github/scripts/check_checker_differential.py @@ -327,16 +327,32 @@ def lookup_allowlist( def ensure_binaries() -> tuple[Path, Path]: - build_cmd = ["cargo", "build", "-p", "tarsier-cli", "-p", "tarsier-certcheck"] + build_cmd = [ + "cargo", + "build", + "-p", + "tarsier-cli", + "-p", + "tarsier-certcheck", + "--features", + "tarsier-cli/governance", + ] print("[info] building checker binaries:", " ".join(build_cmd)) rc, out, err = run_command(build_cmd, ROOT) if rc != 0: sys.stderr.write(out) sys.stderr.write(err) raise RuntimeError("failed to build checker binaries") + metadata_cmd = ["cargo", "metadata", "--no-deps", "--format-version", "1"] + rc, out, err = run_command(metadata_cmd, ROOT) + if rc != 0: + sys.stderr.write(out) + sys.stderr.write(err) + raise RuntimeError("failed to resolve cargo target directory") + target_dir = Path(json.loads(out)["target_directory"]) suffix = ".exe" if sys.platform.startswith("win") else "" - legacy = ROOT / "target" / "debug" / f"tarsier{suffix}" - tiny = ROOT / "target" / "debug" / f"tarsier-certcheck{suffix}" + legacy = target_dir / "debug" / f"tarsier{suffix}" + tiny = target_dir / "debug" / f"tarsier-certcheck{suffix}" if not legacy.exists(): raise RuntimeError(f"missing legacy checker binary: {legacy}") if not tiny.exists(): diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 3bd9768..bcd7883 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -38,6 +38,14 @@ jobs: else base_ref="HEAD" fi + if ! git cat-file -e "${base_ref}^{commit}" 2>/dev/null; then + echo "Base ref ${base_ref} is unavailable; falling back to HEAD^ for maintainability limits." + if git rev-parse --verify HEAD^ >/dev/null 2>&1; then + base_ref="HEAD^" + else + base_ref="HEAD" + fi + fi python3 scripts/check_maintainability_limits.py --base "${base_ref}" - name: Enforce Certification Gate Contract @@ -220,9 +228,9 @@ jobs: - name: Checker Soundness Subset Gate run: | - output=$(cargo test -p tarsier-proof-kernel soundness_subset_ -- --nocapture 2>&1) + output=$(CARGO_TERM_COLOR=never cargo test -p tarsier-proof-kernel soundness_subset_ -- --nocapture 2>&1) echo "$output" - count=$(echo "$output" | grep -Ec 'test tests::soundness_subset_.*\\.\\.\\. ok') + count=$(echo "$output" | grep -Ec '^test tests::soundness_subset_.* \.\.\. ok$') if [ "$count" -lt 2 ]; then echo "ERROR: expected at least 2 checker soundness subset tests to pass, got $count" exit 1 diff --git a/.github/workflows/live-adapter-conformance.yml b/.github/workflows/live-adapter-conformance.yml index 85c991f..ce3f0d7 100644 --- a/.github/workflows/live-adapter-conformance.yml +++ b/.github/workflows/live-adapter-conformance.yml @@ -27,6 +27,7 @@ jobs: runs-on: ubuntu-latest env: CMAKE_POLICY_VERSION_MINIMUM: "3.5" + WAIT_SECS: "120" steps: - name: Checkout uses: actions/checkout@v4 @@ -118,11 +119,13 @@ jobs: REPORT_FILE=artifacts/live-adapter/cometbft-live-report.json \ EVENTS_FILE=artifacts/live-adapter/cometbft-live-events.jsonl \ SERVER_LOG=artifacts/live-adapter/cometbft-live-server.log \ + KEEP_HARNESS=1 \ ./scripts/cometbft-conformance-active-smoke.sh smoke REPORT_FILE=artifacts/live-adapter/etcd-raft-live-report.json \ EVENTS_FILE=artifacts/live-adapter/etcd-raft-live-events.jsonl \ SERVER_LOG=artifacts/live-adapter/etcd-raft-live-server.log \ + KEEP_HARNESS=1 \ ./scripts/etcd-raft-conformance-active-smoke.sh smoke - name: Capture triage details on failure @@ -137,6 +140,12 @@ jobs: docker compose -f integration/etcd-raft-live/docker-compose.yml ps > artifacts/live-adapter/etcd-compose-ps.txt || true docker compose -f integration/etcd-raft-live/docker-compose.yml logs --no-color > artifacts/live-adapter/etcd-compose-logs.txt || true + - name: Stop live harnesses + if: always() + run: | + ./scripts/cometbft-live-harness.sh stop >/dev/null 2>&1 || true + ./scripts/etcd-raft-live-harness.sh stop >/dev/null 2>&1 || true + - name: Upload nightly artifacts if: always() uses: actions/upload-artifact@v4 diff --git a/Cargo.lock b/Cargo.lock index d01820b..e3c244f 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -2068,9 +2068,9 @@ dependencies = [ [[package]] name = "rustls-webpki" -version = "0.103.9" +version = "0.103.13" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d7df23109aa6c1567d1c575b9952556388da57401e4ace1d15f79eedad0d8f53" +checksum = "61c429a8649f110dddef65e2a5ad240f747e85f7758a6bccc7e5777bd33f756e" dependencies = [ "ring", "rustls-pki-types", diff --git a/benchmarks/bymc/Dockerfile b/benchmarks/bymc/Dockerfile index e564212..f494885 100644 --- a/benchmarks/bymc/Dockerfile +++ b/benchmarks/bymc/Dockerfile @@ -1,5 +1,5 @@ # ByMC (Byzantine Model Checker) Docker image -# Pinned to v2.4.4 for reproducible verification runs. +# Pinned to bymc-2.4.2 for reproducible verification runs. # # Build: docker build -t tarsier-bymc:latest benchmarks/bymc/ # Run: docker run --rm -v "$PWD":/work tarsier-bymc:latest /work/model.ta all @@ -7,6 +7,8 @@ FROM ubuntu:18.04 ENV DEBIAN_FRONTEND=noninteractive +ARG OPAM_VERSION=2.1.5 +ARG OPAM_REPOSITORY_REF=2026-05-before-lower-bound-ocaml411 # System dependencies RUN apt-get update && apt-get install -y --no-install-recommends \ @@ -14,20 +16,28 @@ RUN apt-get update && apt-get install -y --no-install-recommends \ ca-certificates \ curl \ git \ + libffi-dev \ + libgmp-dev \ m4 \ + mpi-default-dev \ pkg-config \ + python2.7 \ python3 \ unzip \ wget \ && rm -rf /var/lib/apt/lists/* -# Install opam 2.x -RUN curl -fsSL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh | \ - sh -s -- --version 2.1.5 +# Install a pinned opam binary instead of streaming the mutable installer script. +RUN curl -fsSL \ + "https://github.com/ocaml/opam/releases/download/${OPAM_VERSION}/opam-${OPAM_VERSION}-x86_64-linux" \ + -o /usr/local/bin/opam && \ + chmod +x /usr/local/bin/opam && \ + opam --version # Initialize opam with OCaml 4.06.1 (last version well-supported by ByMC) -RUN opam init --disable-sandboxing --bare -y && \ - opam switch create 4.06.1 && \ +RUN opam init --disable-sandboxing --bare -y --shell=sh \ + default "https://github.com/ocaml/opam-repository.git#${OPAM_REPOSITORY_REF}" && \ + opam switch create 4.06.1 ocaml-base-compiler.4.06.1 -y && \ eval $(opam env) # Install Z3 4.8.7 from GitHub release @@ -38,20 +48,25 @@ RUN wget -q https://github.com/Z3Prover/z3/releases/download/z3-4.8.7/z3-4.8.7-x rm /tmp/z3.zip ENV PATH="/opt/z3/bin:${PATH}" -ENV LD_LIBRARY_PATH="/opt/z3/bin:${LD_LIBRARY_PATH}" +ENV LD_LIBRARY_PATH="/opt/z3/bin" # Install OCaml dependencies via opam RUN eval $(opam env) && \ opam install -y \ + ocamlbuild \ + menhir.20181113 \ batteries \ ocamlgraph \ sexplib \ + lazy-trie.1.2.0 \ + mpi.1.07 \ + z3.4.8.7 \ ctypes \ ctypes-foreign # Clone and build ByMC at pinned tag RUN eval $(opam env) && \ - git clone --depth 1 --branch v2.4.4 https://github.com/konnov/bymc.git /opt/bymc && \ + git clone --depth 1 --branch bymc-2.4.2 https://github.com/konnov/bymc.git /opt/bymc && \ cd /opt/bymc/bymc && \ make diff --git a/crates/tarsier-certcheck/src/tests.rs b/crates/tarsier-certcheck/src/tests.rs index 1447d58..6fc08e7 100644 --- a/crates/tarsier-certcheck/src/tests.rs +++ b/crates/tarsier-certcheck/src/tests.rs @@ -8,7 +8,9 @@ use miette::miette; use std::collections::BTreeMap; use std::fs; use std::path::PathBuf; -use std::time::{SystemTime, UNIX_EPOCH}; +use std::sync::atomic::{AtomicU64, Ordering}; + +static TMP_DIR_COUNTER: AtomicU64 = AtomicU64::new(0); #[test] fn parse_solver_list_dedups_and_sorts() { @@ -115,11 +117,8 @@ fn record_solver_outcome_tracks_per_solver_totals() { fn tmp_dir(prefix: &str) -> PathBuf { let mut path = std::env::temp_dir(); - let nanos = SystemTime::now() - .duration_since(UNIX_EPOCH) - .expect("clock should be monotonic enough for tests") - .as_nanos(); - path.push(format!("{}_{}_{}", prefix, std::process::id(), nanos)); + let seq = TMP_DIR_COUNTER.fetch_add(1, Ordering::Relaxed); + path.push(format!("{}_{}_{}", prefix, std::process::id(), seq)); path } @@ -185,7 +184,11 @@ fn external_solver_runner_rejects_malformed_output() { &smt, ) .expect_err("malformed solver output should be rejected"); - assert!(err.to_string().contains("malformed solver output")); + let msg = err.to_string(); + assert!( + msg.contains("malformed solver output"), + "unexpected solver error: {msg}" + ); fs::remove_dir_all(&dir).ok(); } diff --git a/crates/tarsier-cli/src/commands/proof_export.rs b/crates/tarsier-cli/src/commands/proof_export.rs index 287bfd0..2efa404 100644 --- a/crates/tarsier-cli/src/commands/proof_export.rs +++ b/crates/tarsier-cli/src/commands/proof_export.rs @@ -493,8 +493,11 @@ fn parse_fairness_mode(s: &str) -> miette::Result { #[cfg(test)] mod tests { use super::*; + use std::ffi::OsStr; use std::path::Path; - use std::time::{SystemTime, UNIX_EPOCH}; + use std::process::Stdio; + use std::thread; + use std::time::{Duration, Instant, SystemTime, UNIX_EPOCH}; use tarsier_engine::pipeline::{ProofExportKind, ProofExportObligation}; use tarsier_proof_kernel::CertificateObligationMeta; @@ -522,8 +525,43 @@ mod tests { } } + fn command_output_with_timeout( + binary: &str, + args: I, + timeout: Duration, + ) -> std::io::Result> + where + I: IntoIterator, + S: AsRef, + { + let mut child = Command::new(binary) + .args(args) + .stdout(Stdio::piped()) + .stderr(Stdio::piped()) + .spawn()?; + let deadline = Instant::now() + timeout; + loop { + if child.try_wait()?.is_some() { + return child.wait_with_output().map(Some); + } + if Instant::now() >= deadline { + let _ = child.kill(); + let _ = child.wait(); + return Ok(None); + } + thread::sleep(Duration::from_millis(50)); + } + } + fn compiler_available(binary: &str) -> bool { - Command::new(binary).arg("--version").output().is_ok() + match command_output_with_timeout(binary, ["--version"], Duration::from_secs(5)) { + Ok(Some(output)) => output.status.success(), + Ok(None) => { + eprintln!("skipping compiler smoke: `{binary} --version` timed out"); + false + } + Err(_) => false, + } } fn tmp_smoke_dir(prefix: &str) -> std::path::PathBuf { @@ -727,10 +765,13 @@ mod tests { let module_path = dir.join("TarsierExport.lean"); write_module(&module_path, &out); - let cmd = Command::new("lean").arg(&module_path).output(); + let cmd = + command_output_with_timeout("lean", [module_path.as_os_str()], Duration::from_secs(10)); fs::remove_dir_all(&dir).ok(); - let output = cmd.expect("lean invocation should be spawnable"); + let output = cmd + .expect("lean invocation should be spawnable") + .expect("lean compile smoke should finish before timeout"); assert!( output.status.success(), "lean compile smoke failed.\nstdout:\n{}\nstderr:\n{}", @@ -750,10 +791,13 @@ mod tests { let module_path = dir.join("TarsierExport.v"); write_module(&module_path, &out); - let cmd = Command::new("coqc").arg(&module_path).output(); + let cmd = + command_output_with_timeout("coqc", [module_path.as_os_str()], Duration::from_secs(10)); fs::remove_dir_all(&dir).ok(); - let output = cmd.expect("coqc invocation should be spawnable"); + let output = cmd + .expect("coqc invocation should be spawnable") + .expect("coqc compile smoke should finish before timeout"); assert!( output.status.success(), "coq compile smoke failed.\nstdout:\n{}\nstderr:\n{}", @@ -763,10 +807,26 @@ mod tests { } #[cfg(unix)] - #[test] - fn run_certcheck_reports_pass_for_valid_json_report() { + fn write_executable_script(path: &std::path::Path, script: &str) { + use std::io::Write; use std::os::unix::fs::PermissionsExt; + let mut file = fs::File::create(path).expect("script should be created"); + file.write_all(script.as_bytes()) + .expect("script should be written"); + file.sync_all().expect("script should be synced"); + drop(file); + + let mut perms = fs::metadata(path) + .expect("script metadata should be readable") + .permissions(); + perms.set_mode(0o755); + fs::set_permissions(path, perms).expect("script should be executable"); + } + + #[cfg(unix)] + #[test] + fn run_certcheck_reports_pass_for_valid_json_report() { let unique = SystemTime::now() .duration_since(UNIX_EPOCH) .expect("clock should be after epoch") @@ -789,12 +849,7 @@ while [ "$#" -gt 0 ]; do done printf '{"overall":"pass"}' > "$REPORT" "#; - fs::write(&script_path, script).expect("script should be written"); - let mut perms = fs::metadata(&script_path) - .expect("script metadata should be readable") - .permissions(); - perms.set_mode(0o755); - fs::set_permissions(&script_path, perms).expect("script should be executable"); + write_executable_script(&script_path, script); let result = run_certcheck(&base, &script_path).expect("certcheck wrapper should pass"); assert_eq!(result.overall, "pass"); @@ -806,8 +861,6 @@ printf '{"overall":"pass"}' > "$REPORT" #[cfg(unix)] #[test] fn run_certcheck_fails_when_report_overall_is_fail() { - use std::os::unix::fs::PermissionsExt; - let unique = SystemTime::now() .duration_since(UNIX_EPOCH) .expect("clock should be after epoch") @@ -830,12 +883,7 @@ while [ "$#" -gt 0 ]; do done printf '{"overall":"fail"}' > "$REPORT" "#; - fs::write(&script_path, script).expect("script should be written"); - let mut perms = fs::metadata(&script_path) - .expect("script metadata should be readable") - .permissions(); - perms.set_mode(0o755); - fs::set_permissions(&script_path, perms).expect("script should be executable"); + write_executable_script(&script_path, script); let err = run_certcheck(&base, &script_path).expect_err("certcheck wrapper should fail"); let msg = format!("{err:?}"); @@ -847,8 +895,6 @@ printf '{"overall":"fail"}' > "$REPORT" #[cfg(unix)] #[test] fn run_certcheck_fails_when_json_report_is_malformed() { - use std::os::unix::fs::PermissionsExt; - let unique = SystemTime::now() .duration_since(UNIX_EPOCH) .expect("clock should be after epoch") @@ -871,12 +917,7 @@ while [ "$#" -gt 0 ]; do done printf '{"overall":' > "$REPORT" "#; - fs::write(&script_path, script).expect("script should be written"); - let mut perms = fs::metadata(&script_path) - .expect("script metadata should be readable") - .permissions(); - perms.set_mode(0o755); - fs::set_permissions(&script_path, perms).expect("script should be executable"); + write_executable_script(&script_path, script); let err = run_certcheck(&base, &script_path).expect_err("malformed report should fail to parse"); diff --git a/crates/tarsier-dsl/src/grammar.pest b/crates/tarsier-dsl/src/grammar.pest index 701d06b..c2f84e3 100644 --- a/crates/tarsier-dsl/src/grammar.pest +++ b/crates/tarsier-dsl/src/grammar.pest @@ -388,7 +388,6 @@ formula_term = _{ | bool_literal | qualified_ident | ident - | "(" ~ formula_expr ~ ")" } formula_op = { "&&" | "||" | "==>" | "<=>" | "U" | "W" | "R" | "~>" } diff --git a/crates/tarsier-dsl/src/parser/tests.rs b/crates/tarsier-dsl/src/parser/tests.rs index 129d319..48c3468 100644 --- a/crates/tarsier-dsl/src/parser/tests.rs +++ b/crates/tarsier-dsl/src/parser/tests.rs @@ -1984,6 +1984,43 @@ fn parse_missing_protocol_keyword_is_error() { assert!(result.is_err()); } +#[test] +fn parse_rejects_nested_malformed_temporal_formula_without_timeout() { + let src = r#" +protocol MultiPhaseLivenessSafe { + params n, t, f; + resilience: n > 2*t; + + adversary { + model: byzantine; + bound: f; + } + + role Replica { + var phase1_done: bool = true; + var phase2_done: bool = true; + var phase3_done: bool = true; + + init committed; + phase committed {} + } + + property progress: liveness { + forall p: Replica. + [] ((((((((((((((((((((((((((((((((((((p.phase1_done == true ~> <> (p.phase2_done == true &&nextss { + forall p: R$ep))) + } +} +"#; + let started = std::time::Instant::now(); + let result = parse(src, "fuzz-timeout.trs"); + assert!( + started.elapsed() < std::time::Duration::from_secs(1), + "malformed temporal formula should fail quickly" + ); + assert!(result.is_err()); +} + #[test] fn parse_unclosed_brace_is_error() { let src = r#" diff --git a/fuzz/Cargo.lock b/fuzz/Cargo.lock index 930b944..fb60f6e 100644 --- a/fuzz/Cargo.lock +++ b/fuzz/Cargo.lock @@ -17,17 +17,6 @@ version = "2.0.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "320119579fcad9c21884f5c4861d16174d0e06250625266f50fe6898340abefa" -[[package]] -name = "aes" -version = "0.8.4" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b169f7a6d4742236a0a00c541b845991d0ac43e546831af1249753ab4c3aa3a0" -dependencies = [ - "cfg-if", - "cipher", - "cpufeatures", -] - [[package]] name = "aho-corasick" version = "1.1.4" @@ -42,9 +31,6 @@ name = "arbitrary" version = "1.4.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "c3d036a3c4ab069c7b410a2ce876bd74808d2d0888a82667669f8e783a898bf1" -dependencies = [ - "derive_arbitrary", -] [[package]] name = "atomic-waker" @@ -133,15 +119,6 @@ version = "1.11.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "1e748733b7cbc798e1434b6ac524f0c1ff2ab456fe201501e6497c8417a4fc33" -[[package]] -name = "bzip2" -version = "0.6.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f3a53fac24f34a81bc9954b5d6cfce0c21e18ec6959f44f56e8e90e4bb7c346c" -dependencies = [ - "libbz2-rs-sys", -] - [[package]] name = "cc" version = "1.2.56" @@ -175,16 +152,6 @@ version = "0.2.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "613afe47fcd5fac7ccf1db93babcb082c5994d996f20b8b159f2ad1658eb5724" -[[package]] -name = "cipher" -version = "0.4.4" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "773f3b9af64447d2ce9850330c473515014aa235e6a783b02db81ff39e4a3dad" -dependencies = [ - "crypto-common", - "inout", -] - [[package]] name = "clang-sys" version = "1.8.1" @@ -196,21 +163,6 @@ dependencies = [ "libloading", ] -[[package]] -name = "cmake" -version = "0.1.57" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "75443c44cd6b379beb8c5b45d85d0773baf31cce901fe7bb252f4eff3008ef7d" -dependencies = [ - "cc", -] - -[[package]] -name = "constant_time_eq" -version = "0.3.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7c74b8349d32d297c9134b8c88677813a227df8f779daa29bfc29c183fe3dca6" - [[package]] name = "cpufeatures" version = "0.2.17" @@ -220,15 +172,6 @@ dependencies = [ "libc", ] -[[package]] -name = "crc32fast" -version = "1.5.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9481c1c90cbf2ac953f07c8d4a58aa3945c425b7185c9154d67a65e4230da511" -dependencies = [ - "cfg-if", -] - [[package]] name = "crypto-common" version = "0.1.7" @@ -239,32 +182,6 @@ dependencies = [ "typenum", ] -[[package]] -name = "deflate64" -version = "0.1.10" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "26bf8fc351c5ed29b5c2f0cbbac1b209b74f60ecd62e675a998df72c49af5204" - -[[package]] -name = "deranged" -version = "0.5.8" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7cd812cc2bc1d69d4764bd80df88b4317eaef9e773c75226407d9bc0876b211c" -dependencies = [ - "powerfmt", -] - -[[package]] -name = "derive_arbitrary" -version = "1.4.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1e567bd82dcff979e4b03460c307b3cdc9e96fde3d73bed1496d2bc75d9dd62a" -dependencies = [ - "proc-macro2", - "quote", - "syn", -] - [[package]] name = "digest" version = "0.10.7" @@ -273,7 +190,6 @@ checksum = "9ed9a281f7bc9b7576e61468ba615a66a5c8cfdff42420a70aa82701a3b1e292" dependencies = [ "block-buffer", "crypto-common", - "subtle", ] [[package]] @@ -315,16 +231,6 @@ version = "0.1.9" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "5baebc0774151f905a1a2cc41989300b1e6fbb29aff0ceffa1064fdd3088d582" -[[package]] -name = "flate2" -version = "1.1.9" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "843fba2746e448b37e26a819579957415c8cef339bf08564fe8b7ddbd959573c" -dependencies = [ - "miniz_oxide", - "zlib-rs", -] - [[package]] name = "form_urlencoded" version = "1.2.2" @@ -438,15 +344,6 @@ version = "0.16.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "841d1cc9bed7f9236f321df977030373f4a4163ae1a7dbfe1a51a2c1a51d9100" -[[package]] -name = "hmac" -version = "0.12.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6c49c37c09c17a53d937dfbb742eb3a961d65a994e6bcdcf37e7399d0cc8ab5e" -dependencies = [ - "digest", -] - [[package]] name = "http" version = "1.4.0" @@ -659,15 +556,6 @@ dependencies = [ "hashbrown", ] -[[package]] -name = "inout" -version = "0.1.4" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "879f10e63c20629ecabbb64a8010319738c66a5cd0c29b02d63d272b03751d01" -dependencies = [ - "generic-array", -] - [[package]] name = "ipnet" version = "2.11.0" @@ -725,12 +613,6 @@ dependencies = [ "wasm-bindgen", ] -[[package]] -name = "libbz2-rs-sys" -version = "0.2.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2c4a545a15244c7d945065b5d392b2d2d7f21526fba56ce51467b06ed445e8f7" - [[package]] name = "libc" version = "0.2.182" @@ -757,26 +639,6 @@ dependencies = [ "windows-link", ] -[[package]] -name = "liblzma" -version = "0.4.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b6033b77c21d1f56deeae8014eb9fbe7bdf1765185a6c508b5ca82eeaed7f899" -dependencies = [ - "liblzma-sys", -] - -[[package]] -name = "liblzma-sys" -version = "0.4.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9f2db66f3268487b5033077f266da6777d057949b8f93c8ad82e441df25e6186" -dependencies = [ - "cc", - "libc", - "pkg-config", -] - [[package]] name = "linux-raw-sys" version = "0.11.0" @@ -850,7 +712,6 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "1fa76a2c86f704bdb222d66965fb3d63269ce38518b83cb0575fca855ebb6316" dependencies = [ "adler2", - "simd-adler32", ] [[package]] @@ -907,12 +768,6 @@ dependencies = [ "num-traits", ] -[[package]] -name = "num-conv" -version = "0.2.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "cf97ec579c3c42f953ef76dbf8d55ac91fb219dde70e49aa4a6b7d74e9919050" - [[package]] name = "num-integer" version = "0.1.46" @@ -974,16 +829,6 @@ version = "4.2.3" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9c6901729fa79e91a0913333229e9ca5dc725089d1c363b2f4b4760709dc4a52" -[[package]] -name = "pbkdf2" -version = "0.12.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f8ed6a7761f76e3b9f92dfb0a60a6a6477c61024b775147ff0973a02653abaf2" -dependencies = [ - "digest", - "hmac", -] - [[package]] name = "percent-encoding" version = "2.3.2" @@ -1060,18 +905,6 @@ dependencies = [ "zerovec", ] -[[package]] -name = "powerfmt" -version = "0.2.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "439ee305def115ba05938db6eb1644ff94165c5ab5e9420d1c1bcedbba909391" - -[[package]] -name = "ppmd-rust" -version = "1.4.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "efca4c95a19a79d1c98f791f10aebd5c1363b473244630bb7dbde1dc98455a24" - [[package]] name = "ppv-lite86" version = "0.2.21" @@ -1323,9 +1156,9 @@ dependencies = [ [[package]] name = "rustls-webpki" -version = "0.103.9" +version = "0.103.13" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d7df23109aa6c1567d1c575b9952556388da57401e4ace1d15f79eedad0d8f53" +checksum = "61c429a8649f110dddef65e2a5ad240f747e85f7758a6bccc7e5777bd33f756e" dependencies = [ "ring", "rustls-pki-types", @@ -1399,17 +1232,6 @@ dependencies = [ "serde", ] -[[package]] -name = "sha1" -version = "0.10.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e3bf829a2d51ab4a5ddf1352d8470c140cadc8301b2ae1789db023f01cedd6ba" -dependencies = [ - "cfg-if", - "cpufeatures", - "digest", -] - [[package]] name = "sha2" version = "0.10.9" @@ -1427,12 +1249,6 @@ version = "1.3.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "0fda2ff0d084019ba4d7c6f371c95d8fd75ce3524c3cb8fb653a3023f6323e64" -[[package]] -name = "simd-adler32" -version = "0.3.8" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e320a6c5ad31d271ad523dcf3ad13e2767ad8b1cb8f047f75a8aeaf8da139da2" - [[package]] name = "slab" version = "0.4.12" @@ -1613,25 +1429,6 @@ dependencies = [ "syn", ] -[[package]] -name = "time" -version = "0.3.47" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "743bd48c283afc0388f9b8827b976905fb217ad9e647fae3a379a9283c4def2c" -dependencies = [ - "deranged", - "num-conv", - "powerfmt", - "serde_core", - "time-core", -] - -[[package]] -name = "time-core" -version = "0.1.8" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7694e1cfe791f8d31026952abf09c69ca6f6fa4e1a1229e18988f06a04a12dca" - [[package]] name = "tinystr" version = "0.8.2" @@ -2156,11 +1953,8 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "7242a9063a67fadfe5b9d2956aa6c493c5159f2e22d69645876ed1bba6204643" dependencies = [ "bindgen", - "cmake", "pkg-config", "reqwest", - "serde_json", - "zip", ] [[package]] @@ -2209,20 +2003,6 @@ name = "zeroize" version = "1.8.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "b97154e67e32c85465826e8bcc1c59429aaaf107c1e4a9e53c8d8ccd5eff88d0" -dependencies = [ - "zeroize_derive", -] - -[[package]] -name = "zeroize_derive" -version = "1.4.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "85a5b4158499876c763cb03bc4e49185d3cccbabb15b33c627f7884f43db852e" -dependencies = [ - "proc-macro2", - "quote", - "syn", -] [[package]] name = "zerotrie" @@ -2257,81 +2037,8 @@ dependencies = [ "syn", ] -[[package]] -name = "zip" -version = "4.6.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "caa8cd6af31c3b31c6631b8f483848b91589021b28fffe50adada48d4f4d2ed1" -dependencies = [ - "aes", - "arbitrary", - "bzip2", - "constant_time_eq", - "crc32fast", - "deflate64", - "flate2", - "getrandom 0.3.4", - "hmac", - "indexmap", - "liblzma", - "memchr", - "pbkdf2", - "ppmd-rust", - "sha1", - "time", - "zeroize", - "zopfli", - "zstd", -] - -[[package]] -name = "zlib-rs" -version = "0.6.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c745c48e1007337ed136dc99df34128b9faa6ed542d80a1c673cf55a6d7236c8" - [[package]] name = "zmij" version = "1.0.21" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "b8848ee67ecc8aedbaf3e4122217aff892639231befc6a1b58d29fff4c2cabaa" - -[[package]] -name = "zopfli" -version = "0.8.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f05cd8797d63865425ff89b5c4a48804f35ba0ce8d125800027ad6017d2b5249" -dependencies = [ - "bumpalo", - "crc32fast", - "log", - "simd-adler32", -] - -[[package]] -name = "zstd" -version = "0.13.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e91ee311a569c327171651566e07972200e76fcfe2242a4fa446149a3881c08a" -dependencies = [ - "zstd-safe", -] - -[[package]] -name = "zstd-safe" -version = "7.2.4" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8f49c4d5f0abb602a93fb8736af2a4f4dd9512e36f7f570d66e65ff867ed3b9d" -dependencies = [ - "zstd-sys", -] - -[[package]] -name = "zstd-sys" -version = "2.0.16+zstd.1.5.7" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "91e19ebc2adc8f83e43039e79776e3fda8ca919132d68a1fed6a5faca2683748" -dependencies = [ - "cc", - "pkg-config", -] diff --git a/fuzz/fuzz_targets/fuzz_encode.rs b/fuzz/fuzz_targets/fuzz_encode.rs index 9080329..8ae6e78 100644 --- a/fuzz/fuzz_targets/fuzz_encode.rs +++ b/fuzz/fuzz_targets/fuzz_encode.rs @@ -6,9 +6,8 @@ fuzz_target!(|data: &[u8]| { if let Ok(program) = tarsier_dsl::parse(s, "fuzz.trs") { if let Ok(ta) = tarsier_ir::lowering::lower(&program) { let property = tarsier_ir::properties::extract_agreement_property(&ta); - let cs = tarsier_ir::counter_system::CounterSystem::new(ta); // Attempt BMC encoding at small depth; skip solving. - let _ = tarsier_smt::encoder::encode_bmc(&cs, &property, 3); + let _ = tarsier_smt::encoder::encode_bmc(&ta, &property, 3); } } } diff --git a/scripts/cometbft-conformance-active-smoke.sh b/scripts/cometbft-conformance-active-smoke.sh index 3995883..e623062 100755 --- a/scripts/cometbft-conformance-active-smoke.sh +++ b/scripts/cometbft-conformance-active-smoke.sh @@ -154,6 +154,14 @@ wait_for_mock_endpoint() { return 1 } +assert_cometbft_rpc_ready() { + local endpoint="$1" + if curl -fsS "${endpoint}/health" >/dev/null 2>&1; then + return 0 + fi + curl -fsS "${endpoint}/status" >/dev/null +} + cleanup() { if [[ -n "${SERVER_PID:-}" ]]; then kill "${SERVER_PID}" >/dev/null 2>&1 || true @@ -175,7 +183,7 @@ run_smoke() { assert_fixture_contract "$HARNESS_SCRIPT" start COMET_ENDPOINT="$("$HARNESS_SCRIPT" endpoint)" - curl -fsS "${COMET_ENDPOINT}/health" >/dev/null + assert_cometbft_rpc_ready "$COMET_ENDPOINT" assert_live_cometbft_contract "$COMET_ENDPOINT" start_mock_live_endpoint @@ -227,7 +235,7 @@ assert any(ev.get("op") == "fault" for ev in events), "no fault events observed" print("live contract assertions ok") PY - curl -fsS "${COMET_ENDPOINT}/health" >/dev/null + assert_cometbft_rpc_ready "$COMET_ENDPOINT" echo "INTEG-03 smoke passed" } diff --git a/scripts/cometbft-live-harness.sh b/scripts/cometbft-live-harness.sh index f66f957..405c65a 100755 --- a/scripts/cometbft-live-harness.sh +++ b/scripts/cometbft-live-harness.sh @@ -5,7 +5,7 @@ ROOT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)" HARNESS_DIR="$ROOT_DIR/integration/cometbft-live" COMPOSE_FILE="$HARNESS_DIR/docker-compose.yml" RPC_URL="${COMETBFT_RPC_URL:-http://127.0.0.1:26657}" -WAIT_SECS="${WAIT_SECS:-60}" +WAIT_SECS="${WAIT_SECS:-120}" usage() { cat </dev/null 2>&1 || \ + curl -fsS "$RPC_URL/status" >/dev/null 2>&1 +} + wait_for_health() { local deadline=$((SECONDS + WAIT_SECS)) while ((SECONDS < deadline)); do - if curl -fsS "$RPC_URL/health" >/dev/null 2>&1; then + if rpc_ready; then echo "CometBFT RPC is healthy at $RPC_URL" return 0 fi sleep 1 done echo "timed out waiting for CometBFT RPC health at $RPC_URL" >&2 + compose ps >&2 || true + compose logs --tail "${TAIL_LINES:-200}" >&2 || true return 1 } diff --git a/scripts/etcd-raft-live-harness.sh b/scripts/etcd-raft-live-harness.sh index ddf1035..b4108d7 100755 --- a/scripts/etcd-raft-live-harness.sh +++ b/scripts/etcd-raft-live-harness.sh @@ -55,13 +55,13 @@ assert_raft_write_read() { local key="tarsier/smoke/${SMOKE_KEY_SUFFIX:-$(date +%s)}" local value="ok-${SMOKE_VALUE_SUFFIX:-$(date +%s)}" - compose exec -T etcd-node0 sh -lc \ - "ETCDCTL_API=3 etcdctl --endpoints=http://127.0.0.1:2379 put '$key' '$value' >/dev/null" + compose exec -T -e ETCDCTL_API=3 etcd-node0 \ + etcdctl --endpoints=http://127.0.0.1:2379 put "$key" "$value" >/dev/null local got got="$( - compose exec -T etcd-node0 sh -lc \ - "ETCDCTL_API=3 etcdctl --endpoints=http://127.0.0.1:2379 get '$key' --print-value-only" + compose exec -T -e ETCDCTL_API=3 etcd-node0 \ + etcdctl --endpoints=http://127.0.0.1:2379 get "$key" --print-value-only )" got="${got//$'\r'/}" got="${got%$'\n'}" @@ -73,8 +73,8 @@ assert_raft_write_read() { local status status="$( - compose exec -T etcd-node0 sh -lc \ - 'ETCDCTL_API=3 etcdctl --endpoints=http://127.0.0.1:2379 endpoint status --write-out=json' + compose exec -T -e ETCDCTL_API=3 etcd-node0 \ + etcdctl --endpoints=http://127.0.0.1:2379 endpoint status --write-out=json )" if [[ "$status" != *'"leader"'* ]]; then echo "endpoint status JSON missing leader metadata" >&2