Spaces:
Sleeping
Sleeping
mike dupont commited on
Commit ·
858cd8d
1
Parent(s): be69792
LMFDB Witness Protocol WASM interface
Browse files- Cargo.toml +17 -0
- Dockerfile +21 -0
- index.html +74 -0
- src/lib.rs +88 -0
Cargo.toml
ADDED
|
@@ -0,0 +1,17 @@
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
+
[package]
|
| 2 |
+
name = "lmfdb-witness-wasm"
|
| 3 |
+
version = "0.1.0"
|
| 4 |
+
edition = "2021"
|
| 5 |
+
|
| 6 |
+
[lib]
|
| 7 |
+
crate-type = ["cdylib", "rlib"]
|
| 8 |
+
|
| 9 |
+
[dependencies]
|
| 10 |
+
wasm-bindgen = "0.2"
|
| 11 |
+
serde = { version = "1.0", features = ["derive"] }
|
| 12 |
+
serde_json = "1.0"
|
| 13 |
+
web-sys = { version = "0.3", features = ["console"] }
|
| 14 |
+
|
| 15 |
+
[profile.release]
|
| 16 |
+
opt-level = "z"
|
| 17 |
+
lto = true
|
Dockerfile
ADDED
|
@@ -0,0 +1,21 @@
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
+
FROM rust:latest
|
| 2 |
+
|
| 3 |
+
WORKDIR /app
|
| 4 |
+
|
| 5 |
+
# Install wasm-pack
|
| 6 |
+
RUN cargo install wasm-pack
|
| 7 |
+
|
| 8 |
+
# Copy source
|
| 9 |
+
COPY . .
|
| 10 |
+
|
| 11 |
+
# Build WASM
|
| 12 |
+
RUN wasm-pack build --target web
|
| 13 |
+
|
| 14 |
+
# Install simple HTTP server
|
| 15 |
+
RUN cargo install miniserve
|
| 16 |
+
|
| 17 |
+
# Expose port
|
| 18 |
+
EXPOSE 7860
|
| 19 |
+
|
| 20 |
+
# Serve on Hugging Face Spaces port
|
| 21 |
+
CMD ["miniserve", "--index", "index.html", "-p", "7860", "."]
|
index.html
ADDED
|
@@ -0,0 +1,74 @@
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
+
<!DOCTYPE html>
|
| 2 |
+
<html>
|
| 3 |
+
<head>
|
| 4 |
+
<title>LMFDB Witness Protocol - Hugging Face Space</title>
|
| 5 |
+
<style>
|
| 6 |
+
body { font-family: monospace; background: #0a0a0a; color: #0f0; padding: 20px; }
|
| 7 |
+
.claim { border: 1px solid #0f0; margin: 10px 0; padding: 10px; }
|
| 8 |
+
.protocol { background: #1a1a1a; padding: 15px; margin-bottom: 20px; }
|
| 9 |
+
h1 { color: #0ff; }
|
| 10 |
+
.field { margin: 5px 0; }
|
| 11 |
+
.label { color: #ff0; }
|
| 12 |
+
</style>
|
| 13 |
+
</head>
|
| 14 |
+
<body>
|
| 15 |
+
<h1>🔮 LMFDB Witness Protocol</h1>
|
| 16 |
+
|
| 17 |
+
<div class="protocol" id="protocol"></div>
|
| 18 |
+
|
| 19 |
+
<h2>Claims</h2>
|
| 20 |
+
<div id="claims"></div>
|
| 21 |
+
|
| 22 |
+
<script type="module">
|
| 23 |
+
import init, { LMFDBWitness } from './pkg/lmfdb_witness_wasm.js';
|
| 24 |
+
|
| 25 |
+
async function run() {
|
| 26 |
+
await init();
|
| 27 |
+
|
| 28 |
+
const witness = new LMFDBWitness();
|
| 29 |
+
|
| 30 |
+
// Display protocol
|
| 31 |
+
const protocol = witness.get_protocol();
|
| 32 |
+
document.getElementById('protocol').innerHTML = `
|
| 33 |
+
<div class="field"><span class="label">N1 (models):</span> ${protocol.n1}</div>
|
| 34 |
+
<div class="field"><span class="label">N2 (size):</span> ${protocol.n2}</div>
|
| 35 |
+
<div class="field"><span class="label">N3 (rounds):</span> ${protocol.n3}</div>
|
| 36 |
+
<div class="field"><span class="label">N4 (rotations):</span> ${protocol.n4}</div>
|
| 37 |
+
<div class="field"><span class="label">Final convergence:</span> ${protocol.final_value}</div>
|
| 38 |
+
<div class="field">${witness.run_convergence()}</div>
|
| 39 |
+
`;
|
| 40 |
+
|
| 41 |
+
// Add sample claim
|
| 42 |
+
witness.add_claim({
|
| 43 |
+
claim: "LMFDB Witness Protocol Initialized",
|
| 44 |
+
bet: "Protocol converges in N3 rounds",
|
| 45 |
+
proof: "N1 models × N2 size → N3 rounds → N4 rotations",
|
| 46 |
+
terms: "N1=24, N2=7, N3=71, N4=17",
|
| 47 |
+
vars: "params: ProtocolParams",
|
| 48 |
+
preconditions: "N1 > 0 ∧ N2 > 0 ∧ N3 = 71 ∧ N4 = 17",
|
| 49 |
+
postconditions: "∃ convergence_value ∈ ℤ/71ℤ",
|
| 50 |
+
invariants: "∀ round ∈ [1..N3]: models evolve via F_ω"
|
| 51 |
+
});
|
| 52 |
+
|
| 53 |
+
// Display claims
|
| 54 |
+
const claims = witness.get_claims();
|
| 55 |
+
const claimsHtml = claims.map(c => `
|
| 56 |
+
<div class="claim">
|
| 57 |
+
<div class="field"><span class="label">CLAIM:</span> ${c.claim}</div>
|
| 58 |
+
<div class="field"><span class="label">BET:</span> ${c.bet}</div>
|
| 59 |
+
<div class="field"><span class="label">PROOF:</span> ${c.proof}</div>
|
| 60 |
+
<div class="field"><span class="label">TERMS:</span> ${c.terms}</div>
|
| 61 |
+
<div class="field"><span class="label">VARS:</span> ${c.vars}</div>
|
| 62 |
+
<div class="field"><span class="label">PRE:</span> ${c.preconditions}</div>
|
| 63 |
+
<div class="field"><span class="label">POST:</span> ${c.postconditions}</div>
|
| 64 |
+
<div class="field"><span class="label">INV:</span> ${c.invariants}</div>
|
| 65 |
+
</div>
|
| 66 |
+
`).join('');
|
| 67 |
+
|
| 68 |
+
document.getElementById('claims').innerHTML = claimsHtml;
|
| 69 |
+
}
|
| 70 |
+
|
| 71 |
+
run();
|
| 72 |
+
</script>
|
| 73 |
+
</body>
|
| 74 |
+
</html>
|
src/lib.rs
ADDED
|
@@ -0,0 +1,88 @@
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
+
use wasm_bindgen::prelude::*;
|
| 2 |
+
use serde::{Deserialize, Serialize};
|
| 3 |
+
|
| 4 |
+
#[wasm_bindgen]
|
| 5 |
+
extern "C" {
|
| 6 |
+
#[wasm_bindgen(js_namespace = console)]
|
| 7 |
+
fn log(s: &str);
|
| 8 |
+
}
|
| 9 |
+
|
| 10 |
+
#[derive(Serialize, Deserialize)]
|
| 11 |
+
pub struct WitnessProtocol {
|
| 12 |
+
pub n1: usize, // models
|
| 13 |
+
pub n2: usize, // size
|
| 14 |
+
pub n3: usize, // rounds
|
| 15 |
+
pub n4: usize, // rotations
|
| 16 |
+
pub final_value: u64,
|
| 17 |
+
}
|
| 18 |
+
|
| 19 |
+
#[derive(Serialize, Deserialize)]
|
| 20 |
+
pub struct Claim {
|
| 21 |
+
pub claim: String,
|
| 22 |
+
pub bet: String,
|
| 23 |
+
pub proof: String,
|
| 24 |
+
pub terms: String,
|
| 25 |
+
pub vars: String,
|
| 26 |
+
pub preconditions: String,
|
| 27 |
+
pub postconditions: String,
|
| 28 |
+
pub invariants: String,
|
| 29 |
+
}
|
| 30 |
+
|
| 31 |
+
#[wasm_bindgen]
|
| 32 |
+
pub struct LMFDBWitness {
|
| 33 |
+
protocol: WitnessProtocol,
|
| 34 |
+
claims: Vec<Claim>,
|
| 35 |
+
}
|
| 36 |
+
|
| 37 |
+
#[wasm_bindgen]
|
| 38 |
+
impl LMFDBWitness {
|
| 39 |
+
#[wasm_bindgen(constructor)]
|
| 40 |
+
pub fn new() -> Self {
|
| 41 |
+
log("LMFDB Witness Protocol initialized");
|
| 42 |
+
|
| 43 |
+
Self {
|
| 44 |
+
protocol: WitnessProtocol {
|
| 45 |
+
n1: 24,
|
| 46 |
+
n2: 7,
|
| 47 |
+
n3: 71,
|
| 48 |
+
n4: 17,
|
| 49 |
+
final_value: 14,
|
| 50 |
+
},
|
| 51 |
+
claims: Vec::new(),
|
| 52 |
+
}
|
| 53 |
+
}
|
| 54 |
+
|
| 55 |
+
#[wasm_bindgen]
|
| 56 |
+
pub fn add_claim(&mut self, claim: JsValue) -> Result<(), JsValue> {
|
| 57 |
+
let claim: Claim = serde_wasm_bindgen::from_value(claim)?;
|
| 58 |
+
self.claims.push(claim);
|
| 59 |
+
Ok(())
|
| 60 |
+
}
|
| 61 |
+
|
| 62 |
+
#[wasm_bindgen]
|
| 63 |
+
pub fn get_protocol(&self) -> JsValue {
|
| 64 |
+
serde_wasm_bindgen::to_value(&self.protocol).unwrap()
|
| 65 |
+
}
|
| 66 |
+
|
| 67 |
+
#[wasm_bindgen]
|
| 68 |
+
pub fn get_claims(&self) -> JsValue {
|
| 69 |
+
serde_wasm_bindgen::to_value(&self.claims).unwrap()
|
| 70 |
+
}
|
| 71 |
+
|
| 72 |
+
#[wasm_bindgen]
|
| 73 |
+
pub fn run_convergence(&self) -> String {
|
| 74 |
+
format!(
|
| 75 |
+
"N1={} models × N2={} size → N3={} rounds → N4={} rotations → Final={}",
|
| 76 |
+
self.protocol.n1,
|
| 77 |
+
self.protocol.n2,
|
| 78 |
+
self.protocol.n3,
|
| 79 |
+
self.protocol.n4,
|
| 80 |
+
self.protocol.final_value
|
| 81 |
+
)
|
| 82 |
+
}
|
| 83 |
+
}
|
| 84 |
+
|
| 85 |
+
#[wasm_bindgen]
|
| 86 |
+
pub fn init() {
|
| 87 |
+
log("LMFDB Witness WASM module loaded");
|
| 88 |
+
}
|