From 39687425b3f62bc2ada62747e082bdf55bca3eed Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Mon, 15 Apr 2024 18:08:01 -0400 Subject: [PATCH 1/6] Allow an 'import' statement in the prelude to import context from other Wiki files --- wiki/elf-to-mdx.mjs | 13 ++- wiki/elf-watcher.mjs | 102 +++++++++++++++++++- wiki/pages/type-safety-for-the-stlc.elf | 119 ++++++++++++++++++++++++ 3 files changed, 226 insertions(+), 8 deletions(-) create mode 100644 wiki/pages/type-safety-for-the-stlc.elf diff --git a/wiki/elf-to-mdx.mjs b/wiki/elf-to-mdx.mjs index c7a834ed..6aa37f7a 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,8 @@ export async function elfToMdx(elfFilename) { /** @type {string[]} */ let body = []; /** @type {string[]} */ - let twelfcontext = []; + let twelfcontext = prelude.slice(); + console.log(twelfcontext); /** @typedef {{ type: "twelf", subtype: null | "hidden" | "checked", accum: string[] }} TwelfState */ /** @typedef {{ type: "markdown-block", subtype: "math" | "twelf" | "checkedtwelf", accum: string[] }} MarkdownBlockState */ @@ -104,7 +107,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..a72c6299 100644 --- a/wiki/elf-watcher.mjs +++ b/wiki/elf-watcher.mjs @@ -1,4 +1,11 @@ -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"; @@ -8,6 +15,73 @@ if (!existsSync(DIR_OF_MDX)) { mkdirSync("src/content/docs/wiki"); } +/** + * 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 {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(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(`${DIR_OF_ELF}/${elfname}`).toString("utf-8"); + for (const importElf in getImportedFilenames(contents)) { + if (!known.has(importElf)) { + known.add(importElf); + dfsAccumImportedPrelude(known, accum, importElf); + } + } + accum.push({ file: elfname, contents }); +} + +/** + * + * @param {string} elfname + */ +function getImportedPrelude(elfname) { + /**@type {Set} */ + const known = new Set(); + + /**@type {{file: string, contents: string}[]} */ + const dependencies = []; + + for (const file of getImportedFilenames( + readFileSync(elfname).toString("utf-8") + )) { + known.add(file); + dfsAccumImportedPrelude(known, dependencies, file); + } + + return dependencies; +} + /** * Convert and store a Wiki Twelf file as MDX * @param {string} file @@ -15,12 +89,30 @@ if (!existsSync(DIR_OF_MDX)) { async function mdxOfFile(file) { const elfname = `${DIR_OF_ELF}/${file}`; if (!file.endsWith(".elf") || !existsSync(elfname)) return; - const base = file.slice(0, file.length - 4); const mdxname = `${DIR_OF_MDX}/${base}.mdx`; - console.log(`elf->mdx transforming ${file}`); - const mdxFile = await elfToMdx(elfname); - writeFileSync(mdxname, mdxFile); + try { + console.log(`elf->mdx transforming ${file}`); + const prelude = getImportedPrelude(elfname); + const mdxFile = await elfToMdx( + elfname, + prelude.map(({ file, contents }) => `%%! file: ${file}\n${contents}\n`) + ); + 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/pages/type-safety-for-the-stlc.elf b/wiki/pages/type-safety-for-the-stlc.elf new file mode 100644 index 00000000..49d485b3 --- /dev/null +++ b/wiki/pages/type-safety-for-the-stlc.elf @@ -0,0 +1,119 @@ +%%! 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. +vos-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 a programming language is as follows: + +> If and , then . + +It's common + +!}% + +preserv : step E E' -> of E T -> of E' T -> type. +%mode preserv +Dstep +Dof -Dof'. + +preserv-app-1 : 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-app-2 : 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-app-beta : 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). +%{!! begin checked !!}% +%worlds () (preserv _ _ _). +%total D (preserv D _ _). +%{!! end checked !!}% + + +%{! + +## Progress + +!}% From 82e98de599c8965540f7269fa8d1679f95141470 Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Mon, 15 Apr 2024 18:29:29 -0400 Subject: [PATCH 2/6] Fix regression tests --- TEST/regression-wiki.mjs | 7 +++- wiki/elf-watcher.mjs | 79 ++------------------------------------- wiki/elf-wiki-imports.mjs | 72 +++++++++++++++++++++++++++++++++++ 3 files changed, 81 insertions(+), 77 deletions(-) create mode 100644 wiki/elf-wiki-imports.mjs diff --git a/TEST/regression-wiki.mjs b/TEST/regression-wiki.mjs index 934825d4..05927e69 100644 --- a/TEST/regression-wiki.mjs +++ b/TEST/regression-wiki.mjs @@ -1,4 +1,5 @@ import { readdirSync, writeFileSync } from "fs"; +import { getImportedPrelude } from "../wiki/elf-wiki-imports.mjs"; /* Only files that are broken *on purpose* (because they're templates * meant to be filled out as exercises) should be added here. @@ -35,7 +36,11 @@ for (const file of readdirSync(WIKI_TWELF_LOC)) { 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); + const dependencies = getImportedPrelude(WIKI_TWELF_LOC, file); + writeFileSync( + WIKI_TWELF_LOC + cfg, + dependencies.map(({ file }) => file + "\n") + file + ); cfgs.push( `test${ UNSAFE_WIKI_FILES.has(base) ? "Unsafe" : "" diff --git a/wiki/elf-watcher.mjs b/wiki/elf-watcher.mjs index a72c6299..2b627437 100644 --- a/wiki/elf-watcher.mjs +++ b/wiki/elf-watcher.mjs @@ -1,13 +1,7 @@ -import { - existsSync, - mkdirSync, - readFileSync, - readdirSync, - watch, - writeFileSync, -} from "fs"; +import { existsSync, mkdirSync, 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"; @@ -15,73 +9,6 @@ if (!existsSync(DIR_OF_MDX)) { mkdirSync("src/content/docs/wiki"); } -/** - * 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 {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(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(`${DIR_OF_ELF}/${elfname}`).toString("utf-8"); - for (const importElf in getImportedFilenames(contents)) { - if (!known.has(importElf)) { - known.add(importElf); - dfsAccumImportedPrelude(known, accum, importElf); - } - } - accum.push({ file: elfname, contents }); -} - -/** - * - * @param {string} elfname - */ -function getImportedPrelude(elfname) { - /**@type {Set} */ - const known = new Set(); - - /**@type {{file: string, contents: string}[]} */ - const dependencies = []; - - for (const file of getImportedFilenames( - readFileSync(elfname).toString("utf-8") - )) { - known.add(file); - dfsAccumImportedPrelude(known, dependencies, file); - } - - return dependencies; -} - /** * Convert and store a Wiki Twelf file as MDX * @param {string} file @@ -93,7 +20,7 @@ async function mdxOfFile(file) { const mdxname = `${DIR_OF_MDX}/${base}.mdx`; try { console.log(`elf->mdx transforming ${file}`); - const prelude = getImportedPrelude(elfname); + const prelude = getImportedPrelude(`${DIR_OF_ELF}/`, file); const mdxFile = await elfToMdx( elfname, prelude.map(({ file, contents }) => `%%! file: ${file}\n${contents}\n`) 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; +} From b0c7608b75120e47eec7a8cd973f69c511dcd4f9 Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Mon, 15 Apr 2024 18:43:50 -0400 Subject: [PATCH 3/6] log-- --- wiki/elf-to-mdx.mjs | 1 - 1 file changed, 1 deletion(-) diff --git a/wiki/elf-to-mdx.mjs b/wiki/elf-to-mdx.mjs index 6aa37f7a..4bb6e075 100644 --- a/wiki/elf-to-mdx.mjs +++ b/wiki/elf-to-mdx.mjs @@ -90,7 +90,6 @@ export async function elfToMdx(elfFilename, prelude = []) { let body = []; /** @type {string[]} */ let twelfcontext = prelude.slice(); - console.log(twelfcontext); /** @typedef {{ type: "twelf", subtype: null | "hidden" | "checked", accum: string[] }} TwelfState */ /** @typedef {{ type: "markdown-block", subtype: "math" | "twelf" | "checkedtwelf", accum: string[] }} MarkdownBlockState */ From 951b5f8fa107a640ee901597c5179649e567c2f2 Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Wed, 17 Apr 2024 17:01:44 -0400 Subject: [PATCH 4/6] Move the cfg generation to be more closely connected to the wiki --- .gitignore | 3 ++- TEST/regression-wiki.mjs | 13 ++++--------- wiki/elf-watcher.mjs | 29 ++++++++++++++++++++++++++++- 3 files changed, 34 insertions(+), 11 deletions(-) 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 05927e69..5d9d233f 100644 --- a/TEST/regression-wiki.mjs +++ b/TEST/regression-wiki.mjs @@ -1,5 +1,5 @@ +import { exec } from "child_process"; import { readdirSync, writeFileSync } from "fs"; -import { getImportedPrelude } from "../wiki/elf-wiki-imports.mjs"; /* Only files that are broken *on purpose* (because they're templates * meant to be filled out as exercises) should be added here. @@ -29,22 +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"; - const dependencies = getImportedPrelude(WIKI_TWELF_LOC, file); - writeFileSync( - WIKI_TWELF_LOC + cfg, - dependencies.map(({ file }) => file + "\n") + file - ); cfgs.push( `test${ UNSAFE_WIKI_FILES.has(base) ? "Unsafe" : "" - } ${WIKI_TWELF_LOC}${cfg}` + } ${WIKI_TWELF_LOC}${file}` ); } } diff --git a/wiki/elf-watcher.mjs b/wiki/elf-watcher.mjs index 2b627437..683dcb82 100644 --- a/wiki/elf-watcher.mjs +++ b/wiki/elf-watcher.mjs @@ -1,4 +1,11 @@ -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"; @@ -17,6 +24,7 @@ async function mdxOfFile(file) { const elfname = `${DIR_OF_ELF}/${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`; try { console.log(`elf->mdx transforming ${file}`); @@ -25,6 +33,25 @@ async function mdxOfFile(file) { 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); From f72a0ae517ff8f91c828e98d016bbb45baefbcfc Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Wed, 17 Apr 2024 19:59:38 -0400 Subject: [PATCH 5/6] Compliant style and complete proof for type safety for the natural numbers --- ...y-assertions-about-the-natural-numbers.elf | 2 +- wiki/pages/type-safety-for-the-stlc.elf | 170 +++++++++++++++--- 2 files changed, 149 insertions(+), 23 deletions(-) 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 index 49d485b3..7f9e7a5f 100644 --- a/wiki/pages/type-safety-for-the-stlc.elf +++ b/wiki/pages/type-safety-for-the-stlc.elf @@ -57,7 +57,7 @@ val-or-step : tm -> type. val-or-step-val : val-or-step E <- value E. -vos-or-step-step : val-or-step E +val-or-step-step : val-or-step E <- step E E'. %{! @@ -75,37 +75,40 @@ The "safety = progress + preservation" formula derives the safety property by pr ## Preservation -The statement of preservation for a programming language is as follows: +The statement of preservation for the STLC is as follows: > If and , then . -It's common - !}% preserv : step E E' -> of E T -> of E' T -> type. %mode preserv +Dstep +Dof -Dof'. -preserv-app-1 : 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-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-app-2 : 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-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-app-beta : 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). +- : 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 _ _). @@ -116,4 +119,127 @@ preserv-app-beta : preserv ## 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 _). From fd2b3c0cfcc35021bfecd557a1ee369a8e9ee0ad Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Wed, 17 Apr 2024 22:08:53 -0400 Subject: [PATCH 6/6] Make diff a bit prettier --- wiki/elf-watcher.mjs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/wiki/elf-watcher.mjs b/wiki/elf-watcher.mjs index 683dcb82..cd58fd0a 100644 --- a/wiki/elf-watcher.mjs +++ b/wiki/elf-watcher.mjs @@ -23,11 +23,12 @@ if (!existsSync(DIR_OF_MDX)) { async function mdxOfFile(file) { const elfname = `${DIR_OF_ELF}/${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}`); try { - console.log(`elf->mdx transforming ${file}`); const prelude = getImportedPrelude(`${DIR_OF_ELF}/`, file); const mdxFile = await elfToMdx( elfname,