Stabilize remote proof endpoint and RDS shims

.mcp.json

@@ -66,7 +66,7 @@
         "4-Infrastructure/infra/remote_lean_proof_mcp.py"
       ],
       "env": {
-        "PROOF_SERVER_URL": "http://75.101.199.58:8787",
+        "PROOF_SERVER_URL": "http://54.236.176.28:8787",
         "PROOF_SERVER_TOKEN_FILE": "/home/allaun/.config/ene/language-proof-server.token"
       }
     },

.vscode/settings.json

@@ -61,7 +61,7 @@
         "shared-data": true
     },
     "git.ignoreLimitWarning": true,
-    "remoteLeanProof.url": "http://75.101.199.58:8787",
+    "remoteLeanProof.url": "http://54.236.176.28:8787",
     "remoteLeanProof.tokenFile": "/home/allaun/.config/ene/language-proof-server.token",
     "remoteLeanProof.checkOnSave": true,
     "remoteLeanProof.checkOnOpen": true,

4-Infrastructure/infra/remote_lean_proof_mcp.py

@@ -14,7 +14,7 @@ from typing import Any
 
 SERVER_NAME = "remote-lean-proof"
 SERVER_VERSION = "0.1.0"
-DEFAULT_URL = "http://75.101.199.58:8787"
+DEFAULT_URL = "http://54.236.176.28:8787"
 DEFAULT_TOKEN_FILE = Path.home() / ".config/ene/language-proof-server.token"
 
 

4-Infrastructure/shim/batch_embed_artifacts.py

