src/lib.rs:18 labels src/kani_execution.rs // Implements: FR-015, but FR-015 is a generation requirement: its Behavior and all six acceptance criteria describe emitting harnesses and typed refusals. No FR says this crate discovers a Kani installation, compares it with committed pins, runs cargo kani, interprets the backend output, or emits execution evidence.
Roughly 870 lines with no owning requirement:
KaniToolPins, KaniInstallation::observe, and the committed pins PINNED_CBMC_VERSION / PINNED_RUST_TOOLCHAIN / PINNED_TARGET_TRIPLE / PINNED_LAUNCHER_SHA256 / PINNED_DRIVER_SHA256 (src/kani_execution.rs:66-72). Only spec/interface/interface-001-codegen-api.md:145 pins cargo-kani 0.67.0; the other five values appear in no artifact.KaniExecutionRefusal::PinDrift and the pre-run refusal (src/kani_execution.rs:432-445).KaniRunOutcome and KaniInconclusiveReason (src/kani_execution.rs:347-390): a seven-value verdict vocabulary with no requirement.KaniExecutionEvidence and KANI_EXECUTION_SCHEMA (src/kani_execution.rs:24, :389-425): an evidence document shape with no Outputs section anywhere that describes it.spec/interface/interface-001-codegen-api.md has slices for the oracle, harness/strategy, bound-strategy, kani (FR-003) and coverage-analysis surfaces and none for this one, nor for FR-014, FR-015 or FR-016.
This is the module that converts a generated harness into an assurance claim, so an unowned verdict vocabulary here is the highest-value gap in the spec.
Resolution: write the requirement for the behaviour that is intended (pin measurement and pre-run drift refusal, the outcome vocabulary and the rule that derives it, the evidence fields, and the non-vacuity gate), with acceptance criteria that can fail, plus the test case, matrix rows and suite registration. Defects found in the same module are filed separately.
src/lib.rs:18 labels
src/kani_execution.rs// Implements: FR-015, but FR-015 is a generation requirement: its Behavior and all six acceptance criteria describe emitting harnesses and typed refusals. No FR says this crate discovers a Kani installation, compares it with committed pins, runscargo kani, interprets the backend output, or emits execution evidence.Roughly 870 lines with no owning requirement:
KaniToolPins,KaniInstallation::observe, and the committed pinsPINNED_CBMC_VERSION/PINNED_RUST_TOOLCHAIN/PINNED_TARGET_TRIPLE/PINNED_LAUNCHER_SHA256/PINNED_DRIVER_SHA256(src/kani_execution.rs:66-72). Onlyspec/interface/interface-001-codegen-api.md:145pinscargo-kani 0.67.0; the other five values appear in no artifact.KaniExecutionRefusal::PinDriftand the pre-run refusal (src/kani_execution.rs:432-445).KaniRunOutcomeandKaniInconclusiveReason(src/kani_execution.rs:347-390): a seven-value verdict vocabulary with no requirement.KaniExecutionEvidenceandKANI_EXECUTION_SCHEMA(src/kani_execution.rs:24, :389-425): an evidence document shape with no Outputs section anywhere that describes it.spec/interface/interface-001-codegen-api.mdhas slices for the oracle, harness/strategy, bound-strategy, kani (FR-003) and coverage-analysis surfaces and none for this one, nor for FR-014, FR-015 or FR-016.This is the module that converts a generated harness into an assurance claim, so an unowned verdict vocabulary here is the highest-value gap in the spec.
Resolution: write the requirement for the behaviour that is intended (pin measurement and pre-run drift refusal, the outcome vocabulary and the rule that derives it, the evidence fields, and the non-vacuity gate), with acceptance criteria that can fail, plus the test case, matrix rows and suite registration. Defects found in the same module are filed separately.