proof.yaml

project:
    name: jsonparser
    # High-assurance posture: the library is a pure function over untrusted,
    # adversarial byte input (fuzz targets, OSS-Fuzz). L3 is the strict
    # non-trivial level that obligates formalization, coverage, and hazard
    # review rather than informal inspection alone.
    assurance_target: L3
    specs:
        - path: specs/stakeholder
          prefix: STK-REQ
          type: stakeholder
        - path: specs/system
          prefix: SYS-REQ
          type: system
          parent_spec: specs/stakeholder
    obligation_classes:
        - nominal
        - missing_path
        - malformed_input
        - truncated_at_value_boundary
        - truncated_mid_structure
        - truncated_mid_key
        - empty_input
        - boundary
        - type_mismatch
        - negative_array_index
        - sentinel_value_boundary
        - error_propagation
        - no_path_provided
        - nested_mutation
        - callback_error_propagation
        - truncated_escape_sequence
        - partial_literal
        - truncated_mid_element
        - determinism
        - idempotency
        - nil_safety
        - encoding_safety
        - edge_case
        - no_input_mutation
        - api_consistency
        - element_type_partition
        - non_array_root_no_callback
    commands:
        build: go build ./...
        # Standard audit test command: runs unit + MC/DC witness tests but
        # SKIPS the heavy iteration-count suites (property-based, reference-
        # oracle, fuzz-harness coverage) so `proof audit` stays fast on every
        # PR. Those suites run via `make test-full` (see Makefile) in the
        # dedicated CI "Fuzzing" job. Go's -skip flag (1.20+) accepts a regex;
        # Fuzz* functions only run under -fuzz anyway.
        test: mkdir -p .proof/coverage .proof/test-results && go test ./... -count=1 -skip='TestProperty|TestOracle|TestFuzz.*Harness' -coverprofile=.proof/coverage/unit.coverprofile -json > .proof/test-results/go-test.json 2>&1
        # Named per-language test commands consumed by code_mcdc (the MC/DC
        # engine needs a discoverable go test command it can instrument and
        # rerun, then collect fingerprints). Mirrors the reqforge schema.
        tests:
            go:
                language: go
                command: mkdir -p .proof/coverage .proof/test-results && go test ./... -count=1 -skip='TestProperty|TestOracle|TestFuzz.*Harness' -coverprofile=.proof/coverage/unit.coverprofile -json > .proof/test-results/go-test.json 2>&1
                # Instrumented execution path used only when the code-level
                # MC/DC engine reruns tests in its temp workspace (cwd =
                # <ws>/module). The engine does NOT inject -coverprofile or
                # -count into a user-provided command, so this must write the
                # managed cover artifact itself: ../cover.out resolves to the
                # workspace root the engine reads. -json is redirected back to
                # the source workspace via REQPROOF_MCDC_ORIGINAL_SOURCE_DIR so
                # test_results auto_link sees a fresh report. The ordinary
                # `command` above still feeds coverage_threshold / test_results
                # for the non-MC/DC path; -race still comes from test_args.
                mcdc_command: go test ./... -coverprofile=../cover.out -json > "$REQPROOF_MCDC_ORIGINAL_SOURCE_DIR/.proof/test-results/go-test.json" 2>&1
    # Fixtures are generated artifacts, not committed to the repo.
    # MC/DC coverage is enforced through test annotations instead.
    # To regenerate locally:
    #   proof testgen specs/system parser --output tests/
    #   proof proptest specs/system parser --source z3 --output tests/parser/
    #
    # Code signals — project-local OpenGrep rule packs.
    #
    # The jsonparser.boundary.unchecked-caller-slice-deref rule closes the
    # gap exposed by the 8th empty-key panic site (parser.go:1000): the
    # prior hazard sweep matched only `identifier[index][0]` and missed the
    # slice-expression variant `keys[depth:][0][0]`. The rule treats
    # slice-expression-then-index, direct-index-then-field, nested direct
    # index, computed-offset byte-slice index, and path-segment index as
    # the SAME hazard class, while excluding `len(X) > N && ...` /
    # `if len(X) > N { ... }` guarded sites and bounded `for i := range`
    # loops. Findings map to the boundary obligation class (already owned
    # by the parser requirement family) so each one opens a real review
    # item. The semantically precise class is panic_free_input_handling;
    # adopting it project-wide is the right follow-up — see the rule file
    # header for the migration note.
    #
    # Local dev / CI install of the analyzer backend:
    #   npm install -g @opengrep/cli@1.22.0
    # `tools.opengrep.auto_download: true` below also fetches the pinned
    # version on the first `proof signals collect --provider opengrep`.
    signals:
        output_dir: proof/signals
        # Keep audit refresh explicit so a missing analyzer in CI does not
        # turn into a spurious red. Run `proof signals collect --provider
        # opengrep` before merge / locally to refresh findings; the audit
        # check consumes whatever cache that command writes.
        refresh_on_audit: false
        defaults: auto
        rule_packs:
            - proof/signals/rules/unchecked-caller-slice-deref.yaml
        providers:
            opengrep:
                enabled: true
                mode: run
                command:
                    - opengrep
                    - scan
                    - '{configs}'
                    - --sarif
                    - --quiet
                    - --no-rewrite-rule-ids
                    - '{include_paths}'
                format: sarif
                include_paths:
                    - parser.go
                    - bytes.go
                    - bytes_safe.go
                    - bytes_unsafe.go
                    - escape.go
                    - fuzz.go
                exclude_paths:
                    - '*_test.go'
                    - benchmark/**
                # `go.parameter-boundary.degenerate` anchors the
                # parameter_boundary_safe catalog class, DEFINED as a
                # Solidity-style governance / operator setter whose value
                # is later consumed in slippage / throttle / timelock
                # arithmetic or truncated by a narrowing cast. This
                # project is a pure-function Go JSON parser library: the
                # only "setters" it exposes are top-level exported
                # functions taking byte slices, none consumed in
                # protection arithmetic and none cast to a narrower type.
                # The class's applies_when is never satisfied here, so
                # the project can neither satisfy nor violate it. The
                # honest record is "rule does not apply", not "83
                # requirement-owners each adjudicated and excused the
                # same site". Rule entries use the ProviderRuleID form
                # (hyphenated), matching how reqforge disables the same
                # rule for the same reason.
                disabled_rules:
                    - go.parameter-boundary.degenerate
                fail_if_missing: false
                timeout_seconds: 120
    tools:
        opengrep:
            version: 1.22.0
            auto_download: true
    checks:
        solver_latency_clean:
            threshold: 360
        coverage_threshold:
            threshold: 80
            auto_link: false
            report_path: .proof/coverage/unit.coverprofile
            format: go-cover
        test_results:
            auto_link: true
            report_path: .proof/test-results/go-test.json
        slow_tests:
            enabled: true
            threshold_seconds: 60
            max_allowed: 5
        code_mcdc:
            severity: warn
            languages:
                go:
                    test_args:
                        - -race
            min_decision_percent: 100
            min_condition_percent: 100
            max_incomplete_decisions: 0
            targets:
                - id: parser
                  enabled: true
                  language: go
                  scope: ./...
        mcdc_coverage: {}
        proof_complexity_clean:
            max_formalized_requirements: 120
            max_variables: 280
            max_guarantees: 120
        evidence_diversity:
            min_classes:
                A: 3
                B: 2
                C: 1
        # Worst-case-first hazard coverage gate (hazard-sweep role precondition).
        # `all` is stricter than proof's built-in default `security`: every
        # in-scope obligation class must carry an enumerated worst_case, so a
        # missing worst-case surfaces as a finding instead of a silent gap.
        hazard_consequence:
            require_worst_case_scope: all
        # Keep every remaining check enabled so the audit surface is fully
        # honest (no silently-disabled gates). Each was verified PASS on this
        # project; keeping them on catches regressions.
        change_evidence_complete:
            enabled: true
        code_signal_obligations_reviewed:
            enabled: true
        code_signal_unbindable:
            enabled: true
        description_grammar_enumeration_complete:
            enabled: true
        no_authored_change_surface_reviewed:
            enabled: true
        property_fixtures_exist:
            enabled: true
        flip_fixtures_exist:
            enabled: false
        fixture_staleness_clean:
            enabled: true
        signal_fixtures_valid:
            enabled: true
        property_based_test_coverage:
            enabled: true
    approval:
        required_for:
            assurance_levels:
                - A
                - B
        roles:
            - system_owner
            - lead_engineer
        comment_required: true
        # Agent-driven review posture (mirrors reqforge self-dogfood): an AI
        # agent driving this repo may run `proof approve` at any assurance
        # level so the spec/hazard review loops can close autonomously. Set
        # `all: false` and enumerate levels to re-human-gate.
        agent_autonomous_for:
            all: true
    audit:
        # CI runs `proof audit --fail-level warn --scope full`; pinning the
        # same posture in config makes local runs match CI exactly.
        fail_level: warn
        scope: full
        invocation_log:
            enabled: true
            path: .proof/invocations.jsonl
    documentation:
        sources:
            - path: .
              type: auto
        threshold: 0
    verification_scope:
        exclude: null
        include: null