@@ -0,0 +1,235 @@
+#!/usr/bin/env python3
+"""Batch-embed ENE artifacts missing embeddings and emit a JSON receipt."""
+
+from __future__ import annotations
+
+import argparse
+import hashlib
+import json
+import os
+import subprocess
+import sys
+import time
+from datetime import datetime, timezone
+from pathlib import Path
+from typing import Any
+from urllib import request
+
+BATCH_SIZE = 50
+TOKEN_REFRESH_SEC = 600
+
+HOST = os.environ.get("RDS_HOST", "database-1-instance-1.cghu8yqogqwo.us-east-1.rds.amazonaws.com")
+PORT = int(os.environ.get("RDS_PORT", "5432"))
+USER = os.environ.get("RDS_USER", "postgres")
+DB = os.environ.get("RDS_DB", os.environ.get("RDS_DBNAME", "postgres"))
+AWS_REGION = os.environ.get("AWS_REGION", "us-east-1")
+
+OLLAMA_URL = os.environ.get("OLLAMA_URL", "http://100.85.244.73:11434").rstrip("/")
+EMBED_MODEL = os.environ.get("EMBED_MODEL", "nomic-embed-text")
+
+
+def utc_now() -> str:
+    return datetime.now(timezone.utc).isoformat()
+
+
+def sha256_text(text: str) -> str:
+    return hashlib.sha256(text.encode("utf-8")).hexdigest()
+
+
+def get_token() -> str:
+    return subprocess.check_output(
+        [
+            "aws",
+            "rds",
+            "generate-db-auth-token",
+            "--region",
+            AWS_REGION,
+            "--hostname",
+            HOST,
+            "--port",
+            str(PORT),
+            "--username",
+            USER,
+        ],
+        text=True,
+        stdin=subprocess.DEVNULL,
+    ).strip()
+
+
+def get_password() -> str:
+    if os.environ.get("RDS_IAM", "1") == "1":
+        return get_token()
+    password = os.environ.get("RDS_PASSWORD")
+    if not password:
+        raise RuntimeError("RDS_PASSWORD is required when RDS_IAM=0")
+    return password
+
+
+def get_conn(password: str):
+    import psycopg2
+
+    return psycopg2.connect(
+        host=HOST,
+        port=PORT,
+        user=USER,
+        password=password,
+        dbname=DB,
+        sslmode="require",
+        connect_timeout=10,
+    )
+
+
+def fetch_batch(cur, batch_size: int) -> list[tuple[Any, str, str]]:
+    cur.execute(
+        "SELECT id, path, content FROM ene.artifacts "
+        "WHERE embedding IS NULL AND content IS NOT NULL AND content != '' "
+        "AND kind NOT IN ('verilog', 'shader', 'schema', 'binary') "
+        "ORDER BY path LIMIT %s",
+        (batch_size,),
+    )
+    return cur.fetchall()
+
+
+def generate_embedding(text: str) -> list[float] | None:
+    payload = json.dumps({"model": EMBED_MODEL, "prompt": text[:2048]}).encode("utf-8")
+    req = request.Request(
+        f"{OLLAMA_URL}/api/embeddings",
+        data=payload,
+        headers={"Content-Type": "application/json"},
+    )
+    with request.urlopen(req, timeout=30) as resp:
+        data = json.loads(resp.read())
+    embedding = data.get("embedding")
+    if not isinstance(embedding, list):
+        return None
+    return embedding
+
+
+def pgvector_literal(values: list[float]) -> str:
+    return "[" + ",".join(format(value, ".16g") for value in values) + "]"
+
+
+def build_receipt(
+    *,
+    started_at: str,
+    processed: int,
+    embedded: int,
+    failed: list[dict[str, str]],
+    dry_run: bool,
+    limit: int | None,
+    duration_sec: float,
+) -> dict[str, Any]:
+    receipt: dict[str, Any] = {
+        "schema": "ene_artifact_embedding_batch_receipt_v1",
+        "version": "1.0.0",
+        "generated_at_utc": utc_now(),
+        "started_at_utc": started_at,
+        "duration_ms": int(duration_sec * 1000),
+        "dry_run": dry_run,
+        "limit": limit,
+        "rds_host": HOST,
+        "rds_db": DB,
+        "ollama_url": OLLAMA_URL,
+        "embed_model": EMBED_MODEL,
+        "processed_count": processed,
+        "embedded_count": embedded,
+        "failed_count": len(failed),
+        "failures": failed[:20],
+    }
+    preimage = {k: v for k, v in receipt.items() if k != "receipt_hash"}
+    receipt["receipt_hash"] = sha256_text(json.dumps(preimage, sort_keys=True))
+    return receipt
+
+
+def write_receipt(receipt: dict[str, Any], path: str | None) -> None:
+    encoded = json.dumps(receipt, sort_keys=True)
+    print(encoded)
+    if path:
+        out = Path(path)
+        out.parent.mkdir(parents=True, exist_ok=True)
+        out.write_text(encoded + "\n", encoding="utf-8")
+
+
+def parse_args() -> argparse.Namespace:
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument("--batch-size", type=int, default=BATCH_SIZE)
+    parser.add_argument("--limit", type=int, default=None)
+    parser.add_argument("--dry-run", action="store_true")
+    parser.add_argument("--receipt-out")
+    return parser.parse_args()
+
+
+def main() -> int:
+    args = parse_args()
+    if args.batch_size <= 0:
+        raise SystemExit("--batch-size must be positive")
+
+    started_at = utc_now()
+    started = time.time()
+    password = get_password()
+    next_refresh = time.time() + TOKEN_REFRESH_SEC
+    conn = get_conn(password)
+    cur = conn.cursor()
+    processed = 0
+    embedded = 0
+    failed: list[dict[str, str]] = []
+    attempted_ids: set[str] = set()
+
+    try:
+        rows = fetch_batch(cur, args.batch_size)
+        while rows and (args.limit is None or processed < args.limit):
+            rows = [row for row in rows if str(row[0]) not in attempted_ids]
+            if not rows:
+                break
+
+            if os.environ.get("RDS_IAM", "1") == "1" and time.time() > next_refresh:
+                password = get_password()
+                conn.close()
+                conn = get_conn(password)
+                cur = conn.cursor()
+                next_refresh = time.time() + TOKEN_REFRESH_SEC
+
+            for aid, path, content in rows:
+                if args.limit is not None and processed >= args.limit:
+                    break
+                attempted_ids.add(str(aid))
+                processed += 1
+                try:
+                    if args.dry_run:
+                        continue
+                    embedding = generate_embedding(content)
+                    if not embedding:
+                        failed.append({"path": path, "error": "embedding response missing vector"})
+                        continue
+                    cur.execute(
+                        "UPDATE ene.artifacts SET embedding = %s::vector WHERE id = %s",
+                        (pgvector_literal(embedding), aid),
+                    )
+                    embedded += 1
+                except Exception as exc:  # noqa: BLE001 - receipt records per-row failure.
+                    failed.append({"path": path, "error": str(exc)})
+
+            if args.dry_run:
+                conn.rollback()
+            else:
+                conn.commit()
+            rows = fetch_batch(cur, args.batch_size)
+    finally:
+        cur.close()
+        conn.close()
+
+    receipt = build_receipt(
+        started_at=started_at,
+        processed=processed,
+        embedded=embedded,
+        failed=failed,
+        dry_run=args.dry_run,
+        limit=args.limit,
+        duration_sec=time.time() - started,
+    )
+    write_receipt(receipt, args.receipt_out)
+    return 0 if not failed else 2
+
+
+if __name__ == "__main__":
+    sys.exit(main())

