- 7 pure-function lemmas added directly on production code, all
  PROVED on Z3: tokenEnd_in_range, tokenStart_in_range,
  nextToken_in_range, lastToken_in_range,
  isUTF16EncodedRune_low_excluded, isUTF16EncodedRune_high_excluded,
  deleteCleanupFixed_prevTok_nonneg.

- Delete-bug demo (Option β, snippet extraction):
  parser_delete_snippet_proof.go encodes the pre-fix /
  post-fix dereference obligations of the OSS-Fuzz panic block
  (testcase 4649128545288192). Z3 returns COUNTEREXAMPLE
  prevTok = -1, remainedTok = 0 on the buggy variant — the exact
  shape of the OSS-Fuzz repro on `,{"test":1{}` — and PROVED on
  the post-fix variant. Snippet is gated behind reqproof_proof
  build tag.

- verify-properties (SYS-REQ): 16 checks, 0 violated, 4 pre-existing
  orphan_no_requirement skips.

- audit: 0 errors, 6 warnings (mostly authored_delta_expected and
  untraced new fuzz wrappers — expected on a feature branch).

- Coverage: 18 / 18 (100%) of branches reached by lemma translation
  are covered.

- Authoring-time refactors of tokenEnd, nextToken, lastToken,
  tokenStart in parser.go and h2I in escape.go: switch -> if-chain
  and character-literals -> ASCII-int. Behavior byte-identical;
  full test suite passes.

- Documented at docs/reqproof-application.md: lemma inventory,
  the Delete-bug COUNTEREXAMPLE in detail, eight translator-gap
  follow-ups including conditional early-return scoping bug,
  E_SWITCH_NOT_SUPPORTED, character literals, type-conversion
  function-call, slice-expr, free package consts, multi-lemma
  per host, Phase AA auto-OOB.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Re-sweep after reqproof translator fixes shipped on
