| # Phase-3 cross-codebase enforcement check (realism-enforcement plan). | |
| # Runs the SAME cli-verify path validated on VibeOS, but on a libredwg parser | |
| # source, with --agentic (enforcement default-ON, no --keep-dynamic-immunity). | |
| # Goal: empirically confirm enforcement does not demote a cross-codebase real. | |
| # Mechanism expectation: libredwg parser bugs are confirmed_system_entry | |
| # (attacker-entry-reachable), which the confirmed_dynamic immunity removal does | |
| # NOT touch -> 0 demotions. This run provides the empirical data point. | |
| set -u | |
| ROOT="${APROVER_ROOT:-$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)}" | |
| cd "$ROOT" || exit 1 | |
| ENVF="$HOME/.config/bmc-agent/env" | |
| [ -f "$ENVF" ] && . "$ENVF" | |
| CORP=/tmp/oss_fuzz_corpora/libredwg | |
| src="${1:-$CORP/src/reedsolomon.c}" | |
| out=findings/phase3_enforce_libredwg | |
| mkdir -p "$out" | |
| timeout 1500 python -m bmc_agent.cli verify \ | |
| --source "$src" \ | |
| --driver ossfz_p3enforce \ | |
| --output "$out" \ | |
| --include-dir "$CORP/_cbmc_build/src" \ | |
| --include-dir "$CORP/src" \ | |
| --include-dir "$CORP/include" \ | |
| --include-dir "$CORP/_cbmc_build" \ | |
| -D DLL_EXPORT -D ENABLE_SHARED -D redwg_EXPORTS -D LTO -D NDEBUG \ | |
| --agentic \ | |
| >"$out/run.log" 2>&1 | |
| echo "DONE libredwg rc=$?" >>"$out/run.log" | |