11// SPDX-License-Identifier: PMPL-1.0-or-later
22// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
33
4- // nesy-solver dev server — Deno (NOT Node) serves static files + stub API.
5- // E3 will replace /api/prove with a proxy to proven-server → echidna :8090.
4+ // nesy-solver dev server — Deno serves static files + proxies the API.
5+ // E3 wires /api/prove and /api/strategy to the V-lang backend
6+ // (proven-nesy-solver-api running on NESY_BACKEND_URL, default :9000),
7+ // which forwards to echidna (:8090) and verisim-api (:8080).
8+ //
9+ // When the backend is unreachable the handlers degrade to a mock response
10+ // with `mock: true` so the frontend never 500s.
611
712import { serveDir } from "@std/http/file-server" ;
813import { join } from "@std/path" ;
914
1015// Default port 8787 to avoid collision with verisim-api (8080) on the dev host.
1116const PORT = Number ( Deno . env . get ( "PORT" ) ?? 8787 ) ;
17+ const BACKEND_URL = Deno . env . get ( "NESY_BACKEND_URL" ) ?? "http://localhost:9000" ;
1218const ROOT = new URL ( "." , import . meta. url ) . pathname ;
1319
14- /**
15- * Mock prove handler. Mirrors echidna /api/verify response shape so the
16- * frontend contract is stable before E3 wires the real backend.
17- *
18- * Request shape: { language, obligationClass, prover, content }
19- * Response shape: { valid, duration_ms, goals_remaining, tactics_used,
20- * prover, strategy_tag, prover_output, mock: true }
21- */
20+ /** POST /api/prove — proxies to V backend /prove, degrades to mock on failure. */
2221async function handleProve ( req ) {
2322 let body ;
2423 try {
@@ -31,42 +30,100 @@ async function handleProve(req) {
3130 return json ( { error : "content required" } , 400 ) ;
3231 }
3332
34- // Deterministic mock: "valid" iff content references `check-sat`, `Qed`, `refl`, `Refl`, or `by`.
33+ try {
34+ const resp = await fetch ( `${ BACKEND_URL } , {
35+ method : "POST" ,
36+ headers : { "Content-Type" : "application/json" } ,
37+ body : JSON . stringify ( { language, obligationClass, prover, content } ) ,
38+ signal : AbortSignal . timeout ( 30_000 ) ,
39+ } ) ;
40+ const bodyText = await resp . text ( ) ;
41+ return new Response ( bodyText , {
42+ status : resp . status ,
43+ headers : {
44+ "Content-Type" : "application/json; charset=utf-8" ,
45+ "Access-Control-Allow-Origin" : "*" ,
46+ } ,
47+ } ) ;
48+ } catch ( err ) {
49+ console . warn ( `backend unreachable: ${ err . message } ) ;
50+ return json ( mockProveResponse ( { language, obligationClass, prover, content } ) ) ;
51+ }
52+ }
53+
54+ /** GET /api/strategy?class=safety — proxies to V backend /strategy/:class. */
55+ async function handleStrategy ( req ) {
56+ const url = new URL ( req . url ) ;
57+ const cls = url . searchParams . get ( "class" ) ?? "safety" ;
58+ try {
59+ const resp = await fetch ( `${ BACKEND_URL } ${ encodeURIComponent ( cls ) } , {
60+ signal : AbortSignal . timeout ( 10_000 ) ,
61+ } ) ;
62+ const bodyText = await resp . text ( ) ;
63+ return new Response ( bodyText , {
64+ status : resp . status ,
65+ headers : {
66+ "Content-Type" : "application/json; charset=utf-8" ,
67+ "Access-Control-Allow-Origin" : "*" ,
68+ } ,
69+ } ) ;
70+ } catch ( err ) {
71+ console . warn ( `backend unreachable: ${ err . message } ) ;
72+ return json ( {
73+ mock : true ,
74+ obligation_class : cls ,
75+ recommendations : [ { prover : "z3" , success_rate : 0 , avg_duration_ms : 0 , total_attempts : 0 } ] ,
76+ } ) ;
77+ }
78+ }
79+
80+ /** GET /api/health — aggregates frontend + backend health. */
81+ async function handleHealth ( ) {
82+ let backend = null ;
83+ try {
84+ const resp = await fetch ( `${ BACKEND_URL } , { signal : AbortSignal . timeout ( 3_000 ) } ) ;
85+ if ( resp . ok ) backend = await resp . json ( ) ;
86+ } catch ( _err ) {
87+ backend = { reachable : false , url : BACKEND_URL } ;
88+ }
89+ return json ( {
90+ status : "ok" ,
91+ version : "0.1.0" ,
92+ frontend_port : PORT ,
93+ backend_url : BACKEND_URL ,
94+ backend,
95+ } ) ;
96+ }
97+
98+ /** Mock prove response used when the V backend is unreachable. */
99+ function mockProveResponse ( { language, obligationClass, prover, content } ) {
35100 const valid = / c h e c k - s a t | Q e d | r e f l | R e f l | b y \s / . test ( content ) ;
36101 const resolvedProver = prover === "auto" ? pickProver ( obligationClass , language ) : prover ;
37102 const duration_ms = 20 + Math . floor ( Math . random ( ) * 80 ) ;
38-
39- return json ( {
103+ return {
40104 valid,
105+ outcome : valid ? "success" : "failure" ,
106+ prover : resolvedProver ,
41107 duration_ms,
42108 goals_remaining : valid ? 0 : 1 ,
43109 tactics_used : valid ? 3 : 0 ,
44- prover : resolvedProver ,
45110 obligation_class : obligationClass ,
46111 language,
47112 strategy_tag : "mock-handler" ,
48113 prover_output : valid
49114 ? `; ${ resolvedProver } ${ content . split ( "\n" ) . length }
50- : `; ${ resolvedProver } ,
115+ : `; ${ resolvedProver } ${ BACKEND_URL } ,
116+ attempt_id : null ,
117+ recorded : false ,
51118 mock : true ,
52- } ) ;
119+ } ;
53120}
54121
55- /** Crude strategy fallback — replaced in E3 by verisim-api /strategy query. */
56122function pickProver ( obligationClass , language ) {
57- const byLang = {
58- smtlib : "Z3" ,
59- lean : "Lean" ,
60- coq : "Coq" ,
61- idris2 : "Idris2" ,
62- agda : "Agda" ,
63- } ;
123+ const byLang = { smtlib : "Z3" , lean : "Lean" , coq : "Coq" , idris2 : "Idris2" , agda : "Agda" } ;
64124 const byClass = {
65- safety : "Z3" ,
66- linearity : "Idris2" ,
67- termination : "Agda" ,
68- equiv : "Lean" ,
69- correctness : "Coq" ,
125+ safety : "Z3" , linearity : "Idris2" , termination : "Agda" ,
126+ equiv : "Lean" , correctness : "Coq" ,
70127 } ;
71128 return byClass [ obligationClass ] ?? byLang [ language ] ?? "Z3" ;
72129}
@@ -81,29 +138,13 @@ function json(payload, status = 200) {
81138 } ) ;
82139}
83140
84- /** Serves index.html at root, static files for /public/*, and API for /api/*. */
85141async function handler ( req ) {
86142 const url = new URL ( req . url ) ;
87143
88- if ( url . pathname === "/api/prove" && req . method === "POST" ) {
89- return handleProve ( req ) ;
90- }
91- if ( url . pathname === "/api/health" && req . method === "GET" ) {
92- return json ( { status : "ok" , version : "0.1.0" , mode : "mock" } ) ;
93- }
94- if ( url . pathname === "/api/strategy" && req . method === "GET" ) {
95- // Mock strategy data — E3 proxies verisim-api /api/v1/proof_attempts/strategy
96- return json ( {
97- mock : true ,
98- classes : {
99- safety : { top : "Z3" , success_rate : 0.92 , n : 24 } ,
100- linearity : { top : "Idris2" , success_rate : 0.78 , n : 9 } ,
101- termination : { top : "Agda" , success_rate : 0.71 , n : 7 } ,
102- } ,
103- } ) ;
104- }
144+ if ( url . pathname === "/api/prove" && req . method === "POST" ) return handleProve ( req ) ;
145+ if ( url . pathname === "/api/strategy" && req . method === "GET" ) return handleStrategy ( req ) ;
146+ if ( url . pathname === "/api/health" && req . method === "GET" ) return handleHealth ( ) ;
105147
106- // Static files
107148 if ( url . pathname === "/" || url . pathname === "/index.html" ) {
108149 const html = await Deno . readTextFile ( join ( ROOT , "index.html" ) ) ;
109150 return new Response ( html , {
@@ -114,5 +155,5 @@ async function handler(req) {
114155}
115156
116157console . log ( `nesy-solver dev server listening on http://localhost:${ PORT } ) ;
117- console . log ( ` mode: mock (echidna backend wires in E3) ` ) ;
158+ console . log ( ` backend: ${ BACKEND_URL } ) ;
118159Deno . serve ( { port : PORT } , handler ) ;
0 commit comments