4-Infrastructure/shim/sync_wiki_to_rds.py

@@ -0,0 +1,191 @@
+#!/usr/bin/env python3
+"""Sync filesystem wiki Markdown files to ENE RDS and emit a JSON receipt."""
+
+from __future__ import annotations
+
+import argparse
+import hashlib
+import json
+import os
+import subprocess
+import sys
+from datetime import datetime, timezone
+from pathlib import Path
+from typing import Any
+
+STACK_ROOT = Path(os.environ.get("STACK_ROOT", "/home/allaun/Research Stack"))
+WIKI_ROOT = Path(os.environ.get("WIKI_ROOT", str(STACK_ROOT / "6-Documentation" / "wiki")))
+
+HOST = os.environ.get("RDS_HOST", "database-1-instance-1.cghu8yqogqwo.us-east-1.rds.amazonaws.com")
+PORT = int(os.environ.get("RDS_PORT", "5432"))
+USER = os.environ.get("RDS_USER", "postgres")
+DB = os.environ.get("RDS_DB", os.environ.get("RDS_DBNAME", "postgres"))
+AWS_REGION = os.environ.get("AWS_REGION", "us-east-1")
+
+
+def utc_now() -> str:
+    return datetime.now(timezone.utc).isoformat()
+
+
+def sha256_text(text: str) -> str:
+    return hashlib.sha256(text.encode("utf-8")).hexdigest()
+
+
+def get_iam_token() -> str:
+    return subprocess.check_output(
+        [
+            "aws",
+            "rds",
+            "generate-db-auth-token",
+            "--region",
+            AWS_REGION,
+            "--hostname",
+            HOST,
+            "--port",
+            str(PORT),
+            "--username",
+            USER,
+        ],
+        text=True,
+        stdin=subprocess.DEVNULL,
+    ).strip()
+
+
+def get_password() -> str:
+    if os.environ.get("RDS_IAM", "1") == "1":
+        return get_iam_token()
+    password = os.environ.get("RDS_PASSWORD")
+    if not password:
+        raise RuntimeError("RDS_PASSWORD is required when RDS_IAM=0")
+    return password
+
+
+def get_conn():
+    import psycopg2
+
+    return psycopg2.connect(
+        host=HOST,
+        port=PORT,
+        user=USER,
+        password=get_password(),
+        dbname=DB,
+        sslmode="require",
+        connect_timeout=10,
+    )
+
+
+def title_from_slug(slug: str) -> str:
+    return slug.replace("-", " ").replace("_", " ").title()
+
+
+def iter_markdown_files(root: Path) -> list[Path]:
+    if not root.exists():
+        raise FileNotFoundError(f"wiki root does not exist: {root}")
+    return sorted(path for path in root.rglob("*.md") if path.is_file())
+
+
+def sync_files(conn, files: list[Path], dry_run: bool) -> tuple[int, int, list[dict[str, str]]]:
+    indexed = 0
+    skipped = 0
+    failures: list[dict[str, str]] = []
+    cur = conn.cursor()
+    try:
+        for fpath in files:
+            try:
+                rel = fpath.relative_to(WIKI_ROOT)
+                slug = rel.with_suffix("").as_posix()
+                title = title_from_slug(slug)
+                content = fpath.read_text(encoding="utf-8", errors="replace")
+
+                cur.execute("SELECT content FROM ene.wiki_pages WHERE slug = %s", (slug,))
+                row = cur.fetchone()
+                if row and row[0] == content:
+                    skipped += 1
+                    continue
+
+                if not dry_run:
+                    cur.execute(
+                        """INSERT INTO ene.wiki_pages (slug, title, content, updated_at)
+                           VALUES (%s, %s, %s, %s)
+                           ON CONFLICT (slug) DO UPDATE SET
+                             title = EXCLUDED.title,
+                             content = EXCLUDED.content,
+                             updated_at = EXCLUDED.updated_at""",
+                        (slug, title, content, utc_now()),
+                    )
+                indexed += 1
+            except Exception as exc:  # noqa: BLE001 - receipt records per-file failure.
+                failures.append({"path": str(fpath), "error": str(exc)})
+        if dry_run:
+            conn.rollback()
+        else:
+            conn.commit()
+    finally:
+        cur.close()
+    return indexed, skipped, failures
+
+
+def build_receipt(
+    *,
+    indexed: int,
+    skipped: int,
+    failures: list[dict[str, str]],
+    dry_run: bool,
+    file_count: int,
+) -> dict[str, Any]:
+    receipt: dict[str, Any] = {
+        "schema": "ene_wiki_to_rds_sync_receipt_v1",
+        "version": "1.0.0",
+        "generated_at_utc": utc_now(),
+        "dry_run": dry_run,
+        "wiki_root": str(WIKI_ROOT),
+        "rds_host": HOST,
+        "rds_db": DB,
+        "file_count": file_count,
+        "indexed_count": indexed,
+        "skipped_count": skipped,
+        "failed_count": len(failures),
+        "failures": failures[:20],
+    }
+    preimage = {k: v for k, v in receipt.items() if k != "receipt_hash"}
+    receipt["receipt_hash"] = sha256_text(json.dumps(preimage, sort_keys=True))
+    return receipt
+
+
+def write_receipt(receipt: dict[str, Any], path: str | None) -> None:
+    encoded = json.dumps(receipt, sort_keys=True)
+    print(encoded)
+    if path:
+        out = Path(path)
+        out.parent.mkdir(parents=True, exist_ok=True)
+        out.write_text(encoded + "\n", encoding="utf-8")
+
+
+def parse_args() -> argparse.Namespace:
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument("--dry-run", action="store_true")
+    parser.add_argument("--receipt-out")
+    return parser.parse_args()
+
+
+def main() -> int:
+    args = parse_args()
+    files = iter_markdown_files(WIKI_ROOT)
+    conn = get_conn()
+    try:
+        indexed, skipped, failures = sync_files(conn, files, args.dry_run)
+    finally:
+        conn.close()
+    receipt = build_receipt(
+        indexed=indexed,
+        skipped=skipped,
+        failures=failures,
+        dry_run=args.dry_run,
+        file_count=len(files),
+    )
+    write_receipt(receipt, args.receipt_out)
+    return 0 if not failures else 2
+
+
+if __name__ == "__main__":
+    sys.exit(main())