Add V2-compatible Library substrate facade

Prover/tests/test_oci_lean_runner.py

@@ -8,7 +8,12 @@
 from pathlib import Path
 
 import pytest
-from autolean_contracts import HashKindV1, ProofSubmissionV1, digest_text
+from autolean_contracts import (
+    HashKindV1,
+    OciVerifierExecutionPolicyV2,
+    ProofSubmissionV1,
+    digest_text,
+)
 from autolean_prover.errors import ValidationError
 from autolean_prover.execution import (
     MaterializedWorkspace,
@@ -186,33 +191,12 @@ def test_oci_lean_runner_uses_fixed_wrapper_argv_and_emits_execution_evidence(tm
     assert len(harness.requests) == 2
     compile_argv = harness.requests[0].argv
     query_argv = harness.requests[1].argv
+    policy = workspace.bundle.contract.formal.environment.verifier_execution_policy
+    assert isinstance(policy, OciVerifierExecutionPolicyV2)
     compile_image_index = compile_argv.index(spec.image)
-    assert compile_argv[compile_image_index:] == (
-        spec.image,
-        "/opt/autolean/bin/autolean-lean-wrapper",
-        "--protocol",
-        "autolean.oci-lean-wrapper.v2",
-        "--phase",
-        "compile",
-        "--candidate",
-        "/input/Candidate.lean",
-        "--output",
-        "/output/Candidate.olean",
-    )
-    image_index = query_argv.index(spec.image)
-    assert query_argv[image_index:] == (
-        spec.image,
-        "/opt/autolean/bin/autolean-lean-wrapper",
-        "--protocol",
-        "autolean.oci-lean-wrapper.v2",
-        "--phase",
-        "query",
-        "--compiled",
-        "/compiled/Candidate.olean",
-        "--declaration",
-        bundle.proof_boundary.expected_declaration,
-        "--type-format",
-        "autolean.lean-pp-expr.v1",
+    assert compile_argv[compile_image_index + 1 :] == policy.compile_wrapper_argv()
+    assert query_argv[query_argv.index(spec.image) + 1 :] == policy.wrapper_argv(
+        bundle.proof_boundary.expected_declaration
     )
     for argv in (compile_argv, query_argv):
         assert (argv[argv.index("--network")], argv[argv.index("--network") + 1]) == (

Prover/worker/Dockerfile.library-substrate

@@ -12,6 +12,8 @@ ARG QUERY_WRAPPER_SHA256
 ARG RECEIPT_TOOL_SHA256
 ARG RUNTIME_SOURCE_CHECKSUM_MANIFEST_SHA256
 ARG RUNTIME_SOURCE_TREE_SHA256
+ARG V2_FACADE_QUERY_HELPER_SHA256
+ARG V2_FACADE_WRAPPER_SHA256
 
 COPY build-input.v1.json /build/input/build-input.v1.json
 COPY runtime-sources.sha256 /build/input/runtime-sources.sha256
@@ -20,6 +22,8 @@ COPY helpers/AutoleanLibrarySubstrateInventory.lean /build/tools/AutoleanLibrary
 COPY helpers/autolean-library-substrate-build /build/tools/autolean-library-substrate-build
 COPY helpers/autolean-library-substrate-independent-query /build/tools/autolean-library-substrate-independent-query
 COPY helpers/autolean-library-substrate-build-receipt /build/tools/autolean-library-substrate-build-receipt
+COPY helpers/AutoleanLibrarySubstrateV2Query.lean /build/tools/AutoleanLibrarySubstrateV2Query.lean
+COPY helpers/autolean-library-substrate-v2-facade /build/tools/autolean-library-substrate-v2-facade
 COPY Dockerfile.library-substrate /build/tools/Dockerfile.library-substrate
 
 RUN /build/tools/autolean-library-substrate-build \
@@ -32,7 +36,9 @@ RUN /build/tools/autolean-library-substrate-build \
       "${QUERY_WRAPPER_SHA256}" \
       "${RECEIPT_TOOL_SHA256}" \
       "${RUNTIME_SOURCE_CHECKSUM_MANIFEST_SHA256}" \
-      "${RUNTIME_SOURCE_TREE_SHA256}"
+      "${RUNTIME_SOURCE_TREE_SHA256}" \
+      "${V2_FACADE_QUERY_HELPER_SHA256}" \
+      "${V2_FACADE_WRAPPER_SHA256}"
 
 FROM autolean/mathlib-worker@sha256:3237192cf627a05367c75d46e61ec9034fefe43a4fd0c06139e38c80358648d6
 
@@ -51,10 +57,20 @@ LABEL org.opencontainers.image.title="AutoLean library-substrate-v1 preflight" \
 
 COPY --from=library-substrate-builder --chown=0:0 \
   /build/final/ /opt/autolean/library-substrate/
+COPY --from=library-substrate-builder --chown=0:0 \
+  /build/final/bin/autolean-library-substrate-v2-facade \
+  /opt/autolean/bin/autolean-lean-wrapper
+COPY --from=library-substrate-builder --chown=0:0 \
+  /build/tools/AutoleanLibrarySubstrateV2Query.lean \
+  /opt/autolean/lib/AutoleanLeanQuery.lean
 
 RUN test -x /opt/autolean/library-substrate/bin/autolean-library-substrate-build-receipt \
     && test -x /opt/autolean/library-substrate/bin/autolean-library-substrate-independent-query \
+    && test -x /opt/autolean/bin/autolean-lean-wrapper \
+    && test -f /opt/autolean/lib/AutoleanLeanQuery.lean \
     && test -z "$(find /opt/autolean/library-substrate -name '*.lean' -o -name '*.ilean')" \
+    && chmod 0555 /opt/autolean/bin/autolean-lean-wrapper \
+    && chmod 0444 /opt/autolean/lib/AutoleanLeanQuery.lean \
     && /opt/autolean/library-substrate/bin/autolean-library-substrate-build-receipt >/dev/null
 
 USER 65532:65532

Prover/worker/library-substrate/AutoleanLibrarySubstrateV2Query.lean

@@ -0,0 +1,64 @@
+import Mathlib.ModelTheory.Semantics
+import Lean.PrettyPrinter
+import Lean.Util.CollectAxioms
+
+open Lean
+
+private def canonicalOptions : Options :=
+  ((((({} : Options).setBool `pp.all true).setBool `pp.explicit true).setBool
+        `pp.universes true).setBool `pp.notation false).set `pp.width (1000000 : Nat)
+
+private def canonicalType (env : Environment) (declaration : Name) : IO String := do
+  let some info := env.checked.get.find? declaration
+    | throw <| IO.userError s!"declaration not found: {declaration}"
+  if info.type.hasMVar then
+    throw <| IO.userError "declaration type contains a metavariable"
+  let rendered :=
+    (← PrettyPrinter.ppExprLegacy env {} {} canonicalOptions info.type).pretty 1000000
+  if rendered.isEmpty || rendered.length > 1000000 then
+    throw <| IO.userError "canonical declaration type is outside the verifier limit"
+  if rendered.any fun char => char == '\x00' || char == '\n' || char == '\r' then
+    throw <| IO.userError "canonical declaration type is not one line"
+  return rendered
+
+private def observedAxioms (env : Environment) (declaration : Name) : IO (Array Name) := do
+  let context : Core.Context := {
+    fileName := "<AutoLeanLibrarySubstrateV2Query>"
+    fileMap := default
+    options := canonicalOptions
+  }
+  let state : Core.State := { env := env }
+  let axioms ← Core.CoreM.toIO' (collectAxioms declaration) context state
+  return Array.qsort axioms fun left right => left.toString < right.toString
+
+private def query (declarationText wrapperSha256 queryHelperSha256 : String) : IO Json := do
+  let environment ← importModules #[{ module := `Candidate }] canonicalOptions
+  let declaration := declarationText.toName
+  return Json.mkObj [
+    ("schema_version", Json.str "autolean.oci-lean-wrapper.v2"),
+    ("declaration", Json.str declarationText),
+    ("canonical_type", Json.str (← canonicalType environment declaration)),
+    ("lean_version", Json.str "v4.28.0"),
+    ("mathlib_revision", Json.str "8f9d9cff6bd728b17a24e163c9402775d9e6a365"),
+    ("lake_manifest_hash",
+      Json.str "e2a93c904f51195d6740cd9abfb35ab155dc0157e0e46642dce0d364b68a9a89"),
+    ("observed_axioms", Json.arr <| (← observedAxioms environment declaration).map fun name =>
+      Json.str name.toString),
+    ("image_identity", Json.mkObj [
+      ("schema_version", Json.str "autolean.image-owned-verifier-identity.v2"),
+      ("wrapper_path", Json.str "/opt/autolean/bin/autolean-lean-wrapper"),
+      ("wrapper_sha256", Json.str wrapperSha256),
+      ("query_helper_path", Json.str "/opt/autolean/lib/AutoleanLeanQuery.lean"),
+      ("query_helper_sha256", Json.str queryHelperSha256)
+    ])
+  ]
+
+def main (arguments : List String) : IO UInt32 := do
+  try
+    let [declaration, wrapperSha256, queryHelperSha256] := arguments
+      | throw <| IO.userError "expected declaration and image-owned identity arguments"
+    IO.println (← query declaration wrapperSha256 queryHelperSha256).compress
+    return (0 : UInt32)
+  catch error =>
+    IO.eprintln s!"autolean-library-substrate-v2-query: {error}"
+    return (2 : UInt32)

Prover/worker/library-substrate/autolean-library-substrate-build

@@ -6,7 +6,7 @@ fail() {
   exit 2
 }
 
-[ "$#" -eq 10 ] || fail "expected the frozen build argument profile"
+[ "$#" -eq 12 ] || fail "expected the frozen build argument profile"
 build_input_sha256=$1
 build_tool_sha256=$2
 dockerfile_sha256=$3
@@ -17,6 +17,8 @@ query_wrapper_sha256=$7
 receipt_tool_sha256=$8
 runtime_source_checksum_manifest_sha256=$9
 runtime_source_tree_sha256=${10}
+v2_facade_query_helper_sha256=${11}
+v2_facade_wrapper_sha256=${12}
 
 for digest in "$@"; do
   case "$digest" in
@@ -50,6 +52,10 @@ test "$(sha256sum "$tools/autolean-library-substrate-independent-query" | awk '{
   "$query_wrapper_sha256"
 test "$(sha256sum "$tools/autolean-library-substrate-build-receipt" | awk '{print $1}')" = \
   "$receipt_tool_sha256"
+test "$(sha256sum "$tools/AutoleanLibrarySubstrateV2Query.lean" | awk '{print $1}')" = \
+  "$v2_facade_query_helper_sha256"
+test "$(sha256sum "$tools/autolean-library-substrate-v2-facade" | awk '{print $1}')" = \
+  "$v2_facade_wrapper_sha256"
 test "$(sha256sum "$parent_receipt" | awk '{print $1}')" = \
   "$parent_receipt_file_sha256"
 test "$(
@@ -187,6 +193,8 @@ cp "$tools/autolean-library-substrate-independent-query" \
   "$final/bin/autolean-library-substrate-independent-query"
 cp "$tools/autolean-library-substrate-build-receipt" \
   "$final/bin/autolean-library-substrate-build-receipt"
+cp "$tools/autolean-library-substrate-v2-facade" \
+  "$final/bin/autolean-library-substrate-v2-facade"
 chmod 0555 "$final/bin/"*
 find "$final/lib" -type f -exec chmod 0444 {} \;
 find "$final/attestations" -type f -exec chmod 0444 {} \;
@@ -254,6 +262,8 @@ runtime_manifest_sha256=$(
   printf '"runtime_manifest_sha256":"%s",' "$runtime_manifest_sha256"
   printf '"runtime_source_checksum_manifest_sha256":"%s",' "$runtime_source_checksum_manifest_sha256"
   printf '"runtime_source_tree_sha256":"%s",' "$runtime_source_tree_sha256"
+  printf '"v2_facade_query_helper_sha256":"%s",' "$v2_facade_query_helper_sha256"
+  printf '"v2_facade_wrapper_sha256":"%s",' "$v2_facade_wrapper_sha256"
   printf '"schema_version":"autolean.library-substrate-image-receipt.v1",'
   printf '"task_mode":"independent_reproof"'
   printf '}\n'

Prover/worker/library-substrate/autolean-library-substrate-build-receipt

@@ -49,6 +49,8 @@ check_hash runtime_source_checksum_manifest_sha256 "$runtime_sources"
 check_hash query_wrapper_sha256 \
   "$root/bin/autolean-library-substrate-independent-query"
 check_hash receipt_tool_sha256 "$root/bin/autolean-library-substrate-build-receipt"
+check_hash v2_facade_wrapper_sha256 /opt/autolean/bin/autolean-lean-wrapper
+check_hash v2_facade_query_helper_sha256 /opt/autolean/lib/AutoleanLeanQuery.lean
 check_hash parent_receipt_file_sha256 \
   /opt/autolean/attestations/mathlib-source-build-receipt.v2.json
 

Prover/worker/library-substrate/autolean-library-substrate-independent-query

@@ -41,6 +41,14 @@ import Lean.Util.FoldConsts
 
 open Lean
 
+private def targetTypeSha256 :=
+  "66d1fe3cbd2a62831bf57b9761248bf3fa5d84b95879be25c7e591c48ebeef8a"
+
+private def expectedAxioms : Array String := #["Classical.choice", "Quot.sound", "propext"]
+
+private def forbiddenDirectDependency :=
+  `AutoLeanLibrary.Fixtures.ModelTheory.UniversalLK.Deriv.sound
+
 private def runtimeModules : Array (Name × System.FilePath) := #[
   (`AutoLeanLibrary.Fixtures.ModelTheory.UniversalLK.Core,
     "/opt/autolean/library-substrate/lib/lean/AutoLeanLibrary/Fixtures/ModelTheory/UniversalLK/Core.olean"),
@@ -80,6 +88,17 @@ private def canonicalType (environment : Environment) (info : ConstantInfo) : IO
     throw <| IO.userError s!"canonical type is not one line: {info.name}"
   return rendered
 
+private def sha256Text (value : String) : IO String := do
+  let path : System.FilePath := "/tmp/autolean-library-substrate-query-type.txt"
+  IO.FS.writeFile path value
+  let output ← IO.Process.output { cmd := "sha256sum", args := #[path.toString] }
+  if output.exitCode != 0 then
+    throw <| IO.userError "sha256sum failed while hashing the target type"
+  let digest := (output.stdout.trimAscii.take 64).toString
+  if digest.length != 64 || !digest.all fun char => char.isDigit || ('a' ≤ char && char ≤ 'f') then
+    throw <| IO.userError "sha256sum emitted an invalid target type digest"
+  return digest
+
 private def observedAxioms (environment : Environment) (name : Name) : IO (Array Name) := do
   let context : Core.Context := {
     fileName := "<AutoLeanLibrarySubstrateIndependentQuery>"
@@ -218,18 +237,28 @@ private def query
   let some targetInfo := environment.checked.get.find? target
     | throw <| IO.userError "owned target has no ConstantInfo"
   let direct := uniqueSortedNames (← targetProof environment target).getUsedConstants
-  let candidateImports := candidate.imports.map (·.module)
+  if direct.any (· == forbiddenDirectDependency) then
+    throw <| IO.userError "Candidate directly depends on the forbidden Deriv.sound declaration"
+  let candidateImports := uniqueSortedNames (candidate.imports.map (·.module))
+  if candidateImports != #[`AutoLeanLibrary.Fixtures.ModelTheory.UniversalLK.RulePrelude, `Init] then
+    throw <| IO.userError "Candidate direct imports differ from the independent substrate profile"
+  let renderedType ← canonicalType environment targetInfo
+  if (← sha256Text renderedType) != targetTypeSha256 then
+    throw <| IO.userError "Candidate target type differs from the historical frozen hash"
+  let axioms ← observedAxioms environment target
+  if axioms.map (·.toString) != expectedAxioms then
+    throw <| IO.userError "Candidate target axioms differ from the historical frozen set"
   return Json.mkObj [
-    ("candidate_direct_imports", namesJson (sortedNames candidateImports)),
+    ("candidate_direct_imports", namesJson candidateImports),
     ("candidate_ir_auxiliary_names", namesJson candidateAuxiliaryNames),
     ("candidate_kernel_names", namesJson candidateKernelNames),
     ("candidate_namespace_disjoint", Json.bool true),
     ("candidate_owns_target", Json.bool true),
-    ("canonical_type", Json.str (← canonicalType environment targetInfo)),
+    ("canonical_type", Json.str renderedType),
     ("declaration", Json.str target.toString),
     ("direct_proof_dependencies", namesJson direct),
     ("loaded_module_closure", namesJson (sortedNames environment.header.moduleNames)),
-    ("observed_axioms", namesJson (← observedAxioms environment target)),
+    ("observed_axioms", namesJson axioms),
     ("runtime_declarations", Json.arr (← runtimeInventory environment)),
     ("runtime_ir_auxiliary_names", Json.arr (← runtimeIrAuxiliaryNames environment)),
     ("schema_version", Json.str "autolean.library-substrate-independent-query.v1"),

Prover/worker/library-substrate/autolean-library-substrate-v2-facade

@@ -0,0 +1,104 @@
+#!/bin/sh
+set -eu
+
+fail() {
+  printf '%s\n' "autolean-library-substrate-v2-facade: $1" >&2
+  exit 2
+}
+
+emit_phase_failure() {
+  failure_phase=$1
+  failure_stdout=$2
+  failure_stderr=$3
+  printf '%s\n' \
+    "autolean-library-substrate-v2-facade: phase=$failure_phase failed" >&2
+  {
+    cat "$failure_stdout"
+    cat "$failure_stderr"
+  } | head -c 4096 >&2
+  printf '\n' >&2
+}
+
+[ "$#" -ge 4 ] || fail "expected the frozen V2 wrapper argument profile"
+[ "$1" = "--protocol" ] || fail "missing protocol argument"
+[ "$2" = "autolean.oci-lean-wrapper.v2" ] || fail "unsupported protocol"
+[ "$3" = "--phase" ] || fail "missing phase argument"
+phase=$4
+
+root=/opt/autolean/library-substrate
+receipt_tool=$root/bin/autolean-library-substrate-build-receipt
+preflight_query=$root/bin/autolean-library-substrate-independent-query
+runtime=$root/lib/lean
+parent_lean_path=$(cat /opt/autolean/environment/lean-path)
+[ -n "$parent_lean_path" ] || fail "image-owned parent LEAN_PATH is unavailable"
+lean_path="$runtime:$parent_lean_path"
+
+# The receipt checker binds this facade and its V2 helper to the build input and runtime manifest
+# before either phase can accept a candidate artifact.
+"$receipt_tool" >/dev/null || fail "image-owned substrate receipt verification failed"
+
+wrapper_sha256=$(sha256sum /opt/autolean/bin/autolean-lean-wrapper | awk '{print $1}')
+query_helper_sha256=$(sha256sum /opt/autolean/lib/AutoleanLeanQuery.lean | awk '{print $1}')
+case "$wrapper_sha256:$query_helper_sha256" in
+  *[!0-9a-f:]*|*:|:*|*::* ) fail "image-owned verifier hashes are malformed" ;;
+esac
+
+scratch=$(mktemp -d /tmp/autolean-library-substrate-v2.XXXXXX)
+cleanup() {
+  rm -rf "$scratch"
+}
+trap cleanup EXIT HUP INT TERM
+
+case "$phase" in
+  compile)
+    [ "$#" -eq 8 ] || fail "expected the frozen V2 compile argument profile"
+    [ "$5" = "--candidate" ] || fail "missing candidate argument"
+    [ "$6" = "/input/Candidate.lean" ] || fail "candidate path is not frozen"
+    [ "$7" = "--output" ] || fail "missing output argument"
+    [ "$8" = "/output/Candidate.olean" ] || fail "compiled output path is not frozen"
+    test -f /input/Candidate.lean && test ! -L /input/Candidate.lean ||
+      fail "candidate source is unavailable"
+    test -d /output && test ! -L /output || fail "compiler output is unavailable"
+    if ! LEAN_PATH="$lean_path" lean -R /input -o /output/Candidate.olean \
+      /input/Candidate.lean >"$scratch/compiler.stdout" 2>"$scratch/compiler.stderr"
+    then
+      emit_phase_failure compile "$scratch/compiler.stdout" "$scratch/compiler.stderr"
+      exit 20
+    fi
+    ;;
+  query)
+    [ "$#" -eq 10 ] || fail "expected the frozen V2 query argument profile"
+    [ "$5" = "--compiled" ] || fail "missing compiled candidate argument"
+    [ "$6" = "/compiled/Candidate.olean" ] || fail "compiled candidate path is not frozen"
+    [ "$7" = "--declaration" ] || fail "missing declaration argument"
+    declaration=$8
+    [ "$9" = "--type-format" ] || fail "missing type-format argument"
+    [ "${10}" = "autolean.lean-pp-expr.v1" ] || fail "unsupported type format"
+    [ "$declaration" = "AutoLeanLibrary.Fixtures.ModelTheory.UniversalLK.Deriv.closed_sound" ] ||
+      fail "unsupported substrate target declaration"
+    test -f /compiled/Candidate.olean && test ! -L /compiled/Candidate.olean ||
+      fail "sealed Candidate.olean is unavailable"
+
+    # This preflight owns all substrate-specific semantics; stdout is intentionally discarded so
+    # the externally visible protocol remains the unchanged V2 single-record result.
+    if ! LEAN_PATH="/compiled:$lean_path" "$preflight_query" --phase query \
+      --target "$declaration" >"$scratch/preflight.stdout" 2>"$scratch/preflight.stderr"
+    then
+      emit_phase_failure query "$scratch/preflight.stdout" "$scratch/preflight.stderr"
+      exit 21
+    fi
+    if ! LEAN_PATH="/compiled:$lean_path" lean --run /opt/autolean/lib/AutoleanLeanQuery.lean \
+      "$declaration" "$wrapper_sha256" "$query_helper_sha256" \
+      >"$scratch/query.stdout" 2>"$scratch/query.stderr"
+    then
+      emit_phase_failure query "$scratch/query.stdout" "$scratch/query.stderr"
+      exit 22
+    fi
+    [ "$(wc -l <"$scratch/query.stdout" | tr -d ' ')" -eq 1 ] ||
+      fail "V2 query helper did not emit exactly one record"
+    cat "$scratch/query.stdout"
+    ;;
+  *)
+    fail "unsupported phase"
+    ;;
+esac