Add AD proof result import gate

Author: jishengyang-cal

Cargo.lock

@@ -5,3 +5,4 @@ edition = "2021"
 
 [dependencies]
 serde_json = "1"
+sha2 = "0.10"

Cargo.toml

@@ -1,8 +1,8 @@
-.PHONY: check fmt test validate eval gradient export-golden validate-proof-boundary doctor-proof-backend gate-proof-backend clean
+.PHONY: check fmt test validate eval gradient export-golden validate-proof-boundary doctor-proof-backend gate-proof-backend ad-proof-result validate-proof-result compare-proof-result gate-ad-proof-import clean
 
 INPUTS=--input action_features=2.0 --input user_features=3.0 --const 1.0
 
-check: fmt test validate eval gradient export-golden validate-proof-boundary doctor-proof-backend gate-proof-backend
+check: fmt test validate eval gradient export-golden validate-proof-boundary doctor-proof-backend gate-proof-backend ad-proof-result validate-proof-result compare-proof-result gate-ad-proof-import
 
 fmt:
 	cargo fmt --check
@@ -31,5 +31,17 @@ doctor-proof-backend:
 gate-proof-backend:
 	! cargo run -- gate-proof-backend examples/proof-backend-boundary.valid.json target/gatl-ad-lab/proof-backend-environment.json --out target/gatl-ad-lab/proof-backend-activation-gate.json
 
+ad-proof-result:
+	cargo run --manifest-path ../gatl-ad-proof-backend/Cargo.toml -- check-fixture target/gatl-ad-lab/derivative-golden.json --proof-certificate ../gatl-ad-proof-backend/examples/proof-certificate.valid.json --out target/gatl-ad-lab/external-ad-proof-result.json --checked-at 2026-06-14T00:00:00Z
+
+validate-proof-result:
+	cargo run -- validate-proof-result target/gatl-ad-lab/external-ad-proof-result.json --out target/gatl-ad-lab/ad-proof-result-validation.json
+
+compare-proof-result:
+	cargo run -- compare-proof-result target/gatl-ad-lab/derivative-golden.json target/gatl-ad-lab/external-ad-proof-result.json --out target/gatl-ad-lab/ad-proof-result-comparison.json
+
+gate-ad-proof-import:
+	cargo run -- gate-ad-proof-import target/gatl-ad-lab/derivative-golden.json target/gatl-ad-lab/external-ad-proof-result.json --out target/gatl-ad-lab/ad-proof-import-gate.json
+
 clean:
 	rm -rf target

Makefile

@@ -72,6 +72,17 @@ cargo run -- gate-proof-backend \
   examples/proof-backend-boundary.valid.json \
   target/gatl-ad-lab/proof-backend-environment.json \
   --out target/gatl-ad-lab/proof-backend-activation-gate.json
+cargo run -- validate-proof-result \
+  target/gatl-ad-lab/external-ad-proof-result.json \
+  --out target/gatl-ad-lab/ad-proof-result-validation.json
+cargo run -- compare-proof-result \
+  target/gatl-ad-lab/derivative-golden.json \
+  target/gatl-ad-lab/external-ad-proof-result.json \
+  --out target/gatl-ad-lab/ad-proof-result-comparison.json
+cargo run -- gate-ad-proof-import \
+  target/gatl-ad-lab/derivative-golden.json \
+  target/gatl-ad-lab/external-ad-proof-result.json \
+  --out target/gatl-ad-lab/ad-proof-import-gate.json
 ```
 
 Local example:
@@ -113,3 +124,10 @@ emits an external AD proof result. Without a local proof certificate it reports
 `gatl-ad-proof-backend/v0.1-proof-certificate` it can report `proved` under the
 backend's local certificate proof system. This still does not move proof
 assistant execution into `gatl-ad-lab`.
+
+`validate-proof-result`, `compare-proof-result`, and `gate-ad-proof-import`
+consume an already-produced external AD proof result. The import gate opens
+only when the proof result is `proved`, `formalProof.proved = true`, the proof
+system is `gatl-local-ad-certificate/v0.1`, and the result's fixture content
+address matches the derivative golden fixture. These commands do not execute
+the proof backend.

README.md

@@ -17,6 +17,8 @@ gatl-core risk-models.json
   -> optional derivative golden fixture for formal proof backends
   -> optional external proof backend boundary validation
   -> optional proof backend activation gate
+  -> optional external AD proof result comparison
+  -> optional AD proof import gate
 ```
 
 ## Trusted Boundary
@@ -29,6 +31,7 @@ The v0.1 trusted boundary is:
 - local pullback rules for smooth scalar primitives;
 - central finite-difference comparison;
 - deterministic derivative golden fixture export.
+- deterministic external AD proof result import comparison.
 
 The lab does not prove AD correctness. It provides an external executable
 sanity check and a report that future proof tooling can consume.
@@ -57,6 +60,12 @@ result artifact. A valid certificate can produce `formalProof.proved = true`
 inside that external backend's local proof system; `gatl-ad-lab` still does not
 run proof jobs or proof assistants.
 