feat/translator-gap-fixes (HEAD 02a8cb94): char literals (Fix #3),
type conversions (Fix #4), package-level const references (Fix #6),
multi-lemma per host (Fix #7).

Coverage went from 18/18 (100%) to 25/25 (100%). Lemma corpus 11 -> 23
(9 -> 21 PROVED via cached path; 22 PROVED + 1 expected COUNTEREXAMPLE
via fresh-translation --coverage path).

- 4 new lemmas via Fix #3 (char literals): h2I_decimal_digit,
  h2I_uppercase_hex, h2I_lowercase_hex, h2I_nondigit_is_badhex.
  All exercise '0'..'9' / 'A'..'F' / 'a'..'f' on h2I.
- Fix #4 (type conversions) is on the same h2I host — its body uses
  int(c-48) etc., which previously made the host untranslatable.
  Without Fix #4 the four char-literal lemmas above would translation-
  error on the host.
- 3 new lemmas via Fix #6 (package consts): h2I_nondigit_is_badhex
  (uses const badHex), isUTF16EncodedRune_const_high_bound (uses const
  highSurrogateOffset), isUTF16EncodedRune_const_bmp_bound (uses const
  basicMultilingualPlaneReservedOffset).
- 6 additional :lemma directives on existing hosts via Fix #7
  (multi-lemma per host): tokenEnd_nonneg, tokenEnd_empty_zero,
  tokenStart_nonneg, tokenStart_empty_zero, nextToken_signed_disjoint,
  lastToken_signed_disjoint. Pre-fix the scanner dropped any second
  :lemma on a host silently.

Tried-and-rejected (still blocked by other deferred translator gaps):
- combineUTF16Surrogates: Fix #6 resolves the package-const refs in
  the body, but `<<` shift op is unsupported (separate gap, not
  one of #1/#2/#5).
- findTokenStart: still blocked by #1 (early-return / __early_val
  scoping bug in switch + return body shape).
- unescapeToUTF8: still blocked by #2 (switch).

No new production bugs surfaced. The single COUNTEREXAMPLE
(deleteCleanupBuggy_prevTok_nonneg_falsifiable) is the existing
documented OSS-Fuzz Delete demo from a6c5ed3 — counterexample
prevTok=-1, remainedTok=0 matches the documented falsifying witness.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

- Lemma corpus: 23 (22 PROVED + 1 CE) -> 30 (29 PROVED + 1 CE)
- 7 new PROVED lemmas (5 path-condition + 2 variadic-callee)
- verify-safety: 11 scanned, 62 skipped, 0 findings
- Real bugs found: 0 new (OSS-Fuzz Delete pre-fix witness still
  surfaces via the dedicated snippet COUNTEREXAMPLE lemma; Delete
  itself remains untranslatable due to E_EARLY_RETURN_NO_ELSE)
- One translator follow-up identified: package-scoped tuple-sort
  preamble poisoning when a multi-return helper sits passively in
  the package (workaround: collapse to single return)
- Documented at docs/reqproof-item3-application.md

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…helpers

Move all reqproof:lemma directives from
parser_delete_snippet_proof.go and parser_item3_lemmas_proof.go onto
the production functions they characterize (tokenEnd, tokenStart,
nextToken, lastToken, h2I) in parser.go and escape.go.

Inline the Delete-cleanup obligation helpers and the variadic
keysCount stand-in at the bottom of parser.go behind a
"// --- reqproof verification helpers ---" delimiter, since those
patterns abstract control-flow shapes that the translator does not
yet support directly on Delete.

Lemma corpus preserved: 30 total = 29 PROVED + 1 CE.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Dogfood the Proof obligation-class catalog v1.0.0 against the
jsonparser corpus — first external-project test of catalog v0.3.0.
Added parser/deserializer/accepts_user_data workload tags to the
7 STK-REQs, resolved 33 baseline-obligation findings (24 accepted +
9 suppressed-with-rationale) and 27 decomposition findings via
suppression entries pointing at the SYS-REQ leaves that bear each
obligation. Each suppression cites JSON-specific semantics or
specific SYS-REQs; no bulk-suppression. Coverage flows OWASP-ASVS-v4,
CWE, MISRA-C, NIST-800-53 and IEC-62304 framework references through
the spec corpus. Refreshed trace reviews on 17 directly-changed +
98 cascade-affected requirements. Case study at
PROOF_CATALOG_DOGFOOD_CASE_STUDY.md.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

After this dogfood surfaced three structural findings (loosened
denial_of_service_resistant trigger, leaf-detection in
obligation_decomposition_complete, three-bucket coverage reporting),
they were fixed in ReqProof v0.3.0 before ship. Update the case study
coverage excerpt to use the new accepted/suppressed/missing buckets
with decided/active coverage percentages, and document the three
findings the dogfood produced.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Clears the authored_delta_expected audit warning that blocked PR #283.
Records explicit no-authored-change impact reviews for all 83 requirements
owning parser.go via the per-branch sidecar (proof/impact-reviews/).

Rationale: the OSS-Fuzz 4649128545288192 Delete panic fix (commit a6c5ed3)
guards the data[prevTok] dereference. The owning requirements already
specified no-panic on malformed input (e.g. SYS-REQ-035 'shall not panic'),
so the authored intent is unchanged -- the implementation now complies
with the existing specification.

- assurance_target: L3 (library is a pure function over untrusted,
  adversarial byte input; obligates formalization + coverage + hazard review)
- audit.fail_level/scope pinned in config so local runs match CI exactly
- audit.invocation_log enabled for auditability
- approval.agent_autonomous_for: all (review loops can close autonomously)
- checks.hazard_consequence.require_worst_case_scope: all (hazard-sweep
  precondition; stricter than the built-in 'security' default so missing
  worst-cases surface as findings instead of silent gaps)
- slow_tests threshold_seconds/max_allowed set

…caffolding

Hazard-sweep finding: Get/Set/Delete/EachKey panicked with
index-out-of-range when a caller passed an empty-string path
component (""). 7 unguarded keys[i][0] dereference sites in
searchKeys, EachKey, createInsertComponent, calcAllocateSpace.
Same bug class as the OSS-Fuzz Delete panic, on the path side.
Fixed by applying the existing len(...) > 0 guard pattern (already
at parser.go:835 in Delete) to all 7 sites. Regression tests in
empty_key_path_test.go. DEFECT-260726-QS2V + KI-1 filed.

Also removed 5 synthetic proof-scaffolding functions that existed
only to game the audit (deleteCleanupBuggyDereferenceObligation,
deleteCleanupFixedDereferenceObligation,
deleteCleanupBuggyFalsifyingWitness, keysCount, isUTF16EncodedRuneNot):
no production caller, hosted reqproof:lemma directives on synthetic
stand-ins rather than real code. Obligations routed honestly to
DEFECT-260726-QS2V / KI-1 / real-function annotations.

Drive the proof audit to zero errors / zero warnings under the L3
strict posture (fail_level: warn, scope: full).

Catalog: 14 jsonparser-specific obligation class overlay entries
(missing_path, truncated_*, sentinel_value_boundary, type_mismatch,
error_propagation, ...) under proof/catalog/.

Hazard review (hazard-sweep + hazard-analysis roles): enumerated
concrete worst_case + severity for every obligation class across
all 7 STK-REQs and 53 SYS-REQs. 9 hunt-campaign vectors filed under
proof/vectors/, each closed-null citing the Fuzz*Native corpus +
regression tests.

Coverage (coverage role): full requirement-side MC/DC (369/369 rows
witnessed, 0 uncovered), code-level MC/DC evidence pipeline, 45
property-based harnesses + honest proptest:skip on test infra,
acceptance-criteria witnesses (15/15), obligation-evidence triples
(94/94). New files: mcdc_spec_witnesses_test.go,
obligation_evidence_test.go, property_test.go.

Governance (govern + formal-proof roles): re-approved 13 stale
SYS-REQs, confirmed 341 suspect trace links, aligned 111 verification
states, independence attestation on parser.vars.yaml, impact reviews
re-recorded for parser.go.

Spec: verification_method schema migration on 7 STK-REQ ACs,
obligation decomposition closed (140/140), assurance_level L3 met.

Final audit: 0 errors, 0 warnings, 11 info.

This reverts commit 9f4a999.

…test annotations

Enable every remaining audit check at severity: warning so the surface
is fully honest (no silently-disabled gates). flip_fixtures_exist stays
disabled (not applicable to a parser library).

Remove 634 // reqproof:proptest:skip annotations that had been added to
TEST functions (Test*/Benchmark*) — test functions are not property-test
subjects, and annotating them was noise. property_based_test_coverage
still reports these as INFO-level gaps because the check scans test
functions with no clean opt-out (verification_scope.exclude is shared
with evidence/acceptance checks that read annotations from test files).
Filed as probelabs/reqproof#968.

Audit: 0 errors, 0 warnings, 3 info (property_based_test_coverage INFO
pending the proof-side fix + flip_fixtures disabled + legacy-field
advisory).