push from SNAPKITTYWEST/snapkitty-clojure-lisp-bridge

119e586 verified 2 months ago

12 kB

// dsssl-synthesis/dsssl-kernel.mjs
//
// DSSSL Kernel — JavaScript runtime for sovereign-dsssl.dsl
//
// Interprets DSSSL construction rules on an SGML grove.
// The style sheet combines:
//   (1) Relational synthesis kernel (lookup, unify-hole, synthesize-bindings)
//   (2) Construction rules (element GROOVE, EXPR, HOLE, INT, OP, LEFT, RIGHT)
//
// This runtime:
//   - Parses the SGML input grove (dsssl-input.sgml)
//   - Runs synthesize-bindings to fill holes
//   - Applies construction rules to produce the verified output grove
//   - Emits JSON synthesis receipt + WORM seal
//
// Connects to:
//   dsssl-synthesis.mjs        (SGML grove parser, already exists)
//   dsssl-synthesis-fixed.mjs  (fixed homoiconic engine)
//   relational-refinement-engine.mjs (LH refinement types)
//
// Ahmad Ali Parr -- Bel Esprit D'Accord Irrevocable Trust -- EIN 42-697643

import { createHash } from 'crypto'

// ── Grove node representation ─────────────────────────────────────────────────
// Mirrors the DSSSL (gi node) / (data node) / (children node) accessors

class GroveNode {
  constructor(gi, data = '', children = [], attrs = {}) {
    this.gi       = gi
    this.data     = data
    this.children = children
    this.attrs    = attrs
  }

  attr(name) { return this.attrs[name] ?? null }

  // DSSSL: (node-list-first (select-elements (children node) "TAG"))
  selectFirst(tag) {
    return this.children.find(c => c.gi === tag) ?? null
  }

  selectAll(tag) {
    return this.children.filter(c => c.gi === tag)
  }
}

// ── SGML grove parser ─────────────────────────────────────────────────────────
// Simplified — handles the input format from dsssl-input.sgml

