Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion internal/probe/alloycheck.go
Original file line number Diff line number Diff line change
Expand Up @@ -77,7 +77,8 @@ type alloyFileRun struct {
var alloyRuns sync.Map // abs model path -> *alloyFileRun

func (AlloyCheckRunner) Run(ctx context.Context, repoDir string, claim schema.Claim, probeID string) schema.Evidence {
ev := schema.Evidence{ClaimID: claim.ID, ProbeID: probeID, Tier: schema.T3Property}
ev := schema.Evidence{ClaimID: claim.ID, ProbeID: probeID, Tier: schema.T3Property,
Mechanism: schema.MechanismAlloyCheck}

file, command, ok := schema.ParseAlloyCheckProbeID(probeID)
if !ok {
Expand Down
138 changes: 138 additions & 0 deletions internal/probe/class_test.go
Original file line number Diff line number Diff line change
@@ -0,0 +1,138 @@
package probe

import (
"context"
"os"
"path/filepath"
"strings"
"testing"

"github.com/joshft/correctful/schema"
)

// TestEvidenceCarriesMechanismAndEnvironment: every runner states its own
// mechanism on the evidence it returns — including early returns, so a
// policy engine never has to parse probe ids — and the go runners measure
// the toolchain the probe actually ran under. Scope stays EMPTY on an
// uninstrumented run: unmeasured is stated as unmeasured.
func TestEvidenceCarriesMechanismAndEnvironment(t *testing.T) {
dir := writeCovModule(t)
pid := schema.GoTestProbeID("gate_test.go", "TestINV900_GateRejectsNil")
ev := GoTestRunner{}.Run(context.Background(), dir, schema.Claim{ID: "C"}, pid)
if ev.Mechanism != schema.MechanismGoTest {
t.Errorf("go-test mechanism = %q", ev.Mechanism)
}
if !strings.HasPrefix(ev.Environment, "go1") || !strings.Contains(ev.Environment, "/") {
t.Errorf("go environment = %q, want measured \"go1... os/arch\"", ev.Environment)
}
if ev.Scope != "" {
t.Errorf("uninstrumented run scope = %q, want unmeasured (empty)", ev.Scope)
}

pairDir := writePairModule(t)
pairID := schema.GoTestPairProbeID(".", "TestAcceptsGood", "TestRejectsBad")
if ev := (GoTestPairRunner{}).Run(context.Background(), pairDir, schema.Claim{ID: "P"}, pairID); ev.Mechanism != schema.MechanismGoTestPair || ev.Environment == "" {
t.Errorf("pair evidence class = %q / %q", ev.Mechanism, ev.Environment)
}

// Early returns keep the mechanism: malformed ids never execute anything,
// yet the evidence still states which runner refused.
if ev := (GoTestRunner{}).Run(context.Background(), dir, schema.Claim{ID: "C"}, "go-test:nofile"); ev.Mechanism != schema.MechanismGoTest {
t.Errorf("malformed go-test mechanism = %q", ev.Mechanism)
}
if ev := (DotnetTestRunner{}).Run(context.Background(), dir, schema.Claim{ID: "C"}, "dotnet-test:x"); ev.Mechanism != schema.MechanismDotnetTest {
t.Errorf("malformed dotnet mechanism = %q", ev.Mechanism)
}
if ev := (AlloyCheckRunner{}).Run(context.Background(), dir, schema.Claim{ID: "C"}, "alloy-check:x"); ev.Mechanism != schema.MechanismAlloyCheck {
t.Errorf("malformed alloy mechanism = %q", ev.Mechanism)
}
}

// TestScopeOfProfile: the footprint reduction. Executed blocks in one
// directory are single-package; a second directory with an executed block
// makes it cross-package; a profile with no executed block stays unmeasured.
func TestScopeOfProfile(t *testing.T) {
single := parseCoverProfile(realProfileSnippet) // executed blocks in cmd/tool only
if got := scopeOf(single); got != schema.ScopeSinglePackage {
t.Errorf("single = %q", got)
}
cross := parseCoverProfile(realProfileSnippet +
"example.com/mod/pkg/other/other.go:9.1,11.2 1 3\n")
if got := scopeOf(cross); got != schema.ScopeCrossPackage {
t.Errorf("cross = %q", got)
}
unexecuted := parseCoverProfile("mode: set\nexample.com/mod/a/a.go:1.1,2.2 1 0\n")
if got := scopeOf(unexecuted); got != "" {
t.Errorf("unexecuted = %q, want unmeasured", got)
}
}

// writeCrossPkgModule creates a real module where the test's execution spans
// two packages: the test (in a) calls through a into b.
func writeCrossPkgModule(t *testing.T) string {
t.Helper()
dir := t.TempDir()
files := map[string]string{
"go.mod": "module example.com/xmod\n\ngo 1.22\n",
"a/a.go": `package a

import "example.com/xmod/b"

func A() int { return b.B() + 1 }
`,
"b/b.go": `package b

func B() int { return 41 }
`,
"a/a_test.go": `package a

import "testing"

func TestAUsesB(t *testing.T) {
if A() != 42 {
t.Fatal("wrong")
}
}
`,
}
for rel, content := range files {
if err := os.MkdirAll(filepath.Dir(filepath.Join(dir, rel)), 0o755); err != nil {
t.Fatal(err)
}
if err := os.WriteFile(filepath.Join(dir, rel), []byte(content), 0o644); err != nil {
t.Fatal(err)
}
}
return dir
}

// TestScopeMeasuredThroughDispatcher: end-to-end — an instrumented run's
// scope lands on the evidence. The cross-package module's test executes a
// and b, so the LLM edge into b/b.go is BOTH confirmed (file-covered) and
// classified cross-package; the single-package module classifies
// single-package on the same path.
func TestScopeMeasuredThroughDispatcher(t *testing.T) {
crossDir := writeCrossPkgModule(t)
crossClaim := schema.Claim{ID: "LLM:b/b.go:cccc", Shape: schema.ShapeAssertion,
Text: "A adds one to B's answer",
Source: schema.Source{Kind: schema.SourceLLM, File: "b/b.go", Ref: "llm"},
ProbeIDs: []string{schema.GoTestProbeID("a/a_test.go", "TestAUsesB")}}
evidence := NewDispatcher(1, GoTestRunner{}).Dispatch(context.Background(), crossDir, []schema.Claim{crossClaim})
ev := evidence[0][0]
if !ev.Ran || !ev.Passed || ev.Binding != schema.BindingFileCovered {
t.Fatalf("cross-module run degraded: %+v", ev)
}
if ev.Scope != schema.ScopeCrossPackage {
t.Errorf("cross-package scope = %q, want %q", ev.Scope, schema.ScopeCrossPackage)
}

singleDir := writeCovModule(t)
singleClaim := schema.Claim{ID: "LLM:gate.go:dddd", Shape: schema.ShapeAssertion,
Text: "gate rejects nil",
Source: schema.Source{Kind: schema.SourceLLM, File: "gate.go", Ref: "llm"},
ProbeIDs: []string{schema.GoTestProbeID("gate_test.go", "TestINV900_GateRejectsNil")}}
evidence = NewDispatcher(1, GoTestRunner{}).Dispatch(context.Background(), singleDir, []schema.Claim{singleClaim})
if got := evidence[0][0].Scope; got != schema.ScopeSinglePackage {
t.Errorf("single-package scope = %q, want %q", got, schema.ScopeSinglePackage)
}
}
26 changes: 26 additions & 0 deletions internal/probe/coverage.go
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@ import (
"go/ast"
"go/parser"
"go/token"
"path"
"path/filepath"
"strconv"
"strings"
Expand Down Expand Up @@ -179,6 +180,31 @@ func fileBindingFor(prof covProfile, relFile string) string {
return schema.BindingFileNotReached
}

// scopeOf reduces a profile to the probe's measured execution footprint: the
// number of distinct package directories holding an EXECUTED block. One
// directory is a single-package run; more is cross-package — the axis a
// policy floor needs to require integration-shaped evidence. A profile with
// no executed blocks stays unmeasured rather than guessing.
func scopeOf(prof covProfile) string {
dirs := map[string]bool{}
for f, blocks := range prof {
for _, b := range blocks {
if b.count > 0 {
dirs[path.Dir(f)] = true
break
}
}
}
switch len(dirs) {
case 0:
return ""
case 1:
return schema.ScopeSinglePackage
default:
return schema.ScopeCrossPackage
}
}

// profileBlocksFor finds the profile entry whose import-qualified path ends
// with the repo-relative file, on a path-component boundary.
func profileBlocksFor(prof covProfile, relFile string) []covBlock {
Expand Down
3 changes: 2 additions & 1 deletion internal/probe/dotnettest.go
Original file line number Diff line number Diff line change
Expand Up @@ -51,7 +51,8 @@ var dotnetPath = sync.OnceValue(func() string {
var projLocks sync.Map // csproj path -> *sync.Mutex

func (DotnetTestRunner) Run(ctx context.Context, repoDir string, claim schema.Claim, probeID string) schema.Evidence {
ev := schema.Evidence{ClaimID: claim.ID, ProbeID: probeID, Tier: schema.T1Assertion}
ev := schema.Evidence{ClaimID: claim.ID, ProbeID: probeID, Tier: schema.T1Assertion,
Mechanism: schema.MechanismDotnetTest}

csproj, classDotMethod, ok := schema.ParseDotnetTestProbeID(probeID)
if !ok {
Expand Down
33 changes: 32 additions & 1 deletion internal/probe/gotest.go
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,9 @@ import (
"os/exec"
"path"
"regexp"
"runtime"
"strings"
"sync"
"time"

"github.com/joshft/correctful/schema"
Expand All @@ -34,7 +36,8 @@ func (GoTestRunner) CanRun(probeID string) bool {
func (GoTestRunner) MaxTier() schema.Tier { return schema.T1Assertion }

func (GoTestRunner) Run(ctx context.Context, repoDir string, claim schema.Claim, probeID string) schema.Evidence {
ev := schema.Evidence{ClaimID: claim.ID, ProbeID: probeID, Tier: schema.T1Assertion}
ev := schema.Evidence{ClaimID: claim.ID, ProbeID: probeID, Tier: schema.T1Assertion,
Mechanism: schema.MechanismGoTest, Environment: goEnvironment(repoDir)}

file, name, ok := schema.ParseGoTestProbeID(probeID)
if !ok {
Expand Down Expand Up @@ -193,3 +196,31 @@ func truncate(s string, n int) string {
}
return s[:n] + "…"
}

// goEnv caches the probe toolchain's identity for the process — one `go env`
// exec, shared by every go probe. Receipts run against one repo per process,
// so a per-repo toolchain directive is honored by the first caller.
var goEnv struct {
once sync.Once
val string
}

// goEnvironment reports the toolchain go probes run under, e.g.
// "go1.24.5 linux/amd64" — measured from the `go` that executes the probes
// (which a go.mod toolchain directive can pin), never assumed from the
// checker's own build. Empty when the measurement fails: unmeasured is
// stated as unmeasured, and the probe run itself would surface the broken
// toolchain loudly.
func goEnvironment(repoDir string) string {
goEnv.once.Do(func() {
cmd := exec.Command("go", "env", "GOVERSION")
cmd.Dir = repoDir
out, err := cmd.Output()
v := strings.TrimSpace(string(out))
if err != nil || v == "" {
return
}
goEnv.val = v + " " + runtime.GOOS + "/" + runtime.GOARCH
})
return goEnv.val
}
3 changes: 2 additions & 1 deletion internal/probe/gotestpair.go
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,8 @@ func (GoTestPairRunner) CanRun(probeID string) bool {
func (GoTestPairRunner) MaxTier() schema.Tier { return schema.T2Adversarial }

func (GoTestPairRunner) Run(ctx context.Context, repoDir string, claim schema.Claim, probeID string) schema.Evidence {
ev := schema.Evidence{ClaimID: claim.ID, ProbeID: probeID, Tier: schema.T2Adversarial}
ev := schema.Evidence{ClaimID: claim.ID, ProbeID: probeID, Tier: schema.T2Adversarial,
Mechanism: schema.MechanismGoTestPair, Environment: goEnvironment(repoDir)}

pkgDir, acceptName, rejectName, ok := schema.ParseGoTestPairProbeID(probeID)
if !ok {
Expand Down
3 changes: 3 additions & 0 deletions internal/probe/probe.go
Original file line number Diff line number Diff line change
Expand Up @@ -125,6 +125,9 @@ func (d *Dispatcher) Dispatch(ctx context.Context, repoDir string, claims []sche
} else {
ev.Binding = bindingFor(repoDir, c.RefSites, p.(covProfile))
}
// Scope is a property of the RUN, identical on every
// edge sharing the probe's single execution.
ev.Scope = scopeOf(p.(covProfile))
}
}
out[i][j] = ev
Expand Down
29 changes: 28 additions & 1 deletion schema/schema.go
Original file line number Diff line number Diff line change
Expand Up @@ -185,8 +185,35 @@ type Evidence struct {
// Binding* constants for the vocabulary. Empty: no coverage check applied
// (no code sites, or the probe kind has no prover yet).
Binding string `json:"binding,omitempty"`
// Mechanism identifies the probe kind that produced this evidence — the
// class axis a policy floor needs beside the tier ("this path requires a
// T2 adversarial pair"). Set by the runner from its own identity, so a
// policy engine never parses probe ids. Empty only when no runner ran.
Mechanism string `json:"mechanism,omitempty"`
// Scope is the probe's MEASURED execution footprint, known only for
// instrumented runs: ScopeSinglePackage when every executed block falls
// in one package directory, ScopeCrossPackage when they span more.
// Empty means unmeasured (no coverage profile) — never assumed.
Scope string `json:"scope,omitempty"`
// Environment records the toolchain the probe ran under, when the runner
// measures it (e.g. "go1.24.5 linux/amd64"). Empty means unmeasured.
Environment string `json:"environment,omitempty"`
}

// Mechanism values — one per runner kind.
const (
MechanismGoTest = "go-test"
MechanismGoTestPair = "go-test-pair"
MechanismDotnetTest = "dotnet-test"
MechanismAlloyCheck = "alloy-check"
)

// Scope values — the measured execution footprint of an instrumented run.
const (
ScopeSinglePackage = "single-package"
ScopeCrossPackage = "cross-package"
)

// Binding values — how a probe→claim edge was checked. The first two apply to
// claims whose id is annotated in shipped code (RefSites); the file-level pair
// applies to LLM-proposed edges, where the claim carries a file but no line.
Expand Down Expand Up @@ -359,4 +386,4 @@ type Receipt struct {
}

// SchemaVersion is the current version of the receipt schema (the payload).
const SchemaVersion = "0.0.8"
const SchemaVersion = "0.0.9"
Loading