diff --git a/.gitignore b/.gitignore index 7a5f3d88..2da01d55 100644 --- a/.gitignore +++ b/.gitignore @@ -1,3 +1,4 @@ CM .cm -src/frontend/buildid.sml \ No newline at end of file +src/frontend/buildid.sml +TEST/regression-wiki.txt \ No newline at end of file diff --git a/TEST/regression-wiki.mjs b/TEST/regression-wiki.mjs index 934825d4..5d9d233f 100644 --- a/TEST/regression-wiki.mjs +++ b/TEST/regression-wiki.mjs @@ -1,3 +1,4 @@ +import { exec } from "child_process"; import { readdirSync, writeFileSync } from "fs"; /* Only files that are broken *on purpose* (because they're templates @@ -28,18 +29,17 @@ const UNSAFE_WIKI_FILES = new Set([ "user-hdeyoung-monweakfoc-elf", ]); +exec("node elf-watcher.mjs", { cwd: "../wiki/" }); const WIKI_TWELF_LOC = "../wiki/pages/"; const cfgs = []; for (const file of readdirSync(WIKI_TWELF_LOC)) { - if (file.endsWith(".elf")) { + if (file.endsWith(".cfg")) { const base = file.slice(0, file.length - 4); if (IGNORED_WIKI_FILES.has(base)) continue; - const cfg = base + ".cfg"; - writeFileSync(WIKI_TWELF_LOC + cfg, file); cfgs.push( `test${ UNSAFE_WIKI_FILES.has(base) ? "Unsafe" : "" - } ${WIKI_TWELF_LOC}${cfg}` + } ${WIKI_TWELF_LOC}${file}` ); } } diff --git a/wiki/elf-to-mdx.mjs b/wiki/elf-to-mdx.mjs index c7a834ed..4bb6e075 100644 --- a/wiki/elf-to-mdx.mjs +++ b/wiki/elf-to-mdx.mjs @@ -67,9 +67,11 @@ async function hashToHex(content) { * * @param {string} elfFilename * The Elf file to process + * @param {string[]} prelude + * Any Elf prelude that should get appended to the Twelf context * @returns {Promise} */ -export async function elfToMdx(elfFilename) { +export async function elfToMdx(elfFilename, prelude = []) { const elfFile = readFileSync(elfFilename, "utf-8"); /* Parse out header */ @@ -87,7 +89,7 @@ export async function elfToMdx(elfFilename) { /** @type {string[]} */ let body = []; /** @type {string[]} */ - let twelfcontext = []; + let twelfcontext = prelude.slice(); /** @typedef {{ type: "twelf", subtype: null | "hidden" | "checked", accum: string[] }} TwelfState */ /** @typedef {{ type: "markdown-block", subtype: "math" | "twelf" | "checkedtwelf", accum: string[] }} MarkdownBlockState */ @@ -104,7 +106,11 @@ export async function elfToMdx(elfFilename) { (state.subtype === "twelf" || state.subtype === "checkedtwelf")) ) ) { - throw new TypeError(`state ${state.type} - ${state.type !== 'markdown' ? state.subtype : 'none'}`); + throw new TypeError( + `state ${state.type} - ${ + state.type !== "markdown" ? state.subtype : "none" + }` + ); } mutablyTrimEmptyLines(state.accum); diff --git a/wiki/elf-watcher.mjs b/wiki/elf-watcher.mjs index 0d754158..cd58fd0a 100644 --- a/wiki/elf-watcher.mjs +++ b/wiki/elf-watcher.mjs @@ -1,6 +1,14 @@ -import { existsSync, mkdirSync, readdirSync, watch, writeFileSync } from "fs"; +import { + existsSync, + mkdirSync, + readFileSync, + readdirSync, + watch, + writeFileSync, +} from "fs"; import { argv } from "process"; import { elfToMdx } from "./elf-to-mdx.mjs"; +import { getImportedPrelude } from "./elf-wiki-imports.mjs"; const DIR_OF_ELF = "pages"; const DIR_OF_MDX = "src/content/docs/wiki"; @@ -17,10 +25,49 @@ async function mdxOfFile(file) { if (!file.endsWith(".elf") || !existsSync(elfname)) return; const base = file.slice(0, file.length - 4); + const cfgname = `${DIR_OF_ELF}/${base}.cfg`; const mdxname = `${DIR_OF_MDX}/${base}.mdx`; console.log(`elf->mdx transforming ${file}`); - const mdxFile = await elfToMdx(elfname); - writeFileSync(mdxname, mdxFile); + try { + const prelude = getImportedPrelude(`${DIR_OF_ELF}/`, file); + const mdxFile = await elfToMdx( + elfname, + prelude.map(({ file, contents }) => `%%! file: ${file}\n${contents}\n`) + ); + const cfg = ` +% DO NOT EDIT +% Automatically generated by running "npm run dev" or "npm run build" in the +% wiki directory. +% Edit twelf/wiki/${file} instead + +${prelude.map(({ file }) => file).join("\n")} +${file} +`.trim(); + if ( + !existsSync(cfgname) || + readFileSync(cfgname).toString("utf-8") !== cfg + ) { + if (existsSync(cfgname)) { + console.log(`elf->mdx: updating ${cfgname}`); + } + writeFileSync(cfgname, cfg); + } + + writeFileSync(mdxname, mdxFile); + } catch (e) { + console.log(e); + writeFileSync( + mdxname, + ` +--- +--- + +Error transforming ${file} + +${e} +` + ); + } } console.log(`elf->mdx checking existing files...`); diff --git a/wiki/elf-wiki-imports.mjs b/wiki/elf-wiki-imports.mjs new file mode 100644 index 00000000..6fe9f8fd --- /dev/null +++ b/wiki/elf-wiki-imports.mjs @@ -0,0 +1,72 @@ +import { readFileSync } from "fs"; + +/** + * Read the file's header to get all of the imported elf files + * (in reverse order) + * + * @param {string} contents + */ +function getImportedFilenames(contents) { + /**@type {string[]} */ + const importStatements = []; + + for (const line of contents.split("\n")) { + if (!line.startsWith("%%! ")) break; + if (line.startsWith("%%! import: ")) { + importStatements.push(line.slice(12).trim()); + } + } + + return importStatements; +} + +/** + * Uses a DFS traversal + * + * @param {string} base + * Relative path of elf files + * @param {Set} known + * Avoids double-importing by tracking all the filenames ever added to `accum` in the process of this traversal + * @param {{file: string, contents: string}[]} accum + * Accumulates the files, making sure that files are added after their dependencies + * @param {string} elfname + * Name of an ELF file that is a dependency of the file we're trying to load + */ +function dfsAccumImportedPrelude(base, known, accum, elfname) { + if (!elfname.match(/^[a-zA-Z.\-_0-9]*[.]elf*$/)) { + throw new Error( + `Imported path ${elfname} invalid: must include only letters, numbers, dashes, and underscores and end in .elf` + ); + } + const contents = readFileSync(`${base}${elfname}`).toString("utf-8"); + for (const importElf in getImportedFilenames(contents)) { + if (!known.has(importElf)) { + known.add(importElf); + dfsAccumImportedPrelude(base, known, accum, importElf); + } + } + accum.push({ file: elfname, contents }); +} + +/** + * + * @param {string} base + * Relative path of elf files + * @param {string} elfname + */ +export function getImportedPrelude(base, elfname) { + /**@type {Set} */ + const known = new Set(); + + /**@type {{file: string, contents: string}[]} */ + const dependencies = []; + + for (const file of getImportedFilenames( + readFileSync(`${base}${elfname}`).toString("utf-8") + )) { + known.add(file); + dfsAccumImportedPrelude(base, known, dependencies, file); + } + + return dependencies; +} diff --git a/wiki/pages/proving-metatheorems-proving-totality-assertions-about-the-natural-numbers.elf b/wiki/pages/proving-metatheorems-proving-totality-assertions-about-the-natural-numbers.elf index 81665d8c..456de978 100644 --- a/wiki/pages/proving-metatheorems-proving-totality-assertions-about-the-natural-numbers.elf +++ b/wiki/pages/proving-metatheorems-proving-totality-assertions-about-the-natural-numbers.elf @@ -142,7 +142,7 @@ plus-bad-output : plus (s N1) N2 (s (s N3)) Here we have insisted that the output of the premise has the form ``s N3`` for some ``N3``. Twelf correctly reports an output coverage error because this condition can fail (for example, if the premise was ``plus-z : plus z z z``). -Pattern-matching the output of a premise is like an [[inversion]] step in a proof: you're insisting that the premise derivation must conclude a particular fact that is more specific than the judgement form itself. For Twelf to accept a relation as total, Twelf must notice that all of these inversions are permissible. Twelf permits such inversions when it is readily apparent that they are justified, and those inversions that Twelf does not accept can be proved explicitly. +Pattern-matching the output of a premise is like an inversion step in a proof: you're insisting that the premise derivation must conclude a particular fact that is more specific than the judgement form itself. For Twelf to accept a relation as total, Twelf must notice that all of these inversions are permissible. Twelf permits such inversions when it is readily apparent that they are justified, and those inversions that Twelf does not accept can be proved explicitly. In this example, we got an output coverage error because we constrained the output of the premise by insisting it be formed by a particular constant. The other way to get output coverage errors is to insist that the output of a premise be a variable that occurs elsewhere in the type. For example: diff --git a/wiki/pages/type-safety-for-the-stlc.elf b/wiki/pages/type-safety-for-the-stlc.elf new file mode 100644 index 00000000..7f9e7a5f --- /dev/null +++ b/wiki/pages/type-safety-for-the-stlc.elf @@ -0,0 +1,245 @@ +%%! title: "Type safety for the simply-typed lambda calculus" +%%! description: "Proving type safety from progress and preservation in the simply-typed lambda calculus" +%%! import: simply-typed-lambda-calculus.elf + +%{! + +This page incorporates the [simply typed lambda calculus](/wiki/simply-typed-lambda-calculus/) with just functions and the unit type. +This is the exact same system that is discussed in the [introduction to proving metatheorems in Twelf](/wiki/proving-metatheorems-representing-the-syntax-of-the-stlc/). + +The motto of type safety, attributed to Robin Milner, is that "well-typed programs can't go wrong." That means program that initially passes the static semantics will be free of undefined behavior: after an arbitrary number of steps, a program is either in a valid halting state (for the STLC, this means it is a _value_) or it can take another step according to the operational semantics. This means that there's always a way for an unfinished program to take a step according to the operational semantics: a well-typed program can't get "stuck." + +### Multistep evaluation + +Multistep evaluation is easy to define as an inductive definition by using single-step evaluation . + +```math +{ + \over + e \mapsto^* e +}\textit{multistep-stop} +\qquad +{ + e_1 \mapsto e_2 + \qquad + e_2 \mapsto^* e_3 + \over + e_1 \mapsto^* e_3 +}\textit{multistep-go} +``` + +This definition translates straightforwardly into Twelf: + +!}% + +multistep : tm -> tm -> type. + +multistep-stop : multistep E E. +multistep-go : multistep E1 E3 + <- step E1 E2 + <- multistep E2 E3. + +%worlds () (multistep _ _). + +%{! + +### Stating the safety theorem + +This definition can used to make the motto "well-typed programs can't go wrong" into a formal logical statement: + +> **Type safety**: if and , then either or there exists an such that . + +Twelf doesn't have a direct way of encoding the "or" part of the conclusion, but the workaround is simple: we define a new relation `val-or-step E` that is true if either `E` is a value or `E` can take a step: + +!}% + +val-or-step : tm -> type. + +val-or-step-val : val-or-step E + <- value E. +val-or-step-step : val-or-step E + <- step E E'. + +%{! + +With that auxillary definition, the statement of type safety is straightforward: + +!}% + +safety : of E T -> multistep E E' -> val-or-step E' -> type. +%mode safety +D1 +D2 -D3. + +%{! + +The "safety = progress + preservation" formula derives the safety property by proving two lemmas. Preservation (and the preservation proof here is [exactly the same as the proof presented in the introduction to proving metatheorems in Twelf](/wiki/proving-metatheorems-proving-metatheorems-about-the-stlc/)). + +## Preservation + +The statement of preservation for the STLC is as follows: + +> If and , then . + +!}% + +preserv : step E E' -> of E T -> of E' T -> type. +%mode preserv +Dstep +Dof -Dof'. + +- : preserv (step-app-1 (DstepE1 : step E1 E1')) + (of-app (DofE2 : of E2 T2) + (DofE1 : of E1 (arrow T2 T))) + (of-app DofE2 DofE1') + <- preserv DstepE1 DofE1 (DofE1' : of E1' (arrow T2 T)). + +- : preserv (step-app-2 (DstepE2 : step E2 E2') (DvalE1 : value E1)) + (of-app (DofE2 : of E2 T2) + (DofE1 : of E1 (arrow T2 T))) + (of-app DofE2' DofE1) + <- preserv DstepE2 DofE2 (DofE2' : of E2' T2). + +- : preserv (step-app-beta (Dval : value E2)) + (of-app (DofE2 : of E2 T2) + (of-lam (([x] [dx] DofE x dx) + : {x : tm} {dx : of x T2} of (E x) T))) + (DofE E2 DofE2). + +%{! + +Preservation can be established by induction on the expression , by induction on the typing dervation , or by induction on the step relation . We give a termination ordering here that corresponds to the third option: + +!}% + + +%{!! begin checked !!}% +%worlds () (preserv _ _ _). +%total D (preserv D _ _). +%{!! end checked !!}% + + +%{! + +## Progress + +The statement of progress for a programming language like this one is: + +> If , then either or there exists an such that . + +We'll operate by induction over the typing derivation: the statement in Twelf uses the `val-or-step` judgment described above. + +!}% + +progress : of E T -> val-or-step E -> type. +%mode progress +Dof -Dvos. + +%{! + +Proceeding by induction over the typing derivation, two of the cases are very simple, since `empty` is a value and so is any function `lam [x] E x`. + +!}% + +- : progress of-empty (val-or-step-val value-empty). + +- : progress (of-lam ([x] [dx] DofE x dx)) (val-or-step-val value-lam). + +%{! + +### The application case and output factoring + +On paper, the progress case for application goes as follows: + +* We have subderivations and for some . +* By induction on these two subderivations, either steps or is a value, and either steps or is a value. +* If steps to , then +* Otherwise, if steps to , then +* Otherwise, and are both values. By a [canonical forms lemma](/wiki/canonical-forms-lemma/), it must be the case that for some , and so . + +A _natural_ way to state these cases and conclude the proof would be as follows: + +```checkedtwelf +- : progress (of-app DofE2 DofE1) (val-or-step-step (step-app-1 DstepE1)) + <- progress DofE1 (val-or-step-step DstepE1). +- : progress (of-app DofE2 DofE1) (val-or-step-step (step-app-2 DstepE2 DvalE1)) + <- progress DofE1 (val-or-step-val DvalE1) + <- progress DofE2 (val-or-step-step DstepE2). +- : progress (of-app DofE2 DofE1) (val-or-step-step (step-app-beta DvalE2)) + <- progress DofE1 (val-or-step-val value-lam) + <- progress DofE2 (val-or-step-val DvalE2). + +%worlds () (progress _ _). +%total D (progress D _). +``` + +But this is asking Twelf to do a lot, more than its relatively simple coverage checking algorithm can handle in its present form. This kind of reasoning, where we need to do different things depending on the result of the inductive call, is exactly when we need to use [output factoring](/wiki/output-factoring/). + +In this case, output factoring looks like adding a lemma that represents what we know after we make the two inductive calls in the on-paper progress lemma. + +> If ,\ +> and , +> and is a value or there exists an such that ,\ +> and is a value or there exists an such that ,\ +> then is a value or there exists an such that +. + +Or, in Twelf: !}% + +progress-app : of E1 (arrow T' T) + -> of E2 T' + -> val-or-step E1 + -> val-or-step E2 + -> val-or-step (app E1 E2) + -> type. +%mode progress-app +DofE1 +DofE2 +DvosE1 +DvosE2 -Dvos. + +- : progress-app DofE2 DofE1 (val-or-step-step DstepE1) _ + (val-or-step-step (step-app-1 DstepE1)). +- : progress-app DofE2 DofE1 (val-or-step-val DvalE1) (val-or-step-step DstepE2) + (val-or-step-step (step-app-2 DstepE2 DvalE1)). +- : progress-app DofE2 DofE1 (val-or-step-val value-lam) (val-or-step-val DvalE2) + (val-or-step-step (step-app-beta DvalE2)). + +%{! These cases includes the appeal to the canonical forms lemma that we saw in the informal proof: the page on [canonical forms lemmas](/wiki/canonical-forms-lemma/) discusses when canonical forms can be established "for free" like this. + +There's no induction in this output factoring lemma, so the `%total` statement doesn't need any arguments. !}% + +%{!! begin checked !!}% +%worlds () (progress-app _ _ _ _ _). +%total {} (progress-app _ _ _ _ _). +%{!! end checked !!}% + + +%{! + +### Completing the progress proof + +The application case of progress is just one case that directly appeals to the `progress-app` lemma, instead of the three cases from our failed attempt. + +!}% + +- : progress (of-app DofE2 DofE1) Dvalorstep + <- progress DofE1 DvalorstepE1 + <- progress DofE2 DvalorstepE2 + <- progress-app DofE1 DofE2 DvalorstepE1 DvalorstepE2 Dvalorstep. + +%worlds () (progress _ _). +%total (D) (progress D _). + +%{! ### Variations + +When using output factoring lemmas, there are usually lots of ways of moving things around. Two variations you might want to try yourself: + +1. At least one of the arguments of `progress-app` can be removed: identify which one and prove progress without that argument. +2. The application case doesn't need to output `val-or-step (app E1 E2)`, because `app E1 E2` always steps. Try re-proving `progress-app` where the output is `step (app E1 E2) E3`, and then fix the proof of `progress` accordingly. + +## Safety + +The proof of safety from the beginning directly proceeds by induction over the definition of multi-step evaluation, appealing to progress in one case and preservation in the other. + +!}% + +- : safety Dof multistep-stop Dvalorstep + <- progress Dof Dvalorstep. +- : safety Dof (multistep-go Dmultistep Dsinglestep) Dvalorstep + <- preserv Dsinglestep Dof Dof' + <- safety Dof' Dmultistep Dvalorstep. + +%worlds () (safety _ _ _). +%total (Dmultistep) (safety _ Dmultistep _).