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
4 changes: 2 additions & 2 deletions BACKLOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -56,11 +56,11 @@ records, generated release manifests, or the owning docs named above.
| BLOCKED | RELOCATION-01 | Add provenance-bounded witness relocation candidates without introducing a second binding path or trusting a caller-authored prior digest; detailed candidate contract is retained in [issue #66](https://github.com/research-engineering/agentic-proofkit/issues/66). | An owner-admitted content-addressed baseline binds witness id, prior path and digest, source revision, evidence class, authentication non-claims, and freshness non-claims; the scanner then proves the zero/one/many match partition while remaining non-current until fresh execution evidence exists. |
| BLOCKED | RELEASE-01 | Prove signed protected-tag release policy as provider-side release governance, not source-only intent. | Repository tag protection/ruleset and release workflow variables require signed annotated release tags; the next public release records provider-side evidence or the row is explicitly retired as an accepted non-claim. |
| DEFERRED | WEB-PUBLISH-DESIGN-01 | Investigate optional publication of the specification browser at a configurable domain with authentication. Preserve local loopback serving and local browser opening as the default workflow; remote publication must be explicit and opt-in. | After the current program, compare static export with external hosting, a bounded deployment adapter, and an authenticated hosted server. Decide whether any capability belongs in Proofkit or should remain external, using a concrete consumer need and maintenance/security costs. The decision must define URL and authentication configuration, hosting/TLS/access-control ownership, source-disclosure and secret boundaries, content freshness, and preservation of derived-view authority. Require a feasibility witness and negative cases for unauthorized access and unintended publication before accepting an implementation plan; otherwise retain local-only behavior and retire the candidate with rationale. This row authorizes investigation, not exposure of the current server or deployment. |
| DEFERRED | TRACEABILITY-DESIGN-01 | Design and validate the complete specification, scenario, native-test and execution-evidence workflow, including source intake, change impact and explanatory diagrams; see the bounded questions below. Start after the already scheduled global phases and existing backlog tasks are completed or explicitly dispositioned. | An owner-reviewed design and implementation decision resolves every question below against current Proofkit, StrictDoc and OpenSpec capabilities; an executable example and adversarial controls justify the selected ownership, storage and invalidation model. Existing mechanisms are reused when sufficient; unsupported additions are explicitly rejected rather than assumed necessary. |
| NEXT | TRACEABILITY-DESIGN-01 | Complete the specification, scenario, native-test and execution-evidence workflow, including source intake, change impact and explanatory diagrams; see the bounded questions below. Reuse current public contracts and retained evidence; lazy input guidance alone does not close the complete workflow. | An owner-reviewed design and implementation decision resolves every question below against current Proofkit, StrictDoc and OpenSpec capabilities; an executable example and adversarial controls justify the selected ownership, storage and invalidation model. Existing mechanisms are reused when sufficient; unsupported additions are explicitly rejected rather than assumed necessary. |

## TRACEABILITY-DESIGN-01

This is deferred design work, not a claim that the following capabilities are
This is active design and validation work, not a claim that the following capabilities are
implemented or absent. First establish the current behavior and reuse existing
owners before proposing a new command, record, parser or workflow engine.

Expand Down
115 changes: 115 additions & 0 deletions internal/app/authoring_sources_test.go
Original file line number Diff line number Diff line change
@@ -0,0 +1,115 @@
package app

import (
"bytes"
"fmt"
"reflect"
"strings"
"testing"
)

func TestAuthoringInputGuideIsLazy(t *testing.T) {
for _, args := range [][]string{{"help"}, {"help", "families"}, {"changed-path-set", "--help"}, {"native-evidence-guidance", "--help"}, {"change", "plan", "--help"}} {
code, output, diagnostic := executeAgentWorkflowCLI(t, args, panicReader{}, PresentationCapabilities{})
if code != 0 || diagnostic != "" || strings.Contains(output, "Requirement authoring input guide:") {
t.Fatalf("authoring guide is not demand-loaded for %v", args)
}
}
_, output := receiptHelpTemplate(t, "requirement-authoring-plan")
if strings.Count(output, "Requirement authoring input guide:") != 1 {
t.Fatal("targeted authoring help lost its unique guide")
}
}

func TestAuthoringSourceClassesPreserveProvenanceAndReviewCLI(t *testing.T) {
input, help := receiptHelpTemplate(t, "requirement-authoring-plan")
for _, text := range []string{
"Admitted reference roles:", "external specifications", "test-coverage observations",
"product intent", "coverage percentage", "not an approval",
} {
if !strings.Contains(help, text) {
t.Fatalf("authoring help omits intake boundary %q", text)
}
}
cases := []struct{ name, kind, path, summary string }{
{"code", "code_summary", "src/request.go", "Observed code rejects empty input; the owner must decide whether this is required."},
{"external-spec", "design_doc", "imports/request-spec.md", "An external specification proposes accepting empty input; it is not this repository's authority."},
{"intent", "clarification_answer", "decisions/intent.md", "The product owner proposes rejection of empty input for review."},
{"design", "design_doc", "design/request.md", "The design proposes rejection of empty input."},
{"plan", "implementation_plan", "plans/request.md", "The implementation plan proposes preserving empty-input rejection."},
{"tests", "test_summary", "tests/request_test.go", "A test asserts empty-input rejection; no execution is asserted."},
{"coverage", "test_summary", "reports/coverage.json", "Coverage-only observation: the empty-input branch is not exercised; no product requirement is inferred."},
{"pr-facts", "pr_facts", "reviews/change.md", "A pull request proposes changing empty-input behavior; approval is unresolved."},
}
for _, mode := range []string{"code-baseline", "audit-from-code"} {
for _, item := range cases {
t.Run(mode+"/"+item.name, func(t *testing.T) {
root := t.TempDir()
materialization := adoptionHelpPacket(t, root, mode)
source := materialization["requirementSources"].([]any)[0].(map[string]any)
empty := cloneMap(t, source)
empty["requirements"] = []any{}
packet := cloneMap(t, input)
packet["currentRequirementSource"] = empty
update := packet["candidateUpdates"].([]any)[0].(map[string]any)
update["candidateRequirement"] = source["requirements"].([]any)[0]
questions := []any{"Does the owner accept the proposed behavior?", "Which conflicting observation should be retained or rejected?"}
update["ownerQuestions"] = questions
ref := packet["authoringRefs"].([]any)[0].(map[string]any)
ref["kind"], ref["path"], ref["summary"] = item.kind, item.path, item.summary
ref["digest"] = "sha256:" + strings.Repeat("a", 64)
ref["nonClaims"] = []any{"Caller-provided observation; no authenticity, execution or approval is established."}
for _, authoringMode := range []string{"retrospective_baseline", "pull_request_design"} {
packet["mode"] = authoringMode
report := runAdoptionHelpCLI(t, adoptionHelpJSON(t, packet), "requirement-authoring-plan", "--input", "-")
if report["state"] != "passed" || !reflect.DeepEqual(report["authoringRefs"], packet["authoringRefs"]) {
t.Fatal("authoring lost an entire admitted reference")
}
changes := report["candidateChangeSet"].([]any)
if len(changes) != 1 || !reflect.DeepEqual(changes[0].(map[string]any)["sourceRefIds"], update["sourceRefIds"]) {
t.Fatal("candidate lost its provenance relation")
}
var ownerAction map[string]any
for _, raw := range report["ownerReviewPlan"].([]any) {
action := raw.(map[string]any)
if action["candidateId"] == update["candidateId"] {
ownerAction = action
}
}
if ownerAction == nil || !reflect.DeepEqual(ownerAction["ownerQuestions"], questions) || !reflect.DeepEqual(ownerAction["evidenceRefs"], update["sourceRefIds"]) {
t.Fatal("unresolved owner questions or evidence links disappeared")
}
preview := report["nonAuthoritativeAdmissionPreview"].(map[string]any)
if preview["authority"] != "candidate_only" || preview["candidateOnly"] != true || preview["ownerReviewRequired"] != true {
t.Fatal("observations or coverage became owner approval")
}
for _, field := range []string{"writtenFileCountNonClaim", "executedWitnessCountNonClaim"} {
if fmt.Sprint(report["summary"].(map[string]any)[field]) != "0" {
t.Fatal("authoring claimed an unperformed effect")
}
}
if !equalCLIJSON(t, preview["requirementSourcePreview"], source) {
t.Fatal("reference role changed canonical requirement meaning")
}
materialization["requirementSources"] = []any{preview["requirementSourcePreview"]}
plan := runAdoptionHelpCLI(t, adoptionHelpJSON(t, materialization), "adopt", "materialize", "plan", "--input", "-", "--repo-root", root)
if plan["state"] != "ready" || plan["sourceIntent"] != mode {
t.Fatal("actual candidate output cannot enter its declared adoption mode")
}
}
for _, field := range []string{"kind", "sourceRefIds"} {
invalid := cloneMap(t, packet)
if field == "kind" {
invalid["authoringRefs"].([]any)[0].(map[string]any)[field] = "unadmitted_kind"
} else {
invalid["candidateUpdates"].([]any)[0].(map[string]any)[field] = []any{"missing.ref"}
}
code, output, diagnostic := executeAgentWorkflowCLI(t, []string{"requirement-authoring-plan", "--input", "-"}, bytes.NewReader(adoptionHelpJSON(t, invalid)), PresentationCapabilities{})
if code != 1 || output != "" || !strings.Contains(diagnostic, field) {
t.Fatalf("invalid %s did not fail at the intended boundary: %d %q %q", field, code, output, diagnostic)
}
}
})
}
}
}
176 changes: 176 additions & 0 deletions internal/app/change_input_guide_test.go
Original file line number Diff line number Diff line change
@@ -0,0 +1,176 @@
package app

import (
"bytes"
"crypto/sha256"
"fmt"
"os"
"path/filepath"
"reflect"
"strings"
"testing"

"github.com/research-engineering/agentic-proofkit/internal/kernel/cliexec"
)

func TestChangeInputGuideIsLazyAndExecutable(t *testing.T) {
packet, help := receiptHelpTemplate(t, "change", "plan")
if len(help) > 10<<10 {
t.Fatal("current-subject help exceeds its bounded context")
}
for _, boundary := range []string{
"does not read", "Do not hash only IDs", "source-qualified pairs",
"required consumer check", "not authenticated approval", "empty prefix reviews architecture",
} {
if !strings.Contains(help, boundary) {
t.Fatalf("guide lost boundary %q", boundary)
}
}
code, output, diagnostic := executeAgentWorkflowCLI(t, []string{"change", "plan", "--input", "-"}, bytes.NewReader(adoptionHelpJSON(t, packet)), PresentationCapabilities{})
if code != 1 || output != "" || diagnostic == "" {
t.Fatal("unfilled template fabricated an admissible assessment")
}
for _, carrier := range []struct{ profile, python string }{
{cliexec.ProfilePath, ""}, {cliexec.ProfileNPMOffline, ""}, {cliexec.ProfilePythonModule, "/example/python 3"},
} {
renderer, err := cliexec.AdmitLauncherProfile(carrier.profile, carrier.python)
if err != nil {
t.Fatal(err)
}
descriptor, _ := commandDescriptorFor("change-workflow-plan")
got := guideCommands(t, commandUsageWithRenderer(descriptor, renderer), "Current-subject review input guide:", renderer)
if !reflect.DeepEqual(got, [][]string{{"change", "plan", "--input", "<checkpoint>"}}) {
t.Fatalf("guide command is not carrier-bound: %v", got)
}
}
for _, args := range [][]string{{"help"}, {"help", "families"}, {"native-evidence-guidance"}, {"changed-path-set", "--help"}} {
code, output, diagnostic := executeAgentWorkflowCLI(t, args, panicReader{}, PresentationCapabilities{})
if code != 0 || diagnostic != "" || strings.Contains(output, "Current-subject review input guide:") {
t.Fatal("current-subject template must remain demand-loaded")
}
}
}

func TestChangeGuideActualFilesInvalidateOldAssessment(t *testing.T) {
template, _ := receiptHelpTemplate(t, "change", "plan")
// This finite consumer owns these inputs. It is not a universal dependency scanner.
files := map[string]string{
"meaning.json": `{"namespace":"alpha","requirementId":"REQ-ONE","invariant":"Reject empty input","scenarioId":"empty","scenarioContext":"empty string"}`,
"bindings.json": `{"witnessId":"native.one","path":"request.test.ts","selector":"test_empty"}`,
"test.ts": `assert.equal(normalize(""), null);`,
"helper.ts": `export const normalize = value => value || null;`,
"command.json": `["node","--test","request.test.ts"]`,
"runtime.json": `{"environment":"local-node","toolchain":"node-fixture-1"}`,
"policy.json": `{"receiptKind":"fixture.native","requireCurrent":true}`,
}
root := t.TempDir()
write := func(name, value string) {
t.Helper()
if err := os.WriteFile(filepath.Join(root, name), []byte(value), 0600); err != nil {
t.Fatal(err)
}
}
for name, value := range files {
write(name, value)
}
// Structured fixtures have JSON value semantics; native code is byte-sensitive.
current := func() string {
t.Helper()
values := map[string]any{}
for name := range files {
data, err := os.ReadFile(filepath.Join(root, name))
if err != nil {
t.Fatal(err)
}
if strings.HasSuffix(name, ".json") {
values[name] = decodeCLIJSON(t, string(data))
} else {
values[name] = string(data)
}
}
return fmt.Sprintf("sha256:%x", sha256.Sum256(adoptionHelpJSON(t, values)))
}
baseline := current()
checkpoint := func(subject, assessment string) map[string]any {
packet := cloneMap(t, template)
value := packet["checkpoint"].(map[string]any)
value["subjectDigest"], value["assessmentSubjectDigest"] = subject, assessment
refs := packet["contextRefs"].([]any)
refs[0].(map[string]any)["subjectDigest"] = fmt.Sprintf("sha256:%x", sha256.Sum256([]byte("fixture owner policy")))
refs[1].(map[string]any)["subjectDigest"] = subject
return packet
}
invoke := func(packet map[string]any, wantCode int, wantError string) map[string]any {
t.Helper()
code, output, diagnostic := executeAgentWorkflowCLI(t, []string{"change", "plan", "--input", "-"}, bytes.NewReader(adoptionHelpJSON(t, packet)), PresentationCapabilities{})
if code != wantCode || (wantError != "" && !strings.Contains(diagnostic, wantError)) || (wantError == "" && diagnostic != "") {
t.Fatalf("unexpected checkpoint result: %d %q %q", code, output, diagnostic)
}
if wantCode != 0 {
if output != "" {
t.Fatal("rejected checkpoint emitted a success packet")
}
return nil
}
return decodeCLIJSON(t, output).(map[string]any)
}
prior := checkpoint(baseline, baseline)
action := invoke(prior, 0, "")
if action["action"] != "accept_stage" {
t.Fatalf("unchanged reviewed subject not accepted: %v", action)
}
// A public consumer applies the actual returned delta, without internal Go APIs.
merged := cloneMap(t, prior)
for key, value := range action["successorStateDelta"].(map[string]any) {
merged[key] = value
}
if next := invoke(merged, 0, ""); next["activeStageId"] != "design" {
t.Fatalf("merged successor did not reach design: %v", next)
}
mutations := []struct{ name, file, before, after string }{
{"namespace", "meaning.json", "alpha", "beta"},
{"requirement", "meaning.json", "REQ-ONE", "REQ-TWO"},
{"invariant", "meaning.json", "Reject empty input", "Accept empty input"},
{"scenario", "meaning.json", `"scenarioId":"empty"`, `"scenarioId":"blank"`},
{"scenario-context", "meaning.json", "empty string", "whitespace"},
{"witness", "bindings.json", "native.one", "native.two"},
{"path", "bindings.json", "request.test.ts", "other.test.ts"},
{"selector", "bindings.json", "test_empty", "test_preserve"},
{"assertion", "test.ts", "null", "true"},
{"helper", "helper.ts", "null", "true"},
{"argv", "command.json", "request.test.ts", "other.test.ts"},
{"environment", "runtime.json", "local-node", "remote-node"},
{"toolchain", "runtime.json", "node-fixture-1", "node-fixture-2"},
{"receipt-policy", "policy.json", "true", "false"},
}
for _, mutation := range mutations {
t.Run(mutation.name, func(t *testing.T) {
before := files[mutation.file]
after := strings.Replace(before, mutation.before, mutation.after, 1)
if before == after {
t.Fatal("mutation failed to change the intended operand")
}
write(mutation.file, after)
defer write(mutation.file, before)
digest := current()
if digest == baseline {
t.Fatal("actual semantic change did not invalidate the current subject")
}
invoke(checkpoint(digest, baseline), 1, "proofkit.workflow.assessment_digest_mismatch")
if got := invoke(checkpoint(digest, digest), 0, ""); got["action"] != "accept_stage" {
t.Fatal("matching retained assessment is not accepted")
}
// CLI admits declared equality, not files. The consumer must recompute.
invoke(prior, 0, "")
if prior["checkpoint"].(map[string]any)["subjectDigest"] == digest {
t.Fatal("consumer failed to detect all-old caller hashes")
}
})
}
write("unrelated.ts", "independent scope changed")
write("meaning.json", "\n "+files["meaning.json"]+"\n")
if current() != baseline {
t.Fatal("unaffected scope or JSON layout invalidated semantic subject")
}
invoke(checkpoint(current(), baseline), 0, "")
}
2 changes: 1 addition & 1 deletion internal/app/cli_contract_test.go
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ import (
)

const (
cliContractPublicABISHA256 = "2867ea2c8caf03e5b88fa46cabee0697e781452af2a8049e70660796730d0b66"
cliContractPublicABISHA256 = "31d82294be58a80cdef00a33a554cfeeb17a03903083ebf56a38a994d7f2def9"
maxAggregateFileReadBytesForContractTest = 64 << 20
maxPackageManifestBytesForContractTest = 256 << 10
maxSourceFileBytesForContractTest = 8 << 20
Expand Down
Loading
Loading