Add derivative golden fixture export

Author: jishengyang-cal

Makefile

@@ -1,8 +1,8 @@
-.PHONY: check fmt test validate eval gradient clean
+.PHONY: check fmt test validate eval gradient export-golden clean
 
 INPUTS=--input action_features=2.0 --input user_features=3.0 --const 1.0
 
-check: fmt test validate eval gradient
+check: fmt test validate eval gradient export-golden
 
 fmt:
 	cargo fmt --check
@@ -19,5 +19,8 @@ eval:
 gradient:
 	cargo run -- check-gradient examples/risk-models.valid.json $(INPUTS) --epsilon 0.000001 --tolerance 0.00001 --out target/gatl-ad-lab/ad-check.json
 
+export-golden:
+	cargo run -- export-golden examples/risk-models.valid.json $(INPUTS) --epsilon 0.000001 --tolerance 0.00001 --out target/gatl-ad-lab/derivative-golden.json
+
 clean:
 	rm -rf target

README.md

@@ -23,7 +23,8 @@ v0.1 supports:
 - scalar primitives `const`, `add`, `sub`, `mul`, `div`, `exp`, `log`,
   `sigmoid`, `dot`, and `matmul`;
 - reverse pullbacks from `derivativeProgram.instructions`;
-- finite-difference gradient comparison.
+- finite-difference gradient comparison;
+- derivative golden fixture export for external formal AD proof backends.
 
 `const` has no literal in current `gatl-core`, so this lab treats it as an
 external numeric assumption. The CLI default is `--const 1.0`, and reports
@@ -55,6 +56,13 @@ cargo run -- check-gradient /home/jisheng-yang/projects/gatl-core/target/gatl/ri
   --epsilon 0.000001 \
   --tolerance 0.00001 \
   --out target/gatl-ad-lab/ad-check.json
+cargo run -- export-golden /home/jisheng-yang/projects/gatl-core/target/gatl/risk-models.json \
+  --input action_features=2.0 \
+  --input user_features=3.0 \
+  --const 1.0 \
+  --epsilon 0.000001 \
+  --tolerance 0.00001 \
+  --out target/gatl-ad-lab/derivative-golden.json
 ```
 
 Local example:
@@ -76,3 +84,7 @@ This is a local numeric lab, not a production AD engine:
 
 Future proof-oriented work should consume the generated AD check report or add
 a separate proof fixture format, not move numeric execution into `gatl-core`.
+`export-golden` emits that first proof-backend handoff fixture: it records the
+typed expression, derivative program, numeric inputs, expected primal value,
+expected reverse gradients, and finite-difference comparison metadata. It does
+not run Lean, Coq, Agda, F*, or any external proof engine.

docs/ad-check-report.md

@@ -35,3 +35,20 @@ abs(reverse - finiteDifference) <= tolerance
 This report is not a formal proof. It is a local executable check that the
 current exported derivative instruction skeleton agrees with a numerical
 finite-difference baseline under declared assumptions.
+
+## Derivative Golden Fixture
+
+`gatl-ad-lab export-golden` emits:
+
+```text
+format = gatl-ad-lab/v0.1-derivative-golden-fixture
+```
+
+The fixture carries the selected typed numeric expression, derivative program,
+numeric input cases, expected primal value, expected reverse gradients, and the
+finite-difference comparison source. It is intended for an external formal AD
+proof backend to import as a deterministic fixture.
+
+The command does not execute a proof assistant or certify correctness. Its
+`proofBackendBoundary` explicitly records that production proof checking is an
+external requirement.

docs/architecture.md

@@ -14,6 +14,7 @@ gatl-core risk-models.json
   -> reverse derivative instruction interpretation
   -> finite-difference comparison
   -> AD check report
+  -> optional derivative golden fixture for formal proof backends
 ```
 
 ## Trusted Boundary
@@ -24,10 +25,14 @@ The v0.1 trusted boundary is:
 - `gatl-core/v0.1-risk-model-analysis` validation;
 - scalar RPN node evaluation;
 - local pullback rules for smooth scalar primitives;
-- central finite-difference comparison.
+- central finite-difference comparison;
+- deterministic derivative golden fixture export.
 
 The lab does not prove AD correctness. It provides an external executable
 sanity check and a report that future proof tooling can consume.
+`export-golden` turns the same check into a proof-backend fixture by preserving
+typedExpression, derivativeProgram, numeric assumptions, expected values, and
+comparison metadata. The formal proof backend remains external.
 
 ## Primitive Semantics
 
@@ -51,6 +56,7 @@ Non-smooth or nondeterministic primitives remain outside this lab.
 - No production AD engine.
 - No TensorFlow, PyTorch, JAX, ONNX, or autograd integration.
 - No proof assistant integration.
+- No production formal proof backend.
 - No network access.
 - No secret handling.
 - No background worker.

docs/compatibility.md

@@ -15,12 +15,14 @@ risk-model artifacts.
 | --- | --- |
 | Evaluation report | `gatl-ad-lab/v0.1-evaluation` |
 | AD check report | `gatl-ad-lab/v0.1-ad-check-report` |
+| Derivative golden fixture | `gatl-ad-lab/v0.1-derivative-golden-fixture` |
 
 ## Release Gate
 
 `make check` is the v0.1 release gate. It validates the risk-model fixture,
 evaluates the typed scalar expression, runs the exported reverse derivative
