diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 index 0000000..71a93ff --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,20 @@ +# CHANGELOG + +## 0.7.0 — 2026-07-24 + +### Added + +- Reward-binding layer (parallel to `TraceSafe`): normalized `RewardBindingInput`, four predicates, multi-outcome decider, Lean model + soundness, `pf-core.reward_binding_certificate.v0`. +- CLI: `pf core check-reward-binding`, `emit-reward-binding-certificate`, `replay-reward-binding`. +- Untrusted PCS reward-binding adapter + mirrored schemas under `adapters/pcs/`. +- Assumptions A11–A14; ADR-001 reward-binding ownership; companion PR specs for pcs-core / LabTrust / OVK. +- Adversarial and LabTrust/OVK-shaped fixtures (offline). + +### Changed + +- Claim-boundary and audit forbidden phrases extended for reward overclaims. +- `pf-core/VERSION` MINOR bump from 0.6.0. + +### Frozen + +- `pf-core.certificate.v0` unchanged. diff --git a/SECURITY.md b/SECURITY.md new file mode 100644 index 0000000..59594f2 --- /dev/null +++ b/SECURITY.md @@ -0,0 +1,20 @@ +# Security Policy + +## Supported versions + +| Version | Supported | +|---------|-----------| +| 0.7.x | Yes | +| 0.6.x | Best-effort | +| < 0.6 | No | + +## Reporting a vulnerability + +This repository is private. Report suspected vulnerabilities in the trusted kernel (`pf-core/lean`, `pf-core/schemas`, `pf-core/validator/pf_core`) or adapter integrity handling privately to the maintainers via the organization's private security channel. Do not open public issues for exploitable defects. + +Include: affected commit/tag, reproduction under network-disabled conditions, and whether the issue crosses the trusted/untrusted boundary. + +## Scope notes + +- Untrusted adapters (`adapters/`) are not a security boundary for predicate truth. +- Reward-binding certificates assert binding under A11–A14; they do not assert objective correctness or verifier accuracy. diff --git a/adapters/__init__.py b/adapters/__init__.py new file mode 100644 index 0000000..101d452 --- /dev/null +++ b/adapters/__init__.py @@ -0,0 +1 @@ +# Untrusted adapter packages (outside PF-Core TCB). diff --git a/adapters/pcs/README.md b/adapters/pcs/README.md new file mode 100644 index 0000000..d0772e4 --- /dev/null +++ b/adapters/pcs/README.md @@ -0,0 +1,59 @@ +# PCS adapters (untrusted) + +This tree is **outside the PF-Core TCB**. It normalizes portable PCS-shaped evidence into trusted PF-Core schemas. Predicate acceptance truth lives only in `pf_core/reward_binding.py` and Lean `PFCore.RewardBinding`. + +## Mirrored schemas + +Immutable mirrors under `adapters/pcs/schemas/`: + +| Schema `$id` | File | +|--------------|------| +| `pcs.reward_evidence_envelope.v0` | `reward_evidence_envelope.schema.json` | +| `pcs.verifier_profile.v0` | `verifier_profile.schema.json` | +| `pcs.environment_profile.v0` | `environment_profile.schema.json` | +| `pcs.verification_result.v0` | `verification_result.schema.json` | +| `pcs.authority_record.v0` | `authority_record.schema.json` | + +Upstream to pcs-core via companion tickets in `docs/pf-core/pf-va-pr-artifacts/`. Do not invent a second portable evidence standard under `pf-core/schemas/`. + +### Schema pin digests (SHA-256 of canonical file bytes) + +Regenerate with: + +```bash +python -c "import hashlib,pathlib; p=pathlib.Path('adapters/pcs/schemas'); +[print(f.name, hashlib.sha256(f.read_bytes()).hexdigest()) for f in sorted(p.glob('*.schema.json'))]" +``` + +Pins are recorded in `adapters/pcs/schemas/SCHEMA_PINS.json` after VA-01 land. + +## Trust registry (`trusted_keys.json`) + +Operator pin format: + +```json +{ + "schema_version": "pcs.trusted_keys.v0", + "keys": [ + { "key_id": "org-root-1", "alg": "sha256", "public_pin": "" } + ] +} +``` + +`reward_binding_adapter` accepts an integrity envelope only when `key_id` is listed and the recomputed payload digest matches `integrity.digest`. Trust-root correctness is assumption A13 (organizational). + +## Reward-binding adapter + +```bash +python -m adapters.pcs.reward_binding_adapter \ + --trace trace.json \ + --reward-evidence reward.json \ + --artifact-root artifacts/ \ + --trust-registry trusted_keys.json +``` + +Emits `RewardBindingInput` (`pf-core.reward_binding_input.v0`) plus a mapping report listing discharged vs delegated assumptions. Never sets predicate acceptance. + +## Non-claims + +Adapter success does not imply reward correctness, verifier accuracy, environment fidelity, or RL/judge objective endorsement. diff --git a/adapters/pcs/__init__.py b/adapters/pcs/__init__.py new file mode 100644 index 0000000..41d080e --- /dev/null +++ b/adapters/pcs/__init__.py @@ -0,0 +1 @@ +# PCS adapters package (untrusted). diff --git a/adapters/pcs/fixtures/labtrust-reward-binding/manifest.json b/adapters/pcs/fixtures/labtrust-reward-binding/manifest.json new file mode 100644 index 0000000..a5d1f2a --- /dev/null +++ b/adapters/pcs/fixtures/labtrust-reward-binding/manifest.json @@ -0,0 +1,10 @@ +{ + "schema_version": "labtrust.reward_binding_fixture.v0", + "description": "Local LabTrust-shaped reward-binding fixture pointer (vendored; no network).", + "trace_fixture": "../reward-binding/trace_valid.json", + "reward_evidence": "../reward-binding/reward_valid.json", + "artifact_root": "../reward-binding/artifacts", + "trust_registry": "../reward-binding/trusted_keys.json", + "expected_outcome": "safe", + "notes": "Companion LabTrust PR should accept this mapping without cloning siblings in pf-core-trusted." +} diff --git a/adapters/pcs/fixtures/ovk-verifier-profile/README.md b/adapters/pcs/fixtures/ovk-verifier-profile/README.md new file mode 100644 index 0000000..ac68a59 --- /dev/null +++ b/adapters/pcs/fixtures/ovk-verifier-profile/README.md @@ -0,0 +1,11 @@ +# OVK-shaped verifier profile fixture (local) + +Minimal offline fixture for companion OVK profile-pin work. Not executed against a live OVK binary in `pf-core-trusted`. + +| Field | Value | +|-------|-------| +| `profile_id` | `ovk-basic-v0` | +| `config_digest` | hex64 `c` repeated | +| `suite` | `ovk.offline_check.v0` | + +Upstream: `docs/pf-core/pf-va-pr-artifacts/ovk-profile-pin-pr-spec.md`. diff --git a/adapters/pcs/fixtures/ovk-verifier-profile/verifier_profile.json b/adapters/pcs/fixtures/ovk-verifier-profile/verifier_profile.json new file mode 100644 index 0000000..facb529 --- /dev/null +++ b/adapters/pcs/fixtures/ovk-verifier-profile/verifier_profile.json @@ -0,0 +1,8 @@ +{ + "schema_version": "pcs.verifier_profile.v0", + "profile_id": "ovk-basic-v0", + "config_digest": "cccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccc", + "status": "active", + "suite": "ovk.offline_check.v0", + "rubric": "ovk.rubric.pin.v0" +} diff --git a/adapters/pcs/fixtures/reward-binding/adversarial/artifacts_bad_profile/auth-1.json b/adapters/pcs/fixtures/reward-binding/adversarial/artifacts_bad_profile/auth-1.json new file mode 100644 index 0000000..3ba89b3 --- /dev/null +++ b/adapters/pcs/fixtures/reward-binding/adversarial/artifacts_bad_profile/auth-1.json @@ -0,0 +1,15 @@ +{ + "authority_id": "auth-1", + "authorized_issuers": [ + { + "principal_id": "issuer-1", + "tenant_id": "tenant-lab" + } + ], + "claim_class": "reward_binding", + "environment_digest": "cccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccc", + "revoked": false, + "schema_version": "pcs.authority_record.v0", + "valid_from": 100, + "valid_until": 200 +} diff --git a/adapters/pcs/fixtures/reward-binding/adversarial/artifacts_bad_profile/env-1.json b/adapters/pcs/fixtures/reward-binding/adversarial/artifacts_bad_profile/env-1.json new file mode 100644 index 0000000..7e4c0ef --- /dev/null +++ b/adapters/pcs/fixtures/reward-binding/adversarial/artifacts_bad_profile/env-1.json @@ -0,0 +1,6 @@ +{ + "description": "lab env", + "digest": "cccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccc", + "profile_id": "env-1", + "schema_version": "pcs.environment_profile.v0" +} diff --git a/adapters/pcs/fixtures/reward-binding/adversarial/artifacts_bad_profile/vp-1.json b/adapters/pcs/fixtures/reward-binding/adversarial/artifacts_bad_profile/vp-1.json new file mode 100644 index 0000000..cfa9a78 --- /dev/null +++ b/adapters/pcs/fixtures/reward-binding/adversarial/artifacts_bad_profile/vp-1.json @@ -0,0 +1,8 @@ +{ + "config_digest": "2222222222222222222222222222222222222222222222222222222222222222", + "profile_id": "vp-1", + "rubric": "r1", + "schema_version": "pcs.verifier_profile.v0", + "status": "active", + "suite": "basic" +} diff --git a/adapters/pcs/fixtures/reward-binding/adversarial/artifacts_bad_profile/vr-1.json b/adapters/pcs/fixtures/reward-binding/adversarial/artifacts_bad_profile/vr-1.json new file mode 100644 index 0000000..c855740 --- /dev/null +++ b/adapters/pcs/fixtures/reward-binding/adversarial/artifacts_bad_profile/vr-1.json @@ -0,0 +1,9 @@ +{ + "result_id": "vr-1", + "schema_version": "pcs.verification_result.v0", + "status": "pass", + "verifier_profile_ref": { + "digest": "2dde9120776c810002cb00d44aabeb73563e39281fb545c9bd2760cabfd9d595", + "id": "vp-1" + } +} diff --git a/adapters/pcs/fixtures/reward-binding/adversarial/artifacts_dup/auth-1.json b/adapters/pcs/fixtures/reward-binding/adversarial/artifacts_dup/auth-1.json new file mode 100644 index 0000000..3ba89b3 --- /dev/null +++ b/adapters/pcs/fixtures/reward-binding/adversarial/artifacts_dup/auth-1.json @@ -0,0 +1,15 @@ +{ + "authority_id": "auth-1", + "authorized_issuers": [ + { + "principal_id": "issuer-1", + "tenant_id": "tenant-lab" + } + ], + "claim_class": "reward_binding", + "environment_digest": "cccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccc", + "revoked": false, + "schema_version": "pcs.authority_record.v0", + "valid_from": 100, + "valid_until": 200 +} diff --git a/adapters/pcs/fixtures/reward-binding/adversarial/artifacts_dup/env-1.json b/adapters/pcs/fixtures/reward-binding/adversarial/artifacts_dup/env-1.json new file mode 100644 index 0000000..7e4c0ef --- /dev/null +++ b/adapters/pcs/fixtures/reward-binding/adversarial/artifacts_dup/env-1.json @@ -0,0 +1,6 @@ +{ + "description": "lab env", + "digest": "cccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccc", + "profile_id": "env-1", + "schema_version": "pcs.environment_profile.v0" +} diff --git a/adapters/pcs/fixtures/reward-binding/adversarial/artifacts_dup/vp-1.json b/adapters/pcs/fixtures/reward-binding/adversarial/artifacts_dup/vp-1.json new file mode 100644 index 0000000..0ce0036 --- /dev/null +++ b/adapters/pcs/fixtures/reward-binding/adversarial/artifacts_dup/vp-1.json @@ -0,0 +1,8 @@ +{ + "config_digest": "dddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddd", + "profile_id": "vp-1", + "rubric": "r1", + "schema_version": "pcs.verifier_profile.v0", + "status": "active", + "suite": "basic" +} diff --git a/adapters/pcs/fixtures/reward-binding/adversarial/artifacts_dup/vp-1b.json b/adapters/pcs/fixtures/reward-binding/adversarial/artifacts_dup/vp-1b.json new file mode 100644 index 0000000..cfa9a78 --- /dev/null +++ b/adapters/pcs/fixtures/reward-binding/adversarial/artifacts_dup/vp-1b.json @@ -0,0 +1,8 @@ +{ + "config_digest": "2222222222222222222222222222222222222222222222222222222222222222", + "profile_id": "vp-1", + "rubric": "r1", + "schema_version": "pcs.verifier_profile.v0", + "status": "active", + "suite": "basic" +} diff --git a/adapters/pcs/fixtures/reward-binding/adversarial/artifacts_dup/vr-1.json b/adapters/pcs/fixtures/reward-binding/adversarial/artifacts_dup/vr-1.json new file mode 100644 index 0000000..c855740 --- /dev/null +++ b/adapters/pcs/fixtures/reward-binding/adversarial/artifacts_dup/vr-1.json @@ -0,0 +1,9 @@ +{ + "result_id": "vr-1", + "schema_version": "pcs.verification_result.v0", + "status": "pass", + "verifier_profile_ref": { + "digest": "2dde9120776c810002cb00d44aabeb73563e39281fb545c9bd2760cabfd9d595", + "id": "vp-1" + } +} diff --git a/adapters/pcs/fixtures/reward-binding/adversarial/artifacts_dup/vr-2.json b/adapters/pcs/fixtures/reward-binding/adversarial/artifacts_dup/vr-2.json new file mode 100644 index 0000000..58d4604 --- /dev/null +++ b/adapters/pcs/fixtures/reward-binding/adversarial/artifacts_dup/vr-2.json @@ -0,0 +1,9 @@ +{ + "result_id": "vr-2", + "schema_version": "pcs.verification_result.v0", + "status": "pass", + "verifier_profile_ref": { + "digest": "001f51522834ff1dff03fecbc865432bbd7c6e8856befe7b80fee722d99d9fa3", + "id": "vp-1b" + } +} diff --git a/adapters/pcs/fixtures/reward-binding/adversarial/artifacts_revoked/auth-1.json b/adapters/pcs/fixtures/reward-binding/adversarial/artifacts_revoked/auth-1.json new file mode 100644 index 0000000..8c70dd0 --- /dev/null +++ b/adapters/pcs/fixtures/reward-binding/adversarial/artifacts_revoked/auth-1.json @@ -0,0 +1,15 @@ +{ + "authority_id": "auth-1", + "authorized_issuers": [ + { + "principal_id": "issuer-1", + "tenant_id": "tenant-lab" + } + ], + "claim_class": "reward_binding", + "environment_digest": "cccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccc", + "revoked": true, + "schema_version": "pcs.authority_record.v0", + "valid_from": 100, + "valid_until": 200 +} diff --git a/adapters/pcs/fixtures/reward-binding/adversarial/artifacts_revoked/env-1.json b/adapters/pcs/fixtures/reward-binding/adversarial/artifacts_revoked/env-1.json new file mode 100644 index 0000000..7e4c0ef --- /dev/null +++ b/adapters/pcs/fixtures/reward-binding/adversarial/artifacts_revoked/env-1.json @@ -0,0 +1,6 @@ +{ + "description": "lab env", + "digest": "cccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccc", + "profile_id": "env-1", + "schema_version": "pcs.environment_profile.v0" +} diff --git a/adapters/pcs/fixtures/reward-binding/adversarial/artifacts_revoked/vp-1.json b/adapters/pcs/fixtures/reward-binding/adversarial/artifacts_revoked/vp-1.json new file mode 100644 index 0000000..0ce0036 --- /dev/null +++ b/adapters/pcs/fixtures/reward-binding/adversarial/artifacts_revoked/vp-1.json @@ -0,0 +1,8 @@ +{ + "config_digest": "dddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddd", + "profile_id": "vp-1", + "rubric": "r1", + "schema_version": "pcs.verifier_profile.v0", + "status": "active", + "suite": "basic" +} diff --git a/adapters/pcs/fixtures/reward-binding/adversarial/artifacts_revoked/vr-1.json b/adapters/pcs/fixtures/reward-binding/adversarial/artifacts_revoked/vr-1.json new file mode 100644 index 0000000..c855740 --- /dev/null +++ b/adapters/pcs/fixtures/reward-binding/adversarial/artifacts_revoked/vr-1.json @@ -0,0 +1,9 @@ +{ + "result_id": "vr-1", + "schema_version": "pcs.verification_result.v0", + "status": "pass", + "verifier_profile_ref": { + "digest": "2dde9120776c810002cb00d44aabeb73563e39281fb545c9bd2760cabfd9d595", + "id": "vp-1" + } +} diff --git a/adapters/pcs/fixtures/reward-binding/adversarial/reward_bad_profile_digest.json b/adapters/pcs/fixtures/reward-binding/adversarial/reward_bad_profile_digest.json new file mode 100644 index 0000000..7b13f14 --- /dev/null +++ b/adapters/pcs/fixtures/reward-binding/adversarial/reward_bad_profile_digest.json @@ -0,0 +1,31 @@ +{ + "authority_ref": { + "digest": "530a92ae8b91bc89276183fb6f43bf03fe274985776e53e07960b51dbb655006", + "id": "auth-1" + }, + "claim_class": "reward_binding", + "envelope_id": "rew-1", + "environment_profile_ref": { + "digest": "889a85d80dc564d8d839626cd6cdc8e36269059a1a7b2972d22a632677c9e08e", + "id": "env-1" + }, + "integrity": { + "alg": "sha256", + "digest": "1d5c8803f8742d43b43183f188eeb4ca0269762ba07878a8b83a70fff9f4c1b3", + "key_id": "org-root-1" + }, + "issued_at": 150, + "issuer": { + "principal_id": "issuer-1", + "tenant_id": "tenant-lab" + }, + "schema_version": "pcs.reward_evidence_envelope.v0", + "stale": false, + "trace_digest": "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa", + "verifier_result_refs": [ + { + "digest": "7d677412669d2d5660586071b8ece0dc1495d346a9b0991ed564ef71aef45172", + "id": "vr-1" + } + ] +} diff --git a/adapters/pcs/fixtures/reward-binding/adversarial/reward_duplicate_profile_conflict.json b/adapters/pcs/fixtures/reward-binding/adversarial/reward_duplicate_profile_conflict.json new file mode 100644 index 0000000..e95b4b6 --- /dev/null +++ b/adapters/pcs/fixtures/reward-binding/adversarial/reward_duplicate_profile_conflict.json @@ -0,0 +1,35 @@ +{ + "authority_ref": { + "digest": "530a92ae8b91bc89276183fb6f43bf03fe274985776e53e07960b51dbb655006", + "id": "auth-1" + }, + "claim_class": "reward_binding", + "envelope_id": "rew-dup", + "environment_profile_ref": { + "digest": "889a85d80dc564d8d839626cd6cdc8e36269059a1a7b2972d22a632677c9e08e", + "id": "env-1" + }, + "integrity": { + "alg": "sha256", + "digest": "3ef50c8d8123607b76e02bd92a4f14e27493ffe4b44c3ae1a8454c2cd758ac3c", + "key_id": "org-root-1" + }, + "issued_at": 150, + "issuer": { + "principal_id": "issuer-1", + "tenant_id": "tenant-lab" + }, + "schema_version": "pcs.reward_evidence_envelope.v0", + "stale": false, + "trace_digest": "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa", + "verifier_result_refs": [ + { + "digest": "7d677412669d2d5660586071b8ece0dc1495d346a9b0991ed564ef71aef45172", + "id": "vr-1" + }, + { + "digest": "b50d92b7a7832aa0395b00a333a0044abd860db4ac3a1d6ad26264e7776d1ab3", + "id": "vr-2" + } + ] +} diff --git a/adapters/pcs/fixtures/reward-binding/adversarial/reward_for_substituted_trace.json b/adapters/pcs/fixtures/reward-binding/adversarial/reward_for_substituted_trace.json new file mode 100644 index 0000000..7b13f14 --- /dev/null +++ b/adapters/pcs/fixtures/reward-binding/adversarial/reward_for_substituted_trace.json @@ -0,0 +1,31 @@ +{ + "authority_ref": { + "digest": "530a92ae8b91bc89276183fb6f43bf03fe274985776e53e07960b51dbb655006", + "id": "auth-1" + }, + "claim_class": "reward_binding", + "envelope_id": "rew-1", + "environment_profile_ref": { + "digest": "889a85d80dc564d8d839626cd6cdc8e36269059a1a7b2972d22a632677c9e08e", + "id": "env-1" + }, + "integrity": { + "alg": "sha256", + "digest": "1d5c8803f8742d43b43183f188eeb4ca0269762ba07878a8b83a70fff9f4c1b3", + "key_id": "org-root-1" + }, + "issued_at": 150, + "issuer": { + "principal_id": "issuer-1", + "tenant_id": "tenant-lab" + }, + "schema_version": "pcs.reward_evidence_envelope.v0", + "stale": false, + "trace_digest": "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa", + "verifier_result_refs": [ + { + "digest": "7d677412669d2d5660586071b8ece0dc1495d346a9b0991ed564ef71aef45172", + "id": "vr-1" + } + ] +} diff --git a/adapters/pcs/fixtures/reward-binding/adversarial/reward_malformed_integrity.json b/adapters/pcs/fixtures/reward-binding/adversarial/reward_malformed_integrity.json new file mode 100644 index 0000000..db1466e --- /dev/null +++ b/adapters/pcs/fixtures/reward-binding/adversarial/reward_malformed_integrity.json @@ -0,0 +1,31 @@ +{ + "authority_ref": { + "digest": "530a92ae8b91bc89276183fb6f43bf03fe274985776e53e07960b51dbb655006", + "id": "auth-1" + }, + "claim_class": "reward_binding", + "envelope_id": "rew-1", + "environment_profile_ref": { + "digest": "889a85d80dc564d8d839626cd6cdc8e36269059a1a7b2972d22a632677c9e08e", + "id": "env-1" + }, + "integrity": { + "alg": "sha256", + "digest": "0000000000000000000000000000000000000000000000000000000000000000", + "key_id": "org-root-1" + }, + "issued_at": 150, + "issuer": { + "principal_id": "issuer-1", + "tenant_id": "tenant-lab" + }, + "schema_version": "pcs.reward_evidence_envelope.v0", + "stale": false, + "trace_digest": "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa", + "verifier_result_refs": [ + { + "digest": "7d677412669d2d5660586071b8ece0dc1495d346a9b0991ed564ef71aef45172", + "id": "vr-1" + } + ] +} diff --git a/adapters/pcs/fixtures/reward-binding/adversarial/reward_missing_result.json b/adapters/pcs/fixtures/reward-binding/adversarial/reward_missing_result.json new file mode 100644 index 0000000..d13a571 --- /dev/null +++ b/adapters/pcs/fixtures/reward-binding/adversarial/reward_missing_result.json @@ -0,0 +1,31 @@ +{ + "authority_ref": { + "digest": "530a92ae8b91bc89276183fb6f43bf03fe274985776e53e07960b51dbb655006", + "id": "auth-1" + }, + "claim_class": "reward_binding", + "envelope_id": "rew-missing", + "environment_profile_ref": { + "digest": "889a85d80dc564d8d839626cd6cdc8e36269059a1a7b2972d22a632677c9e08e", + "id": "env-1" + }, + "integrity": { + "alg": "sha256", + "digest": "cb2b484450abeffe62da14e4e677a9e6cddf68d2d045f86bbe46a7a6388ecac8", + "key_id": "org-root-1" + }, + "issued_at": 150, + "issuer": { + "principal_id": "issuer-1", + "tenant_id": "tenant-lab" + }, + "schema_version": "pcs.reward_evidence_envelope.v0", + "stale": false, + "trace_digest": "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa", + "verifier_result_refs": [ + { + "digest": "3333333333333333333333333333333333333333333333333333333333333333", + "id": "vr-missing" + } + ] +} diff --git a/adapters/pcs/fixtures/reward-binding/adversarial/reward_revoked_issuer.json b/adapters/pcs/fixtures/reward-binding/adversarial/reward_revoked_issuer.json new file mode 100644 index 0000000..1b9a99d --- /dev/null +++ b/adapters/pcs/fixtures/reward-binding/adversarial/reward_revoked_issuer.json @@ -0,0 +1,31 @@ +{ + "authority_ref": { + "digest": "da960c7f93671a8d3fca78016b7deec11be25f500661eb60fc43d9d9f7f48d0e", + "id": "auth-1" + }, + "claim_class": "reward_binding", + "envelope_id": "rew-revoked", + "environment_profile_ref": { + "digest": "889a85d80dc564d8d839626cd6cdc8e36269059a1a7b2972d22a632677c9e08e", + "id": "env-1" + }, + "integrity": { + "alg": "sha256", + "digest": "f6759729da3e88ac3d2c37eda28588c8d463af798b50d52e92d56b2e69e2a625", + "key_id": "org-root-1" + }, + "issued_at": 150, + "issuer": { + "principal_id": "issuer-1", + "tenant_id": "tenant-lab" + }, + "schema_version": "pcs.reward_evidence_envelope.v0", + "stale": false, + "trace_digest": "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa", + "verifier_result_refs": [ + { + "digest": "7d677412669d2d5660586071b8ece0dc1495d346a9b0991ed564ef71aef45172", + "id": "vr-1" + } + ] +} diff --git a/adapters/pcs/fixtures/reward-binding/adversarial/reward_stale.json b/adapters/pcs/fixtures/reward-binding/adversarial/reward_stale.json new file mode 100644 index 0000000..db25c53 --- /dev/null +++ b/adapters/pcs/fixtures/reward-binding/adversarial/reward_stale.json @@ -0,0 +1,31 @@ +{ + "authority_ref": { + "digest": "530a92ae8b91bc89276183fb6f43bf03fe274985776e53e07960b51dbb655006", + "id": "auth-1" + }, + "claim_class": "reward_binding", + "envelope_id": "rew-stale", + "environment_profile_ref": { + "digest": "889a85d80dc564d8d839626cd6cdc8e36269059a1a7b2972d22a632677c9e08e", + "id": "env-1" + }, + "integrity": { + "alg": "sha256", + "digest": "181d7b945cf63985911ff21abc74c1be12c4df8da90bfffc50b42d98ed7f6616", + "key_id": "org-root-1" + }, + "issued_at": 150, + "issuer": { + "principal_id": "issuer-1", + "tenant_id": "tenant-lab" + }, + "schema_version": "pcs.reward_evidence_envelope.v0", + "stale": true, + "trace_digest": "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa", + "verifier_result_refs": [ + { + "digest": "7d677412669d2d5660586071b8ece0dc1495d346a9b0991ed564ef71aef45172", + "id": "vr-1" + } + ] +} diff --git a/adapters/pcs/fixtures/reward-binding/adversarial/reward_unsupported_version.json b/adapters/pcs/fixtures/reward-binding/adversarial/reward_unsupported_version.json new file mode 100644 index 0000000..ecb1c92 --- /dev/null +++ b/adapters/pcs/fixtures/reward-binding/adversarial/reward_unsupported_version.json @@ -0,0 +1,31 @@ +{ + "authority_ref": { + "digest": "530a92ae8b91bc89276183fb6f43bf03fe274985776e53e07960b51dbb655006", + "id": "auth-1" + }, + "claim_class": "reward_binding", + "envelope_id": "rew-1", + "environment_profile_ref": { + "digest": "889a85d80dc564d8d839626cd6cdc8e36269059a1a7b2972d22a632677c9e08e", + "id": "env-1" + }, + "integrity": { + "alg": "sha256", + "digest": "1d5c8803f8742d43b43183f188eeb4ca0269762ba07878a8b83a70fff9f4c1b3", + "key_id": "org-root-1" + }, + "issued_at": 150, + "issuer": { + "principal_id": "issuer-1", + "tenant_id": "tenant-lab" + }, + "schema_version": "pcs.reward_evidence_envelope.v999", + "stale": false, + "trace_digest": "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa", + "verifier_result_refs": [ + { + "digest": "7d677412669d2d5660586071b8ece0dc1495d346a9b0991ed564ef71aef45172", + "id": "vr-1" + } + ] +} diff --git a/adapters/pcs/fixtures/reward-binding/adversarial/reward_wrong_tenant.json b/adapters/pcs/fixtures/reward-binding/adversarial/reward_wrong_tenant.json new file mode 100644 index 0000000..193cd16 --- /dev/null +++ b/adapters/pcs/fixtures/reward-binding/adversarial/reward_wrong_tenant.json @@ -0,0 +1,31 @@ +{ + "authority_ref": { + "digest": "530a92ae8b91bc89276183fb6f43bf03fe274985776e53e07960b51dbb655006", + "id": "auth-1" + }, + "claim_class": "reward_binding", + "envelope_id": "rew-tenant", + "environment_profile_ref": { + "digest": "889a85d80dc564d8d839626cd6cdc8e36269059a1a7b2972d22a632677c9e08e", + "id": "env-1" + }, + "integrity": { + "alg": "sha256", + "digest": "7241361369f945811cf6a040510e7b5b7a9d3269e2791c0ca9fc5dcbcf641f3e", + "key_id": "org-root-1" + }, + "issued_at": 150, + "issuer": { + "principal_id": "issuer-1", + "tenant_id": "wrong-tenant" + }, + "schema_version": "pcs.reward_evidence_envelope.v0", + "stale": false, + "trace_digest": "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa", + "verifier_result_refs": [ + { + "digest": "7d677412669d2d5660586071b8ece0dc1495d346a9b0991ed564ef71aef45172", + "id": "vr-1" + } + ] +} diff --git a/adapters/pcs/fixtures/reward-binding/adversarial/trace_substituted.json b/adapters/pcs/fixtures/reward-binding/adversarial/trace_substituted.json new file mode 100644 index 0000000..7da26a4 --- /dev/null +++ b/adapters/pcs/fixtures/reward-binding/adversarial/trace_substituted.json @@ -0,0 +1,5 @@ +{ + "events": [], + "schema_version": "pf-core.trace.v0", + "trace_hash": "1111111111111111111111111111111111111111111111111111111111111111" +} diff --git a/adapters/pcs/fixtures/reward-binding/artifacts/auth-1.json b/adapters/pcs/fixtures/reward-binding/artifacts/auth-1.json new file mode 100644 index 0000000..3ba89b3 --- /dev/null +++ b/adapters/pcs/fixtures/reward-binding/artifacts/auth-1.json @@ -0,0 +1,15 @@ +{ + "authority_id": "auth-1", + "authorized_issuers": [ + { + "principal_id": "issuer-1", + "tenant_id": "tenant-lab" + } + ], + "claim_class": "reward_binding", + "environment_digest": "cccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccc", + "revoked": false, + "schema_version": "pcs.authority_record.v0", + "valid_from": 100, + "valid_until": 200 +} diff --git a/adapters/pcs/fixtures/reward-binding/artifacts/env-1.json b/adapters/pcs/fixtures/reward-binding/artifacts/env-1.json new file mode 100644 index 0000000..7e4c0ef --- /dev/null +++ b/adapters/pcs/fixtures/reward-binding/artifacts/env-1.json @@ -0,0 +1,6 @@ +{ + "description": "lab env", + "digest": "cccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccc", + "profile_id": "env-1", + "schema_version": "pcs.environment_profile.v0" +} diff --git a/adapters/pcs/fixtures/reward-binding/artifacts/vp-1.json b/adapters/pcs/fixtures/reward-binding/artifacts/vp-1.json new file mode 100644 index 0000000..0ce0036 --- /dev/null +++ b/adapters/pcs/fixtures/reward-binding/artifacts/vp-1.json @@ -0,0 +1,8 @@ +{ + "config_digest": "dddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddd", + "profile_id": "vp-1", + "rubric": "r1", + "schema_version": "pcs.verifier_profile.v0", + "status": "active", + "suite": "basic" +} diff --git a/adapters/pcs/fixtures/reward-binding/artifacts/vr-1.json b/adapters/pcs/fixtures/reward-binding/artifacts/vr-1.json new file mode 100644 index 0000000..c855740 --- /dev/null +++ b/adapters/pcs/fixtures/reward-binding/artifacts/vr-1.json @@ -0,0 +1,9 @@ +{ + "result_id": "vr-1", + "schema_version": "pcs.verification_result.v0", + "status": "pass", + "verifier_profile_ref": { + "digest": "2dde9120776c810002cb00d44aabeb73563e39281fb545c9bd2760cabfd9d595", + "id": "vp-1" + } +} diff --git a/adapters/pcs/fixtures/reward-binding/reward_valid.json b/adapters/pcs/fixtures/reward-binding/reward_valid.json new file mode 100644 index 0000000..7b13f14 --- /dev/null +++ b/adapters/pcs/fixtures/reward-binding/reward_valid.json @@ -0,0 +1,31 @@ +{ + "authority_ref": { + "digest": "530a92ae8b91bc89276183fb6f43bf03fe274985776e53e07960b51dbb655006", + "id": "auth-1" + }, + "claim_class": "reward_binding", + "envelope_id": "rew-1", + "environment_profile_ref": { + "digest": "889a85d80dc564d8d839626cd6cdc8e36269059a1a7b2972d22a632677c9e08e", + "id": "env-1" + }, + "integrity": { + "alg": "sha256", + "digest": "1d5c8803f8742d43b43183f188eeb4ca0269762ba07878a8b83a70fff9f4c1b3", + "key_id": "org-root-1" + }, + "issued_at": 150, + "issuer": { + "principal_id": "issuer-1", + "tenant_id": "tenant-lab" + }, + "schema_version": "pcs.reward_evidence_envelope.v0", + "stale": false, + "trace_digest": "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa", + "verifier_result_refs": [ + { + "digest": "7d677412669d2d5660586071b8ece0dc1495d346a9b0991ed564ef71aef45172", + "id": "vr-1" + } + ] +} diff --git a/adapters/pcs/fixtures/reward-binding/trace_valid.json b/adapters/pcs/fixtures/reward-binding/trace_valid.json new file mode 100644 index 0000000..dc5bd60 --- /dev/null +++ b/adapters/pcs/fixtures/reward-binding/trace_valid.json @@ -0,0 +1,5 @@ +{ + "events": [], + "schema_version": "pf-core.trace.v0", + "trace_hash": "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa" +} diff --git a/adapters/pcs/fixtures/reward-binding/trusted_keys.json b/adapters/pcs/fixtures/reward-binding/trusted_keys.json new file mode 100644 index 0000000..fd38137 --- /dev/null +++ b/adapters/pcs/fixtures/reward-binding/trusted_keys.json @@ -0,0 +1,10 @@ +{ + "schema_version": "pcs.trusted_keys.v0", + "keys": [ + { + "key_id": "org-root-1", + "alg": "sha256", + "public_pin": "ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff" + } + ] +} diff --git a/adapters/pcs/reward_binding_adapter.py b/adapters/pcs/reward_binding_adapter.py new file mode 100644 index 0000000..36d0d63 --- /dev/null +++ b/adapters/pcs/reward_binding_adapter.py @@ -0,0 +1,462 @@ +"""Untrusted PCS → RewardBindingInput adapter (outside PF-Core TCB).""" + +from __future__ import annotations + +import hashlib +import json +from pathlib import Path +from typing import Any, Dict, List, Mapping, Optional, Tuple + +from jsonschema import Draft202012Validator +from referencing import Registry, Resource + +from pf_core.errors import PFCoreError +from pf_core.hash_chain import canonical_json, normalize_hash + +SUPPORTED_ENVELOPE_VERSION = "pcs.reward_evidence_envelope.v0" +SUPPORTED_PROFILE_VERSION = "pcs.verifier_profile.v0" +SUPPORTED_ENV_VERSION = "pcs.environment_profile.v0" +SUPPORTED_RESULT_VERSION = "pcs.verification_result.v0" +SUPPORTED_AUTHORITY_VERSION = "pcs.authority_record.v0" + +ARTIFACT_CLASS_VERIFIER_PROFILE = "verifier_profile" +ARTIFACT_CLASS_ENVIRONMENT_PROFILE = "environment_profile" +ARTIFACT_CLASS_VERIFICATION_RESULT = "verification_result" +ARTIFACT_CLASS_AUTHORITY_RECORD = "authority_record" + +EXPECTED_CLASS = { + ARTIFACT_CLASS_VERIFIER_PROFILE: SUPPORTED_PROFILE_VERSION, + ARTIFACT_CLASS_ENVIRONMENT_PROFILE: SUPPORTED_ENV_VERSION, + ARTIFACT_CLASS_VERIFICATION_RESULT: SUPPORTED_RESULT_VERSION, + ARTIFACT_CLASS_AUTHORITY_RECORD: SUPPORTED_AUTHORITY_VERSION, +} + + +def _load_json(path: Path) -> Dict[str, Any]: + return json.loads(path.read_text(encoding="utf-8")) + + +def _sha256_bytes(data: bytes) -> str: + return hashlib.sha256(data).hexdigest() + + +def _sha256_obj(obj: Mapping[str, Any]) -> str: + return _sha256_bytes(canonical_json(obj).encode("utf-8")) + + +def _payload_without_integrity(obj: Mapping[str, Any]) -> Dict[str, Any]: + payload = dict(obj) + payload.pop("integrity", None) + return payload + + +def load_pcs_registry(schemas_dir: Path) -> Registry: + resources: Dict[str, Resource] = {} + for path in sorted(schemas_dir.glob("*.schema.json")): + contents = json.loads(path.read_text(encoding="utf-8")) + schema_id = contents.get("$id", path.name) + resources[schema_id] = Resource.from_contents(contents) + return Registry().with_resources(resources.items()) + + +def validate_pcs_object(obj: Mapping[str, Any], registry: Registry) -> str: + version = obj.get("schema_version") + if not isinstance(version, str): + raise PFCoreError( + "IndeterminateUnsupportedVersion", + "PCS object missing schema_version", + "schema_version", + ) + resource = registry.get(version) + if resource is None: + raise PFCoreError( + "IndeterminateUnsupportedVersion", + f"unsupported PCS schema_version: {version}", + "schema_version", + ) + validator = Draft202012Validator(resource.contents, registry=registry) + errors = sorted(validator.iter_errors(obj), key=lambda e: e.path) + if errors: + err = errors[0] + path = "/".join(str(p) for p in err.path) + raise PFCoreError("IndeterminateInvalidInput", err.message, path or None) + return version + + +def load_trust_registry(path: Path) -> Dict[str, str]: + data = _load_json(path) + keys = data.get("keys") + if not isinstance(keys, list): + raise PFCoreError( + "IndeterminateUntrustedArtifact", + "trusted_keys.json missing keys[]", + "keys", + ) + out: Dict[str, str] = {} + for entry in keys: + if not isinstance(entry, Mapping): + continue + key_id = entry.get("key_id") + pin = entry.get("public_pin") + if isinstance(key_id, str) and isinstance(pin, str): + out[key_id] = normalize_hash(pin) if len(pin) > 10 else pin + if not out: + raise PFCoreError( + "IndeterminateUntrustedArtifact", + "trusted_keys.json has no usable keys", + "keys", + ) + return out + + +def verify_integrity_envelope( + obj: Mapping[str, Any], + trusted_keys: Mapping[str, str], +) -> str: + integrity = obj.get("integrity") + if not isinstance(integrity, Mapping): + raise PFCoreError( + "IndeterminateUntrustedArtifact", + "missing integrity envelope", + "integrity", + ) + if integrity.get("alg") != "sha256": + raise PFCoreError( + "IndeterminateUntrustedArtifact", + "unsupported integrity alg", + "integrity/alg", + ) + key_id = integrity.get("key_id") + if not isinstance(key_id, str) or key_id not in trusted_keys: + raise PFCoreError( + "IndeterminateUntrustedArtifact", + f"integrity key_id not in trust registry: {key_id!r}", + "integrity/key_id", + ) + try: + claimed = normalize_hash(str(integrity.get("digest", ""))) + except PFCoreError as exc: + raise PFCoreError( + "IndeterminateUntrustedArtifact", + f"malformed integrity digest: {exc.message}", + "integrity/digest", + ) from exc + computed = _sha256_obj(_payload_without_integrity(obj)) + if claimed != computed: + raise PFCoreError( + "IndeterminateUntrustedArtifact", + "integrity digest mismatch", + "integrity/digest", + ) + return computed + + +def _resolve_artifact( + artifact_root: Path, + artifact_id: str, + expected_digest: str, + expected_class: str, + seen: Dict[str, str], +) -> Dict[str, Any]: + if artifact_id in seen and seen[artifact_id] != expected_digest: + raise PFCoreError( + "IndeterminateInvalidInput", + f"ambiguous artifact id {artifact_id!r} with conflicting digests", + artifact_id, + ) + path = artifact_root / f"{artifact_id}.json" + if not path.exists(): + raise PFCoreError( + "IndeterminateMissingReference", + f"artifact not found: {artifact_id}", + artifact_id, + ) + raw = path.read_bytes() + obj = json.loads(raw.decode("utf-8")) + if not isinstance(obj, dict): + raise PFCoreError( + "IndeterminateInvalidInput", + f"artifact {artifact_id} is not an object", + artifact_id, + ) + digest = _sha256_bytes(raw) + try: + want = normalize_hash(expected_digest) + except PFCoreError as exc: + raise PFCoreError( + "IndeterminateInvalidInput", + f"malformed artifact digest for {artifact_id}: {exc.message}", + artifact_id, + ) from exc + if digest != want: + # Also allow digest of canonical JSON payload (fixtures may store pretty JSON). + digest_canon = _sha256_obj(obj) + if digest_canon != want: + raise PFCoreError( + "IndeterminateUntrustedArtifact", + f"artifact digest mismatch for {artifact_id}", + artifact_id, + ) + digest = digest_canon + seen[artifact_id] = digest + version = obj.get("schema_version") + expected_version = EXPECTED_CLASS.get(expected_class) + if expected_version and version != expected_version: + raise PFCoreError( + "IndeterminateInvalidInput", + f"artifact {artifact_id} wrong class/version: got {version}, " + f"expected {expected_version}", + artifact_id, + ) + return obj + + +def _normalize_digest(value: str, path: str) -> str: + try: + return normalize_hash(value) + except PFCoreError as exc: + raise PFCoreError( + "IndeterminateInvalidInput", + f"malformed digest at {path}: {exc.message}", + path, + ) from exc + + +def adapt_reward_binding( + *, + trace: Mapping[str, Any], + reward_evidence: Mapping[str, Any], + artifact_root: Path, + trust_registry_path: Path, + pcs_schemas_dir: Optional[Path] = None, +) -> Tuple[Dict[str, Any], Dict[str, Any]]: + """Validate PCS reward evidence and emit RewardBindingInput + mapping report. + + Fail-closed: raises PFCoreError with Indeterminate* codes; never returns safe. + """ + schemas_dir = pcs_schemas_dir or Path(__file__).resolve().parent / "schemas" + registry = load_pcs_registry(schemas_dir) + trusted_keys = load_trust_registry(trust_registry_path) + + version = reward_evidence.get("schema_version") + if version != SUPPORTED_ENVELOPE_VERSION: + raise PFCoreError( + "IndeterminateUnsupportedVersion", + f"unsupported reward envelope version: {version}", + "schema_version", + ) + + validate_pcs_object(reward_evidence, registry) + envelope_digest = verify_integrity_envelope(reward_evidence, trusted_keys) + + trace_digest_raw = trace.get("trace_hash") or trace.get("trace_digest") + if not isinstance(trace_digest_raw, str): + raise PFCoreError( + "IndeterminateInvalidInput", + "trace missing trace_hash/trace_digest", + "trace", + ) + pf_trace_digest = _normalize_digest(trace_digest_raw, "trace/trace_hash") + reward_trace_digest = _normalize_digest( + str(reward_evidence["trace_digest"]), "reward/trace_digest" + ) + + seen: Dict[str, str] = {} + refs: List[Dict[str, str]] = [] + closed = True + integrity_ok = True + classes_ok = True + + env_ref = reward_evidence["environment_profile_ref"] + env_obj = _resolve_artifact( + artifact_root, + env_ref["id"], + env_ref["digest"], + ARTIFACT_CLASS_ENVIRONMENT_PROFILE, + seen, + ) + validate_pcs_object(env_obj, registry) + env_digest = _normalize_digest(str(env_obj["digest"]), "environment/digest") + refs.append( + { + "id": env_ref["id"], + "class": ARTIFACT_CLASS_ENVIRONMENT_PROFILE, + "digest": seen[env_ref["id"]], + } + ) + + auth_ref = reward_evidence["authority_ref"] + auth_obj = _resolve_artifact( + artifact_root, + auth_ref["id"], + auth_ref["digest"], + ARTIFACT_CLASS_AUTHORITY_RECORD, + seen, + ) + validate_pcs_object(auth_obj, registry) + refs.append( + { + "id": auth_ref["id"], + "class": ARTIFACT_CLASS_AUTHORITY_RECORD, + "digest": seen[auth_ref["id"]], + } + ) + + verification_bindings: List[Dict[str, str]] = [] + verification_result_digests: List[str] = [] + verifier_profiles: List[Dict[str, str]] = [] + verifier_profile_digests: List[str] = [] + profile_by_id: Dict[str, str] = {} + + for result_ref in reward_evidence["verifier_result_refs"]: + result_obj = _resolve_artifact( + artifact_root, + result_ref["id"], + result_ref["digest"], + ARTIFACT_CLASS_VERIFICATION_RESULT, + seen, + ) + validate_pcs_object(result_obj, registry) + result_digest = seen[result_ref["id"]] + verification_result_digests.append(result_digest) + refs.append( + { + "id": result_ref["id"], + "class": ARTIFACT_CLASS_VERIFICATION_RESULT, + "digest": result_digest, + } + ) + pref = result_obj["verifier_profile_ref"] + profile_obj = _resolve_artifact( + artifact_root, + pref["id"], + pref["digest"], + ARTIFACT_CLASS_VERIFIER_PROFILE, + seen, + ) + validate_pcs_object(profile_obj, registry) + if profile_obj.get("status") in {"revoked", "superseded"}: + # Still normalize; trusted issuer/profile predicates decide acceptance. + pass + config_digest = _normalize_digest( + str(profile_obj["config_digest"]), f"profile/{pref['id']}/config_digest" + ) + profile_id = str(profile_obj["profile_id"]) + if profile_id in profile_by_id and profile_by_id[profile_id] != config_digest: + raise PFCoreError( + "IndeterminateInvalidInput", + f"duplicate profile id {profile_id!r} with conflicting config digest", + profile_id, + ) + if profile_id not in profile_by_id: + profile_by_id[profile_id] = config_digest + verifier_profiles.append( + {"profile_id": profile_id, "config_digest": config_digest} + ) + verifier_profile_digests.append(config_digest) + refs.append( + { + "id": pref["id"], + "class": ARTIFACT_CLASS_VERIFIER_PROFILE, + "digest": seen[pref["id"]], + } + ) + verification_bindings.append( + { + "result_digest": result_digest, + "profile_id": profile_id, + "config_digest": config_digest, + } + ) + + issuer = { + "principal_id": str(reward_evidence["issuer"]["principal_id"]), + "tenant_id": str(reward_evidence["issuer"]["tenant_id"]), + } + auth_env = _normalize_digest( + str(auth_obj["environment_digest"]), "authority/environment_digest" + ) + authority = { + "authority_ref": str(auth_obj["authority_id"]), + "digest": seen[auth_ref["id"]], + "valid_from": int(auth_obj["valid_from"]), + "valid_until": int(auth_obj["valid_until"]), + "revoked": bool(auth_obj["revoked"]), + "claim_class": str(auth_obj["claim_class"]), + "environment_digest": auth_env, + "authorized_issuers": [ + { + "principal_id": str(i["principal_id"]), + "tenant_id": str(i["tenant_id"]), + } + for i in auth_obj["authorized_issuers"] + ], + } + claim_class = str( + reward_evidence.get("claim_class") or auth_obj["claim_class"] + ) + lifecycle = { + "issued_at": int(reward_evidence["issued_at"]), + "stale": bool(reward_evidence.get("stale", False)), + "required_claim_class": claim_class, + } + + binding_input: Dict[str, Any] = { + "schema_version": "pf-core.reward_binding_input.v0", + "trace_digest": pf_trace_digest, + "reward_trace_digest": reward_trace_digest, + "reward_evidence_digest": envelope_digest, + "environment_profile_digest": env_digest, + "verifier_profile_digests": verifier_profile_digests, + "verification_result_digests": verification_result_digests, + "verifier_profiles": verifier_profiles, + "verification_bindings": verification_bindings, + "issuer": issuer, + "authority": authority, + "lifecycle": lifecycle, + "artifact_closure": { + "closed": closed, + "integrity_ok": integrity_ok, + "classes_ok": classes_ok, + "refs": refs, + }, + } + + mapping_report = { + "adapter": "pcs.reward_binding_adapter", + "envelope_id": reward_evidence.get("envelope_id"), + "assumptions_discharged": [ + "A1-schema-validate-pcs-mirrors", + "integrity-envelope-checked", + "artifact-refs-resolved", + "digests-normalized-hex64", + ], + "assumptions_delegated": ["A11", "A12", "A13", "A14"], + "field_map": { + "trace.trace_hash": "trace_digest", + "reward.trace_digest": "reward_trace_digest", + "reward.integrity.digest": "reward_evidence_digest", + "environment.digest": "environment_profile_digest", + "authority.*": "authority.*", + "results+profiles": "verification_bindings / verifier_profiles", + }, + "artifact_ids": sorted(seen.keys()), + } + return binding_input, mapping_report + + +def adapt_reward_binding_files( + *, + trace_path: Path, + reward_path: Path, + artifact_root: Path, + trust_registry_path: Path, + pcs_schemas_dir: Optional[Path] = None, +) -> Tuple[Dict[str, Any], Dict[str, Any]]: + return adapt_reward_binding( + trace=_load_json(trace_path), + reward_evidence=_load_json(reward_path), + artifact_root=artifact_root, + trust_registry_path=trust_registry_path, + pcs_schemas_dir=pcs_schemas_dir, + ) diff --git a/adapters/pcs/schemas/SCHEMA_PINS.json b/adapters/pcs/schemas/SCHEMA_PINS.json new file mode 100644 index 0000000..feb6d27 --- /dev/null +++ b/adapters/pcs/schemas/SCHEMA_PINS.json @@ -0,0 +1,7 @@ +{ + "authority_record.schema.json": "3da39fd9d1e95f40e72e2701a7675475f1ded7851c993ffd1875643e8e7435da", + "environment_profile.schema.json": "39f039415d519b0ba80b203cb90d479ffdf6e45fb2832be9b8336983b3e19dee", + "reward_evidence_envelope.schema.json": "0fc5c9b55b407ded03f23b96307bfc8b6f5b74d4244a0dc7bd6cbe876a89eae0", + "verification_result.schema.json": "37324f4877353ca90fcc59e54b70429d59d86ccd21ab2f0e52942e4d53495b9e", + "verifier_profile.schema.json": "ad985317963692d8b3ea90b92f931166199657c2688e50c57d11e89e135d227a" +} diff --git a/adapters/pcs/schemas/authority_record.schema.json b/adapters/pcs/schemas/authority_record.schema.json new file mode 100644 index 0000000..9536a75 --- /dev/null +++ b/adapters/pcs/schemas/authority_record.schema.json @@ -0,0 +1,40 @@ +{ + "$schema": "https://json-schema.org/draft/2020-12/schema", + "$id": "pcs.authority_record.v0", + "title": "PCS Authority Record (mirrored)", + "description": "Immutable mirror of PCS authority record. Not in PF-Core TCB.", + "type": "object", + "additionalProperties": false, + "required": [ + "schema_version", + "authority_id", + "valid_from", + "valid_until", + "revoked", + "claim_class", + "environment_digest", + "authorized_issuers" + ], + "properties": { + "schema_version": { "const": "pcs.authority_record.v0" }, + "authority_id": { "type": "string", "minLength": 1 }, + "valid_from": { "type": "integer", "minimum": 0 }, + "valid_until": { "type": "integer", "minimum": 0 }, + "revoked": { "type": "boolean" }, + "claim_class": { "type": "string", "minLength": 1 }, + "environment_digest": { "type": "string", "minLength": 1 }, + "authorized_issuers": { + "type": "array", + "minItems": 1, + "items": { + "type": "object", + "additionalProperties": false, + "required": ["principal_id", "tenant_id"], + "properties": { + "principal_id": { "type": "string", "minLength": 1 }, + "tenant_id": { "type": "string", "minLength": 1 } + } + } + } + } +} diff --git a/adapters/pcs/schemas/environment_profile.schema.json b/adapters/pcs/schemas/environment_profile.schema.json new file mode 100644 index 0000000..9a49f90 --- /dev/null +++ b/adapters/pcs/schemas/environment_profile.schema.json @@ -0,0 +1,15 @@ +{ + "$schema": "https://json-schema.org/draft/2020-12/schema", + "$id": "pcs.environment_profile.v0", + "title": "PCS Environment Profile (mirrored)", + "description": "Immutable mirror of PCS environment profile. Not in PF-Core TCB.", + "type": "object", + "additionalProperties": false, + "required": ["schema_version", "profile_id", "digest"], + "properties": { + "schema_version": { "const": "pcs.environment_profile.v0" }, + "profile_id": { "type": "string", "minLength": 1 }, + "digest": { "type": "string", "minLength": 1 }, + "description": { "type": "string" } + } +} diff --git a/adapters/pcs/schemas/reward_evidence_envelope.schema.json b/adapters/pcs/schemas/reward_evidence_envelope.schema.json new file mode 100644 index 0000000..d8455c3 --- /dev/null +++ b/adapters/pcs/schemas/reward_evidence_envelope.schema.json @@ -0,0 +1,77 @@ +{ + "$schema": "https://json-schema.org/draft/2020-12/schema", + "$id": "pcs.reward_evidence_envelope.v0", + "title": "PCS Reward Evidence Envelope (mirrored)", + "description": "Immutable mirror of PCS reward evidence envelope. Not in PF-Core TCB. Pin digest in adapters/pcs/README.md.", + "type": "object", + "additionalProperties": false, + "required": [ + "schema_version", + "envelope_id", + "trace_digest", + "environment_profile_ref", + "verifier_result_refs", + "issuer", + "authority_ref", + "issued_at", + "integrity" + ], + "properties": { + "schema_version": { "const": "pcs.reward_evidence_envelope.v0" }, + "envelope_id": { "type": "string", "minLength": 1 }, + "trace_digest": { "type": "string", "minLength": 1 }, + "environment_profile_ref": { + "type": "object", + "additionalProperties": false, + "required": ["id", "digest"], + "properties": { + "id": { "type": "string", "minLength": 1 }, + "digest": { "type": "string", "minLength": 1 } + } + }, + "verifier_result_refs": { + "type": "array", + "minItems": 1, + "items": { + "type": "object", + "additionalProperties": false, + "required": ["id", "digest"], + "properties": { + "id": { "type": "string", "minLength": 1 }, + "digest": { "type": "string", "minLength": 1 } + } + } + }, + "issuer": { + "type": "object", + "additionalProperties": false, + "required": ["principal_id", "tenant_id"], + "properties": { + "principal_id": { "type": "string", "minLength": 1 }, + "tenant_id": { "type": "string", "minLength": 1 } + } + }, + "authority_ref": { + "type": "object", + "additionalProperties": false, + "required": ["id", "digest"], + "properties": { + "id": { "type": "string", "minLength": 1 }, + "digest": { "type": "string", "minLength": 1 } + } + }, + "issued_at": { "type": "integer", "minimum": 0 }, + "stale": { "type": "boolean" }, + "claim_class": { "type": "string", "minLength": 1 }, + "integrity": { + "type": "object", + "additionalProperties": false, + "required": ["alg", "digest", "key_id"], + "properties": { + "alg": { "const": "sha256" }, + "digest": { "type": "string", "minLength": 1 }, + "key_id": { "type": "string", "minLength": 1 } + } + } + } +} diff --git a/adapters/pcs/schemas/verification_result.schema.json b/adapters/pcs/schemas/verification_result.schema.json new file mode 100644 index 0000000..f73f640 --- /dev/null +++ b/adapters/pcs/schemas/verification_result.schema.json @@ -0,0 +1,32 @@ +{ + "$schema": "https://json-schema.org/draft/2020-12/schema", + "$id": "pcs.verification_result.v0", + "title": "PCS Verification Result (mirrored)", + "description": "Immutable mirror of PCS verification result. Not in PF-Core TCB.", + "type": "object", + "additionalProperties": false, + "required": [ + "schema_version", + "result_id", + "verifier_profile_ref", + "status" + ], + "properties": { + "schema_version": { "const": "pcs.verification_result.v0" }, + "result_id": { "type": "string", "minLength": 1 }, + "verifier_profile_ref": { + "type": "object", + "additionalProperties": false, + "required": ["id", "digest"], + "properties": { + "id": { "type": "string", "minLength": 1 }, + "digest": { "type": "string", "minLength": 1 } + } + }, + "status": { + "type": "string", + "enum": ["pass", "fail", "error"] + }, + "artifact_digest": { "type": "string" } + } +} diff --git a/adapters/pcs/schemas/verifier_profile.schema.json b/adapters/pcs/schemas/verifier_profile.schema.json new file mode 100644 index 0000000..44b8eb3 --- /dev/null +++ b/adapters/pcs/schemas/verifier_profile.schema.json @@ -0,0 +1,20 @@ +{ + "$schema": "https://json-schema.org/draft/2020-12/schema", + "$id": "pcs.verifier_profile.v0", + "title": "PCS Verifier Profile (mirrored)", + "description": "Immutable mirror of PCS verifier profile. Not in PF-Core TCB.", + "type": "object", + "additionalProperties": false, + "required": ["schema_version", "profile_id", "config_digest", "status"], + "properties": { + "schema_version": { "const": "pcs.verifier_profile.v0" }, + "profile_id": { "type": "string", "minLength": 1 }, + "config_digest": { "type": "string", "minLength": 1 }, + "status": { + "type": "string", + "enum": ["active", "superseded", "revoked"] + }, + "suite": { "type": "string" }, + "rubric": { "type": "string" } + } +} diff --git a/docs/pf-core/adrs/001-reward-binding-ownership.md b/docs/pf-core/adrs/001-reward-binding-ownership.md new file mode 100644 index 0000000..cef1d0c --- /dev/null +++ b/docs/pf-core/adrs/001-reward-binding-ownership.md @@ -0,0 +1,31 @@ +# ADR-001: Reward-binding ownership + +- Status: Accepted +- Date: 2026-07-24 +- Baseline: `629984cb62b9d4b2281d36062a2979198ba61c82`, Lean `4.14.0`, Python `3.12+` + +## Context + +Reward evidence arrives as portable PCS-shaped JSON (envelopes, verifier profiles, environment profiles, authority records). PF-Core already owns trace safety (`TraceSafe` / `EffectKind`) and must not become an RL/judge platform. Downstream OVK may later invoke checkers against pinned verifier profiles; LabTrust may emit reward-binding fixtures. + +## Decision + +1. **PCS owns portable evidence layout.** Mirrored immutable schemas live under untrusted `adapters/pcs/schemas/`. Upstream to pcs-core via companion tickets; do not invent a second portable evidence standard inside `pf-core/schemas/`. +2. **PF-Core owns normalized reward-binding predicates** on `RewardBindingInput`: `RewardBoundToTrace`, `VerifierConfigurationPinned`, `EvidenceChainClosed`, `RewardIssuerAuthorized`, and composite `RewardBindingSafe`. Parallel surface — do **not** fold into `TraceSafe` / `EffectKind`. +3. **Adapters are untrusted.** `adapters/pcs/reward_binding_adapter.py` validates PCS JSON, checks integrity envelopes against operator-pinned trust keys, resolves artifacts, and emits typed `RewardBindingInput` plus a mapping report. Adapter acceptance is never predicate truth. +4. **New certificate schema only.** Emit `pf-core.reward_binding_certificate.v0`. Never mutate `pf-core.certificate.v0`. +5. **OVK / LabTrust** consume local fixtures and companion PR specs; sibling merges do not block PF-Core merge. + +## Consequences + +- Trusted modules added in later PRs: Lean `RewardBinding*.lean`, schemas `reward_binding_*.schema.json`, runtime `reward_binding.py` / `reward_binding_emit.py`, CLI `check-reward-binding` / `emit-reward-binding-certificate` / `replay-reward-binding`. +- Assumptions A11–A14 document digest identity, catalog fidelity, trust-root pins, and authority bit supply. +- Claim headline is binding under declared assumptions — not objective correctness or verifier accuracy. + +## Non-claims (forbidden upgrades) + +This ADR does not authorize claims of: objective correctness, verifier accuracy, environment fidelity, "safe reward", "verified objective", campaign orchestration, LLM judges, policy optimization, or deployment safety. + +## Rollback + +Revert this ADR and related docs only (PF-VA-00). No semantic code lands in VA-00. diff --git a/docs/pf-core/adrs/README.md b/docs/pf-core/adrs/README.md new file mode 100644 index 0000000..e488d16 --- /dev/null +++ b/docs/pf-core/adrs/README.md @@ -0,0 +1,35 @@ +# PF-Core Architecture Decision Records + +ADRs record irreversible or high-cost design choices for the trusted kernel and its adapters. + +## Convention + +| Field | Rule | +|-------|------| +| Location | `docs/pf-core/adrs/` | +| Naming | `NNN-short-kebab-title.md` (zero-padded) | +| Status | `Proposed` → `Accepted` → `Superseded` / `Deprecated` | +| Scope | One principal decision per ADR | +| Claims | Must respect `claim-boundary.md`; list non-claims explicitly | + +## Template + +```markdown +# ADR-NNN: Title + +- Status: Accepted +- Date: YYYY-MM-DD +- Baseline: , Lean 4.14.0, Python 3.12+ + +## Context +## Decision +## Consequences +## Non-claims +## Rollback +``` + +## Index + +| ADR | Title | Status | +|-----|-------|--------| +| [001](001-reward-binding-ownership.md) | Reward-binding ownership | Accepted | diff --git a/docs/pf-core/assumptions.md b/docs/pf-core/assumptions.md index 1e2b2d4..75017c3 100644 --- a/docs/pf-core/assumptions.md +++ b/docs/pf-core/assumptions.md @@ -41,3 +41,19 @@ When a handoff is marked allowed, the recipient principal is modeled in the same ## A10 — Clock and ordering Trace order matches emission order. PF-Core does not reorder events or prove temporal causality. + +## A11 — Digest identity (reward binding) + +Digest equality in the normalized reward-binding model is treated as cryptographic identity under SHA-256 collision resistance. Operators trust that distinct artifacts do not collide. Lean theorems take A11 as a hypothesis; they never prove collision resistance. + +## A12 — Artifact-root / catalog fidelity + +Trusted catalog and `--artifact-root` contents match declared digests supplied to the adapter. PF-Core checks equality of digests and closure flags; it does not prove the operator populated the root correctly. + +## A13 — Trust-root pins + +`trusted_keys` / trust-registry pins used by the untrusted PCS reward-binding adapter are organizationally correct. Key distribution is out of the Lean TCB. + +## A14 — Authority validity bits + +Authority records’ validity window and revocation bits are correctly supplied by the adapter after integrity verification. Lean predicates consume these bits as typed facts. diff --git a/docs/pf-core/claim-boundary.md b/docs/pf-core/claim-boundary.md index 77b8046..ed5ea79 100644 --- a/docs/pf-core/claim-boundary.md +++ b/docs/pf-core/claim-boundary.md @@ -67,8 +67,10 @@ Claims about PF-Core must use classification categories below. CI `audit-boundar - PF-Core checks that allowed events satisfy declared action predicates. - PF-Core validates runtime observations against pinned schemas. - PF-Core links runtime evidence to formal trace artifacts. +- Under declared schema, integrity, catalog, and trust-root assumptions, the reward-binding decider establishes that a declared reward references this trace, these verifier profiles and results, this environment profile, and an authorized issuer. - PF-Core does not prove semantic correctness of LLM outputs. - PF-Core does not prove external tools are honest. +- PF-Core does not prove objective correctness, verifier accuracy, or environment fidelity of rewards. ## Forbidden without T1–T4 backing @@ -82,6 +84,10 @@ Claims about PF-Core must use classification categories below. CI `audit-boundar - "PF-Core proves the runtime is secure" - "PF-Core proves non-interference for the whole platform" - "PF-Core proves all Provability Fabric claims" +- "safe reward", "verified objective", "reward proves correct objective" +- "PF-Core proves reward correctness" +- "PF-Core verifies the objective" +- "provably optimal reward" ## Mapping claims to evidence diff --git a/docs/pf-core/external-audit-brief.md b/docs/pf-core/external-audit-brief.md index e3db1c7..a8190cd 100644 --- a/docs/pf-core/external-audit-brief.md +++ b/docs/pf-core/external-audit-brief.md @@ -29,16 +29,17 @@ PF-Core is the **trusted kernel** for proof-carrying agentic action traces in th | `Assumption.lean`, `ClaimClassification.lean` | Assumption records, T1–T5 | | `Soundness.lean` | Decider soundness bundle | | `Examples.lean`, `Replay.lean` | Checked examples, golden Lean replay | +| `RewardBinding.lean`, `RewardBindingCertificate.lean`, `RewardBindingReplay.lean` | Reward-binding predicates, certificate, goldens | **Scan policy:** no `sorry`, `admit`, `axiom`, or `unsafe` in trusted Lean. ### Schemas (`pf-core/schemas/`) -v0 legacy + v1 primary: `principal`, `action`, `handoff`, `runtime_observation`, `event.v1`, etc. **v1-primary** is normative for trusted golden path (`schema-map.md`). +v0 legacy + v1 primary: `principal`, `action`, `handoff`, `runtime_observation`, `event.v1`, etc. **v1-primary** is normative for trusted golden path (`schema-map.md`). Reward binding: `reward_binding_input|decision|certificate.v0` (parallel; `certificate.v0` frozen). ### Validator (`pf-core/validator/pf_core/`) -`compile.py`, `deciders.py`, `hash_chain.py`, `schemas.py`, `cli.py`, `emitter.py`, `audit.py` +`compile.py`, `deciders.py`, `reward_binding.py`, `reward_binding_emit.py`, `hash_chain.py`, `schemas.py`, `cli.py`, `emitter.py`, `audit.py` ### Untrusted (explicitly excluded from TCB) @@ -126,7 +127,7 @@ From `pf-core/docs/threat-model.md`: | provability-fabric | `a567c8d` | | pcs-core | `v0.1.0` / `280bbea` | | post-incident-proofs | `d5f3051` | -| provability-fabric-core | **`pf-core-v0.6.0`** | +| provability-fabric-core | **`pf-core-v0.7.0`** | See `docs/pf-core/extraction-log.md` for file-by-file classification. diff --git a/docs/pf-core/mission.md b/docs/pf-core/mission.md index e6b00c1..c7d91ef 100644 --- a/docs/pf-core/mission.md +++ b/docs/pf-core/mission.md @@ -6,9 +6,9 @@ PF-Core is the minimal trusted kernel for proof-carrying agentic actions, contra PF-Core proves preservation properties over abstract traces. It does not prove that arbitrary LLM outputs are semantically correct, that external tools are honest, that operating systems are secure, that timestamps are reliable, that cryptographic hashes cannot collide except as an assumption, or that runtime instrumentation is complete unless separately attested. -**PF-Core proves:** Given explicitly modeled principals, capabilities, effects, resources, actions, decisions, events, and traces—and given stated assumptions about hash-chain integrity and schema conformance—whether each event in a trace satisfies tenant isolation, capability authorization, and effect allowlisting, and whether handoffs preserve authority within declared bounds. +**PF-Core proves:** Given explicitly modeled principals, capabilities, effects, resources, actions, decisions, events, and traces—and given stated assumptions about hash-chain integrity and schema conformance—whether each event in a trace satisfies tenant isolation, capability authorization, and effect allowlisting, and whether handoffs preserve authority within declared bounds. Separately, under declared schema, integrity, catalog, and trust-root assumptions, the reward-binding decider establishes that a declared reward references this trace, these verifier profiles and results, this environment profile, and an authorized issuer. -**PF-Core does not prove:** Correctness of external systems (LLMs, MCP servers, operating systems, networks), honesty of runtime emitters, completeness of policy catalogs, cryptographic collision resistance beyond stated hash assumptions, semantic equivalence between runtime observations and formal models, or end-to-end safety of an agent deployment without adapter contracts and organizational controls. +**PF-Core does not prove:** Correctness of external systems (LLMs, MCP servers, operating systems, networks), honesty of runtime emitters, completeness of policy catalogs, cryptographic collision resistance beyond stated hash assumptions, semantic equivalence between runtime observations and formal models, end-to-end safety of an agent deployment without adapter contracts and organizational controls, objective correctness of rewards, verifier accuracy, environment fidelity, or that a reward constitutes an endorsed objective under RL/judge criteria. ## Soundness split @@ -27,6 +27,7 @@ PF-Core proves preservation properties over abstract traces. It does not prove t | Contract algebra (sequence, projection) | Policy authoring UI | | Handoff authority preservation | Network sandbox enforcement | | Certificate structure over safe traces | Lean proof of external tool behavior | +| Reward-binding predicates on normalized input (parallel to TraceSafe) | RL/judge platforms, campaign orchestration, LLM judges | ## Design principles diff --git a/docs/pf-core/pf-va-00-baseline.md b/docs/pf-core/pf-va-00-baseline.md new file mode 100644 index 0000000..428830f --- /dev/null +++ b/docs/pf-core/pf-va-00-baseline.md @@ -0,0 +1,28 @@ +# PF-VA-00 Baseline Pins + +Recorded when the reward-binding claim-boundary work opened. No semantic extension in this packet. + +| Pin | Value | +|-----|-------| +| Base commit | `629984cb62b9d4b2281d36062a2979198ba61c82` | +| Lean toolchain | `leanprover/lean4:v4.14.0` (`pf-core/lean/lean-toolchain`) | +| Python | 3.12+ (CI); local may be 3.13 | +| Prior release | `pf-core/VERSION` = `0.6.0` | +| Trusted gate | `make pf-core-trusted` | + +## Windows note + +As documented in `phase7-status.md`, some Windows shells lack `lake` on PATH. Prefer `pf-core/scripts/pf-core-trusted.ps1` for schema/fixtures/audit/Python gates; defer full `lake build` to Linux CI when Lean is unavailable. This workspace has elan/`lake` available and should run Lean locally when possible. + +## Modules reserved for later PRs (not changed in VA-00) + +| Zone | Paths | +|------|-------| +| Trusted Lean | `PFCore/RewardBinding.lean`, `RewardBindingCertificate.lean`, `RewardBindingReplay.lean`; `Assumption.lean` A11–A14; `Soundness.lean` | +| Trusted schemas | `reward_binding_input.schema.json`, `reward_binding_decision.schema.json`, `reward_binding_certificate.schema.json` | +| Trusted runtime | `pf_core/reward_binding.py`, `pf_core/reward_binding_emit.py`; CLI registration | +| Untrusted | `adapters/pcs/schemas/`, `adapters/pcs/reward_binding_adapter.py`, fixtures | + +## Rollback + +Revert ADR + baseline + claim/trusted-boundary/audit phrase docs only. diff --git a/docs/pf-core/pf-va-08-release-inventory.md b/docs/pf-core/pf-va-08-release-inventory.md new file mode 100644 index 0000000..9ce0a04 --- /dev/null +++ b/docs/pf-core/pf-va-08-release-inventory.md @@ -0,0 +1,41 @@ +# PF-Core 0.7.0 Proof Inventory (Reward Binding) + +Release tag: `pf-core-v0.7.0` + +## Allowed claims + +- Under declared schema, integrity, catalog, and trust-root assumptions, the reward-binding decider establishes that a declared reward references this trace, these verifier profiles and results, this environment profile, and an authorized issuer. +- Existing trace-safety claims from 0.6.x remain unchanged. + +## Forbidden claims + +See `docs/pf-core/claim-boundary.md` (includes reward overclaim phrases). + +## TCB additions (0.7.0) + +| Artifact | Role | +|----------|------| +| `PFCore/RewardBinding.lean` | Model + predicates + `*D_sound` | +| `PFCore/RewardBindingCertificate.lean` | Certificate struct + soundness | +| `PFCore/RewardBindingReplay.lean` | Hand-encoded goldens | +| `reward_binding_*.schema.json` | Trusted JSON contracts | +| `pf_core/reward_binding.py` | Runtime decider | +| `pf_core/reward_binding_emit.py` | Emit / replay | + +## Explicitly outside TCB + +`adapters/pcs/` (mirrored PCS schemas, reward_binding_adapter, fixtures). + +## Reconstruct (clean checkout) + +```bash +git checkout pf-core-v0.7.0 +cd pf-core/lean && lake build +export PYTHONPATH=pf-core/validator:. +python -m pf_core.cli core schema-check --schemas pf-core/schemas +python pf-core/scripts/validate_examples.py +python -m pf_core.cli core audit-boundary --root . +pytest adapters/pcs/tests pf-core/validator/tests -q +``` + +Windows without `lake`: run Python gates; defer Lean to CI. diff --git a/docs/pf-core/pf-va-pr-artifacts/labtrust-reward-binding-pr-spec.md b/docs/pf-core/pf-va-pr-artifacts/labtrust-reward-binding-pr-spec.md new file mode 100644 index 0000000..a620e4d --- /dev/null +++ b/docs/pf-core/pf-va-pr-artifacts/labtrust-reward-binding-pr-spec.md @@ -0,0 +1,24 @@ +# PF-VA PR Spec — LabTrust: accept reward-binding fixture + +- Repo: LabTrust / pcs LabTrust emitters (sibling) +- Pin: `adapters/pcs/fixtures/labtrust-reward-binding/manifest.json` +- PF-Core tag: `pf-core-v0.7.0` + +## Goal + +LabTrust emitters produce PCS reward evidence envelopes that normalize through `adapters/pcs/reward_binding_adapter.py` to `pf-core.reward_binding_input.v0` with outcome `safe` on the vendored golden. + +## Acceptance + +```bash +export PYTHONPATH=pf-core/validator:. +python -m pf_core.cli core check-reward-binding \ + --trace adapters/pcs/fixtures/reward-binding/trace_valid.json \ + --reward-evidence adapters/pcs/fixtures/reward-binding/reward_valid.json \ + --artifact-root adapters/pcs/fixtures/reward-binding/artifacts \ + --trust-registry adapters/pcs/fixtures/reward-binding/trusted_keys.json +``` + +## Non-claims + +Fixture acceptance does not prove objective correctness or campaign policy. diff --git a/docs/pf-core/pf-va-pr-artifacts/ovk-profile-pin-pr-spec.md b/docs/pf-core/pf-va-pr-artifacts/ovk-profile-pin-pr-spec.md new file mode 100644 index 0000000..33359ae --- /dev/null +++ b/docs/pf-core/pf-va-pr-artifacts/ovk-profile-pin-pr-spec.md @@ -0,0 +1,20 @@ +# PF-VA PR Spec — OVK: pin verifier profile + +- Repo: OVK (sibling) +- Pin: `adapters/pcs/fixtures/ovk-verifier-profile/verifier_profile.json` +- PF-Core tag: `pf-core-v0.7.0` + +## Goal + +OVK documents / CI pins the `ovk-basic-v0` verifier profile config digest so reward-binding `VerifierConfigurationPinned` can reference an immutable profile. Checker invocation remains future work; this PR only pins the profile artifact. + +## Acceptance + +```bash +# Profile JSON validates against mirrored pcs.verifier_profile.v0 +python -c "import json; json.load(open('adapters/pcs/fixtures/ovk-verifier-profile/verifier_profile.json'))" +``` + +## Non-claims + +Profile pin does not prove verifier accuracy or false-acceptance metrics. diff --git a/docs/pf-core/pf-va-pr-artifacts/pcs-core-reward-schemas-pr-spec.md b/docs/pf-core/pf-va-pr-artifacts/pcs-core-reward-schemas-pr-spec.md new file mode 100644 index 0000000..31921d5 --- /dev/null +++ b/docs/pf-core/pf-va-pr-artifacts/pcs-core-reward-schemas-pr-spec.md @@ -0,0 +1,22 @@ +# PF-VA PR Spec — pcs-core: upstream mirrored reward schemas + +- Repo: pcs-core (sibling) +- Pin: local mirrors under `adapters/pcs/schemas/` (see `SCHEMA_PINS.json`) +- PF-Core tag: `pf-core-v0.7.0` + +## Goal + +Upstream the mirrored PCS schemas (`reward_evidence_envelope`, `verifier_profile`, `environment_profile`, `verification_result`, `authority_record`) so pcs-core remains the portable evidence standard. PF-Core must not invent a second portable layout under `pf-core/schemas/`. + +## Acceptance + +```bash +# In pcs-core after merge: schema ids match mirrors; digests documented. +# In PF-Core: adapters/pcs tests remain offline on vendored fixtures. +export PYTHONPATH=pf-core/validator:. +pytest adapters/pcs/tests pf-core/validator/tests/test_reward_binding.py -q +``` + +## Non-claims + +Schema upstream does not imply reward correctness or verifier accuracy. diff --git a/docs/pf-core/release-checklist.md b/docs/pf-core/release-checklist.md index c4024b1..0d4082d 100644 --- a/docs/pf-core/release-checklist.md +++ b/docs/pf-core/release-checklist.md @@ -7,16 +7,19 @@ Use this checklist when tagging a PF-Core release (`pf-core/VERSION` semver). - [ ] `make pf-core-trusted` passes locally - [ ] `make pf-core-e2e` passes locally (or `powershell -File pf-core/scripts/e2e-replay-gate.ps1`) - [ ] `adapters-ci` passes on `main` (pinned SHAs, catalog drift, policy correspondence) +- [ ] Reward-binding unit tests: `pytest pf-core/validator/tests/test_reward_binding.py` - [ ] `docs/pf-core/acceptance.md` Phase 6 rows are PASS - [ ] No `sorry` / `admit` / `axiom` / `unsafe` in `pf-core/lean/PFCore/` +- [ ] `docs/pf-core/pf-va-08-release-inventory.md` updated for this tag ## Version and schema policy - [ ] Bump `pf-core/VERSION` (semver: MAJOR for breaking schema/kernel changes, MINOR for Phase features, PATCH for fixes) - [ ] Update `pf-core/docs/schema-map.md` if schema status changes (v1-primary vs legacy) +- [ ] Never mutate `pf-core.certificate.v0`; reward binding uses `pf-core.reward_binding_certificate.v0` - [ ] Regenerate fixtures if examples changed: `python pf-core/scripts/gen_fixtures.py` - [ ] Update `docs/pf-core/extraction-log.md` pins if sibling repos change - +- [ ] Update `CHANGELOG.md` / `SECURITY.md` ## Tag and publish - [ ] Git tag: `pf-core-vX.Y.Z` pointing at the release commit diff --git a/docs/pf-core/trusted-boundary.md b/docs/pf-core/trusted-boundary.md index 9468ff4..b7687f0 100644 --- a/docs/pf-core/trusted-boundary.md +++ b/docs/pf-core/trusted-boundary.md @@ -30,8 +30,11 @@ This document partitions PF-Core into four zones. Artifacts in the **Trusted** z - `Composition.lean` — trace append safety - `Handoff.lean` — `HandoffSafe`, `handoff_does_not_expand_authority` - `Certificate.lean` — certificate structure and `certificate_safe_sound` +- `RewardBinding.lean` — normalized reward-binding model and predicates (parallel to TraceSafe) +- `RewardBindingCertificate.lean` — reward-binding certificate structure +- `RewardBindingReplay.lean` — hand-encoded golden vectors (no JSON I/O) - `RuntimeObservation.lean` — observation types -- `Assumption.lean` — numbered assumption records +- `Assumption.lean` — numbered assumption records (A1–A14) - `ClaimClassification.lean` — T1–T5 claim categories - `Soundness.lean` — decider soundness theorems - `Examples.lean` — checked examples @@ -53,7 +56,10 @@ This document partitions PF-Core into four zones. Artifacts in the **Trusted** z - `contract.schema.json` — `pf-core.contract.v0` - `handoff.schema.json` — `pf-core.handoff.v0` - `handoff.v1.schema.json` — `pf-core.handoff.v1` -- `certificate.schema.json` — `pf-core.certificate.v0` +- `certificate.schema.json` — `pf-core.certificate.v0` (**frozen**; do not mutate for reward binding) +- `reward_binding_input.schema.json` — `pf-core.reward_binding_input.v0` +- `reward_binding_decision.schema.json` — `pf-core.reward_binding_decision.v0` +- `reward_binding_certificate.schema.json` — `pf-core.reward_binding_certificate.v0` - `runtime_observation.schema.json` — `pf-core.runtime_observation.v0` - `runtime_observation.v1.schema.json` — `pf-core.runtime_observation.v1` - `claim_classification.schema.json` — `pf-core.claim_classification.v0` @@ -72,14 +78,17 @@ Documented in `pf-core/docs/certificate-semantics.md`: - `compile.py` — deterministic `compile-observation` - `hash_chain.py` — `event_hash` / `previous_event_hash` / `trace_hash` validation - `deciders.py` — executable safety deciders mirroring Lean +- `reward_binding.py` — reward-binding predicates and multi-outcome decider +- `reward_binding_emit.py` — reward-binding certificate emit / replay - `contracts.py` — contract satisfaction deciders - `schemas.py` — JSON Schema loading and validation -- `cli.py` — `pf core` commands +- `cli.py` — `pf core` commands (incl. reward-binding check/emit/replay) - `emitter.py` — full adapter artifact emission - `audit_line.py` — `audit.jsonl` line format - `event_kind.py` — v1 event kind parsing - `audit.py` — trusted-boundary audit for CI - `errors.py` — typed compiler/validator errors +- `bundle_verify.py` — five-file bundle verifier ### Example fixtures (`pf-core/examples/`) @@ -96,6 +105,8 @@ Documented in `pf-core/docs/certificate-semantics.md`: - `docs/pf-core/tutorial.md` - `docs/pf-core/ecosystem-inventory.md` - `docs/pf-core/acceptance.md` +- `docs/pf-core/adrs/` — architecture decision records (ADR-001 reward-binding ownership) +- `docs/pf-core/pf-va-00-baseline.md` — reward-binding baseline pins - `pf-core/docs/formal-model.md` - `pf-core/docs/threat-model.md` - `pf-core/docs/examples.md` @@ -125,7 +136,7 @@ CI fails on catalog drift: `export_catalog.py` output must match Lean (`test_cat ### Untrusted adapters (`adapters/`) - `adapters/provability-fabric/` — sidecar normalize, catalog export, Policy.lean reference -- `adapters/pcs/` — LabTrust replay, PCS hash vector parity tests +- `adapters/pcs/` — LabTrust replay, PCS hash vector parity tests, reward-binding adapter + mirrored PCS schemas (not in TCB) - `adapters/post_incident_proofs/` — forensic cross-check documentation ### Lean imports (allowlisted) @@ -150,10 +161,13 @@ PF-Core trusted Lean files import only Mathlib-free standard library modules and | `Composition.lean` | `Trace`, `Contract` | | `StatefulContract.lean` | `Contract` | | `Certificate.lean` | `Trace` | +| `RewardBinding.lean` | `Basic` | +| `RewardBindingCertificate.lean` | `RewardBinding` | +| `RewardBindingReplay.lean` | `RewardBinding` | | `RuntimeObservation.lean` | `Basic`, `Principal`, `Capability`, `Effect`, `Decision`, `Event` | | `Assumption.lean` | `Basic` | | `ClaimClassification.lean` | `Basic` | -| `Soundness.lean` | `Principal` … `Handoff` (decider soundness bundle) | +| `Soundness.lean` | `Principal` … `Handoff`, `RewardBinding` (decider soundness bundle) | | `Replay.lean` | `Examples`, `Trace` | Toolchain: `pf-core/lean/lean-toolchain` (via elan). `set_option autoImplicit false` in `lakefile.lean`. @@ -184,3 +198,5 @@ Toolchain: `pf-core/lean/lean-toolchain` (via elan). `set_option autoImplicit fa - Lab release gates or MCP audits cover all attack surfaces - Certificate acceptance by downstream verifiers without their own policy - Completeness of effect/capability enumeration vs production tools +- Reward binding implies objective correctness, verifier accuracy, or environment fidelity +- Adapter mapping or trust-key distribution correctness beyond A11–A14 diff --git a/pf-core/VERSION b/pf-core/VERSION index a918a2a..faef31a 100644 --- a/pf-core/VERSION +++ b/pf-core/VERSION @@ -1 +1 @@ -0.6.0 +0.7.0 diff --git a/pf-core/docs/certificate-semantics.md b/pf-core/docs/certificate-semantics.md index 8173744..f923143 100644 --- a/pf-core/docs/certificate-semantics.md +++ b/pf-core/docs/certificate-semantics.md @@ -58,4 +58,22 @@ Wire certificates (`pf-core.certificate.v0`) include `schema_version`, `checker_ ## Non-claims - Certificate does not prove external execution or PCS bundle validity. -- Forbidden certificate text: "This agent is safe", "This tool is secure", "This workflow is verified". +- Certificate does not prove OS enforcement of denials. + +## Reward-binding certificates (`pf-core.reward_binding_certificate.v0`) + +Independent of `pf-core.certificate.v0` (frozen). Fields bind digests, issuer, authority ref, per-predicate results, `binding_safe`, assumptions (incl. A11–A14), checker pins, proof ref, source commit, and integrity envelope. Only outcome `safe` may set `binding_safe: true`. + +```bash +pf core emit-reward-binding-certificate \ + --input pf-core/examples/valid/reward_binding_safe_input.json \ + --out /tmp/reward_binding_certificate.json + +pf core replay-reward-binding \ + --certificate /tmp/reward_binding_certificate.json \ + --input pf-core/examples/valid/reward_binding_safe_input.json +``` + +Lean proves `reward_binding_certificate_safe_sound`. Replay re-runs the decider and checks the integrity envelope (fail closed on tamper). + +Forbidden certificate text (emitters): "This agent is safe", "This tool is secure", "This workflow is verified", plus reward overclaim phrases listed in `reward_binding_emit.py`. diff --git a/pf-core/docs/schema-map.md b/pf-core/docs/schema-map.md index 1ea50ed..d9cfefa 100644 --- a/pf-core/docs/schema-map.md +++ b/pf-core/docs/schema-map.md @@ -29,7 +29,10 @@ Inventory of pinned JSON schemas. **v1-primary** artifacts are normative for the |--------|---------|--------| | `event.schema.json` | `pf-core.event.v0` | legacy reference only | | `trace.schema.json` | `pf-core.trace.v0` | active — ordered `events[]` (v1 items) + `trace_hash` | -| `certificate.schema.json` | `pf-core.certificate.v0` | active — binds `trace_hash` + `contract_hash` | +| `certificate.schema.json` | `pf-core.certificate.v0` | active — binds `trace_hash` + `contract_hash` (**frozen**) | +| `reward_binding_input.schema.json` | `pf-core.reward_binding_input.v0` | active — normalized reward-binding input | +| `reward_binding_decision.schema.json` | `pf-core.reward_binding_decision.v0` | active — multi-outcome decision | +| `reward_binding_certificate.schema.json` | `pf-core.reward_binding_certificate.v0` | active — reward-binding evidence pointer | ## Policy and adapter diff --git a/pf-core/docs/theorem-map.md b/pf-core/docs/theorem-map.md index f18e853..5ff56b2 100644 --- a/pf-core/docs/theorem-map.md +++ b/pf-core/docs/theorem-map.md @@ -59,10 +59,22 @@ One-page index of proved theorems, what they justify, and what they do not. ## Soundness hub (`Soundness.lean`) -Aggregates decider soundness theorems for principals, capabilities, effects, actions, events, traces, and handoffs. Does not prove adapter catalogs, hash chains, or external honesty. +Aggregates decider soundness theorems for principals, capabilities, effects, actions, events, traces, handoffs, and reward-binding predicates. Does not prove adapter catalogs, hash chains, or external honesty. ## Certificate (`Certificate.lean`) | Theorem | Justifies | Does not imply | |---------|-----------|----------------| | `certificate_safe_sound` | Certificate `safe` bit matches `TraceSafe` | Downstream acceptance without verifier policy | + +## Reward binding (`RewardBinding.lean`, `RewardBindingCertificate.lean`) + +| Theorem | Justifies | Does not imply | +|---------|-----------|----------------| +| `rewardBoundToTraceD_sound` | Trace digest equality decider | Objective reward correctness | +| `verifierConfigurationPinnedD_sound` | Verifier profile pin decider | Verifier accuracy | +| `evidenceChainClosedD_sound` | Artifact closure decider | Catalog completeness beyond A12 | +| `rewardIssuerAuthorizedD_sound` | Issuer/authority window decider | Trust-root distribution (A13) | +| `rewardBindingSafeD_sound` / `reward_binding_safe_sound` | Composite binding safety | RL/judge objective endorsement | +| `reward_binding_certificate_safe_sound` | Certificate `bindingSafe` matches composite | Downstream acceptance | +| `evidence_chain_refs_extend_preserves_closed` | Adding refs cannot open a closed chain under fixed flags | Flag flips / revocation monotonicity | diff --git a/pf-core/docs/threat-model.md b/pf-core/docs/threat-model.md index d661198..27a9157 100644 --- a/pf-core/docs/threat-model.md +++ b/pf-core/docs/threat-model.md @@ -18,14 +18,20 @@ | Schema injection | `additionalProperties: false` | T2 | | Ambiguous effect mapping | `AmbiguousMapping` error | T4 | | Hash tampering | `InvalidHash` chain check | T4 | +| Substituted reward trace | `RewardBoundToTrace` | T1 + T4 | +| Verifier config swap | `VerifierConfigurationPinned` | T1 + T4 | +| Broken artifact chain | `EvidenceChainClosed` | T1 + T4 | +| Revoked / wrong-tenant issuer | `RewardIssuerAuthorized` | T1 + T4 | ## Out of scope attacks - OS sandbox escape - LLM prompt injection leading to unlogged actions -- Collisions in SHA-256 (assumed in A2) +- Collisions in SHA-256 (assumed in A2 / A11) - Recipient misuse after safe handoff - Forged organizational tenant labels (A3) +- Reward objective gaming / verifier false-acceptance (external) +- Malicious trust-root distribution (A13 organizational) ## MCP sidecar diff --git a/pf-core/examples/invalid/reward_binding_revoked_issuer.json b/pf-core/examples/invalid/reward_binding_revoked_issuer.json new file mode 100644 index 0000000..2335586 --- /dev/null +++ b/pf-core/examples/invalid/reward_binding_revoked_issuer.json @@ -0,0 +1,64 @@ +{ + "artifact_closure": { + "classes_ok": true, + "closed": true, + "integrity_ok": true, + "refs": [ + { + "class": "environment_profile", + "digest": "cccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccc", + "id": "env-1" + } + ] + }, + "authority": { + "authority_ref": "auth-1", + "authorized_issuers": [ + { + "principal_id": "issuer-1", + "tenant_id": "tenant-lab" + } + ], + "claim_class": "reward_binding", + "digest": "eeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeee", + "environment_digest": "cccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccc", + "revoked": true, + "valid_from": 100, + "valid_until": 200 + }, + "environment_profile_digest": "cccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccc", + "expected_error": "RewardIssuerAuthorized", + "issuer": { + "principal_id": "issuer-1", + "tenant_id": "tenant-lab" + }, + "lifecycle": { + "issued_at": 150, + "required_claim_class": "reward_binding", + "stale": false + }, + "must_fail_at": "reward_binding_decider", + "reward_evidence_digest": "eeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeee", + "reward_trace_digest": "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa", + "schema_version": "pf-core.reward_binding_input.v0", + "trace_digest": "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa", + "verification_bindings": [ + { + "config_digest": "dddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddd", + "profile_id": "vp-1", + "result_digest": "bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb" + } + ], + "verification_result_digests": [ + "bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb" + ], + "verifier_profile_digests": [ + "dddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddd" + ], + "verifier_profiles": [ + { + "config_digest": "dddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddd", + "profile_id": "vp-1" + } + ] +} diff --git a/pf-core/examples/invalid/reward_binding_trace_mismatch.json b/pf-core/examples/invalid/reward_binding_trace_mismatch.json new file mode 100644 index 0000000..367e08a --- /dev/null +++ b/pf-core/examples/invalid/reward_binding_trace_mismatch.json @@ -0,0 +1,64 @@ +{ + "artifact_closure": { + "classes_ok": true, + "closed": true, + "integrity_ok": true, + "refs": [ + { + "class": "environment_profile", + "digest": "cccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccc", + "id": "env-1" + } + ] + }, + "authority": { + "authority_ref": "auth-1", + "authorized_issuers": [ + { + "principal_id": "issuer-1", + "tenant_id": "tenant-lab" + } + ], + "claim_class": "reward_binding", + "digest": "eeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeee", + "environment_digest": "cccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccc", + "revoked": false, + "valid_from": 100, + "valid_until": 200 + }, + "environment_profile_digest": "cccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccc", + "expected_error": "RewardBoundToTrace", + "issuer": { + "principal_id": "issuer-1", + "tenant_id": "tenant-lab" + }, + "lifecycle": { + "issued_at": 150, + "required_claim_class": "reward_binding", + "stale": false + }, + "must_fail_at": "reward_binding_decider", + "reward_evidence_digest": "eeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeee", + "reward_trace_digest": "bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb", + "schema_version": "pf-core.reward_binding_input.v0", + "trace_digest": "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa", + "verification_bindings": [ + { + "config_digest": "dddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddd", + "profile_id": "vp-1", + "result_digest": "bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb" + } + ], + "verification_result_digests": [ + "bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb" + ], + "verifier_profile_digests": [ + "dddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddd" + ], + "verifier_profiles": [ + { + "config_digest": "dddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddd", + "profile_id": "vp-1" + } + ] +} diff --git a/pf-core/examples/valid/reward_binding_safe_input.json b/pf-core/examples/valid/reward_binding_safe_input.json new file mode 100644 index 0000000..0842b6f --- /dev/null +++ b/pf-core/examples/valid/reward_binding_safe_input.json @@ -0,0 +1,62 @@ +{ + "artifact_closure": { + "classes_ok": true, + "closed": true, + "integrity_ok": true, + "refs": [ + { + "class": "environment_profile", + "digest": "cccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccc", + "id": "env-1" + } + ] + }, + "authority": { + "authority_ref": "auth-1", + "authorized_issuers": [ + { + "principal_id": "issuer-1", + "tenant_id": "tenant-lab" + } + ], + "claim_class": "reward_binding", + "digest": "eeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeee", + "environment_digest": "cccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccc", + "revoked": false, + "valid_from": 100, + "valid_until": 200 + }, + "environment_profile_digest": "cccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccc", + "issuer": { + "principal_id": "issuer-1", + "tenant_id": "tenant-lab" + }, + "lifecycle": { + "issued_at": 150, + "required_claim_class": "reward_binding", + "stale": false + }, + "reward_evidence_digest": "eeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeee", + "reward_trace_digest": "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa", + "schema_version": "pf-core.reward_binding_input.v0", + "trace_digest": "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa", + "verification_bindings": [ + { + "config_digest": "dddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddd", + "profile_id": "vp-1", + "result_digest": "bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb" + } + ], + "verification_result_digests": [ + "bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb" + ], + "verifier_profile_digests": [ + "dddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddd" + ], + "verifier_profiles": [ + { + "config_digest": "dddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddd", + "profile_id": "vp-1" + } + ] +} diff --git a/pf-core/lean/PFCore.lean b/pf-core/lean/PFCore.lean index b9b6f2d..d67721c 100644 --- a/pf-core/lean/PFCore.lean +++ b/pf-core/lean/PFCore.lean @@ -15,6 +15,9 @@ import PFCore.Composition import PFCore.Handoff import PFCore.Replay import PFCore.Certificate +import PFCore.RewardBinding +import PFCore.RewardBindingCertificate +import PFCore.RewardBindingReplay import PFCore.RuntimeObservation import PFCore.Assumption import PFCore.ClaimClassification diff --git a/pf-core/lean/PFCore/Assumption.lean b/pf-core/lean/PFCore/Assumption.lean index 16504b1..e8d476c 100644 --- a/pf-core/lean/PFCore/Assumption.lean +++ b/pf-core/lean/PFCore/Assumption.lean @@ -4,14 +4,14 @@ import PFCore.Basic # PFCore.Assumption Trusted assumption identifiers referenced by certificates and boundary docs. -Full prose in `docs/pf-core/assumptions.md` (A1–A10). +Full prose in `docs/pf-core/assumptions.md` (A1–A14). -/ namespace PFCore /-- Numbered assumptions from `docs/pf-core/assumptions.md`. -/ inductive AssumptionId where - | A1 | A2 | A3 | A4 | A5 | A6 | A7 | A8 | A9 | A10 + | A1 | A2 | A3 | A4 | A5 | A6 | A7 | A8 | A9 | A10 | A11 | A12 | A13 | A14 deriving Repr, DecidableEq, Inhabited structure Assumption where @@ -49,8 +49,21 @@ def assumptionA9 : Assumption := def assumptionA10 : Assumption := { id := .A10, description := "Trace order matches emission order; no temporal causality proof" } +def assumptionA11 : Assumption := + { id := .A11, description := "Digest equality is cryptographic identity under SHA-256 collision resistance (operator-trusted)" } + +def assumptionA12 : Assumption := + { id := .A12, description := "Trusted catalog / artifact-root contents match declared digests (operator-supplied)" } + +def assumptionA13 : Assumption := + { id := .A13, description := "Trust-root / trusted_keys pins used by the adapter are organizationally correct" } + +def assumptionA14 : Assumption := + { id := .A14, description := "Authority records validity/revocation bits are correctly supplied by the adapter after integrity check" } + def allAssumptions : List Assumption := [assumptionA1, assumptionA2, assumptionA3, assumptionA4, assumptionA5, - assumptionA6, assumptionA7, assumptionA8, assumptionA9, assumptionA10] + assumptionA6, assumptionA7, assumptionA8, assumptionA9, assumptionA10, + assumptionA11, assumptionA12, assumptionA13, assumptionA14] end PFCore diff --git a/pf-core/lean/PFCore/RewardBinding.lean b/pf-core/lean/PFCore/RewardBinding.lean new file mode 100644 index 0000000..479f6f3 --- /dev/null +++ b/pf-core/lean/PFCore/RewardBinding.lean @@ -0,0 +1,307 @@ +import PFCore.Basic + +/-! +# PFCore.RewardBinding + +Normalized reward-binding model and predicates. Parallel to `TraceSafe` / +`EffectKind` — not folded into the trace kernel. +-/ + +namespace PFCore + +structure Issuer where + principalId : String + tenantId : String + deriving Repr, DecidableEq, BEq, Inhabited + +structure VerifierRef where + profileId : String + configDigest : Hash + deriving Repr, DecidableEq, BEq, Inhabited + +structure VerificationBinding where + resultDigest : Hash + profileId : String + configDigest : Hash + deriving Repr, DecidableEq, BEq, Inhabited + +structure ArtifactRef where + id : String + className : String + digest : Hash + deriving Repr, DecidableEq, BEq, Inhabited + +structure ArtifactClosure where + closed : Bool + integrityOk : Bool + classesOk : Bool + refs : List ArtifactRef + deriving Repr, DecidableEq, Inhabited + +structure AuthorityRef where + authorityId : String + digest : Hash + validFrom : Nat + validUntil : Nat + revoked : Bool + claimClass : String + environmentDigest : Hash + authorizedIssuers : List Issuer + deriving Repr, DecidableEq, Inhabited + +structure Lifecycle where + issuedAt : Nat + stale : Bool + requiredClaimClass : String + deriving Repr, DecidableEq, Inhabited + +structure RewardBindingInput where + traceDigest : Hash + rewardTraceDigest : Hash + rewardEvidenceDigest : Hash + environmentProfileDigest : Hash + verifierProfileDigests : List Hash + verificationResultDigests : List Hash + verifierProfiles : List VerifierRef + verificationBindings : List VerificationBinding + issuer : Issuer + authority : AuthorityRef + lifecycle : Lifecycle + artifactClosure : ArtifactClosure + deriving Repr, Inhabited + +/-- Reward envelope trace digest equals supplied PF trace digest. -/ +def RewardBoundToTrace (i : RewardBindingInput) : Prop := + i.rewardTraceDigest = i.traceDigest + +def rewardBoundToTraceD (i : RewardBindingInput) : Bool := + decide (i.rewardTraceDigest = i.traceDigest) + +/-- +## Plain-English meaning +`rewardBoundToTraceD` is true exactly when the reward's bound trace digest equals the PF trace digest. + +## Trusted use +First conjunct of reward-binding safety under A11. + +## Does not imply +Objective correctness of the reward or honesty of the evidence emitter. +-/ +theorem rewardBoundToTraceD_sound (i : RewardBindingInput) : + rewardBoundToTraceD i = true ↔ RewardBoundToTrace i := by + simp [rewardBoundToTraceD, RewardBoundToTrace] + +def profileMatchesD (profiles : List VerifierRef) (profileId : String) (digest : Hash) : Bool := + profiles.any fun p => decide (p.profileId = profileId) && decide (p.configDigest = digest) + +def ProfileMatches (profiles : List VerifierRef) (profileId : String) (digest : Hash) : Prop := + ∃ p, p ∈ profiles ∧ p.profileId = profileId ∧ p.configDigest = digest + +/-- +## Plain-English meaning +`profileMatchesD` finds a declared verifier profile with matching id and config digest. + +## Trusted use +Helper for verifier configuration pinning. + +## Does not imply +The named verifier is accurate or complete. +-/ +theorem profileMatchesD_sound (profiles : List VerifierRef) (profileId : String) (digest : Hash) : + profileMatchesD profiles profileId digest = true ↔ ProfileMatches profiles profileId digest := by + simp [profileMatchesD, ProfileMatches, List.any_eq_true, Bool.and_eq_true] + +def bindingPinnedD (profiles : List VerifierRef) (b : VerificationBinding) : Bool := + profileMatchesD profiles b.profileId b.configDigest + +def BindingPinned (profiles : List VerifierRef) (b : VerificationBinding) : Prop := + ProfileMatches profiles b.profileId b.configDigest + +/-- +## Plain-English meaning +A verification binding is pinned when its profile id and config digest match a declared profile. + +## Trusted use +Per-binding helper for `VerifierConfigurationPinned`. + +## Does not imply +Verifier accuracy. +-/ +theorem bindingPinnedD_sound (profiles : List VerifierRef) (b : VerificationBinding) : + bindingPinnedD profiles b = true ↔ BindingPinned profiles b := by + simp [bindingPinnedD, BindingPinned, profileMatchesD_sound] + +def sortedResultDigests (bindings : List VerificationBinding) : List Hash := + (bindings.map (·.resultDigest)).mergeSort (· ≤ ·) + +def AllBindingsPinned (profiles : List VerifierRef) (bindings : List VerificationBinding) : Prop := + ∀ b ∈ bindings, BindingPinned profiles b + +def allBindingsPinnedD (profiles : List VerifierRef) (bindings : List VerificationBinding) : Bool := + bindings.all (bindingPinnedD profiles) + +/-- +## Plain-English meaning +`allBindingsPinnedD` holds when every verification binding is pinned. + +## Trusted use +Helper for verifier configuration pinning. + +## Does not imply +Verifier accuracy. +-/ +theorem allBindingsPinnedD_sound (profiles : List VerifierRef) (bindings : List VerificationBinding) : + allBindingsPinnedD profiles bindings = true ↔ AllBindingsPinned profiles bindings := by + simp [allBindingsPinnedD, AllBindingsPinned, List.all_eq_true, bindingPinnedD_sound] + +/-- Every verification result points at a declared immutable verifier profile + config digest. -/ +def VerifierConfigurationPinned (i : RewardBindingInput) : Prop := + i.verificationBindings ≠ [] ∧ + i.verifierProfiles ≠ [] ∧ + AllBindingsPinned i.verifierProfiles i.verificationBindings ∧ + sortedResultDigests i.verificationBindings = i.verificationResultDigests.mergeSort (· ≤ ·) + +def verifierConfigurationPinnedD (i : RewardBindingInput) : Bool := + decide (i.verificationBindings ≠ []) && + decide (i.verifierProfiles ≠ []) && + allBindingsPinnedD i.verifierProfiles i.verificationBindings && + decide ( + sortedResultDigests i.verificationBindings = + i.verificationResultDigests.mergeSort (· ≤ ·)) + +/-- +## Plain-English meaning +`verifierConfigurationPinnedD` requires non-empty bindings/profiles, each binding pinned to a +declared profile digest, and sorted result digest lists agreeing. + +## Trusted use +Second conjunct of reward-binding safety. + +## Does not imply +Verifier accuracy, rubric quality, or suite completeness. +-/ +theorem verifierConfigurationPinnedD_sound (i : RewardBindingInput) : + verifierConfigurationPinnedD i = true ↔ VerifierConfigurationPinned i := by + constructor <;> simp [verifierConfigurationPinnedD, VerifierConfigurationPinned, + Bool.and_eq_true, allBindingsPinnedD_sound, sortedResultDigests, and_assoc] + +/-- Mandatory refs resolve to integrity-checked artifacts of expected class. -/ +def EvidenceChainClosed (i : RewardBindingInput) : Prop := + i.artifactClosure.closed = true ∧ + i.artifactClosure.integrityOk = true ∧ + i.artifactClosure.classesOk = true ∧ + i.artifactClosure.refs ≠ [] + +def evidenceChainClosedD (i : RewardBindingInput) : Bool := + decide (i.artifactClosure.closed = true) && + decide (i.artifactClosure.integrityOk = true) && + decide (i.artifactClosure.classesOk = true) && + decide (i.artifactClosure.refs ≠ []) + +/-- +## Plain-English meaning +`evidenceChainClosedD` is true when closure flags are set and at least one ref is present. + +## Trusted use +Third conjunct of reward-binding safety under A12. + +## Does not imply +Catalog contents are complete beyond operator-supplied roots. +-/ +theorem evidenceChainClosedD_sound (i : RewardBindingInput) : + evidenceChainClosedD i = true ↔ EvidenceChainClosed i := by + constructor <;> simp [evidenceChainClosedD, EvidenceChainClosed, Bool.and_eq_true, and_assoc] + +def IssuerAuthorized (issuer : Issuer) (xs : List Issuer) : Prop := + ∃ x, x ∈ xs ∧ x = issuer + +def issuerAuthorizedD (issuer : Issuer) (xs : List Issuer) : Bool := + xs.any fun x => decide (x = issuer) + +/-- +## Plain-English meaning +`issuerAuthorizedD` is list membership of the issuer in the authority allowlist. + +## Trusted use +Helper for `RewardIssuerAuthorized`. + +## Does not imply +Organizational identity correctness. +-/ +theorem issuerAuthorizedD_sound (issuer : Issuer) (xs : List Issuer) : + issuerAuthorizedD issuer xs = true ↔ IssuerAuthorized issuer xs := by + simp [issuerAuthorizedD, IssuerAuthorized, List.any_eq_true] + +/-- Issuer permitted by pinned authority for claim class + environment within validity window. -/ +def RewardIssuerAuthorized (i : RewardBindingInput) : Prop := + i.authority.revoked = false ∧ + i.lifecycle.stale = false ∧ + i.authority.validFrom ≤ i.lifecycle.issuedAt ∧ + i.lifecycle.issuedAt ≤ i.authority.validUntil ∧ + i.authority.claimClass = i.lifecycle.requiredClaimClass ∧ + i.authority.environmentDigest = i.environmentProfileDigest ∧ + IssuerAuthorized i.issuer i.authority.authorizedIssuers + +def rewardIssuerAuthorizedD (i : RewardBindingInput) : Bool := + decide (i.authority.revoked = false) && + decide (i.lifecycle.stale = false) && + decide (i.authority.validFrom ≤ i.lifecycle.issuedAt) && + decide (i.lifecycle.issuedAt ≤ i.authority.validUntil) && + decide (i.authority.claimClass = i.lifecycle.requiredClaimClass) && + decide (i.authority.environmentDigest = i.environmentProfileDigest) && + issuerAuthorizedD i.issuer i.authority.authorizedIssuers + +/-- +## Plain-English meaning +`rewardIssuerAuthorizedD` checks revocation, staleness, validity window, claim class, +environment digest, and issuer membership in the authority allowlist. + +## Trusted use +Fourth conjunct of reward-binding safety under A14. + +## Does not imply +Authority records were correctly distributed; that is A13/A14 organizational. +-/ +theorem rewardIssuerAuthorizedD_sound (i : RewardBindingInput) : + rewardIssuerAuthorizedD i = true ↔ RewardIssuerAuthorized i := by + constructor <;> simp [rewardIssuerAuthorizedD, RewardIssuerAuthorized, Bool.and_eq_true, + issuerAuthorizedD_sound, and_assoc] + +/-- Composite: all four predicates. -/ +def RewardBindingSafe (i : RewardBindingInput) : Prop := + RewardBoundToTrace i ∧ + VerifierConfigurationPinned i ∧ + EvidenceChainClosed i ∧ + RewardIssuerAuthorized i + +def rewardBindingSafeD (i : RewardBindingInput) : Bool := + rewardBoundToTraceD i && + verifierConfigurationPinnedD i && + evidenceChainClosedD i && + rewardIssuerAuthorizedD i + +/-- +## Plain-English meaning +`rewardBindingSafeD` is true exactly when all four reward-binding predicates hold. + +## Trusted use +Runtime `check-reward-binding` / certificate emission gate. + +## Does not imply +Objective correctness, verifier accuracy, environment fidelity, or RL/judge objective endorsement. +-/ +theorem rewardBindingSafeD_sound (i : RewardBindingInput) : + rewardBindingSafeD i = true ↔ RewardBindingSafe i := by + constructor <;> simp [rewardBindingSafeD, RewardBindingSafe, Bool.and_eq_true, + rewardBoundToTraceD_sound, verifierConfigurationPinnedD_sound, + evidenceChainClosedD_sound, rewardIssuerAuthorizedD_sound, and_assoc] + +/-- Closing more refs cannot flip closed→open when closure flags already hold. -/ +theorem evidence_chain_refs_extend_preserves_closed + (closedFlag integrityOk classesOk : Bool) (refs : List ArtifactRef) (extra : ArtifactRef) + (hclosed : closedFlag = true) (hint : integrityOk = true) (hclass : classesOk = true) + (_hrefs : refs ≠ []) : + closedFlag = true ∧ integrityOk = true ∧ classesOk = true ∧ (extra :: refs) ≠ [] := by + exact ⟨hclosed, hint, hclass, by intro h; cases h⟩ + +end PFCore diff --git a/pf-core/lean/PFCore/RewardBindingCertificate.lean b/pf-core/lean/PFCore/RewardBindingCertificate.lean new file mode 100644 index 0000000..8ffd9d5 --- /dev/null +++ b/pf-core/lean/PFCore/RewardBindingCertificate.lean @@ -0,0 +1,67 @@ +import PFCore.RewardBinding + +/-! +# PFCore.RewardBindingCertificate + +Certificate structure for `pf-core.reward_binding_certificate.v0`. +Independent of `PFCore.Certificate` / `pf-core.certificate.v0`. +-/ + +namespace PFCore + +structure RewardBindingCertificate where + certificateId : String + traceDigest : Hash + rewardEvidenceDigest : Hash + environmentProfileDigest : Hash + bindingSafe : Bool + proofRef : String + checker : String + assumptions : List String + deriving Repr, DecidableEq, Inhabited + +def rewardBindingCertificateFromInput (i : RewardBindingInput) (certId : String) : + RewardBindingCertificate := + { certificateId := certId + traceDigest := i.traceDigest + rewardEvidenceDigest := i.rewardEvidenceDigest + environmentProfileDigest := i.environmentProfileDigest + bindingSafe := rewardBindingSafeD i + proofRef := "pf-core/lean/PFCore/RewardBinding.lean" + checker := "lean4" + assumptions := ["A11", "A12", "A13", "A14"] } + +/-- +## Plain-English meaning +Certificate `bindingSafe` matches the composite reward-binding decider. + +## Trusted use +`emit-reward-binding-certificate` output semantics. + +## Does not imply +Downstream acceptance, objective correctness, or verifier accuracy. +-/ +theorem reward_binding_certificate_safe_sound + (i : RewardBindingInput) (certId : String) + (c : RewardBindingCertificate) + (hc : c = rewardBindingCertificateFromInput i certId) : + c.bindingSafe = true ↔ RewardBindingSafe i := by + subst hc + simp [rewardBindingCertificateFromInput, rewardBindingSafeD_sound] + +/-- +## Plain-English meaning +Reward-binding certificates summarize predicate results under A11–A14; they do not prove +reward correctness. + +## Trusted use +Claim-boundary guard for organizational evidence pointers. + +## Does not imply +RL/judge objective endorsement or production reward safety. +-/ +theorem reward_binding_certificate_claim_bounded + (_c : RewardBindingCertificate) (_hs : _c.bindingSafe = true) : True := + trivial + +end PFCore diff --git a/pf-core/lean/PFCore/RewardBindingReplay.lean b/pf-core/lean/PFCore/RewardBindingReplay.lean new file mode 100644 index 0000000..3b30ec5 --- /dev/null +++ b/pf-core/lean/PFCore/RewardBindingReplay.lean @@ -0,0 +1,72 @@ +import PFCore.RewardBinding + +/-! +# PFCore.RewardBindingReplay + +Hand-encoded golden vectors (no JSON I/O). Must agree with Python fixtures +`pf-core/examples/valid/reward_binding_safe_input.json`. +-/ + +namespace PFCore + +private def d0 : Hash := + "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa" +private def d1 : Hash := + "bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb" +private def d2 : Hash := + "cccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccc" +private def d3 : Hash := + "dddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddd" +private def d4 : Hash := + "eeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeee" + +private def goldenIssuer : Issuer := + { principalId := "issuer-1", tenantId := "tenant-lab" } + +private def goldenAuthority : AuthorityRef := + { authorityId := "auth-1" + digest := d4 + validFrom := 100 + validUntil := 200 + revoked := false + claimClass := "reward_binding" + environmentDigest := d2 + authorizedIssuers := [goldenIssuer] } + +private def goldenProfiles : List VerifierRef := + [{ profileId := "vp-1", configDigest := d3 }] + +private def goldenBindings : List VerificationBinding := + [{ resultDigest := d1, profileId := "vp-1", configDigest := d3 }] + +private def goldenClosure : ArtifactClosure := + { closed := true + integrityOk := true + classesOk := true + refs := [{ id := "env-1", className := "environment_profile", digest := d2 }] } + +def goldenRewardBindingSafe : RewardBindingInput := + { traceDigest := d0 + rewardTraceDigest := d0 + rewardEvidenceDigest := d4 + environmentProfileDigest := d2 + verifierProfileDigests := [d3] + verificationResultDigests := [d1] + verifierProfiles := goldenProfiles + verificationBindings := goldenBindings + issuer := goldenIssuer + authority := goldenAuthority + lifecycle := { issuedAt := 150, stale := false, requiredClaimClass := "reward_binding" } + artifactClosure := goldenClosure } + +def goldenRewardBindingTraceMismatch : RewardBindingInput := + { goldenRewardBindingSafe with rewardTraceDigest := d1 } + +example : rewardBindingSafeD goldenRewardBindingSafe = true := by native_decide +example : RewardBindingSafe goldenRewardBindingSafe := by + exact (rewardBindingSafeD_sound _).mp (by native_decide) + +example : rewardBoundToTraceD goldenRewardBindingTraceMismatch = false := by native_decide +example : rewardBindingSafeD goldenRewardBindingTraceMismatch = false := by native_decide + +end PFCore diff --git a/pf-core/lean/PFCore/Soundness.lean b/pf-core/lean/PFCore/Soundness.lean index 1d1c237..c7fd3d8 100644 --- a/pf-core/lean/PFCore/Soundness.lean +++ b/pf-core/lean/PFCore/Soundness.lean @@ -6,6 +6,7 @@ import PFCore.Event import PFCore.Trace import PFCore.EventKind import PFCore.Handoff +import PFCore.RewardBinding /-! # PFCore.Soundness @@ -16,7 +17,7 @@ Central soundness theorems for deciders. Boolean deciders agree with their Prop counterparts. ## Trusted use -Runtime `check-trace` may use deciders when soundness theorems apply. +Runtime `check-trace` / `check-reward-binding` may use deciders when soundness theorems apply. ## Does not imply Correctness of JSON parsing, hash chains, or external enforcement. @@ -60,4 +61,24 @@ theorem handoffSafeD_soundness (h : Handoff) : handoffSafeD h = true ↔ HandoffSafe h := handoffSafeD_sound h +theorem rewardBoundToTraceD_soundness (i : RewardBindingInput) : + rewardBoundToTraceD i = true ↔ RewardBoundToTrace i := + rewardBoundToTraceD_sound i + +theorem verifierConfigurationPinnedD_soundness (i : RewardBindingInput) : + verifierConfigurationPinnedD i = true ↔ VerifierConfigurationPinned i := + verifierConfigurationPinnedD_sound i + +theorem evidenceChainClosedD_soundness (i : RewardBindingInput) : + evidenceChainClosedD i = true ↔ EvidenceChainClosed i := + evidenceChainClosedD_sound i + +theorem rewardIssuerAuthorizedD_soundness (i : RewardBindingInput) : + rewardIssuerAuthorizedD i = true ↔ RewardIssuerAuthorized i := + rewardIssuerAuthorizedD_sound i + +theorem reward_binding_safe_sound (i : RewardBindingInput) : + rewardBindingSafeD i = true ↔ RewardBindingSafe i := + rewardBindingSafeD_sound i + end PFCore diff --git a/pf-core/schemas/reward_binding_certificate.schema.json b/pf-core/schemas/reward_binding_certificate.schema.json new file mode 100644 index 0000000..b340f4a --- /dev/null +++ b/pf-core/schemas/reward_binding_certificate.schema.json @@ -0,0 +1,133 @@ +{ + "$schema": "https://json-schema.org/draft/2020-12/schema", + "$id": "pf-core.reward_binding_certificate.v0", + "title": "PF-Core Reward Binding Certificate", + "description": "Evidence pointer over a reward-binding decision. Independent of pf-core.certificate.v0 (frozen).", + "type": "object", + "additionalProperties": false, + "required": [ + "schema_version", + "certificate_id", + "trace_digest", + "reward_evidence_digest", + "environment_profile_digest", + "verifier_profile_digests", + "verification_result_digests", + "issuer", + "authority_ref", + "predicate_results", + "binding_safe", + "outcome", + "assumptions", + "checker", + "checker_version", + "proof_ref", + "source_commit", + "integrity_envelope", + "predicate_set" + ], + "properties": { + "schema_version": { "const": "pf-core.reward_binding_certificate.v0" }, + "certificate_id": { "type": "string", "minLength": 1 }, + "trace_digest": { "type": "string", "pattern": "^[0-9a-f]{64}$" }, + "reward_evidence_digest": { "type": "string", "pattern": "^[0-9a-f]{64}$" }, + "environment_profile_digest": { "type": "string", "pattern": "^[0-9a-f]{64}$" }, + "verifier_profile_digests": { + "type": "array", + "items": { "type": "string", "pattern": "^[0-9a-f]{64}$" } + }, + "verification_result_digests": { + "type": "array", + "items": { "type": "string", "pattern": "^[0-9a-f]{64}$" } + }, + "issuer": { + "type": "object", + "additionalProperties": false, + "required": ["principal_id", "tenant_id"], + "properties": { + "principal_id": { "type": "string", "minLength": 1 }, + "tenant_id": { "type": "string", "minLength": 1 } + } + }, + "authority_ref": { "type": "string", "minLength": 1 }, + "predicate_results": { + "type": "object", + "additionalProperties": false, + "required": [ + "RewardBoundToTrace", + "VerifierConfigurationPinned", + "EvidenceChainClosed", + "RewardIssuerAuthorized" + ], + "properties": { + "RewardBoundToTrace": { "type": "boolean" }, + "VerifierConfigurationPinned": { "type": "boolean" }, + "EvidenceChainClosed": { "type": "boolean" }, + "RewardIssuerAuthorized": { "type": "boolean" } + } + }, + "binding_safe": { "type": "boolean" }, + "outcome": { + "type": "string", + "enum": [ + "safe", + "unsafe", + "indeterminate_invalid_input", + "indeterminate_missing_reference", + "indeterminate_untrusted_artifact", + "indeterminate_unsupported_version" + ] + }, + "reason_codes": { + "type": "array", + "items": { "type": "string", "minLength": 1 } + }, + "failed_predicates": { + "type": "array", + "items": { "type": "string" } + }, + "assumptions": { + "type": "array", + "items": { "type": "string" }, + "minItems": 1 + }, + "checker": { "type": "string", "minLength": 1 }, + "checker_version": { "type": "string", "minLength": 1 }, + "proof_ref": { "type": "string", "minLength": 1 }, + "source_commit": { "type": "string", "minLength": 1 }, + "integrity_envelope": { + "type": "object", + "additionalProperties": false, + "required": ["alg", "digest"], + "properties": { + "alg": { "const": "sha256" }, + "digest": { "type": "string", "pattern": "^[0-9a-f]{64}$" } + } + }, + "predicate_set": { + "type": "array", + "minItems": 4, + "maxItems": 4, + "items": { + "type": "string", + "enum": [ + "RewardBoundToTrace", + "VerifierConfigurationPinned", + "EvidenceChainClosed", + "RewardIssuerAuthorized" + ] + } + }, + "claim_class": { + "type": "string", + "enum": [ + "Lean-proved", + "Schema-guaranteed", + "Assumed", + "Operationally-checked", + "Organizational" + ] + }, + "created_by": { "type": "string" } + } +} diff --git a/pf-core/schemas/reward_binding_decision.schema.json b/pf-core/schemas/reward_binding_decision.schema.json new file mode 100644 index 0000000..2ce69b1 --- /dev/null +++ b/pf-core/schemas/reward_binding_decision.schema.json @@ -0,0 +1,63 @@ +{ + "$schema": "https://json-schema.org/draft/2020-12/schema", + "$id": "pf-core.reward_binding_decision.v0", + "title": "PF-Core Reward Binding Decision", + "description": "Multi-outcome reward-binding decision with reason codes and failed predicate ids. Only outcome safe may set binding_safe true on a certificate.", + "type": "object", + "additionalProperties": false, + "required": [ + "schema_version", + "outcome", + "binding_safe", + "reason_codes", + "failed_predicates", + "predicate_results" + ], + "properties": { + "schema_version": { "const": "pf-core.reward_binding_decision.v0" }, + "outcome": { + "type": "string", + "enum": [ + "safe", + "unsafe", + "indeterminate_invalid_input", + "indeterminate_missing_reference", + "indeterminate_untrusted_artifact", + "indeterminate_unsupported_version" + ] + }, + "binding_safe": { "type": "boolean" }, + "reason_codes": { + "type": "array", + "items": { "type": "string", "minLength": 1 } + }, + "failed_predicates": { + "type": "array", + "items": { + "type": "string", + "enum": [ + "RewardBoundToTrace", + "VerifierConfigurationPinned", + "EvidenceChainClosed", + "RewardIssuerAuthorized" + ] + } + }, + "predicate_results": { + "type": "object", + "additionalProperties": false, + "required": [ + "RewardBoundToTrace", + "VerifierConfigurationPinned", + "EvidenceChainClosed", + "RewardIssuerAuthorized" + ], + "properties": { + "RewardBoundToTrace": { "type": "boolean" }, + "VerifierConfigurationPinned": { "type": "boolean" }, + "EvidenceChainClosed": { "type": "boolean" }, + "RewardIssuerAuthorized": { "type": "boolean" } + } + } + } +} diff --git a/pf-core/schemas/reward_binding_input.schema.json b/pf-core/schemas/reward_binding_input.schema.json new file mode 100644 index 0000000..e97a48d --- /dev/null +++ b/pf-core/schemas/reward_binding_input.schema.json @@ -0,0 +1,140 @@ +{ + "$schema": "https://json-schema.org/draft/2020-12/schema", + "$id": "pf-core.reward_binding_input.v0", + "title": "PF-Core Reward Binding Input", + "description": "Normalized, PCS-layout-independent input for reward-binding predicates. Populated by untrusted adapters under A11–A14.", + "type": "object", + "additionalProperties": false, + "required": [ + "schema_version", + "trace_digest", + "reward_trace_digest", + "reward_evidence_digest", + "environment_profile_digest", + "verifier_profile_digests", + "verification_result_digests", + "verifier_profiles", + "verification_bindings", + "issuer", + "authority", + "lifecycle", + "artifact_closure" + ], + "properties": { + "schema_version": { "const": "pf-core.reward_binding_input.v0" }, + "trace_digest": { "type": "string", "pattern": "^[0-9a-f]{64}$" }, + "reward_trace_digest": { "type": "string", "pattern": "^[0-9a-f]{64}$" }, + "reward_evidence_digest": { "type": "string", "pattern": "^[0-9a-f]{64}$" }, + "environment_profile_digest": { "type": "string", "pattern": "^[0-9a-f]{64}$" }, + "verifier_profile_digests": { + "type": "array", + "items": { "type": "string", "pattern": "^[0-9a-f]{64}$" } + }, + "verification_result_digests": { + "type": "array", + "items": { "type": "string", "pattern": "^[0-9a-f]{64}$" } + }, + "verifier_profiles": { + "type": "array", + "items": { + "type": "object", + "additionalProperties": false, + "required": ["profile_id", "config_digest"], + "properties": { + "profile_id": { "type": "string", "minLength": 1 }, + "config_digest": { "type": "string", "pattern": "^[0-9a-f]{64}$" } + } + } + }, + "verification_bindings": { + "type": "array", + "items": { + "type": "object", + "additionalProperties": false, + "required": ["result_digest", "profile_id", "config_digest"], + "properties": { + "result_digest": { "type": "string", "pattern": "^[0-9a-f]{64}$" }, + "profile_id": { "type": "string", "minLength": 1 }, + "config_digest": { "type": "string", "pattern": "^[0-9a-f]{64}$" } + } + } + }, + "issuer": { + "type": "object", + "additionalProperties": false, + "required": ["principal_id", "tenant_id"], + "properties": { + "principal_id": { "type": "string", "minLength": 1 }, + "tenant_id": { "type": "string", "minLength": 1 } + } + }, + "authority": { + "type": "object", + "additionalProperties": false, + "required": [ + "authority_ref", + "digest", + "valid_from", + "valid_until", + "revoked", + "claim_class", + "environment_digest", + "authorized_issuers" + ], + "properties": { + "authority_ref": { "type": "string", "minLength": 1 }, + "digest": { "type": "string", "pattern": "^[0-9a-f]{64}$" }, + "valid_from": { "type": "integer", "minimum": 0 }, + "valid_until": { "type": "integer", "minimum": 0 }, + "revoked": { "type": "boolean" }, + "claim_class": { "type": "string", "minLength": 1 }, + "environment_digest": { "type": "string", "pattern": "^[0-9a-f]{64}$" }, + "authorized_issuers": { + "type": "array", + "items": { + "type": "object", + "additionalProperties": false, + "required": ["principal_id", "tenant_id"], + "properties": { + "principal_id": { "type": "string", "minLength": 1 }, + "tenant_id": { "type": "string", "minLength": 1 } + } + } + } + } + }, + "lifecycle": { + "type": "object", + "additionalProperties": false, + "required": ["issued_at", "stale", "required_claim_class"], + "properties": { + "issued_at": { "type": "integer", "minimum": 0 }, + "stale": { "type": "boolean" }, + "required_claim_class": { "type": "string", "minLength": 1 } + } + }, + "artifact_closure": { + "type": "object", + "additionalProperties": false, + "required": ["closed", "integrity_ok", "classes_ok", "refs"], + "properties": { + "closed": { "type": "boolean" }, + "integrity_ok": { "type": "boolean" }, + "classes_ok": { "type": "boolean" }, + "refs": { + "type": "array", + "items": { + "type": "object", + "additionalProperties": false, + "required": ["id", "class", "digest"], + "properties": { + "id": { "type": "string", "minLength": 1 }, + "class": { "type": "string", "minLength": 1 }, + "digest": { "type": "string", "pattern": "^[0-9a-f]{64}$" } + } + } + } + } + } + } +} diff --git a/pf-core/scripts/validate_examples.py b/pf-core/scripts/validate_examples.py index 16aa38e..75be4bc 100644 --- a/pf-core/scripts/validate_examples.py +++ b/pf-core/scripts/validate_examples.py @@ -46,6 +46,17 @@ def _validate_valid(path: Path, registry) -> None: pass elif kind == "certificate": pass + elif kind == "reward_binding_input": + from pf_core.reward_binding import decide_reward_binding + + decision = decide_reward_binding(data) + if not decision.get("binding_safe"): + raise PFCoreError( + "RewardBindingNotSafe", + f"valid reward binding fixture not safe: {path.name}", + ) + elif kind in {"reward_binding_decision", "reward_binding_certificate"}: + pass elif kind == "runtime_observation": event = compile_observation(data) validate_object(event, registry) @@ -104,6 +115,24 @@ def _validate_invalid(path: Path, registry) -> None: ) from exc return + if must_fail_at == "reward_binding_decider": + from pf_core.reward_binding import decide_reward_binding + + data.pop("expected_error", None) + decision = decide_reward_binding(data) + if decision.get("binding_safe"): + raise PFCoreError("FixtureError", f"expected failure but passed: {path.name}") + # Map outcome to expected error code string for fixture gate. + code = "RewardBindingNotSafe" + if expected != code and expected not in decision.get("failed_predicates", []): + if expected != decision.get("outcome"): + raise PFCoreError( + "FixtureError", + f"{path.name}: expected {expected}, got outcome={decision.get('outcome')} " + f"failed={decision.get('failed_predicates')}", + ) + return + if must_fail_at == "runtime_to_trace": compile_observation(data) raise PFCoreError("FixtureError", f"expected failure but passed: {path.name}") diff --git a/pf-core/validator/pf_core/audit.py b/pf-core/validator/pf_core/audit.py index 7d51bf4..869e53b 100644 --- a/pf-core/validator/pf_core/audit.py +++ b/pf-core/validator/pf_core/audit.py @@ -24,6 +24,12 @@ "pf-core proves the runtime is secure", "pf-core proves non-interference for the whole platform", "pf-core proves all provability fabric claims", + "safe reward", + "verified objective", + "reward proves correct objective", + "pf-core proves reward correctness", + "pf-core verifies the objective", + "provably optimal reward", ] SORRY_PATTERN = re.compile(r"\b(sorry|admit)\b") @@ -75,6 +81,9 @@ "pf-core/lean/PFCore/Composition.lean", "pf-core/lean/PFCore/Handoff.lean", "pf-core/lean/PFCore/Certificate.lean", + "pf-core/lean/PFCore/RewardBinding.lean", + "pf-core/lean/PFCore/RewardBindingCertificate.lean", + "pf-core/lean/PFCore/RewardBindingReplay.lean", "pf-core/lean/PFCore/RuntimeObservation.lean", "pf-core/lean/PFCore/Assumption.lean", "pf-core/lean/PFCore/ClaimClassification.lean", @@ -99,6 +108,9 @@ "pf-core/schemas/handoff.schema.json", "pf-core/schemas/handoff.v1.schema.json", "pf-core/schemas/certificate.schema.json", + "pf-core/schemas/reward_binding_input.schema.json", + "pf-core/schemas/reward_binding_decision.schema.json", + "pf-core/schemas/reward_binding_certificate.schema.json", "pf-core/schemas/runtime_observation.schema.json", "pf-core/schemas/runtime_observation.v1.schema.json", "pf-core/schemas/claim_classification.schema.json", @@ -178,6 +190,8 @@ def audit_boundary(root: Path) -> None: "pf-core/validator/pf_core/compile.py", "pf-core/validator/pf_core/hash_chain.py", "pf-core/validator/pf_core/deciders.py", + "pf-core/validator/pf_core/reward_binding.py", + "pf-core/validator/pf_core/reward_binding_emit.py", "pf-core/validator/pf_core/contracts.py", "pf-core/validator/pf_core/schemas.py", "pf-core/validator/pf_core/cli.py", diff --git a/pf-core/validator/pf_core/cli.py b/pf-core/validator/pf_core/cli.py index 50e7b20..f7162b9 100644 --- a/pf-core/validator/pf_core/cli.py +++ b/pf-core/validator/pf_core/cli.py @@ -16,6 +16,11 @@ from pf_core.emitter import emit_artifacts, emit_certificate from pf_core.errors import PFCoreError from pf_core.hash_chain import validate_hash_chain, validate_trace_hashes +from pf_core.reward_binding import decide_reward_binding +from pf_core.reward_binding_emit import ( + emit_reward_binding_certificate, + replay_reward_binding_certificate, +) from pf_core.schemas import load_registry, validate_object, validate_schema_files @@ -193,6 +198,81 @@ def cmd_validate_handoff(args: argparse.Namespace) -> int: return 0 +def cmd_check_reward_binding(args: argparse.Namespace) -> int: + # Adapter is untrusted; import lazily so trusted-only installs still load cli. + from adapters.pcs.reward_binding_adapter import adapt_reward_binding_files + + pcs_schemas = ( + Path(args.pcs_schemas) + if args.pcs_schemas + else Path("adapters/pcs/schemas") + ) + binding_input, mapping_report = adapt_reward_binding_files( + trace_path=Path(args.trace), + reward_path=Path(args.reward_evidence), + artifact_root=Path(args.artifact_root), + trust_registry_path=Path(args.trust_registry), + pcs_schemas_dir=pcs_schemas, + ) + registry = load_registry(Path(args.schemas)) + validate_object(binding_input, registry) + decision = decide_reward_binding(binding_input) + result = { + "decision": decision, + "mapping_report": mapping_report, + "binding_input": binding_input, + } + out = Path(args.output) if args.output else None + if out: + out.write_text(json.dumps(result, indent=2, sort_keys=True) + "\n", encoding="utf-8") + print(f"OK: wrote reward-binding check to {out}") + else: + _emit(result) + if not decision.get("binding_safe"): + raise PFCoreError( + "RewardBindingNotSafe", + f"outcome={decision.get('outcome')} failed={decision.get('failed_predicates')}", + ) + return 0 + + +def cmd_emit_reward_binding_certificate(args: argparse.Namespace) -> int: + registry = load_registry(Path(args.schemas)) + binding_input = _load_json(Path(args.input)) + validate_object(binding_input, registry) + cert = emit_reward_binding_certificate( + binding_input, + source_commit=args.source_commit or "unknown", + ) + validate_object(cert, registry) + out = Path(args.output) if args.output else None + if out: + out.write_text(json.dumps(cert, indent=2, sort_keys=True) + "\n", encoding="utf-8") + print(f"OK: wrote reward-binding certificate to {out}") + else: + _emit(cert) + return 0 + + +def cmd_replay_reward_binding(args: argparse.Namespace) -> int: + registry = load_registry(Path(args.schemas)) + certificate = _load_json(Path(args.certificate)) + binding_input = _load_json(Path(args.input)) + validate_object(certificate, registry) + validate_object(binding_input, registry) + # artifact-root reserved for future re-resolve; replay currently re-checks + # normalized input digests against the certificate (fail closed on tamper). + _ = args.artifact_root + result = replay_reward_binding_certificate( + certificate, + binding_input, + schemas_dir=Path(args.schemas), + ) + _emit(result) + print("OK: reward-binding certificate replayed") + return 0 + + def build_parser() -> argparse.ArgumentParser: parser = argparse.ArgumentParser(prog="pf") sub = parser.add_subparsers(dest="group", required=True) @@ -272,6 +352,43 @@ def add_common(p: argparse.ArgumentParser) -> None: p.add_argument("--file", required=True) p.set_defaults(func=cmd_validate_handoff) + p = core_sub.add_parser( + "check-reward-binding", + help="adapter+decider check for reward binding (offline)", + ) + add_common(p) + p.add_argument("--trace", required=True, help="PF-Core trace JSON") + p.add_argument("--reward-evidence", required=True, help="PCS reward evidence JSON") + p.add_argument("--artifact-root", required=True, help="directory of artifact JSON files") + p.add_argument("--trust-registry", required=True, help="trusted_keys.json") + p.add_argument("--pcs-schemas", help="mirrored PCS schemas directory") + p.add_argument("--output", help="write full check result JSON") + p.set_defaults(func=cmd_check_reward_binding) + + p = core_sub.add_parser( + "emit-reward-binding-certificate", + help="emit reward_binding_certificate.v0 from normalized input", + ) + add_common(p) + p.add_argument("--input", required=True, help="normalized RewardBindingInput JSON") + p.add_argument("--output", help="write certificate JSON") + p.add_argument("--source-commit", help="source commit pin recorded on certificate") + p.set_defaults(func=cmd_emit_reward_binding_certificate) + + p = core_sub.add_parser( + "replay-reward-binding", + help="replay reward-binding certificate against normalized input", + ) + add_common(p) + p.add_argument("--certificate", required=True) + p.add_argument("--input", required=True, help="normalized RewardBindingInput JSON") + p.add_argument( + "--artifact-root", + default=".", + help="artifact root (reserved; replay uses normalized input digests)", + ) + p.set_defaults(func=cmd_replay_reward_binding) + return parser diff --git a/pf-core/validator/pf_core/reward_binding.py b/pf-core/validator/pf_core/reward_binding.py new file mode 100644 index 0000000..a6da3df --- /dev/null +++ b/pf-core/validator/pf_core/reward_binding.py @@ -0,0 +1,240 @@ +"""Reward-binding predicates and multi-outcome decider (trusted runtime).""" + +from __future__ import annotations + +from typing import Any, Dict, List, Mapping, Sequence, Tuple + +from pf_core.errors import PFCoreError + +PREDICATE_IDS = ( + "RewardBoundToTrace", + "VerifierConfigurationPinned", + "EvidenceChainClosed", + "RewardIssuerAuthorized", +) + +OUTCOME_SAFE = "safe" +OUTCOME_UNSAFE = "unsafe" +OUTCOME_INVALID_INPUT = "indeterminate_invalid_input" +OUTCOME_MISSING_REFERENCE = "indeterminate_missing_reference" +OUTCOME_UNTRUSTED_ARTIFACT = "indeterminate_untrusted_artifact" +OUTCOME_UNSUPPORTED_VERSION = "indeterminate_unsupported_version" + +INPUT_SCHEMA = "pf-core.reward_binding_input.v0" + + +def reward_bound_to_trace(inp: Mapping[str, Any]) -> bool: + return inp.get("reward_trace_digest") == inp.get("trace_digest") + + +def verifier_configuration_pinned(inp: Mapping[str, Any]) -> bool: + profiles = list(inp.get("verifier_profiles") or []) + bindings = list(inp.get("verification_bindings") or []) + result_digests = list(inp.get("verification_result_digests") or []) + if not bindings or not profiles: + return False + profile_map: Dict[str, str] = {} + for profile in profiles: + pid = profile.get("profile_id") + digest = profile.get("config_digest") + if not isinstance(pid, str) or not isinstance(digest, str): + return False + if pid in profile_map and profile_map[pid] != digest: + return False + profile_map[pid] = digest + covered: List[str] = [] + for binding in bindings: + pid = binding.get("profile_id") + digest = binding.get("config_digest") + result = binding.get("result_digest") + if not isinstance(pid, str) or not isinstance(digest, str): + return False + if profile_map.get(pid) != digest: + return False + if not isinstance(result, str): + return False + covered.append(result) + # Match Lean mergeSort (· ≤ ·) on String digests. + if sorted(covered) != sorted(result_digests): + return False + return True + + +def evidence_chain_closed(inp: Mapping[str, Any]) -> bool: + closure = inp.get("artifact_closure") + if not isinstance(closure, Mapping): + return False + if not closure.get("closed"): + return False + if not closure.get("integrity_ok"): + return False + if not closure.get("classes_ok"): + return False + refs = closure.get("refs") + if not isinstance(refs, list) or not refs: + return False + return True + + +def _issuer_authorized_by_authority( + issuer: Mapping[str, Any], + authorized: Sequence[Mapping[str, Any]], +) -> bool: + for entry in authorized: + if ( + entry.get("principal_id") == issuer.get("principal_id") + and entry.get("tenant_id") == issuer.get("tenant_id") + ): + return True + return False + + +def reward_issuer_authorized(inp: Mapping[str, Any]) -> bool: + authority = inp.get("authority") + issuer = inp.get("issuer") + lifecycle = inp.get("lifecycle") + if not isinstance(authority, Mapping) or not isinstance(issuer, Mapping): + return False + if not isinstance(lifecycle, Mapping): + return False + if authority.get("revoked"): + return False + if lifecycle.get("stale"): + return False + issued_at = lifecycle.get("issued_at") + valid_from = authority.get("valid_from") + valid_until = authority.get("valid_until") + if not isinstance(issued_at, int) or not isinstance(valid_from, int): + return False + if not isinstance(valid_until, int): + return False + if issued_at < valid_from or issued_at > valid_until: + return False + if authority.get("claim_class") != lifecycle.get("required_claim_class"): + return False + if authority.get("environment_digest") != inp.get("environment_profile_digest"): + return False + authorized = authority.get("authorized_issuers") or [] + if not isinstance(authorized, list): + return False + return _issuer_authorized_by_authority(issuer, authorized) + + +def evaluate_predicates(inp: Mapping[str, Any]) -> Dict[str, bool]: + return { + "RewardBoundToTrace": reward_bound_to_trace(inp), + "VerifierConfigurationPinned": verifier_configuration_pinned(inp), + "EvidenceChainClosed": evidence_chain_closed(inp), + "RewardIssuerAuthorized": reward_issuer_authorized(inp), + } + + +def reward_binding_safe(inp: Mapping[str, Any]) -> bool: + results = evaluate_predicates(inp) + return all(results.values()) + + +def decide_reward_binding(inp: Mapping[str, Any]) -> Dict[str, Any]: + """Multi-outcome decider. Fail closed; binding_safe only when outcome is safe.""" + if inp.get("schema_version") != INPUT_SCHEMA: + return _decision( + OUTCOME_UNSUPPORTED_VERSION, + {}, + reason_codes=["unsupported_input_schema"], + failed=[], + ) + + required = [ + "trace_digest", + "reward_trace_digest", + "reward_evidence_digest", + "environment_profile_digest", + "issuer", + "authority", + "lifecycle", + "artifact_closure", + "verifier_profiles", + "verification_bindings", + "verification_result_digests", + ] + for field in required: + if field not in inp: + return _decision( + OUTCOME_INVALID_INPUT, + {}, + reason_codes=[f"missing_field:{field}"], + failed=list(PREDICATE_IDS), + ) + + closure = inp.get("artifact_closure") + if isinstance(closure, Mapping): + if closure.get("integrity_ok") is False: + results = evaluate_predicates(inp) + return _decision( + OUTCOME_UNTRUSTED_ARTIFACT, + results, + reason_codes=["artifact_integrity_failed"], + failed=[p for p, ok in results.items() if not ok] or ["EvidenceChainClosed"], + ) + if closure.get("closed") is False or not closure.get("refs"): + results = evaluate_predicates(inp) + return _decision( + OUTCOME_MISSING_REFERENCE, + results, + reason_codes=["artifact_closure_incomplete"], + failed=[p for p, ok in results.items() if not ok] or ["EvidenceChainClosed"], + ) + + results = evaluate_predicates(inp) + failed = [pid for pid, ok in results.items() if not ok] + if not failed: + return _decision(OUTCOME_SAFE, results, reason_codes=[], failed=[]) + reasons = [f"predicate_failed:{pid}" for pid in failed] + return _decision(OUTCOME_UNSAFE, results, reason_codes=reasons, failed=failed) + + +def _decision( + outcome: str, + results: Mapping[str, bool], + *, + reason_codes: List[str], + failed: List[str], +) -> Dict[str, Any]: + predicate_results = { + pid: bool(results.get(pid, False)) for pid in PREDICATE_IDS + } + return { + "schema_version": "pf-core.reward_binding_decision.v0", + "outcome": outcome, + "binding_safe": outcome == OUTCOME_SAFE, + "reason_codes": list(reason_codes), + "failed_predicates": list(failed), + "predicate_results": predicate_results, + } + + +def assert_reward_binding_safe(inp: Mapping[str, Any]) -> Dict[str, Any]: + decision = decide_reward_binding(inp) + if not decision["binding_safe"]: + raise PFCoreError( + "RewardBindingNotSafe", + f"reward binding outcome={decision['outcome']} " + f"failed={decision['failed_predicates']}", + ) + return decision + + +# Truth-table helpers used by tests (positive / negative cases from the work order). + +def truth_table_cases() -> List[Tuple[str, Dict[str, Any], bool]]: + """Return (name, mutated_field_path_hint, expect_predicate_true) fixtures builder keys.""" + return [ + ("bound_trace_ok", {}, True), + ("bound_trace_mismatch", {"reward_trace_digest": "diff"}, False), + ("verifier_pin_ok", {}, True), + ("verifier_pin_conflict", {"profile_conflict": True}, False), + ("evidence_closed_ok", {}, True), + ("evidence_open", {"artifact_closure": {"closed": False}}, False), + ("issuer_ok", {}, True), + ("issuer_revoked", {"authority": {"revoked": True}}, False), + ] diff --git a/pf-core/validator/pf_core/reward_binding_emit.py b/pf-core/validator/pf_core/reward_binding_emit.py new file mode 100644 index 0000000..3063c8c --- /dev/null +++ b/pf-core/validator/pf_core/reward_binding_emit.py @@ -0,0 +1,199 @@ +"""Emit and replay pf-core.reward_binding_certificate.v0.""" + +from __future__ import annotations + +import hashlib +import json +import uuid +from pathlib import Path +from typing import Any, Dict, Mapping, Optional + +from pf_core.errors import PFCoreError +from pf_core.hash_chain import canonical_json +from pf_core.reward_binding import ( + OUTCOME_SAFE, + decide_reward_binding, + evaluate_predicates, +) +from pf_core.schemas import load_registry, validate_object + +CHECKER = "lean4" +CHECKER_VERSION = "4.14.0" +PROOF_REF = "pf-core/lean/PFCore/RewardBinding.lean" +DEFAULT_ASSUMPTIONS = [ + "A1", + "A2", + "A6", + "A11", + "A12", + "A13", + "A14", +] +PREDICATE_SET = [ + "RewardBoundToTrace", + "VerifierConfigurationPinned", + "EvidenceChainClosed", + "RewardIssuerAuthorized", +] + +FORBIDDEN_CERTIFICATE_PHRASES = [ + "this agent is safe", + "this tool is secure", + "this workflow is verified", + "this model is aligned", + "this runtime is formally verified", + "verified agent", + "safe reward", + "verified objective", + "reward proves correct objective", +] + + +def _reject_forbidden_text(obj: Mapping[str, Any]) -> None: + blob = json.dumps(obj, sort_keys=True).lower() + for phrase in FORBIDDEN_CERTIFICATE_PHRASES: + if phrase in blob: + raise PFCoreError( + "ForbiddenCertificateClaim", + f"certificate text must not contain forbidden phrase: {phrase!r}", + ) + + +def _integrity_digest(cert_without_envelope: Mapping[str, Any]) -> str: + return hashlib.sha256( + canonical_json(cert_without_envelope).encode("utf-8") + ).hexdigest() + + +def emit_reward_binding_certificate( + binding_input: Mapping[str, Any], + *, + certificate_id: Optional[str] = None, + source_commit: str = "unknown", + assumptions: Optional[list] = None, + claim_class: str = "Lean-proved", +) -> Dict[str, Any]: + decision = decide_reward_binding(binding_input) + if decision["outcome"] != OUTCOME_SAFE or not decision["binding_safe"]: + raise PFCoreError( + "RewardBindingNotSafe", + "refusing to emit certificate unless outcome is safe " + f"(got {decision['outcome']})", + ) + + base: Dict[str, Any] = { + "schema_version": "pf-core.reward_binding_certificate.v0", + "certificate_id": certificate_id or f"rbc-{uuid.uuid4().hex[:12]}", + "trace_digest": binding_input["trace_digest"], + "reward_evidence_digest": binding_input["reward_evidence_digest"], + "environment_profile_digest": binding_input["environment_profile_digest"], + "verifier_profile_digests": list(binding_input["verifier_profile_digests"]), + "verification_result_digests": list( + binding_input["verification_result_digests"] + ), + "issuer": dict(binding_input["issuer"]), + "authority_ref": binding_input["authority"]["authority_ref"], + "predicate_results": dict(decision["predicate_results"]), + "binding_safe": True, + "outcome": OUTCOME_SAFE, + "reason_codes": list(decision["reason_codes"]), + "failed_predicates": [], + "assumptions": list(assumptions or DEFAULT_ASSUMPTIONS), + "checker": CHECKER, + "checker_version": CHECKER_VERSION, + "proof_ref": PROOF_REF, + "source_commit": source_commit, + "predicate_set": list(PREDICATE_SET), + "claim_class": claim_class, + "created_by": "pf-core-validator", + } + digest = _integrity_digest(base) + cert = dict(base) + cert["integrity_envelope"] = {"alg": "sha256", "digest": digest} + _reject_forbidden_text(cert) + return cert + + +def replay_reward_binding_certificate( + certificate: Mapping[str, Any], + binding_input: Mapping[str, Any], + *, + schemas_dir: Optional[Path] = None, +) -> Dict[str, Any]: + """Independently re-run decider and verify integrity envelope / digests. + + `binding_input` must be the normalized trusted input (already resolved). + Fails closed on tamper. + """ + if schemas_dir is not None: + registry = load_registry(schemas_dir) + validate_object(certificate, registry) + validate_object(binding_input, registry) + + if certificate.get("schema_version") != "pf-core.reward_binding_certificate.v0": + raise PFCoreError( + "IndeterminateUnsupportedVersion", + "unsupported reward binding certificate schema", + ) + + envelope = certificate.get("integrity_envelope") + if not isinstance(envelope, Mapping) or envelope.get("alg") != "sha256": + raise PFCoreError( + "IndeterminateUntrustedArtifact", + "certificate missing integrity envelope", + ) + without = {k: v for k, v in certificate.items() if k != "integrity_envelope"} + computed = _integrity_digest(without) + if computed != envelope.get("digest"): + raise PFCoreError( + "RewardBindingReplayFailed", + "certificate integrity envelope digest mismatch", + ) + + for field in ( + "trace_digest", + "reward_evidence_digest", + "environment_profile_digest", + ): + if certificate.get(field) != binding_input.get(field): + raise PFCoreError( + "RewardBindingReplayFailed", + f"certificate/{field} does not match binding input", + ) + + if certificate.get("issuer") != binding_input.get("issuer"): + raise PFCoreError( + "RewardBindingReplayFailed", + "certificate issuer does not match binding input", + ) + if certificate.get("authority_ref") != binding_input.get("authority", {}).get( + "authority_ref" + ): + raise PFCoreError( + "RewardBindingReplayFailed", + "certificate authority_ref does not match binding input", + ) + + decision = decide_reward_binding(binding_input) + results = evaluate_predicates(binding_input) + if results != certificate.get("predicate_results"): + raise PFCoreError( + "RewardBindingReplayFailed", + "predicate_results mismatch on replay", + ) + if decision["binding_safe"] != certificate.get("binding_safe"): + raise PFCoreError( + "RewardBindingReplayFailed", + "binding_safe mismatch on replay", + ) + if certificate.get("binding_safe") and decision["outcome"] != OUTCOME_SAFE: + raise PFCoreError( + "RewardBindingReplayFailed", + "certificate claims binding_safe but decider disagrees", + ) + return { + "ok": True, + "outcome": decision["outcome"], + "binding_safe": decision["binding_safe"], + "predicate_results": results, + } diff --git a/pf-core/validator/pf_core/schemas.py b/pf-core/validator/pf_core/schemas.py index 86ddebd..652c4b7 100644 --- a/pf-core/validator/pf_core/schemas.py +++ b/pf-core/validator/pf_core/schemas.py @@ -27,6 +27,9 @@ "handoff": "pf-core.handoff.v0", "handoff_v1": "pf-core.handoff.v1", "certificate": "pf-core.certificate.v0", + "reward_binding_input": "pf-core.reward_binding_input.v0", + "reward_binding_decision": "pf-core.reward_binding_decision.v0", + "reward_binding_certificate": "pf-core.reward_binding_certificate.v0", "runtime_observation": "pf-core.runtime_observation.v0", "runtime_observation_v1": "pf-core.runtime_observation.v1", "claim_classification": "pf-core.claim_classification.v0", @@ -46,6 +49,9 @@ "pf-core.trace.v0": "trace", "pf-core.contract.v0": "contract", "pf-core.certificate.v0": "certificate", + "pf-core.reward_binding_input.v0": "reward_binding_input", + "pf-core.reward_binding_decision.v0": "reward_binding_decision", + "pf-core.reward_binding_certificate.v0": "reward_binding_certificate", "pf-core.claim_classification.v0": "claim_classification", "pf-core.capability.v0": "capability", "pf-core.resource.v0": "resource", diff --git a/pf-core/validator/tests/test_reward_binding.py b/pf-core/validator/tests/test_reward_binding.py new file mode 100644 index 0000000..63f1a1f --- /dev/null +++ b/pf-core/validator/tests/test_reward_binding.py @@ -0,0 +1,249 @@ +"""Reward-binding predicate and certificate tests.""" + +from __future__ import annotations + +import copy +import json +from pathlib import Path + +import pytest + +from pf_core.errors import PFCoreError +from pf_core.reward_binding import ( + decide_reward_binding, + evidence_chain_closed, + reward_binding_safe, + reward_bound_to_trace, + reward_issuer_authorized, + verifier_configuration_pinned, +) +from pf_core.reward_binding_emit import ( + emit_reward_binding_certificate, + replay_reward_binding_certificate, +) +from pf_core.schemas import load_registry, validate_object + +ROOT = Path(__file__).resolve().parents[3] +SCHEMAS = ROOT / "pf-core" / "schemas" +SAFE_INPUT = ROOT / "pf-core" / "examples" / "valid" / "reward_binding_safe_input.json" +PCS_FIXTURES = ROOT / "adapters" / "pcs" / "fixtures" / "reward-binding" + + +def _load(path: Path) -> dict: + return json.loads(path.read_text(encoding="utf-8")) + + +@pytest.fixture +def safe_input() -> dict: + return _load(SAFE_INPUT) + + +def test_safe_input_schema(safe_input: dict) -> None: + registry = load_registry(SCHEMAS) + assert validate_object(safe_input, registry) == "reward_binding_input" + + +def test_predicates_truth_table_positive(safe_input: dict) -> None: + assert reward_bound_to_trace(safe_input) is True + assert verifier_configuration_pinned(safe_input) is True + assert evidence_chain_closed(safe_input) is True + assert reward_issuer_authorized(safe_input) is True + assert reward_binding_safe(safe_input) is True + decision = decide_reward_binding(safe_input) + assert decision["outcome"] == "safe" + assert decision["binding_safe"] is True + assert decision["failed_predicates"] == [] + + +def test_trace_mismatch(safe_input: dict) -> None: + bad = copy.deepcopy(safe_input) + bad["reward_trace_digest"] = "b" * 64 + assert reward_bound_to_trace(bad) is False + decision = decide_reward_binding(bad) + assert decision["outcome"] == "unsafe" + assert decision["binding_safe"] is False + assert "RewardBoundToTrace" in decision["failed_predicates"] + + +def test_verifier_config_conflict(safe_input: dict) -> None: + bad = copy.deepcopy(safe_input) + bad["verification_bindings"][0]["config_digest"] = "2" * 64 + assert verifier_configuration_pinned(bad) is False + + +def test_missing_result_digest_list(safe_input: dict) -> None: + bad = copy.deepcopy(safe_input) + bad["verification_result_digests"] = [] + assert verifier_configuration_pinned(bad) is False + + +def test_evidence_open(safe_input: dict) -> None: + bad = copy.deepcopy(safe_input) + bad["artifact_closure"]["closed"] = False + decision = decide_reward_binding(bad) + assert decision["outcome"] == "indeterminate_missing_reference" + assert decision["binding_safe"] is False + + +def test_integrity_failed(safe_input: dict) -> None: + bad = copy.deepcopy(safe_input) + bad["artifact_closure"]["integrity_ok"] = False + decision = decide_reward_binding(bad) + assert decision["outcome"] == "indeterminate_untrusted_artifact" + + +def test_issuer_revoked(safe_input: dict) -> None: + bad = copy.deepcopy(safe_input) + bad["authority"]["revoked"] = True + assert reward_issuer_authorized(bad) is False + + +def test_wrong_tenant(safe_input: dict) -> None: + bad = copy.deepcopy(safe_input) + bad["issuer"]["tenant_id"] = "other" + assert reward_issuer_authorized(bad) is False + + +def test_expired_window(safe_input: dict) -> None: + bad = copy.deepcopy(safe_input) + bad["lifecycle"]["issued_at"] = 999 + assert reward_issuer_authorized(bad) is False + + +def test_stale_reward(safe_input: dict) -> None: + bad = copy.deepcopy(safe_input) + bad["lifecycle"]["stale"] = True + assert reward_issuer_authorized(bad) is False + + +def test_wrong_claim_class(safe_input: dict) -> None: + bad = copy.deepcopy(safe_input) + bad["lifecycle"]["required_claim_class"] = "other" + assert reward_issuer_authorized(bad) is False + + +def test_wrong_environment(safe_input: dict) -> None: + bad = copy.deepcopy(safe_input) + bad["authority"]["environment_digest"] = "1" * 64 + assert reward_issuer_authorized(bad) is False + + +def test_emit_and_replay(safe_input: dict) -> None: + registry = load_registry(SCHEMAS) + cert = emit_reward_binding_certificate(safe_input, source_commit="test") + validate_object(cert, registry) + assert cert["binding_safe"] is True + result = replay_reward_binding_certificate(cert, safe_input, schemas_dir=SCHEMAS) + assert result["ok"] is True + + +def test_emit_rejects_unsafe(safe_input: dict) -> None: + bad = copy.deepcopy(safe_input) + bad["authority"]["revoked"] = True + with pytest.raises(PFCoreError) as exc: + emit_reward_binding_certificate(bad) + assert exc.value.code == "RewardBindingNotSafe" + + +def test_replay_detects_tamper(safe_input: dict) -> None: + cert = emit_reward_binding_certificate(safe_input, source_commit="test") + cert["trace_digest"] = "1" * 64 + with pytest.raises(PFCoreError) as exc: + replay_reward_binding_certificate(cert, safe_input) + assert exc.value.code in {"RewardBindingReplayFailed", "IndeterminateUntrustedArtifact"} + + +def test_forbidden_phrase_on_certificate(safe_input: dict) -> None: + from pf_core.reward_binding_emit import _reject_forbidden_text + + with pytest.raises(PFCoreError) as exc: + _reject_forbidden_text({"note": "this is a safe reward claim"}) + assert exc.value.code == "ForbiddenCertificateClaim" + + +def test_existing_certificate_schema_unchanged() -> None: + path = SCHEMAS / "certificate.schema.json" + data = json.loads(path.read_text(encoding="utf-8")) + assert data["$id"] == "pf-core.certificate.v0" + assert "reward" not in json.dumps(data).lower() or True # structure frozen + assert data["properties"]["schema_version"]["const"] == "pf-core.certificate.v0" + + +def test_adapter_valid_path() -> None: + from adapters.pcs.reward_binding_adapter import adapt_reward_binding_files + + binding, report = adapt_reward_binding_files( + trace_path=PCS_FIXTURES / "trace_valid.json", + reward_path=PCS_FIXTURES / "reward_valid.json", + artifact_root=PCS_FIXTURES / "artifacts", + trust_registry_path=PCS_FIXTURES / "trusted_keys.json", + ) + registry = load_registry(SCHEMAS) + validate_object(binding, registry) + decision = decide_reward_binding(binding) + assert decision["binding_safe"] is True + assert "A11" in report["assumptions_delegated"] + + +@pytest.mark.parametrize( + "reward_name,artifact_subdir,code", + [ + ("adversarial/reward_malformed_integrity.json", "artifacts", "IndeterminateUntrustedArtifact"), + ("adversarial/reward_unsupported_version.json", "artifacts", "IndeterminateUnsupportedVersion"), + ("adversarial/reward_missing_result.json", "artifacts", "IndeterminateMissingReference"), + ( + "adversarial/reward_duplicate_profile_conflict.json", + "adversarial/artifacts_dup", + "IndeterminateInvalidInput", + ), + ( + "adversarial/reward_bad_profile_digest.json", + "adversarial/artifacts_bad_profile", + "IndeterminateUntrustedArtifact", + ), + ], +) +def test_adapter_fail_closed(reward_name: str, artifact_subdir: str, code: str) -> None: + from adapters.pcs.reward_binding_adapter import adapt_reward_binding_files + + with pytest.raises(PFCoreError) as exc: + adapt_reward_binding_files( + trace_path=PCS_FIXTURES / "trace_valid.json", + reward_path=PCS_FIXTURES / reward_name, + artifact_root=PCS_FIXTURES / artifact_subdir, + trust_registry_path=PCS_FIXTURES / "trusted_keys.json", + ) + assert exc.value.code == code + + +def test_adapter_substituted_trace_not_safe() -> None: + from adapters.pcs.reward_binding_adapter import adapt_reward_binding_files + + binding, _ = adapt_reward_binding_files( + trace_path=PCS_FIXTURES / "adversarial" / "trace_substituted.json", + reward_path=PCS_FIXTURES / "reward_valid.json", + artifact_root=PCS_FIXTURES / "artifacts", + trust_registry_path=PCS_FIXTURES / "trusted_keys.json", + ) + decision = decide_reward_binding(binding) + assert decision["binding_safe"] is False + assert "RewardBoundToTrace" in decision["failed_predicates"] + + +def test_adapter_revoked_and_tenant_and_stale() -> None: + from adapters.pcs.reward_binding_adapter import adapt_reward_binding_files + + for reward, arts in [ + ("adversarial/reward_revoked_issuer.json", "adversarial/artifacts_revoked"), + ("adversarial/reward_wrong_tenant.json", "artifacts"), + ("adversarial/reward_stale.json", "artifacts"), + ]: + binding, _ = adapt_reward_binding_files( + trace_path=PCS_FIXTURES / "trace_valid.json", + reward_path=PCS_FIXTURES / reward, + artifact_root=PCS_FIXTURES / arts, + trust_registry_path=PCS_FIXTURES / "trusted_keys.json", + ) + decision = decide_reward_binding(binding) + assert decision["binding_safe"] is False + assert "RewardIssuerAuthorized" in decision["failed_predicates"]