Skip to content

Commit 869e5c1

Browse files
morlutomorluto
committed
Merge remote-tracking branch 'origin/main' into agent/modularize-make-and-retire-c901
# Conflicts: # benchmarks/datasets/provider-feasibility-v1/cddlib/tests/Dockerfile # benchmarks/datasets/provider-feasibility-v1/cgal/tests/Dockerfile # benchmarks/datasets/provider-feasibility-v1/gudhi/tests/Dockerfile # benchmarks/datasets/provider-feasibility-v1/nauty/tests/Dockerfile # benchmarks/datasets/provider-feasibility-v1/regina/tests/Dockerfile # src/jacobian/lean_frontend/proof_state.py # src/jacobian_checkers/smt.py
2 parents 65213b7 + 228e494 commit 869e5c1

312 files changed

Lines changed: 6946 additions & 901 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎.github/workflows/lean-images.yml‎

Lines changed: 153 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,153 @@
1+
name: Lean Evaluation Images
2+
3+
on:
4+
pull_request:
5+
branches: [main]
6+
paths:
7+
- "containers/lean-checker/**"
8+
- "containers/lean-repl-agent/**"
9+
- ".github/workflows/lean-images.yml"
10+
push:
11+
branches: [main]
12+
paths:
13+
- "containers/lean-checker/**"
14+
- "containers/lean-repl-agent/**"
15+
- ".github/workflows/lean-images.yml"
16+
workflow_dispatch:
17+
18+
concurrency:
19+
group: lean-images-${{ github.workflow }}-${{ github.ref }}
20+
cancel-in-progress: ${{ github.event_name == 'pull_request' }}
21+
22+
permissions:
23+
contents: read
24+
25+
env:
26+
REGISTRY: ghcr.io
27+
PLATFORM: linux/amd64
28+
29+
jobs:
30+
build-pr:
31+
name: Build ${{ matrix.image }}
32+
if: github.event_name == 'pull_request' || github.event_name == 'workflow_dispatch'
33+
runs-on: ubuntu-latest
34+
timeout-minutes: 30
35+
strategy:
36+
fail-fast: false
37+
matrix:
38+
include:
39+
- image: jacobian-lean-checker
40+
directory: lean-checker
41+
- image: jacobian-lean-repl-agent
42+
directory: lean-repl-agent
43+
steps:
44+
- uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
45+
with:
46+
persist-credentials: false
47+
- uses: docker/setup-buildx-action@bb05f3f5519dd87d3ba754cc423b652a5edd6d2c # v4
48+
- name: Build and load image for measurement
49+
uses: docker/build-push-action@53b7df96c91f9c12dcc8a07bcb9ccacbed38856a # v7
50+
with:
51+
context: .
52+
file: containers/${{ matrix.directory }}/Dockerfile
53+
platforms: ${{ env.PLATFORM }}
54+
load: true
55+
push: false
56+
tags: local/${{ matrix.image }}:${{ github.sha }}
57+
cache-from: type=gha,scope=${{ matrix.image }}
58+
cache-to: type=gha,mode=max,scope=${{ matrix.image }}
59+
- name: Record unpacked image size
60+
env:
61+
IMAGE: local/${{ matrix.image }}:${{ github.sha }}
62+
run: |
63+
bytes=$(docker image inspect "$IMAGE" --format '{{.Size}}')
64+
jq -n \
65+
--arg image "$IMAGE" \
66+
--arg source_sha "$GITHUB_SHA" \
67+
--arg platform "$PLATFORM" \
68+
--argjson unpacked_size_bytes "$bytes" \
69+
'{image: $image, source_sha: $source_sha, platform: $platform, unpacked_size_bytes: $unpacked_size_bytes}' \
70+
| tee "$RUNNER_TEMP/${{ matrix.image }}-size.json" \
71+
>> "$GITHUB_STEP_SUMMARY"
72+
- name: Upload size evidence
73+
uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1
74+
with:
75+
name: ${{ matrix.image }}-size-${{ github.sha }}
76+
path: ${{ runner.temp }}/${{ matrix.image }}-size.json
77+
if-no-files-found: error
78+
retention-days: 90
79+
80+
publish:
81+
name: Publish ${{ matrix.image }}
82+
if: github.event_name == 'push'
83+
runs-on: ubuntu-latest
84+
timeout-minutes: 30
85+
permissions:
86+
contents: read
87+
packages: write
88+
strategy:
89+
fail-fast: false
90+
matrix:
91+
include:
92+
- image: jacobian-lean-checker
93+
directory: lean-checker
94+
- image: jacobian-lean-repl-agent
95+
directory: lean-repl-agent
96+
steps:
97+
- uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
98+
with:
99+
persist-credentials: false
100+
- uses: docker/setup-buildx-action@bb05f3f5519dd87d3ba754cc423b652a5edd6d2c # v4
101+
- name: Log in to GHCR
102+
uses: docker/login-action@dbcb813823bdd20940b903addbd779551569679f # v4
103+
with:
104+
registry: ${{ env.REGISTRY }}
105+
username: ${{ github.actor }}
106+
password: ${{ secrets.GITHUB_TOKEN }}
107+
- id: meta
108+
uses: docker/metadata-action@dc802804100637a589fabce1cb79ff13a1411302 # v6
109+
with:
110+
images: ${{ env.REGISTRY }}/${{ github.repository_owner }}/${{ matrix.image }}
111+
tags: |
112+
type=raw,value=sha-${{ github.sha }}
113+
type=raw,value=main
114+
labels: |
115+
org.opencontainers.image.revision=${{ github.sha }}
116+
io.jacobian.source-dirty=false
117+
- id: build
118+
name: Build and publish
119+
uses: docker/build-push-action@53b7df96c91f9c12dcc8a07bcb9ccacbed38856a # v7
120+
with:
121+
context: .
122+
file: containers/${{ matrix.directory }}/Dockerfile
123+
platforms: ${{ env.PLATFORM }}
124+
push: true
125+
tags: ${{ steps.meta.outputs.tags }}
126+
labels: ${{ steps.meta.outputs.labels }}
127+
cache-from: type=gha,scope=${{ matrix.image }}
128+
cache-to: type=gha,mode=max,scope=${{ matrix.image }}
129+
provenance: mode=max
130+
sbom: true
131+
- name: Record digest and unpacked size
132+
env:
133+
IMAGE: ${{ env.REGISTRY }}/${{ github.repository_owner }}/${{ matrix.image }}
134+
DIGEST: ${{ steps.build.outputs.digest }}
135+
run: |
136+
docker pull "$IMAGE@$DIGEST"
137+
size=$(docker image inspect "$IMAGE@$DIGEST" --format '{{.Size}}')
138+
jq -n \
139+
--arg source_sha "$GITHUB_SHA" \
140+
--arg image "$IMAGE@$DIGEST" \
141+
--arg image_digest "$DIGEST" \
142+
--arg platform "$PLATFORM" \
143+
--argjson unpacked_size_bytes "$size" \
144+
'{source_sha: $source_sha, image: $image, image_digest: $image_digest, platform: $platform, unpacked_size_bytes: $unpacked_size_bytes}' \
145+
| tee "$RUNNER_TEMP/${{ matrix.image }}-publication.json" \
146+
>> "$GITHUB_STEP_SUMMARY"
147+
- name: Upload publication evidence
148+
uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1
149+
with:
150+
name: ${{ matrix.image }}-publication-${{ github.sha }}
151+
path: ${{ runner.temp }}/${{ matrix.image }}-publication.json
152+
if-no-files-found: error
153+
retention-days: 90