-instruction skeleton, and compares the result with finite differences.
+instruction skeleton, compares the result with finite differences, and exports
+a derivative golden fixture for external formal proof backends.
 
 ## Boundary
 

src/lib.rs

@@ -4,6 +4,7 @@ use serde_json::{json, Value};
 
 pub const LAB_VERSION: &str = "gatl-ad-lab/v0.1";
 pub const REPORT_FORMAT: &str = "gatl-ad-lab/v0.1-ad-check-report";
+pub const DERIVATIVE_GOLDEN_FORMAT: &str = "gatl-ad-lab/v0.1-derivative-golden-fixture";
 
 #[derive(Clone, Debug, PartialEq)]
 pub struct LabError {
@@ -194,6 +195,46 @@ pub fn gradient_check_report(
     }))
 }
 
+pub fn derivative_golden_fixture(
+    root: &Value,
+    options: &EvaluationOptions,
+) -> Result<Value, Vec<LabError>> {
+    let model = select_model(root, options)?;
+    let result = gradient_check_model(&model, options)?;
+    let input_cases = options
+        .inputs
+        .iter()
+        .map(|(name, value)| {
+            json!({
+                "name": name,
+                "value": value
+            })
+        })
+        .collect::<Vec<_>>();
+    Ok(json!({
+        "apiVersion": "gatl.dev/v0.1",
+        "kind": "GATLDerivativeGoldenFixture",
+        "version": LAB_VERSION,
+        "format": DERIVATIVE_GOLDEN_FORMAT,
+        "modelId": result.model_id,
+        "assumptions": assumptions_json(options),
+        "inputCases": input_cases,
+        "expectedValue": result.value,
+        "expectedReverseGradients": result.reverse_gradients,
+        "comparisonSource": {
+            "finiteDifferenceEpsilon": options.epsilon,
+            "tolerance": options.tolerance,
+            "maxAbsError": result.max_abs_error,
+            "passed": result.passed
+        },
+        "proofBackendBoundary": {
+            "status": "external-proof-backend-required",
+            "consumes": "typedExpression + derivativeProgram + expectedReverseGradients",
+            "executesProofBackend": false
+        }
+    }))
+}
+
 fn gradient_check_model(
     model: &RiskModel,
     options: &EvaluationOptions,
@@ -885,6 +926,19 @@ mod tests {
         assert!((result.reverse_gradients["y"] - 2.0).abs() < 1e-9);
     }
 
+    #[test]
+    fn exports_derivative_golden_fixture() {
+        let fixture = derivative_golden_fixture(&report(), &options()).expect("golden");
+        assert_eq!(
+            fixture.pointer("/format"),
+            Some(&json!(DERIVATIVE_GOLDEN_FORMAT))
+        );
+        assert_eq!(
+            fixture.pointer("/expectedReverseGradients/x"),
+            Some(&json!(3.0))
+        );
+    }
+
     #[test]
     fn rejects_missing_input() {
         let mut options = options();

src/main.rs

@@ -4,7 +4,8 @@ use std::fs;
 use std::path::PathBuf;
 
 use gatl_ad_lab::{
-    evaluate_report, gradient_check_report, validate_risk_models, EvaluationOptions, LabError,
+    derivative_golden_fixture, evaluate_report, gradient_check_report, validate_risk_models,
+    EvaluationOptions, LabError,
 };
 use serde_json::Value;
 
@@ -21,13 +22,43 @@ fn run(args: Vec<String>) -> i32 {
         "validate" => validate_command(&args[1..]),
         "eval" => eval_command(&args[1..]),
         "check-gradient" => check_gradient_command(&args[1..]),
+        "export-golden" => export_golden_command(&args[1..]),
         _ => {
             usage();
             2
         }
     }
 }
 
+fn export_golden_command(args: &[String]) -> i32 {
+    let (path, out, options) = match parse_report_options(args, true) {
+        Ok(parsed) => parsed,
+        Err(ParseOutcome::Usage) => {
+            usage();
+            return 2;
+        }
+        Err(ParseOutcome::Message(message)) => {
+            eprintln!("error: {message}");
+            return 2;
+        }
+    };
+    let report = match read_json(&path) {
+        Ok(value) => value,
+        Err(error) => {
+            eprintln!("error: {error}");
+            return 1;
+        }
+    };
+    let output = match derivative_golden_fixture(&report, &options) {
+        Ok(value) => value,
+        Err(errors) => {
+            print_errors(&errors);
+            return 1;
+        }
+    };
+    write_or_print("derivative-golden", output, out)
+}
+
 fn validate_command(args: &[String]) -> i32 {
     let [path] = args else {
         usage();
@@ -267,6 +298,7 @@ fn usage() {
     eprintln!("  gatl-ad-lab validate <risk-models.json>");
     eprintln!("  gatl-ad-lab eval <risk-models.json> [--model <id>] --input name=value [--input name=value ...] [--const <value>] [--out <path>]");
     eprintln!("  gatl-ad-lab check-gradient <risk-models.json> [--model <id>] --input name=value [--input name=value ...] [--const <value>] [--epsilon <value>] [--tolerance <value>] [--out <path>]");
+    eprintln!("  gatl-ad-lab export-golden <risk-models.json> [--model <id>] --input name=value [--input name=value ...] [--const <value>] [--epsilon <value>] [--tolerance <value>] [--out <path>]");
 }
 
 enum ParseOutcome {