Skip to content

refactor: semantic port TS to AffineScript #110

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
hyperpolymath merged 1 commit into from
Aug 24, 2026
+68 −80
Merged

refactor: semantic port TS to AffineScript #110

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 3 additions & 7 deletions scripts/bundle.affine
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,11 +1,8 @@
// SPDX-License-Identifier: MPL-2.0
// Ported via Harvard Engine mechanical processor
// Ported via Harvard Engine (Semantic pass)

module bundle;

// TODO: Complete semantic implementation

/* === ORIGINAL TYPESCRIPT CONTEXT ===
// SPDX-License-Identifier: MPL-2.0
// esbuild bundler for PanLL — resolves bare npm specifiers that WebKitGTK
// cannot handle via import maps.
Expand All @@ -16,9 +13,9 @@ module bundle;

import * as esbuild from "npm:esbuild@0.24";

const watch = Deno.args.includes("--watch");
let watch = Deno.args.includes("--watch");

const ctx = await esbuild.context({
let ctx = await esbuild.context({
entryPoints: ["src/App.res.js"],
bundle: true,
format: "esm",
Expand All @@ -40,4 +37,3 @@ if (watch) {
await ctx.dispose();
}

==================================== */
16 changes: 6 additions & 10 deletions scripts/dev-server.affine
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,11 +1,8 @@
// SPDX-License-Identifier: MPL-2.0
// Ported via Harvard Engine mechanical processor
// Ported via Harvard Engine (Semantic pass)

module dev-server;

// TODO: Complete semantic implementation

/* === ORIGINAL TYPESCRIPT CONTEXT ===
// SPDX-License-Identifier: MPL-2.0
// Deno static file server for PanLL dev mode — replaces python3 http.server
//
Expand All @@ -18,21 +15,21 @@ module dev-server;

import { serveDir } from "jsr:@std/http@1/file-server";

const port = 8000;
let port = 8000;

// Allowlist of file extensions the dev server will serve.
// Anything not matching gets a 403.
const ALLOWED_EXTENSIONS = new Set([
let ALLOWED_EXTENSIONS = new Set([
".html", ".css", ".js", ".mjs", ".ts",
".json", ".map",
".png", ".jpg", ".jpeg", ".gif", ".svg", ".ico", ".webp",
".woff", ".woff2", ".ttf", ".eot",
]);

function isAllowedPath(pathname: string): boolean {
fn isAllowedPath(pathname: string): boolean {
// Allow directory paths (trailing slash) — needed for index.html resolution
if (pathname.endsWith("/")) return true;
const dot = pathname.lastIndexOf(".");
let dot = pathname.lastIndexOf(".");
if (dot === -1) return false;
return ALLOWED_EXTENSIONS.has(pathname.slice(dot).toLowerCase());
}
Expand All @@ -41,7 +38,7 @@ Deno.serve({ port, hostname: "127.0.0.1", onListen: () => {
console.log(`PanLL dev server: http://localhost:${port}/public/`);
console.log("Serving project root (filtered by extension allowlist)");
}}, (req: Request) => {
const url = new URL(req.url);
let url = new URL(req.url);

if (!isAllowedPath(url.pathname)) {
return new Response("403 Forbidden\n", { status: 403 });
Expand All @@ -50,4 +47,3 @@ Deno.serve({ port, hostname: "127.0.0.1", onListen: () => {
return serveDir(req, { fsRoot: ".", quiet: true });
});

==================================== */
122 changes: 59 additions & 63 deletions scripts/mock-echidna.affine
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,11 +1,8 @@
// SPDX-License-Identifier: MPL-2.0
// Ported via Harvard Engine mechanical processor
// Ported via Harvard Engine (Semantic pass)

module mock-echidna;

// TODO: Complete semantic implementation