‎AGENTS.md‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -78,6 +78,21 @@ backend-native values and call typed mathematical kernels directly; they must
7878
not invoke `math.run`, construct a capability runtime, or expose MCP,
7979
artifact, provider-loading, or installation objects.
8080

81+
### Mathematical interoperability
82+
83+
Capabilities interoperate through shared, typed domain values and artifacts—not
84+
backend-specific objects, JSON round-trips, or wire encodings. Reuse existing
85+
contract models and typed kernels; add explicit domain-owned conversions when
86+
representations differ. Cover producer-to-consumer compatibility and canonical
87+
or backend-native round trips in tests. Architecture checks must reject internal
88+
JSON round-trips and unsafe canonical conversions.
89+
90+
Canonical decimal strings are wire and persistence values, not computational
91+
values. Use the canonical conversion API before calling backends or constructing
92+
results. Do not directly apply `int()` or `str()` to canonical components or
93+
change `sys.set_int_max_str_digits()` as a workaround. Keep backend coercion in
94+
thin adapters, and test above 4,300 digits whenever the contract permits it.
95+
8196
Keep Pydantic models authoritative at capability, persistence, artifact, and
8297
wire boundaries. Domain implementations and operation factories must preserve
8398
their concrete request, result, and obligation types: do not accept

‎README.md‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@
55
<h1 align="center">Jacobian</h1>
66

