# Roadmap Expansion Tasks Report — PBI-012

Date: 2026-06-04

## Completed tasks

1. **Docs checkpoint update**
   - Updated symbolic modeling, SAST/DAST roadmap, and maturity docs to reflect completed branch-order P-Code exploration, AccessPath havoc, latent/precondition detector evidence, hybrid profile merge, assertion behavior, and full-suite status.

2. **Production guarded-fact read API**
   - Added `SymbolicEnv` facade methods over `GuardedFactStore`:
     - `guardedFacts()`
     - `addFact`, `clearFacts`
     - `markFactNonNull`, `markFactNonZero`
     - `setFactRange`, `setFactMemberValue`
     - `isFactNonNull`, `isFactNonZero`, `factRange`, `factMemberValue`
   - Added env-level tests using current-path implications.

3. **Div-by-zero guarded-fact migration**
   - Mirrored AccessPath range/nonzero assignments into guarded facts.
   - Div/rem encoder call sites now suppress observer emission when live env guarded facts prove the denominator non-zero.
   - Avoided stale deferred-observer `SymbolicEnv*` access by checking facts at the live encoder point.

4. **Null-deref/OOB guarded-query migration**
   - Mirrored non-null marks into guarded facts.
   - Pointer deref encoder call sites skip null-deref observer emission when guarded facts prove non-null.
   - OOB focused tests remain green after range fact mirroring.

5. **Precise AccessPath havoc dependencies**
   - Added `ir::isSameOrDescendantAccessPath(candidate, root)`.
   - Added `GuardedFactStore::clearDescendantsOf(root)`.
   - Added `SymbolicEnv::clearAccessPathFacts(root)` for root-scoped invalidation.
   - Unknown-call havoc now clears only roots for mutable refs, `&aggregate`, and pointer-reachable args when roots are known; falls back to coarse clear on unknown roots.

6. **Generic assertion/contract macro modeling**
   - Added `isContractAssumeCall` for `assert`, `Expects`, `Ensures`, `FOLD_ASSERT`, `FOLD_PRECONDITION`, `FOLD_POSTCONDITION`, `FOLD_DCHECK`, `fold_assume`, and `FOLD_ASSUME`.
   - Function-style contract calls now conjoin their first boolean argument into the symbolic path.
   - Existing null-check extractor marks pointer args non-null for contract predicates such as `p != nullptr`.

7. **Benchmark baseline maturity gate**
   - Added `--baseline-dir` and `--require-baselines` to `scripts/benchmarks/summarize_maturity.py`.
   - Required-baseline mode fails closed on missing, malformed, or non-object baseline JSON.
   - Documented required-baseline usage in `tests/benchmarks/README.md`.

## Focused validation passed

```sh
ninja -C build/release \
  tests/unit/test_access_path tests/unit/test_guarded_facts \
  tests/unit/test_div_by_zero tests/unit/test_null_deref \
  tests/unit/test_oob_access tests/unit/test_encoder_callee_predicates

meson test -C build/release \
  fold:access_path fold:guarded_facts fold:div_by_zero \
  fold:null_deref fold:oob_access fold:encoder_callee_predicates \
  --print-errorlogs

python3 -m py_compile scripts/benchmarks/summarize_maturity.py
git diff --check
```

Result: `6/6 OK`, LSP diagnostics reported 0 errors for touched C++ files.

Additional benchmark smoke:

```sh
scripts/benchmarks/summarize_maturity.py --build build/release --source \
  --output-dir /tmp/fold-maturity-source-check
```

Result: `status=ok`, `source_goldens=ok`.

Required-baseline negative checks passed for missing and malformed baseline JSON.

## Full suite

Full validation is running under monitor `#4`:

```sh
ninja -C build/release && meson test -C build/release --print-errorlogs && git diff --check
```