/* === ORIGINAL TYPESCRIPT CONTEXT ===
// SPDX-License-Identifier: MPL-2.0

/// Mock ECHIDNA REST Server for PanLL development.
Expand All @@ -21,7 +18,7 @@ module mock-echidna;
// Types
// ---------------------------------------------------------------------------

interface ProofSession {
struct ProofSession {
id: string;
prover: string;
goal: string;
Expand All @@ -35,7 +32,7 @@ interface ProofSession {
created_at: number;
}

interface TacticScenario {
struct TacticScenario {
initial_goals: string[];
tactics: Record<string, { removes_goal: number; description: string }>;
suggestions: Array<{
Expand All @@ -51,7 +48,7 @@ interface TacticScenario {
// Demo data — prover catalog
// ---------------------------------------------------------------------------

const PROVERS = [
let PROVERS = [
{ name: "coq", tier: "ITP", complexity: "high" },
{ name: "lean4", tier: "ITP", complexity: "high" },
{ name: "z3", tier: "SMT", complexity: "medium" },
Expand Down Expand Up @@ -114,7 +111,7 @@ const SCENARIOS: Array<{ match: string; scenario: TacticScenario }> = [
},
];

/// Fallback scenario for goals that don't match any built-in pattern.
/// Fallback scenario for goals that don't match unknown built-in pattern.
const DEFAULT_SCENARIO: TacticScenario = {
initial_goals: ["Goal 1: primary obligation", "Goal 2: secondary obligation"],
tactics: {
Expand All @@ -134,7 +131,7 @@ const DEFAULT_SCENARIO: TacticScenario = {
// Demo data — theorem search corpus
// ---------------------------------------------------------------------------

const THEOREM_CORPUS = [
let THEOREM_CORPUS = [
{ name: "Nat.add_zero_r", statement: "forall n : nat, n + 0 = n", prover: "coq", tags: ["arithmetic", "identity"] },
{ name: "Nat.add_comm", statement: "forall n m : nat, n + m = m + n", prover: "coq", tags: ["arithmetic", "commutativity"] },
{ name: "Nat.add_assoc", statement: "forall n m p : nat, n + (m + p) = (n + m) + p", prover: "coq", tags: ["arithmetic", "associativity"] },
Expand All @@ -149,16 +146,16 @@ const THEOREM_CORPUS = [
// Session store
// ---------------------------------------------------------------------------

const sessions = new Map<string, ProofSession>();
let sessions = new Map<string, ProofSession>();

/// Generate a UUID-like session identifier.
function generateSessionId(): string {
const hex = () => Math.random().toString(16).slice(2, 6);
fn generateSessionId(): string {
let hex = () => Math.random().toString(16).slice(2, 6);
return `sess-${hex()}-${hex()}-${hex()}`;
}

/// Find the matching proof scenario for a goal string.
function findScenario(goal: string): TacticScenario {
fn findScenario(goal: string): TacticScenario {
for (const entry of SCENARIOS) {
if (goal.includes(entry.match)) {
return entry.scenario;
Expand All @@ -168,8 +165,8 @@ function findScenario(goal: string): TacticScenario {
}

/// Simulate network latency (200-500ms).
function randomDelay(): Promise<void> {
const ms = 200 + Math.floor(Math.random() * 300);
fn randomDelay(): void {
let ms = 200 + Math.floor(Math.random() * 300);
return new Promise((resolve) => setTimeout(resolve, ms));
}

Expand All @@ -179,27 +176,27 @@ function randomDelay(): Promise<void> {

/// GET /api/v1/health — server health check.
/// Returns a plain string (the parser expects raw text, not structured JSON).
function handleHealth(): Response {
fn handleHealth(): Response {
return new Response("ECHIDNA 1.5.0-mock (PanLL development server)", {
headers: { "Content-Type": "text/plain" },
});
}

/// GET /api/v1/provers — list available prover backends.
function handleListProvers(): Response {
fn handleListProvers(): Response {
return Response.json(PROVERS);
}

/// POST /api/v1/prove — dispatch a proof obligation to the solver portfolio.
async function handleProve(req: Request): Promise<Response> {
async fn handleProve(req: Request): Response {
await randomDelay();
const body = await req.json();
const goal = body.content ?? body.goal ?? "";
const prover = body.prover ?? "z3";
let body = await req.json();
let goal = body.content ?? body.goal ?? "";
let prover = body.prover ?? "z3";

const hasAxiomRisk = goal.includes("believe_me") || goal.includes("Admitted") || goal.includes("sorry");
const trustLevel = hasAxiomRisk ? 1 : 4;
const dangerLevel = hasAxiomRisk ? "reject" : "safe";
let hasAxiomRisk = goal.includes("believe_me") || goal.includes("Admitted") || goal.includes("sorry");
let trustLevel = hasAxiomRisk ? 1 : 4;
let dangerLevel = hasAxiomRisk ? "reject" : "safe";

return Response.json({
verified: !hasAxiomRisk,
Expand All @@ -217,17 +214,17 @@ async function handleProve(req: Request): Promise<Response> {
}

/// POST /api/v1/verify — verify an existing proof (same shape as prove).
async function handleVerify(req: Request): Promise<Response> {
async fn handleVerify(req: Request): Response {
return handleProve(req);
}

/// GET /api/v1/search?q=... — search the theorem corpus.
function handleSearch(url: URL): Response {
const query = (url.searchParams.get("q") ?? "").toLowerCase();
fn handleSearch(url: URL): Response {
let query = (url.searchParams.get("q") ?? "").toLowerCase();
if (!query) {
return Response.json([]);
}
const matches = THEOREM_CORPUS.filter(
let matches = THEOREM_CORPUS.filter(
(t) =>
t.name.toLowerCase().includes(query) ||
t.statement.toLowerCase().includes(query) ||
Expand All @@ -237,13 +234,13 @@ function handleSearch(url: URL): Response {
}

/// POST /api/v1/proofs — create a new interactive proof session.
async function handleCreateSession(req: Request): Promise<Response> {
async fn handleCreateSession(req: Request): Response {
await randomDelay();
const body = await req.json();
const goal = body.goal ?? "";
const prover = body.prover ?? "coq";
const scenario = findScenario(goal);
const sessionId = generateSessionId();
let body = await req.json();
let goal = body.goal ?? "";
let prover = body.prover ?? "coq";
let scenario = findScenario(goal);
let sessionId = generateSessionId();

const session: ProofSession = {
id: sessionId,
Expand All @@ -264,8 +261,8 @@ async function handleCreateSession(req: Request): Promise<Response> {
}

/// GET /api/v1/proofs/:id — get current session state.
function handleGetSession(sessionId: string): Response {
const session = sessions.get(sessionId);
fn handleGetSession(sessionId: string): Response {
let session = sessions.get(sessionId);
if (!session) {
return Response.json(
{ error: `Session ${sessionId} not found` },
Expand All @@ -276,27 +273,27 @@ function handleGetSession(sessionId: string): Response {
}

/// POST /api/v1/proofs/:id/tactics — apply a tactic to the session.
async function handleApplyTactic(
async fn handleApplyTactic(
sessionId: string,
req: Request,
): Promise<Response> {
): Response {
await randomDelay();
const session = sessions.get(sessionId);
let session = sessions.get(sessionId);
if (!session) {
return Response.json(
{ success: false, proof_state: { id: "", prover: "", goal: "", status: "error", goals: [], proof_script: [], complete: false, tactics_applied: [], time_elapsed: 0, error_message: `Session ${sessionId} not found` } },
{ status: 404 },
);
}

const body = await req.json();
const tacticName = body.name ?? body.tactic ?? "auto";
let body = await req.json();
let tacticName = body.name ?? body.tactic ?? "auto";
const tacticArgs: string[] = body.args ?? [];
const fullTactic = tacticArgs.length > 0 ? `${tacticName} ${tacticArgs.join(" ")}` : tacticName;
let fullTactic = tacticArgs.length > 0 ? `${tacticName} ${tacticArgs.join(" ")}` : tacticName;

// Look up the scenario for this session's goal
const scenario = findScenario(session.goal);
const tacticEntry = scenario.tactics[fullTactic] ?? scenario.tactics[tacticName];
let scenario = findScenario(session.goal);
let tacticEntry = scenario.tactics[fullTactic] ?? scenario.tactics[tacticName];

session.tactics_applied.push(fullTactic);
session.proof_script.push(fullTactic + ".");
Expand All @@ -305,7 +302,7 @@ async function handleApplyTactic(

if (tacticEntry && tacticEntry.removes_goal >= 0 && session.goals.length > 0) {
// Remove the specified goal (clamped to valid index)
const idx = Math.min(tacticEntry.removes_goal, session.goals.length - 1);
let idx = Math.min(tacticEntry.removes_goal, session.goals.length - 1);
session.goals.splice(idx, 1);
}

Expand All @@ -322,17 +319,17 @@ async function handleApplyTactic(
}

/// GET /api/v1/proofs/:id/tactics/suggest?limit=N — tactic suggestions.
function handleSuggestTactics(sessionId: string, url: URL): Response {
const session = sessions.get(sessionId);
fn handleSuggestTactics(sessionId: string, url: URL): Response {
let session = sessions.get(sessionId);
if (!session) {
return Response.json([], { status: 404 });
}

const limit = parseInt(url.searchParams.get("limit") ?? "5", 10);
const scenario = findScenario(session.goal);
let limit = parseInt(url.searchParams.get("limit") ?? "5", 10);
let scenario = findScenario(session.goal);

// Filter out tactics already applied, then take up to limit
const available = scenario.suggestions.filter(
let available = scenario.suggestions.filter(
(s) => !session.tactics_applied.includes(s.name) &&
!session.tactics_applied.includes(`${s.name} ${s.args.join(" ")}`.trim()),
);
Expand All @@ -346,13 +343,13 @@ function handleSuggestTactics(sessionId: string, url: URL): Response {

/// Route an incoming request to the appropriate handler.
/// All paths are under /api/v1/.
async function handleRequest(req: Request): Promise<Response> {
const url = new URL(req.url);
const path = url.pathname;
const method = req.method;
async fn handleRequest(req: Request): Response {
let url = new URL(req.url);
let path = url.pathname;
let method = req.method;

// CORS headers for Tauri webview requests
const corsHeaders = {
let corsHeaders = {
"Access-Control-Allow-Origin": "*",
"Access-Control-Allow-Methods": "GET, POST, OPTIONS",
"Access-Control-Allow-Headers": "Content-Type",
Expand Down Expand Up @@ -392,9 +389,9 @@ async function handleRequest(req: Request): Promise<Response> {

// Session and tactic routes: /api/v1/proofs/:id/...
} else if (path.startsWith("/api/v1/proofs/")) {
const rest = path.slice("/api/v1/proofs/".length);
const segments = rest.split("/").filter(Boolean);
const sessionId = segments[0];
let rest = path.slice("/api/v1/proofs/".length);
let segments = rest.split("/").filter(Boolean);
let sessionId = segments[0];

if (!sessionId) {
response = Response.json({ error: "Missing session ID" }, { status: 400 });
Expand All @@ -419,7 +416,7 @@ async function handleRequest(req: Request): Promise<Response> {
response = Response.json({ error: `Unknown route: ${method} ${path}` }, { status: 404 });
}
} catch (err) {
const message = err instanceof Error ? err.message : String(err);
let message = err instanceof Error ? err.message : String(err);
console.error(`[ECHIDNA-MOCK] Error handling ${method} ${path}: ${message}`);
response = Response.json({ error: message }, { status: 500 });
}
Expand All @@ -430,8 +427,8 @@ async function handleRequest(req: Request): Promise<Response> {
}

// Log the request
const status = response.status;
const sessionCount = sessions.size;
let status = response.status;
let sessionCount = sessions.size;
console.log(`[ECHIDNA-MOCK] ${method} ${path} -> ${status} (${sessionCount} active sessions)`);

return response;
Expand All @@ -441,7 +438,7 @@ async function handleRequest(req: Request): Promise<Response> {
// Server entry point
// ---------------------------------------------------------------------------

const PORT = 9000;
let PORT = 9000;

console.log(`
╔══════════════════════════════════════════════════════╗
Expand All @@ -468,4 +465,3 @@ console.log(`

Deno.serve({ port: PORT, hostname: "127.0.0.1" }, handleRequest);

==================================== */
Loading