function parseGrove(sgml) {
  const stripped = sgml
    .replace(/<!--[\s\S]*?-->/g, '')
    .replace(/<\?[^>]*>/g, '')
    .replace(/<!DOCTYPE[\s\S]*?]>/i, '')
    .replace(/<!SGML[\s\S]*?>/i, '')
    .trim()

  let pos = 0

  function skipWS() {
    while (pos < stripped.length && /\s/.test(stripped[pos])) pos++
  }

  function parseNode() {
    skipWS()
    if (pos >= stripped.length || stripped[pos] !== '<') return null
    if (stripped[pos + 1] === '/') return null

    pos++ // skip <
    let tagEnd = stripped.indexOf('>', pos)
    if (tagEnd === -1) return null
    const tagContent = stripped.slice(pos, tagEnd).trim()
    pos = tagEnd + 1

    const parts = tagContent.split(/\s+/)
    const gi    = parts[0].toUpperCase()
    const attrs = {}
    for (let i = 1; i < parts.length; i++) {
      const [k, v] = parts[i].split('=')
      if (v) attrs[k.toUpperCase()] = v.replace(/['"]/g, '')
    }

    // EMPTY elements (HOLE)
    if (gi === 'HOLE') return new GroveNode(gi, '', [], attrs)

    const children = []
    let   textData = ''

    while (pos < stripped.length) {
      skipWS()
      if (pos >= stripped.length) break
      if (stripped[pos] === '<') {
        if (stripped[pos + 1] === '/') {
          pos = stripped.indexOf('>', pos) + 1
          break
        }
        const child = parseNode()
        if (child) children.push(child)
      } else {
        const nextTag = stripped.indexOf('<', pos)
        const end     = nextTag === -1 ? stripped.length : nextTag
        const txt     = stripped.slice(pos, end).trim()
        if (txt) textData += txt
        pos = end
      }
    }

    return new GroveNode(gi, textData, children, attrs)
  }

  return parseNode()
}

// ── DSSSL Synthesis Kernel ────────────────────────────────────────────────────
// Direct port of the Scheme functions from sovereign-dsssl.dsl

function lookup(varName, env) {
  const cell = env.find(([k]) => k === varName)
  return cell ? cell[1] : null
}

function unifyHole(varName, candidate, env) {
  const bound = lookup(varName, env)
  if (bound === null)            return [[varName, candidate], ...env]
  if (bound === candidate)       return env
  return null  // contradiction
}

function evalGroveNode(node, env) {
  if (!node) return 'UNBOUND'
  const gi = node.gi

  if (gi === 'INT') {
    const n = Number(node.data)
    return isNaN(n) ? 'UNBOUND' : n
  }

  if (gi === 'HOLE') {
    const varName = node.attr('VAR') || node.attr('var')
    const val     = lookup(varName, env)
    return val !== null ? val : 'UNBOUND'
  }

  if (gi === 'EXPR') {
    const opNode    = node.selectFirst('OP')
    const leftNode  = node.selectFirst('LEFT')
    const rightNode = node.selectFirst('RIGHT')
    if (!opNode || !leftNode || !rightNode) return 'UNBOUND'

    const op    = opNode.data.trim()
    const lNode = leftNode.children[0]
    const rNode = rightNode.children[0]
    const lVal  = evalGroveNode(lNode, env)
    const rVal  = evalGroveNode(rNode, env)

    if (lVal === 'UNBOUND' || rVal === 'UNBOUND') return 'UNBOUND'
    if (op === '+') return lVal + rVal
    if (op === '*') return lVal * rVal
    if (op === '-') return lVal - rVal
    if (op === '/') return rVal !== 0 ? lVal / rVal : 'UNBOUND'
    return 0
  }

  return 'UNBOUND'
}

const TARGET_INVARIANT = 20

function synthesizeBindings(holeVar, candidates, env, rootNode) {
  for (const cand of candidates) {
    const testEnv = unifyHole(holeVar, cand, env)
    if (testEnv !== null) {
      const result = evalGroveNode(rootNode, testEnv)
      if (result === TARGET_INVARIANT) {
        return { env: testEnv, candidate: cand, result }
      }
    }
  }
  return null
}

// ── DSSSL Construction Rules ──────────────────────────────────────────────────
// Each rule matches a gi (element type) and produces a new GroveNode.
// Mirrors the (element TAG ...) construction rules in sovereign-dsssl.dsl.

function applyRule(node, solvedEnv) {
  if (!node) return null
  const gi = node.gi

  if (gi === 'GROVE') {
    const candidates  = [1, 2, 3, 4, 5]
    const rootExpr    = node.selectFirst('EXPR') || node.children[0]
    const synthesis   = synthesizeBindings('?x', candidates, [], rootExpr)
    const status      = synthesis ? 'VERIFIED' : 'FAILED'
    const env         = synthesis ? synthesis.env : []

    return new GroveNode('SYNTHESIZED-GROVE', '', [
      applyRule(rootExpr, env)
    ], { STATUS: status })
  }

  if (gi === 'EXPR') {
    return new GroveNode('EXPR', '', node.children.map(c => applyRule(c, solvedEnv)),
      { ID: node.attr('ID') || node.attr('id') || '' })
  }

  if (gi === 'OP' || gi === 'INT') {
    return new GroveNode(gi, node.data, [], {})
  }

  if (gi === 'LEFT' || gi === 'RIGHT') {
    return new GroveNode(gi, '', node.children.map(c => applyRule(c, solvedEnv)), {})
  }

  if (gi === 'HOLE') {
    const varName  = node.attr('VAR') || node.attr('var')
    const resolved = lookup(varName, solvedEnv)
    if (resolved !== null) {
      return new GroveNode('SYNTHESIZED-INT', String(resolved), [], { 'RESOLVED-FROM': varName })
    }
    return new GroveNode('UNRESOLVED-HOLE', '', [], { VAR: varName })
  }

  // Default: pass through
  return new GroveNode(gi, node.data, node.children.map(c => applyRule(c, solvedEnv)), node.attrs)
}

// ── Grove serializer → SGML output ───────────────────────────────────────────

function serializeGrove(node, indent = 0) {
  if (!node) return ''
  const pad    = '  '.repeat(indent)
  const attrs  = Object.entries(node.attrs)
    .map(([k, v]) => ` ${k}="${v}"`).join('')
  const hasContent = node.children.length > 0 || node.data.trim()

  if (!hasContent) return `${pad}<${node.gi}${attrs}>`

  const inner = node.data.trim()
    ? node.data.trim()
    : '\n' + node.children.map(c => serializeGrove(c, indent + 1)).join('\n') + '\n' + pad

  return `${pad}<${node.gi}${attrs}>${inner}</${node.gi}>`
}

// ── Main ──────────────────────────────────────────────────────────────────────

export async function runDSSL(sgmlInput, options = {}) {
  // 1. Parse SGML grove
  const grove = parseGrove(sgmlInput)
  if (!grove) throw new Error('DSSSL: failed to parse SGML input grove')

  // 2. Find hole variable and candidates
  const holeVars  = []
  const findHoles = (node) => {
    if (!node) return
    if (node.gi === 'HOLE') holeVars.push(node.attr('VAR') || node.attr('var'))
    node.children.forEach(findHoles)
  }
  findHoles(grove)

  // 3. Run synthesis kernel (GROVE construction rule)
  const rootExpr   = grove.selectFirst('EXPR') || grove.children[0]
  const candidates = options.candidates || [1, 2, 3, 4, 5]
  const synthesis  = synthesizeBindings('?x', candidates, [], rootExpr)

  // 4. Apply construction rules
  const outputGrove = applyRule(grove, synthesis?.env || [])

  // 5. Serialize output
  const outputSGML = serializeGrove(outputGrove)

  // 6. Verify: re-evaluate with solved binding
  let verifiedResult = null
  if (synthesis) {
    verifiedResult = evalGroveNode(rootExpr, synthesis.env)
  }

  // 7. WORM seal
  const seal = createHash('sha256')
    .update(JSON.stringify({ output: outputSGML, synthesis }))
    .digest('hex')

  return {
    status:               synthesis ? 'VERIFIED' : 'FAILED',
    transformation_summary: synthesis
      ? `Hole ?x resolved to ${synthesis.candidate}. Grove evaluates to ${verifiedResult} (target: ${TARGET_INVARIANT}).`
      : `No candidate satisfies invariant = ${TARGET_INVARIANT}.`,
    holes_found:          holeVars,
    synthesis: synthesis ? {
      hole_var:   '?x',
      candidate:  synthesis.candidate,
      env:        synthesis.env,
      result:     synthesis.result,
    } : null,
    output_grove_sgml:    outputSGML,
    worm_seal:            seal.slice(0, 16),
    verification_trace: {
      target_invariant:  TARGET_INVARIANT,
      candidates_tried:  candidates,
      smt_proof_status:  synthesis ? 'SAT' : 'UNSAT',
    },
  }
}

// ── CLI ───────────────────────────────────────────────────────────────────────

if (process.argv[1]?.endsWith('dsssl-kernel.mjs')) {
  const { readFileSync } = await import('fs')
  const { fileURLToPath } = await import('url')
  const { dirname, join } = await import('path')

  const __dir = dirname(fileURLToPath(import.meta.url))
  const inputPath = process.argv[2] || join(__dir, 'dsssl-input.sgml')

  let sgmlInput
  try {
    sgmlInput = readFileSync(inputPath, 'utf8')
  } catch {
    // Use embedded example if file not present
    sgmlInput = `<GROVE><EXPR id="root"><OP>*</OP><LEFT><EXPR id="inner"><OP>+</OP><LEFT><HOLE var="?x"></LEFT><RIGHT><INT>4</INT></RIGHT></EXPR></LEFT><RIGHT><INT>4</INT></RIGHT></EXPR></GROVE>`
  }

  const result = await runDSSL(sgmlInput)

  console.log('══════════════════════════════════════════════════')
  console.log('  DSSSL SYNTHESIS KERNEL')
  console.log('  sovereign-dsssl.dsl → verified output grove')
  console.log('══════════════════════════════════════════════════')
  console.log(JSON.stringify(result, null, 2))
}

	// dsssl-synthesis/dsssl-kernel.mjs
	//
	// DSSSL Kernel — JavaScript runtime for sovereign-dsssl.dsl
	//
	// Interprets DSSSL construction rules on an SGML grove.
	// The style sheet combines:
	// (1) Relational synthesis kernel (lookup, unify-hole, synthesize-bindings)
	// (2) Construction rules (element GROOVE, EXPR, HOLE, INT, OP, LEFT, RIGHT)
	//
	// This runtime:
	// - Parses the SGML input grove (dsssl-input.sgml)
	// - Runs synthesize-bindings to fill holes
	// - Applies construction rules to produce the verified output grove
	// - Emits JSON synthesis receipt + WORM seal
	//
	// Connects to:
	// dsssl-synthesis.mjs (SGML grove parser, already exists)
	// dsssl-synthesis-fixed.mjs (fixed homoiconic engine)
	// relational-refinement-engine.mjs (LH refinement types)
	//
	// Ahmad Ali Parr -- Bel Esprit D'Accord Irrevocable Trust -- EIN 42-697643

	import { createHash } from 'crypto'

	// ── Grove node representation ─────────────────────────────────────────────────
	// Mirrors the DSSSL (gi node) / (data node) / (children node) accessors

	class GroveNode {
	constructor(gi, data = '', children = [], attrs = {}) {
	this.gi = gi
	this.data = data
	this.children = children
	this.attrs = attrs
	}

	attr(name) { return this.attrs[name] ?? null }

	// DSSSL: (node-list-first (select-elements (children node) "TAG"))
	selectFirst(tag) {
	return this.children.find(c => c.gi === tag) ?? null
	}

	selectAll(tag) {
	return this.children.filter(c => c.gi === tag)
	}
	}

	// ── SGML grove parser ─────────────────────────────────────────────────────────
	// Simplified — handles the input format from dsssl-input.sgml

	function parseGrove(sgml) {
	const stripped = sgml
	.replace(/<!--[\s\S]*?-->/g, '')
	.replace(/<\?[^>]*>/g, '')
	.replace(/<!DOCTYPE[\s\S]*?]>/i, '')
	.replace(/<!SGML[\s\S]*?>/i, '')
	.trim()

	let pos = 0

	function skipWS() {
	while (pos < stripped.length && /\s/.test(stripped[pos])) pos++
	}

	function parseNode() {
	skipWS()
	if (pos >= stripped.length \|\| stripped[pos] !== '<') return null
	if (stripped[pos + 1] === '/') return null

	pos++ // skip <
	let tagEnd = stripped.indexOf('>', pos)
	if (tagEnd === -1) return null
	const tagContent = stripped.slice(pos, tagEnd).trim()
	pos = tagEnd + 1

	const parts = tagContent.split(/\s+/)
	const gi = parts[0].toUpperCase()
	const attrs = {}
	for (let i = 1; i < parts.length; i++) {
	const [k, v] = parts[i].split('=')
	if (v) attrs[k.toUpperCase()] = v.replace(/['"]/g, '')
	}

	// EMPTY elements (HOLE)
	if (gi === 'HOLE') return new GroveNode(gi, '', [], attrs)

	const children = []
	let textData = ''

	while (pos < stripped.length) {
	skipWS()
	if (pos >= stripped.length) break
	if (stripped[pos] === '<') {
	if (stripped[pos + 1] === '/') {
	pos = stripped.indexOf('>', pos) + 1
	break
	}
	const child = parseNode()
	if (child) children.push(child)
	} else {
	const nextTag = stripped.indexOf('<', pos)
	const end = nextTag === -1 ? stripped.length : nextTag
	const txt = stripped.slice(pos, end).trim()
	if (txt) textData += txt
	pos = end
	}
	}

	return new GroveNode(gi, textData, children, attrs)
	}

	return parseNode()
	}

	// ── DSSSL Synthesis Kernel ────────────────────────────────────────────────────
	// Direct port of the Scheme functions from sovereign-dsssl.dsl

	function lookup(varName, env) {
	const cell = env.find(([k]) => k === varName)
	return cell ? cell[1] : null
	}

	function unifyHole(varName, candidate, env) {
	const bound = lookup(varName, env)
	if (bound === null) return [[varName, candidate], ...env]
	if (bound === candidate) return env
	return null // contradiction
	}

	function evalGroveNode(node, env) {
	if (!node) return 'UNBOUND'
	const gi = node.gi

	if (gi === 'INT') {
	const n = Number(node.data)
	return isNaN(n) ? 'UNBOUND' : n
	}

	if (gi === 'HOLE') {
	const varName = node.attr('VAR') \|\| node.attr('var')
	const val = lookup(varName, env)
	return val !== null ? val : 'UNBOUND'
	}

	if (gi === 'EXPR') {
	const opNode = node.selectFirst('OP')
	const leftNode = node.selectFirst('LEFT')
	const rightNode = node.selectFirst('RIGHT')
	if (!opNode \|\| !leftNode \|\| !rightNode) return 'UNBOUND'

	const op = opNode.data.trim()
	const lNode = leftNode.children[0]
	const rNode = rightNode.children[0]
	const lVal = evalGroveNode(lNode, env)
	const rVal = evalGroveNode(rNode, env)

	if (lVal === 'UNBOUND' \|\| rVal === 'UNBOUND') return 'UNBOUND'
	if (op === '+') return lVal + rVal
	if (op === '') return lVal rVal
	if (op === '-') return lVal - rVal
	if (op === '/') return rVal !== 0 ? lVal / rVal : 'UNBOUND'
	return 0
	}

	return 'UNBOUND'
	}

	const TARGET_INVARIANT = 20

	function synthesizeBindings(holeVar, candidates, env, rootNode) {
	for (const cand of candidates) {
	const testEnv = unifyHole(holeVar, cand, env)
	if (testEnv !== null) {
	const result = evalGroveNode(rootNode, testEnv)
	if (result === TARGET_INVARIANT) {
	return { env: testEnv, candidate: cand, result }
	}
	}
	}
	return null
	}

	// ── DSSSL Construction Rules ──────────────────────────────────────────────────
	// Each rule matches a gi (element type) and produces a new GroveNode.
	// Mirrors the (element TAG ...) construction rules in sovereign-dsssl.dsl.

	function applyRule(node, solvedEnv) {
	if (!node) return null
	const gi = node.gi

	if (gi === 'GROVE') {
	const candidates = [1, 2, 3, 4, 5]
	const rootExpr = node.selectFirst('EXPR') \|\| node.children[0]
	const synthesis = synthesizeBindings('?x', candidates, [], rootExpr)
	const status = synthesis ? 'VERIFIED' : 'FAILED'
	const env = synthesis ? synthesis.env : []

	return new GroveNode('SYNTHESIZED-GROVE', '', [
	applyRule(rootExpr, env)
	], { STATUS: status })
	}

	if (gi === 'EXPR') {
	return new GroveNode('EXPR', '', node.children.map(c => applyRule(c, solvedEnv)),
	{ ID: node.attr('ID') \|\| node.attr('id') \|\| '' })
	}

	if (gi === 'OP' \|\| gi === 'INT') {
	return new GroveNode(gi, node.data, [], {})
	}

	if (gi === 'LEFT' \|\| gi === 'RIGHT') {
	return new GroveNode(gi, '', node.children.map(c => applyRule(c, solvedEnv)), {})
	}

	if (gi === 'HOLE') {
	const varName = node.attr('VAR') \|\| node.attr('var')
	const resolved = lookup(varName, solvedEnv)
	if (resolved !== null) {
	return new GroveNode('SYNTHESIZED-INT', String(resolved), [], { 'RESOLVED-FROM': varName })
	}
	return new GroveNode('UNRESOLVED-HOLE', '', [], { VAR: varName })
	}

	// Default: pass through
	return new GroveNode(gi, node.data, node.children.map(c => applyRule(c, solvedEnv)), node.attrs)
	}

	// ── Grove serializer → SGML output ───────────────────────────────────────────

	function serializeGrove(node, indent = 0) {
	if (!node) return ''
	const pad = ' '.repeat(indent)
	const attrs = Object.entries(node.attrs)
	.map(([k, v]) => ` ${k}="${v}"`).join('')
	const hasContent = node.children.length > 0 \|\| node.data.trim()

	if (!hasContent) return `${pad}<${node.gi}${attrs}>`

	const inner = node.data.trim()
	? node.data.trim()
	: '\n' + node.children.map(c => serializeGrove(c, indent + 1)).join('\n') + '\n' + pad

	return `${pad}<${node.gi}${attrs}>${inner}</${node.gi}>`
	}

	// ── Main ──────────────────────────────────────────────────────────────────────

	export async function runDSSL(sgmlInput, options = {}) {
	// 1. Parse SGML grove
	const grove = parseGrove(sgmlInput)
	if (!grove) throw new Error('DSSSL: failed to parse SGML input grove')

	// 2. Find hole variable and candidates
	const holeVars = []
	const findHoles = (node) => {
	if (!node) return
	if (node.gi === 'HOLE') holeVars.push(node.attr('VAR') \|\| node.attr('var'))
	node.children.forEach(findHoles)
	}
	findHoles(grove)

	// 3. Run synthesis kernel (GROVE construction rule)
	const rootExpr = grove.selectFirst('EXPR') \|\| grove.children[0]
	const candidates = options.candidates \|\| [1, 2, 3, 4, 5]
	const synthesis = synthesizeBindings('?x', candidates, [], rootExpr)

	// 4. Apply construction rules
	const outputGrove = applyRule(grove, synthesis?.env \|\| [])

	// 5. Serialize output
	const outputSGML = serializeGrove(outputGrove)

	// 6. Verify: re-evaluate with solved binding
	let verifiedResult = null
	if (synthesis) {
	verifiedResult = evalGroveNode(rootExpr, synthesis.env)
	}

	// 7. WORM seal
	const seal = createHash('sha256')
	.update(JSON.stringify({ output: outputSGML, synthesis }))
	.digest('hex')

	return {
	status: synthesis ? 'VERIFIED' : 'FAILED',
	transformation_summary: synthesis
	? `Hole ?x resolved to ${synthesis.candidate}. Grove evaluates to ${verifiedResult} (target: ${TARGET_INVARIANT}).`
	: `No candidate satisfies invariant = ${TARGET_INVARIANT}.`,
	holes_found: holeVars,
	synthesis: synthesis ? {
	hole_var: '?x',
	candidate: synthesis.candidate,
	env: synthesis.env,
	result: synthesis.result,
	} : null,
	output_grove_sgml: outputSGML,
	worm_seal: seal.slice(0, 16),
	verification_trace: {
	target_invariant: TARGET_INVARIANT,
	candidates_tried: candidates,
	smt_proof_status: synthesis ? 'SAT' : 'UNSAT',
	},
	}
	}

	// ── CLI ───────────────────────────────────────────────────────────────────────

	if (process.argv[1]?.endsWith('dsssl-kernel.mjs')) {
	const { readFileSync } = await import('fs')
	const { fileURLToPath } = await import('url')
	const { dirname, join } = await import('path')

	const __dir = dirname(fileURLToPath(import.meta.url))
	const inputPath = process.argv[2] \|\| join(__dir, 'dsssl-input.sgml')

	let sgmlInput
	try {
	sgmlInput = readFileSync(inputPath, 'utf8')
	} catch {
	// Use embedded example if file not present
	sgmlInput = `<GROVE><EXPR id="root"><OP>*</OP><LEFT><EXPR id="inner"><OP>+</OP><LEFT><HOLE var="?x"></LEFT><RIGHT><INT>4</INT></RIGHT></EXPR></LEFT><RIGHT><INT>4</INT></RIGHT></EXPR></GROVE>`
	}

	const result = await runDSSL(sgmlInput)

	console.log('══════════════════════════════════════════════════')
	console.log(' DSSSL SYNTHESIS KERNEL')
	console.log(' sovereign-dsssl.dsl → verified output grove')
	console.log('══════════════════════════════════════════════════')
	console.log(JSON.stringify(result, null, 2))
	}