+`validate-proof-result`, `compare-proof-result`, and `gate-ad-proof-import`
+are the import side of the same boundary. They consume an already-produced
+`gatl-ad-lab/v0.1-external-ad-proof-result`, require `status = proved`,
+`formalProof.proved = true`, and bind the result to the derivative golden
+fixture by SHA-256 content address. They do not run the proof backend.
+
 ## Primitive Semantics
 
 Supported scalar primitives:

docs/architecture.md

@@ -8,6 +8,8 @@ risk-model artifacts.
 | Input | Producer | Required format |
 | --- | --- | --- |
 | Risk model analysis | `gatl-core risk-models` | `gatl-core/v0.1-risk-model-analysis` |
+| Derivative golden fixture | `gatl-ad-lab export-golden` | `gatl-ad-lab/v0.1-derivative-golden-fixture` |
+| External AD proof result | `gatl-ad-proof-backend` | `gatl-ad-lab/v0.1-external-ad-proof-result` |
 
 ## Produced Artifacts
 
@@ -17,6 +19,9 @@ risk-model artifacts.
 | AD check report | `gatl-ad-lab/v0.1-ad-check-report` |
 | Derivative golden fixture | `gatl-ad-lab/v0.1-derivative-golden-fixture` |
 | External AD proof result placeholder | `gatl-ad-lab/v0.1-external-ad-proof-result` |
+| AD proof result validation | `gatl-ad-lab/v0.1-ad-proof-result-validation` |
+| AD proof result comparison | `gatl-ad-lab/v0.1-ad-proof-result-comparison` |
+| AD proof import gate | `gatl-ad-lab/v0.1-ad-proof-import-gate` |
 | Proof backend boundary validation | `gatl-ad-lab/v0.1-proof-backend-boundary-validation` |
 | Proof backend environment report | `gatl-ad-lab/v0.1-proof-backend-environment` |
 | Proof backend activation gate | `gatl-ad-lab/v0.1-proof-backend-activation-gate` |
@@ -28,8 +33,10 @@ evaluates the typed scalar expression, runs the exported reverse derivative
 instruction skeleton, compares the result with finite differences, and exports
 a derivative golden fixture for external formal proof backends. It also
 validates the proof backend boundary manifest, emits a local environment probe,
-and verifies that the activation gate remains closed when the external proof
-backend command is missing.
+verifies that the activation gate remains closed when the external proof
+backend command is missing, generates an external AD proof result through the
+separate `gatl-ad-proof-backend` repo, validates that result, compares it to
+the derivative golden fixture, and opens the AD proof import gate.
 
 ## Boundary
 
@@ -41,3 +48,6 @@ The proof backend activation gate is only a readiness artifact for external
 deployment automation. It must be consumed by a separate production proof
 service before proof jobs run; `gatl-ad-lab` itself does not run the proof
 backend beyond an explicit `--version` probe.
+
+The AD proof import gate is a result-consumption artifact. It only imports an
+already-produced proof result and requires a matching fixture content address.

docs/compatibility.md

@@ -30,13 +30,31 @@ cargo run -- gate-proof-backend \
   examples/proof-backend-boundary.valid.json \
   target/production-probes/proof-backend-environment.after-backend.json \
   --out target/production-probes/proof-backend-activation-gate.after-backend.json
+cargo run --manifest-path ../gatl-ad-proof-backend/Cargo.toml -- check-fixture \
+  target/production-probes/derivative-golden.actual.json \
+  --proof-certificate ../gatl-ad-proof-backend/examples/proof-certificate.valid.json \
+  --checked-at 2026-06-14T00:00:00Z \
+  --out target/production-probes/external-ad-proof-result.after-certificate.json
+cargo run -- validate-proof-result \
+  target/production-probes/external-ad-proof-result.after-certificate.json \
+  --out target/production-probes/ad-proof-result-validation.after-certificate.json
+cargo run -- compare-proof-result \
+  target/production-probes/derivative-golden.actual.json \
+  target/production-probes/external-ad-proof-result.after-certificate.json \
+  --out target/production-probes/ad-proof-result-comparison.after-certificate.json
+cargo run -- gate-ad-proof-import \
+  target/production-probes/derivative-golden.actual.json \
+  target/production-probes/external-ad-proof-result.after-certificate.json \
+  --out target/production-probes/ad-proof-import-gate.after-certificate.json
 ```
 
 Expected result:
 
 - boundary validation is valid;
 - backend environment is production-ready;
 - activation gate is open.
+- external AD proof result validation is valid;
+- AD proof import gate is open.
 
 ## Boundary
 
@@ -47,3 +65,5 @@ without a certificate it remains `validated-not-proved`; with a valid
 `gatl-ad-proof-backend/v0.1-proof-certificate`, the external backend can emit a
 `proved` result under `gatl-local-ad-certificate/v0.1`. Production proof
 assistant execution remains outside `gatl-ad-lab`.
+The import commands consume the produced proof result, but do not execute the
+backend themselves.