77
<p align="center">
8-
<strong>Jacobian gives AI agents reliable mathematical tools that produce evidence an independent checker can verify.</strong>
8+
<strong>Pure mathematics for agents: search for examples and counterexamples, compute exactly, and independently check what a result proves.</strong>
99
</p>
1010

1111
<p align="center">

‎benchmarks/datasets/conjecture-probes-v1/bsd-infinite-order-certificate/tests/verifier_support.py‎

Lines changed: 21 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -68,6 +68,17 @@ def _finite_json_float(value: str) -> float:
6868
return parsed
6969

7070

71+
def _reject_duplicate_keys(pairs: list[tuple[str, Any]]) -> dict[str, Any]:
72+
"""Reject JSON objects with duplicate names at any nesting level."""
73+
74+
seen: set[str] = set()
75+
for key, _ in pairs:
76+
if key in seen:
77+
raise ValueError(f"duplicate JSON object key: {key}")
78+
seen.add(key)
79+
return dict(pairs)
80+
81+
7182
def _load_public_contract(
7283
path: Path = TESTS / "public_contract.json",
7384
) -> dict[str, Any] | None:
@@ -76,6 +87,7 @@ def _load_public_contract(
7687
try:
7788
contract = json.loads(
7889
path.read_text(),
90+
object_pairs_hook=_reject_duplicate_keys,
7991
parse_constant=_reject_nonfinite_json,
8092
parse_float=_finite_json_float,
8193
)
@@ -110,6 +122,7 @@ def load_submission(
110122
try:
111123
value = json.loads(
112124
path.read_text(),
125+
object_pairs_hook=_reject_duplicate_keys,
113126
parse_constant=_reject_nonfinite_json,
114127
parse_float=_finite_json_float,
115128
)
@@ -267,7 +280,10 @@ def read_evidence_json(
267280
if target is None:
268281
return None
269282
try:
270-
value = json.loads(target.read_text())
283+
value = json.loads(
284+
target.read_text(),
285+
object_pairs_hook=_reject_duplicate_keys,
286+
)
271287
except (OSError, ValueError, RecursionError, MemoryError):
272288
return None
273289
return value if isinstance(value, dict) else None
@@ -306,7 +322,10 @@ def authorized_record_is_bound(
306322
expected_path="evidence/verification-record.json",
307323
)
308324
try:
309-
authorized = json.loads(authorized_path.read_text())
325+
authorized = json.loads(
326+
authorized_path.read_text(),
327+
object_pairs_hook=_reject_duplicate_keys,
328+
)
310329
except (OSError, ValueError):
311330
return False
312331
if not isinstance(actual, dict) or not isinstance(authorized, dict):

‎benchmarks/datasets/conjecture-probes-v1/hadamard-order12-construction/tests/verifier_support.py‎

Lines changed: 21 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -68,6 +68,17 @@ def _finite_json_float(value: str) -> float:
6868
return parsed
6969

7070

71+
def _reject_duplicate_keys(pairs: list[tuple[str, Any]]) -> dict[str, Any]:
72+
"""Reject JSON objects with duplicate names at any nesting level."""
73+
74+
seen: set[str] = set()
75+
for key, _ in pairs:
76+
if key in seen:
77+
raise ValueError(f"duplicate JSON object key: {key}")
78+
seen.add(key)
79+
return dict(pairs)
80+
81+
7182
def _load_public_contract(
7283
path: Path = TESTS / "public_contract.json",
7384
) -> dict[str, Any] | None:
@@ -76,6 +87,7 @@ def _load_public_contract(
7687
try:
7788
contract = json.loads(
7889
path.read_text(),
90+
object_pairs_hook=_reject_duplicate_keys,
7991
parse_constant=_reject_nonfinite_json,
8092
parse_float=_finite_json_float,
8193
)
@@ -110,6 +122,7 @@ def load_submission(
110122
try:
111123
value = json.loads(
112124
path.read_text(),
125+
object_pairs_hook=_reject_duplicate_keys,
113126
parse_constant=_reject_nonfinite_json,
114127
parse_float=_finite_json_float,
115128
)
@@ -267,7 +280,10 @@ def read_evidence_json(
267280
if target is None:
268281
return None
269282
try:
270-
value = json.loads(target.read_text())
283+
value = json.loads(
284+
target.read_text(),
285+
object_pairs_hook=_reject_duplicate_keys,
286+
)
271287
except (OSError, ValueError, RecursionError, MemoryError):
272288
return None
273289
return value if isinstance(value, dict) else None
@@ -306,7 +322,10 @@ def authorized_record_is_bound(
306322
expected_path="evidence/verification-record.json",
307323
)
308324
try:
309-
authorized = json.loads(authorized_path.read_text())
325+
authorized = json.loads(
326+
authorized_path.read_text(),
327+
object_pairs_hook=_reject_duplicate_keys,
328+
)
310329
except (OSError, ValueError):
311330
return False
312331
if not isinstance(actual, dict) or not isinstance(authorized, dict):

‎benchmarks/datasets/conjecture-probes-v1/hadwiger-triangle-free-minor-certificate/tests/verifier_support.py‎

Lines changed: 21 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -68,6 +68,17 @@ def _finite_json_float(value: str) -> float:
6868
return parsed
6969

7070

71+
def _reject_duplicate_keys(pairs: list[tuple[str, Any]]) -> dict[str, Any]:
72+
"""Reject JSON objects with duplicate names at any nesting level."""
73+
74+
seen: set[str] = set()
75+
for key, _ in pairs:
76+
if key in seen:
77+
raise ValueError(f"duplicate JSON object key: {key}")
78+
seen.add(key)
79+
return dict(pairs)
80+
81+
7182
def _load_public_contract(
7283
path: Path = TESTS / "public_contract.json",
7384
) -> dict[str, Any] | None:
@@ -76,6 +87,7 @@ def _load_public_contract(
7687
try:
7788
contract = json.loads(
7889
path.read_text(),
90+
object_pairs_hook=_reject_duplicate_keys,
7991
parse_constant=_reject_nonfinite_json,
8092
parse_float=_finite_json_float,
8193
)
@@ -110,6 +122,7 @@ def load_submission(
110122
try:
111123
value = json.loads(
112124
path.read_text(),
125+
object_pairs_hook=_reject_duplicate_keys,
113126
parse_constant=_reject_nonfinite_json,
114127
parse_float=_finite_json_float,
115128
)
@@ -267,7 +280,10 @@ def read_evidence_json(
267280
if target is None:
268281
return None
269282
try:
270-
value = json.loads(target.read_text())
283+
value = json.loads(
284+
target.read_text(),
285+
object_pairs_hook=_reject_duplicate_keys,
286+
)
271287
except (OSError, ValueError, RecursionError, MemoryError):
272288
return None
273289
return value if isinstance(value, dict) else None
@@ -306,7 +322,10 @@ def authorized_record_is_bound(
306322
expected_path="evidence/verification-record.json",
307323
)
308324
try:
309-
authorized = json.loads(authorized_path.read_text())
325+
authorized = json.loads(
326+
authorized_path.read_text(),
327+
object_pairs_hook=_reject_duplicate_keys,
328+
)
310329
except (OSError, ValueError):
311330
return False
312331
if not isinstance(actual, dict) or not isinstance(authorized, dict):

0 commit comments

Comments
 (0)