From 192d48d0e352cf94f92a6fcd1111d1f2d53611db Mon Sep 17 00:00:00 2001 From: giles Date: Mon, 9 Mar 2026 00:45:07 +0000 Subject: [PATCH] Add self-hosting bootstrapper plan: py.sx design document MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Plan for py.sx — an SX-to-Python translator written in SX that replaces bootstrap_py.py. Covers translation rules, statement vs expression modes, mutation/cell variables, five implementation phases, fixed-point verification, and implications for multi-host bootstrapping. Co-Authored-By: Claude Opus 4.6 --- sx/sx/nav-data.sx | 2 + sx/sx/plans/self-hosting-bootstrapper.sx | 378 +++++++++++++++++++++++ sx/sxc/pages/docs.sx | 1 + 3 files changed, 381 insertions(+) create mode 100644 sx/sx/plans/self-hosting-bootstrapper.sx diff --git a/sx/sx/nav-data.sx b/sx/sx/nav-data.sx index b2096cb..24cada4 100644 --- a/sx/sx/nav-data.sx +++ b/sx/sx/nav-data.sx @@ -159,6 +159,8 @@ :summary "Live demo: #z3 translates SX spec declarations to SMT-LIB verification conditions.") (dict :label "Theorem Prover" :href "/plans/theorem-prover" :summary "prove.sx — constraint solver and property prover for SX primitives, written in SX.") + (dict :label "Self-Hosting Bootstrapper" :href "/plans/self-hosting-bootstrapper" + :summary "py.sx — an SX-to-Python translator written in SX. The bootstrapper bootstraps itself.") (dict :label "SX-Activity" :href "/plans/sx-activity" :summary "A new web built on SX — executable content, shared components, parsers, and logic on IPFS, provenance on Bitcoin, all running within your own security context.") (dict :label "Predictive Prefetching" :href "/plans/predictive-prefetch" diff --git a/sx/sx/plans/self-hosting-bootstrapper.sx b/sx/sx/plans/self-hosting-bootstrapper.sx new file mode 100644 index 0000000..398646b --- /dev/null +++ b/sx/sx/plans/self-hosting-bootstrapper.sx @@ -0,0 +1,378 @@ +;; --------------------------------------------------------------------------- +;; Self-Hosting Bootstrapper — py.sx +;; --------------------------------------------------------------------------- + +(defcomp ~plan-self-hosting-bootstrapper-content () + (~doc-page :title "Self-Hosting Bootstrapper" + + ;; ----------------------------------------------------------------------- + ;; The Idea + ;; ----------------------------------------------------------------------- + + (~doc-section :title "The Idea" :id "idea" + (p "We have " (code "bootstrap_py.py") " — a Python program that reads " + (code ".sx") " spec files and emits " (code "sx_ref.py") + ", a standalone Python evaluator. It's a compiler written in the host language.") + (p "We also have " (code "z3.sx") " — a translator written in SX itself that " + "converts SX spec declarations into SMT-LIB for Z3. It's proof that " + "SX can generate code in another language.") + (p "The next step: " (strong "py.sx") " — an SX-to-Python translator written in SX. " + "Feed it through the existing Python evaluator against the spec files and it produces " + (code "sx_ref.py") ". The bootstrapper bootstraps itself.") + (p "If " (code "py.sx") " produces output identical to " (code "bootstrap_py.py") + ", the Python bootstrapper becomes redundant. " + "The spec defines itself.")) + + ;; ----------------------------------------------------------------------- + ;; Architecture + ;; ----------------------------------------------------------------------- + + (~doc-section :title "Architecture" :id "architecture" + (p "Three bootstrapper generations:") + (div :class "overflow-x-auto rounded border border-stone-200 my-4" + (table :class "w-full text-sm" + (thead :class "bg-stone-50" + (tr + (th :class "px-4 py-2 text-left font-semibold text-stone-700" "Gen") + (th :class "px-4 py-2 text-left font-semibold text-stone-700" "Source") + (th :class "px-4 py-2 text-left font-semibold text-stone-700" "Runs on") + (th :class "px-4 py-2 text-left font-semibold text-stone-700" "Reads") + (th :class "px-4 py-2 text-left font-semibold text-stone-700" "Produces"))) + (tbody + (tr :class "border-t border-stone-100" + (td :class "px-4 py-2 font-mono text-stone-600" "G0") + (td :class "px-4 py-2" (code "bootstrap_py.py")) + (td :class "px-4 py-2" "Python (manual)") + (td :class "px-4 py-2" (code "eval.sx") ", " (code "render.sx") ", ...") + (td :class "px-4 py-2" (code "sx_ref.py"))) + (tr :class "border-t border-stone-100 bg-violet-50" + (td :class "px-4 py-2 font-mono text-violet-700" "G1") + (td :class "px-4 py-2" (code "py.sx")) + (td :class "px-4 py-2" "Python evaluator + SX") + (td :class "px-4 py-2" (code "eval.sx") ", " (code "render.sx") ", ...") + (td :class "px-4 py-2" (code "sx_ref.py") " (identical)")) + (tr :class "border-t border-stone-100" + (td :class "px-4 py-2 font-mono text-stone-600" "G2") + (td :class "px-4 py-2" (code "py.sx")) + (td :class "px-4 py-2" (code "sx_ref.py") " from G1 + SX") + (td :class "px-4 py-2" (code "eval.sx") ", " (code "render.sx") ", ...") + (td :class "px-4 py-2" (code "sx_ref.py") " (fixed-point)"))))) + + (p "G0 is the hand-written compiler. G1 replaces it with SX. " + "G2 proves the fixed-point: " (code "py.sx") " compiled by its own output " + "produces the same output. That's the definition of self-hosting.")) + + ;; ----------------------------------------------------------------------- + ;; Translation Rules + ;; ----------------------------------------------------------------------- + + (~doc-section :title "Translation Rules" :id "translation" + + (~doc-subsection :title "Name Mangling" + (p "SX identifiers become valid Python identifiers:") + (div :class "overflow-x-auto rounded border border-stone-200 my-4" + (table :class "w-full text-sm" + (thead :class "bg-stone-50" + (tr + (th :class "px-4 py-2 text-left font-semibold text-stone-700" "SX") + (th :class "px-4 py-2 text-left font-semibold text-stone-700" "Python") + (th :class "px-4 py-2 text-left font-semibold text-stone-700" "Rule"))) + (tbody + (tr :class "border-t border-stone-100" + (td :class "px-4 py-2 font-mono" "eval-expr") + (td :class "px-4 py-2 font-mono" "eval_expr") + (td :class "px-4 py-2" "kebab → snake")) + (tr :class "border-t border-stone-100" + (td :class "px-4 py-2 font-mono" "nil?") + (td :class "px-4 py-2 font-mono" "is_nil") + (td :class "px-4 py-2" "predicate rename")) + (tr :class "border-t border-stone-100" + (td :class "px-4 py-2 font-mono" "empty?") + (td :class "px-4 py-2 font-mono" "empty_p") + (td :class "px-4 py-2" "? → _p (general)")) + (tr :class "border-t border-stone-100" + (td :class "px-4 py-2 font-mono" "set!") + (td :class "px-4 py-2 font-mono" "set_b") + (td :class "px-4 py-2" "! → _b")) + (tr :class "border-t border-stone-100" + (td :class "px-4 py-2 font-mono" "make-lambda") + (td :class "px-4 py-2 font-mono" "make_lambda") + (td :class "px-4 py-2" "platform function rename")) + (tr :class "border-t border-stone-100" + (td :class "px-4 py-2 font-mono" "type") + (td :class "px-4 py-2 font-mono" "type_") + (td :class "px-4 py-2" "Python reserved word escape")))))) + + (~doc-subsection :title "Literals" + (~doc-code :code (highlight "(define py-literal + (fn (expr) + (cond + ;; Bool before number (Python: bool subclass of int) + (= expr true) \"True\" + (= expr false) \"False\" + (nil? expr) \"NIL\" + (number? expr) (str expr) + (string? expr) (py-quote-string expr) + (= (type-of expr) \"keyword\") (py-quote-string (keyword-name expr)) + (= (type-of expr) \"symbol\") (py-mangle (symbol-name expr)) + :else (str expr))))" "lisp"))) + + (~doc-subsection :title "Special Forms" + (p "Each SX special form maps to a Python expression pattern:") + (div :class "overflow-x-auto rounded border border-stone-200 my-4" + (table :class "w-full text-sm" + (thead :class "bg-stone-50" + (tr + (th :class "px-4 py-2 text-left font-semibold text-stone-700" "SX") + (th :class "px-4 py-2 text-left font-semibold text-stone-700" "Python"))) + (tbody + (tr :class "border-t border-stone-100" + (td :class "px-4 py-2 font-mono" "(if c t e)") + (td :class "px-4 py-2 font-mono" "(t if sx_truthy(c) else e)")) + (tr :class "border-t border-stone-100" + (td :class "px-4 py-2 font-mono" "(when c body)") + (td :class "px-4 py-2 font-mono" "(body if sx_truthy(c) else NIL)")) + (tr :class "border-t border-stone-100" + (td :class "px-4 py-2 font-mono" "(let ((a 1)) body)") + (td :class "px-4 py-2 font-mono" "(lambda a: body)(1)")) + (tr :class "border-t border-stone-100" + (td :class "px-4 py-2 font-mono" "(fn (x) body)") + (td :class "px-4 py-2 font-mono" "lambda x: body")) + (tr :class "border-t border-stone-100" + (td :class "px-4 py-2 font-mono" "(define name val)") + (td :class "px-4 py-2 font-mono" "name = val")) + (tr :class "border-t border-stone-100" + (td :class "px-4 py-2 font-mono" "(and a b c)") + (td :class "px-4 py-2 font-mono" "(a if not sx_truthy(a) else (b if ... else c))")) + (tr :class "border-t border-stone-100" + (td :class "px-4 py-2 font-mono" "(or a b c)") + (td :class "px-4 py-2 font-mono" "(a if sx_truthy(a) else (b if ... else c))")) + (tr :class "border-t border-stone-100" + (td :class "px-4 py-2 font-mono" "(case x \"a\" 1 \"b\" 2)") + (td :class "px-4 py-2 font-mono" "_sx_case(x, [(\"a\", lambda: 1), ...])")) + (tr :class "border-t border-stone-100" + (td :class "px-4 py-2 font-mono" "(str a b c)") + (td :class "px-4 py-2 font-mono" "sx_str(a, b, c)")) + (tr :class "border-t border-stone-100" + (td :class "px-4 py-2 font-mono" "(+ a b)") + (td :class "px-4 py-2 font-mono" "(a + b)")) + (tr :class "border-t border-stone-100" + (td :class "px-4 py-2 font-mono" "(= a b)") + (td :class "px-4 py-2 font-mono" "(a == b)")) + (tr :class "border-t border-stone-100" + (td :class "px-4 py-2 font-mono" "&rest args") + (td :class "px-4 py-2 font-mono" "*args")))))) + + (~doc-subsection :title "Mutation: set! and Cell Variables" + (p "Python closures can read but not rebind outer variables. " + "SX " (code "set!") " from nested lambdas requires a cell indirection pattern:") + (~doc-code :code (highlight ";; SX +(define counter + (fn () + (let ((n 0)) + (fn () (set! n (+ n 1)) n)))) + +;; Python (impossible with plain lambda) +;; → uses _cells dict for mutable bindings +def counter(): + _cells = {} + _cells['n'] = 0 + return lambda: _sx_begin( + _sx_cell_set(_cells, 'n', (_cells['n'] + 1)), + _cells['n'])" "python")) + (p (code "py.sx") " must detect " (code "set!") " targets that cross lambda boundaries " + "and route them through the cell dictionary. " + "This is the hardest translation rule — the existing bootstrapper's " + (code "_find_nested_set_vars") " and " (code "_emit_define_as_def") " handle it."))) + + ;; ----------------------------------------------------------------------- + ;; Statement vs Expression + ;; ----------------------------------------------------------------------- + + (~doc-section :title "Statement vs Expression Mode" :id "modes" + (p "The fundamental tension: SX is expression-oriented (everything returns a value). " + "Python has both expressions and statements. " (code "define") " must be a statement. " + (code "for-each") " with side effects wants a " (code "for") " loop.") + (p "The existing bootstrapper handles this with two methods:") + (ul :class "list-disc pl-6 space-y-2 text-stone-700" + (li (code "emit(expr)") " → Python expression (used inside other expressions)") + (li (code "emit_statement(expr, indent)") " → Python statement (used at top level and in def bodies)")) + (p (code "py.sx") " needs the same dual-mode emission. Top-level " (code "define") " forms " + "emit as statements. Everything else emits as expressions. Functions with " + (code "set!") " emit as " (code "def") " with proper statements instead of lambda expressions.")) + + ;; ----------------------------------------------------------------------- + ;; Implementation Plan + ;; ----------------------------------------------------------------------- + + (~doc-section :title "Implementation" :id "implementation" + (p "Build " (code "py.sx") " incrementally:") + + (~doc-subsection :title "Phase 1: Core Expression Translator" + (p "Translate the SX subset used in the spec to Python expressions.") + (ul :class "list-disc pl-6 space-y-1 text-stone-700" + (li (code "py-mangle") " — SX name → Python identifier (RENAMES table + general rules)") + (li (code "py-literal") " — atoms: numbers, strings, booleans, nil, symbols, keywords") + (li (code "py-expr") " — recursive expression translator") + (li "Infix operators: " (code "+") ", " (code "-") ", " (code "*") ", " + (code "/") ", " (code "=") "→" (code "==") ", " (code "!=") ", " + (code "<") ", " (code ">") ", " (code "<=") ", " (code ">=") ", " (code "mod") "→" (code "%")) + (li "Special forms: " (code "if") ", " (code "when") ", " (code "cond") ", " + (code "case") ", " (code "and") ", " (code "or") ", " (code "not")) + (li (code "let") " → nested IIFE lambdas") + (li (code "fn") "/" (code "lambda") " → Python " (code "lambda")) + (li (code "str") " → " (code "sx_str()")) + (li (code "list") " → " (code "[...]") " literal") + (li (code "dict") " → " (code "{...}") " literal") + (li (code "quote") " → AST constructor literals"))) + + (~doc-subsection :title "Phase 2: Statement Translator" + (p "Top-level forms and function bodies need statement mode:") + (ul :class "list-disc pl-6 space-y-1 text-stone-700" + (li (code "py-statement") " — emit as Python statement with indentation") + (li (code "define") " → " (code "name = expr") " or " (code "def name(): ...")) + (li (code "set!") " → assignment (direct or via _cells)") + (li (code "for-each") " → " (code "for") " loop") + (li (code "do") "/" (code "begin") " → sequential statements") + (li (code "when") " → " (code "if:") " block") + (li "Mutation detection: scan for " (code "set!") " across lambda boundaries"))) + + (~doc-subsection :title "Phase 3: File Translator" + (p "Process spec files the same way " (code "bootstrap_py.py") " does:") + (ul :class "list-disc pl-6 space-y-1 text-stone-700" + (li (code "py-extract-defines") " — parse .sx source, collect top-level defines") + (li (code "py-translate-file") " — translate a list of define expressions") + (li (code "py-translate-module") " — read a .sx file and produce Python source") + (li "Section labels: " (code "# === Transpiled from eval ===") " etc."))) + + (~doc-subsection :title "Phase 4: Bootstrap Runner" + (p "A thin Python script that:") + (ol :class "list-decimal pl-6 space-y-1 text-stone-700" + (li "Loads " (code "py.sx") " into the SX evaluator") + (li "Parses each spec file (" (code "eval.sx") ", " (code "render.sx") ", etc.)") + (li "Calls " (code "py-translate-file") " on the parsed expressions") + (li "Emits the static preamble (types, platform interface)") + (li "Concatenates translated sections") + (li "Emits the static postamble (fixups, public API)")) + (p "The static sections (preamble, platform, primitives) stay in Python — " + "they're host-specific by definition. Only the transpilation of " + (code ".sx") " spec logic moves to SX.")) + + (~doc-subsection :title "Phase 5: Verification" + (p "Prove correctness by comparing outputs:") + (~doc-code :code (highlight "# Generate with hand-written bootstrapper +python bootstrap_py.py > sx_ref_g0.py + +# Generate with py.sx (G1) +python run_py_sx.py > sx_ref_g1.py + +# They must be identical +diff sx_ref_g0.py sx_ref_g1.py + +# Generate with G1 output running py.sx (G2) +python run_py_sx_with_ref.py > sx_ref_g2.py + +# Fixed-point: G1 == G2 +diff sx_ref_g1.py sx_ref_g2.py" "bash")) + (p "When all three diffs are empty, the bootstrapper is self-hosting."))) + + ;; ----------------------------------------------------------------------- + ;; What py.sx is NOT + ;; ----------------------------------------------------------------------- + + (~doc-section :title "Scope and Non-Goals" :id "scope" + (p (code "py.sx") " is " (em "not") " a general-purpose SX-to-Python compiler. " + "It only needs to translate the restricted SX subset used in the spec files:") + (ul :class "list-disc pl-6 space-y-1 text-stone-700" + (li "No " (code "defcomp") " / " (code "defmacro") " emission — those are runtime constructs that " (code "eval.sx") " itself handles") + (li "No HTML rendering — that's inside the spec, not the translation") + (li "No I/O — the spec is pure functions") + (li "No " (code "defpage") " / " (code "defhandler") " — those are app-level forms")) + (p "The full RENAMES table from " (code "bootstrap_py.py") " (200+ entries) moves into " + (code "py.sx") " as a dict literal. This is the largest single piece — " + "a mapping from SX names to their exact Python equivalents.")) + + ;; ----------------------------------------------------------------------- + ;; Implications + ;; ----------------------------------------------------------------------- + + (~doc-section :title "Implications" :id "implications" + (~doc-subsection :title "Level 1: Practical" + (p "One less Python file to maintain. Changes to the transpilation logic " + "are written in SX and tested with the SX test harness. The spec and its " + "compiler live in the same language.")) + + (~doc-subsection :title "Level 2: Architectural" + (p "With " (code "z3.sx") " (SMT-LIB), " (code "py.sx") " (Python), and " + (code "bootstrap_js.py") " → future " (code "js.sx") " (JavaScript), " + "the pattern is clear: SX translators are SX programs. " + "Adding a new target language means writing one " (code ".sx") " file, " + "not a new Python compiler.") + (p "The roadmap:") + (ul :class "list-disc pl-6 space-y-1 text-stone-700" + (li (code "py.sx") " → Python (this plan)") + (li (code "js.sx") " → JavaScript (replaces " (code "bootstrap_js.py") ")") + (li (code "go.sx") " → Go (new host)") + (li (code "rs.sx") " → Rust (new host)") + (li (code "hs.sx") " → Haskell (new host)")) + (p "Each new host only needs: (1) a minimal evaluator to run " (code "py.sx") " / " + (code "{host}.sx") " once, and (2) the platform interface in the target language.")) + + (~doc-subsection :title "Level 3: Philosophical" + (p "A self-hosting bootstrapper is a fixed point. The spec defines behavior. " + "The translator is itself defined in terms of that behavior. Running the " + "translator on the spec produces a program that can run the translator on " + "the spec and get the same program.") + (p "This is the same structure as a quine — a program that outputs itself. " + "But instead of textual self-reproduction, it's " (em "semantic") " " + "self-reproduction: the spec's meaning is preserved across the translation, " + "and the translation process is defined within the spec's language.") + (p "Gödel showed that any sufficiently powerful formal system can encode statements " + "about itself. A self-hosting bootstrapper is the constructive version: " + "the system doesn't just " (em "talk") " about itself, it " (em "builds") " itself."))) + + ;; ----------------------------------------------------------------------- + ;; Existing Patterns + ;; ----------------------------------------------------------------------- + + (~doc-section :title "Existing Patterns" :id "patterns" + (p "The " (code "z3.sx") " translator establishes the pattern " (code "py.sx") " follows:") + (div :class "overflow-x-auto rounded border border-stone-200 my-4" + (table :class "w-full text-sm" + (thead :class "bg-stone-50" + (tr + (th :class "px-4 py-2 text-left font-semibold text-stone-700" "Concern") + (th :class "px-4 py-2 text-left font-semibold text-stone-700" (code "z3.sx")) + (th :class "px-4 py-2 text-left font-semibold text-stone-700" (code "py.sx")))) + (tbody + (tr :class "border-t border-stone-100" + (td :class "px-4 py-2" "Name mapping") + (td :class "px-4 py-2 font-mono" "z3-name, z3-sym") + (td :class "px-4 py-2 font-mono" "py-mangle")) + (tr :class "border-t border-stone-100" + (td :class "px-4 py-2" "Type mapping") + (td :class "px-4 py-2 font-mono" "z3-sort") + (td :class "px-4 py-2 font-mono" "—")) + (tr :class "border-t border-stone-100" + (td :class "px-4 py-2" "Expression emission") + (td :class "px-4 py-2 font-mono" "z3-expr") + (td :class "px-4 py-2 font-mono" "py-expr")) + (tr :class "border-t border-stone-100" + (td :class "px-4 py-2" "Keyword extraction") + (td :class "px-4 py-2 font-mono" "z3-extract-kwargs") + (td :class "px-4 py-2 font-mono" "py-extract-defines")) + (tr :class "border-t border-stone-100" + (td :class "px-4 py-2" "File translation") + (td :class "px-4 py-2 font-mono" "z3-translate-file") + (td :class "px-4 py-2 font-mono" "py-translate-file")) + (tr :class "border-t border-stone-100" + (td :class "px-4 py-2" "Reader macro") + (td :class "px-4 py-2 font-mono" "#z3 expr") + (td :class "px-4 py-2 font-mono" "#py expr")) + (tr :class "border-t border-stone-100" + (td :class "px-4 py-2" "Complexity") + (td :class "px-4 py-2" "~360 lines") + (td :class "px-4 py-2" "~800-1000 lines (set!, statements)"))))) + (p (code "py.sx") " is larger because Python's statement/expression duality " + "and closure mutation rules demand more translation machinery. " + "SMT-LIB is expression-only, so " (code "z3.sx") " never needs statement mode.")))) diff --git a/sx/sxc/pages/docs.sx b/sx/sxc/pages/docs.sx index a02eb02..01d6aa3 100644 --- a/sx/sxc/pages/docs.sx +++ b/sx/sxc/pages/docs.sx @@ -634,6 +634,7 @@ "reader-macros" (~plan-reader-macros-content) "reader-macro-demo" (~plan-reader-macro-demo-content) "theorem-prover" (~plan-theorem-prover-content) + "self-hosting-bootstrapper" (~plan-self-hosting-bootstrapper-content) "sx-activity" (~plan-sx-activity-content) "predictive-prefetch" (~plan-predictive-prefetch-content) "content-addressed-components" (~plan-content-addressed-components-content)