diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml new file mode 100644 index 000000000..68f829011 --- /dev/null +++ b/.github/workflows/docs.yml @@ -0,0 +1,104 @@ +name: Build documentation + +on: + push: + branches: + - "main" + pull_request: + +permissions: + contents: read + pages: write + id-token: write + +concurrency: + group: "pages" + cancel-in-progress: true + +jobs: + build: + runs-on: ubuntu-latest + + steps: + - name: Checkout + uses: actions/checkout@v4 + + - name: Set up Node.js + uses: actions/setup-node@v4 + with: + node-version: "20" + + - name: Install npm dependencies + run: | + make -C doc ecproof-deps + + - name: Set up Python + uses: actions/setup-python@v5 + with: + python-version: "3.13" + + - name: Install Python dependencies + run: | + make -C doc sphinx-deps + + - name: Set-up OCaml + uses: ocaml/setup-ocaml@v3 + with: + ocaml-compiler: 5.4 + opam-disable-sandboxing: true + dune-cache: true + + - name: Install EasyCrypt dependencies + run: | + opam pin add -n easycrypt . + opam install --deps-only --depext-only --confirm-level=unsafe-yes easycrypt + opam install --deps-only easycrypt + + - name: Compile & Install EasyCrypt + run: | + opam exec -- make PROFILE=release install + + - name: Build Sphinx HTML + run: | + opam exec -- make -C doc ecproof-bundle sphinx-html + + - name: Upload Pages artifact + uses: actions/upload-pages-artifact@v3 + with: + path: doc/_build/html + + deploy: + runs-on: ubuntu-latest + if: github.event_name == 'push' && github.ref == 'refs/heads/main' + + steps: + - name: Deploy documentation + env: + PAGES_TOKEN: ${{ secrets.PAGES_REPO_TOKEN }} + PAGES_REPO: EasyCrypt/refman + TARGET_DIR: refman + BUILD_DIR: doc/_build/html + + run: | + set -euo pipefail + + git config --global user.name "github-actions[bot]" + git config --global user.email "github-actions[bot]@users.noreply.github.com" + + git clone --depth 1 https://x-access-token:${PAGES_TOKEN}@github.com/${PAGES_REPO}.git pages-repo + + rm -rf "pages-repo/${TARGET_DIR}" + mkdir -p "pages-repo/${TARGET_DIR}" + touch "pages-repo/${TARGET_DIR}"/.keep + + cp -a "${BUILD_DIR}/." "pages-repo/${TARGET_DIR}/" + + git -C pages-repo add -A + + if git -C pages-repo diff --cached --quiet; then + echo "No changes to deploy." + exit 0 + fi + + git -C pages-repo commit -m "Update docs: ${GITHUB_REPOSITORY}@${GITHUB_SHA}" + git -C pages-repo push origin main diff --git a/doc/.gitignore b/doc/.gitignore new file mode 100644 index 000000000..88503a8c6 --- /dev/null +++ b/doc/.gitignore @@ -0,0 +1,2 @@ +__pycache__/ +_build/ diff --git a/doc/Makefile b/doc/Makefile new file mode 100644 index 000000000..bb8b8c368 --- /dev/null +++ b/doc/Makefile @@ -0,0 +1,45 @@ +# -*- Makefile -*- + +# ------------------------------------------------------------------------ +SPHINXBUILD ?= sphinx-build +SPHINXOPTS ?= +SOURCEDIR = . +BUILDDIR = _build +NPM ?= npm + +# ------------------------------------------------------------------------ +.PHONY: + +default: + @echo "make [ecproof-deps | ecproof-bundle| sphinx-html]" >&2 + +# ------------------------------------------------------------------------ +.PHONY: sphinx-help sphinx-deps __force__ + +sphinx-help: + @$(SPHINXBUILD) -M help "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(SPHINXOPTS) + +sphinx-deps: + pip install -r requirements.txt + +sphinx-%: __force__ + @$(SPHINXBUILD) -M $* "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(SPHINXOPTS) + +# ------------------------------------------------------------------------ +.PHONY: ecproof-deps ecproof-bundle + +ECPROOFDIR = extensions/ecproofs/proofnav + +ecproof-deps: + $(NPM) --prefix="$(ECPROOFDIR)" install + +ecproof-bundle: + $(NPM) --prefix="$(ECPROOFDIR)" run build + +# ------------------------------------------------------------------------ +clean: + rm -rf _build + rm -rf "$(ECPROOFDIR)"/dist + +mrproper: clean + rm -rf "$(ECPROOFDIR)"/node_modules diff --git a/doc/_static/.keep b/doc/_static/.keep new file mode 100644 index 000000000..e69de29bb diff --git a/doc/conf.py b/doc/conf.py new file mode 100644 index 000000000..265f3262e --- /dev/null +++ b/doc/conf.py @@ -0,0 +1,38 @@ +# Configuration file for the Sphinx documentation builder. +# +# For the full list of built-in configuration values, see the documentation: +# https://www.sphinx-doc.org/en/master/usage/configuration.html + +import pathlib +import sys + +# -- Project information ----------------------------------------------------- +# https://www.sphinx-doc.org/en/master/usage/configuration.html#project-information + +project = 'EasyCrypt refman' +copyright = '2026, EasyCrypt development team' +author = 'EasyCrypt development team' + +# -- General configuration --------------------------------------------------- +# https://www.sphinx-doc.org/en/master/usage/configuration.html#general-configuration + +EXTENSIONS = pathlib.Path('extensions').resolve() +for x in ['ecpygment', 'ecproofs']: + sys.path.append(str(EXTENSIONS / x)) + +extensions = [ + 'sphinx_rtd_theme', + 'sphinx_design', + 'ecpygment', + 'ecproofs', +] + +templates_path = ['_templates'] +exclude_patterns = ['_build', 'Thumbs.db', '.DS_Store'] + +# -- Options for HTML output ------------------------------------------------- +# https://www.sphinx-doc.org/en/master/usage/configuration.html#options-for-html-output + +html_theme = 'sphinx_rtd_theme' +html_static_path = ['_static'] +highlight_language = 'easycrypt' diff --git a/doc/extensions/ecproofs/ecproofs.py b/doc/extensions/ecproofs/ecproofs.py new file mode 100644 index 000000000..55f23ed72 --- /dev/null +++ b/doc/extensions/ecproofs/ecproofs.py @@ -0,0 +1,141 @@ +# -------------------------------------------------------------- +from __future__ import annotations + +import docutils as du + +import sphinx.application as sa +import sphinx.errors as se +import sphinx.util as su + +import bisect +import json +import os +import re +import subprocess as subp +import tempfile + +# ====================================================================== +ROOT = os.path.dirname(__file__) + +# ====================================================================== +class ProofnavNode(du.nodes.General, du.nodes.Element): + @staticmethod + def visit_proofnav_node_html(self, node: ProofnavNode): + pass + + @staticmethod + def depart_proofnav_node_html(self, node: ProofnavNode): + uid = node["uid"] + json = node["json"] + + html = f""" +
+
+ +
+""" + + self.body.append(html) + +# ====================================================================== +class EasyCryptProofDirective(su.docutils.SphinxDirective): + has_content = True + + option_spec = { + 'title': su.docutils.directives.unchanged, + } + + def run(self): + env = self.state.document.settings.env + + rawcode = '\n'.join(self.content) + '\n' + + # Find the trap + if (trap := re.search(r'\(\*\s*\$\s*\*\)\s*', rawcode, re.MULTILINE)) is None: + raise se.SphinxError('Cannot find the trap') + code = rawcode[:trap.start()] + rawcode[trap.end():] + + # Find the trap sentence number + sentences = [ + m.end() - 1 + for m in re.finditer(r'\.(\s+|\$)', code) + ] + sentence = bisect.bisect_left(sentences, trap.start()) + + # Run EasyCrypt and extract the proof trace + with tempfile.TemporaryDirectory(delete = False) as tmpdir: + ecfile = os.path.join(tmpdir, 'input.ec') + ecofile = os.path.join(tmpdir, 'input.eco') + with open(ecfile, 'w') as ecstream: + ecstream.write(code) + subp.check_call( + ['easycrypt', 'compile', '-pragmas', 'Proofs:weak', '-trace', ecfile], + stdout = subp.DEVNULL, + stderr = subp.DEVNULL, + ) + with open(ecofile) as ecostream: + eco = json.load(ecostream) + + serial = env.new_serialno("proofnav") + uid = f"proofnav-{serial}" + + # Create widget metadata + data = dict() + + data["source"] = code + data["sentenceEnds"] = [x["position"] for x in eco["trace"][1:]] + data["sentences"] = [ + dict(goals = x["goals"], message = x["messages"]) + for x in eco["trace"][1:] + ] + data["initialSentence"] = sentence - 1 + + if 'title' in self.options: + data['title'] = self.options['title'] + + node = ProofnavNode() + node["uid"] = uid + node["json"] = json.dumps(data, ensure_ascii = False, separators = (",", ":")) + + return [node] + +# ====================================================================== +def on_builder_inited(app: sa.Sphinx): + out_dir = os.path.join(app.outdir, "_static", "proofnav") + os.makedirs(out_dir, exist_ok = True) + + js = os.path.join(ROOT, "proofnav", "dist", "proofnav.bundle.js") + css = os.path.join(ROOT, "proofnav", "proofnav.css") + + if not os.path.exists(js): + raise se.SphinxError( + "proofnav: bundle not found. Run the frontend build to generate " + f"{js}" + ) + + su.fileutil.copy_asset(js, out_dir) + su.fileutil.copy_asset(js + ".map", out_dir) + su.fileutil.copy_asset(css, out_dir) + +# ====================================================================== +def setup(app: sa.Sphinx) -> su.typing.ExtensionMetadata: + app.add_node( + ProofnavNode, + html = ( + ProofnavNode.visit_proofnav_node_html, + ProofnavNode.depart_proofnav_node_html, + ) + ) + + app.add_js_file("proofnav/proofnav.bundle.js", defer = "defer") + app.add_css_file("proofnav/proofnav.css") + + app.connect("builder-inited", on_builder_inited) + + app.add_directive('ecproof', EasyCryptProofDirective) + + return { + 'version': '0.1', + 'parallel_read_safe': True, + 'parallel_write_safe': True, + } diff --git a/doc/extensions/ecproofs/proofnav/.gitignore b/doc/extensions/ecproofs/proofnav/.gitignore new file mode 100644 index 000000000..3d2bc6269 --- /dev/null +++ b/doc/extensions/ecproofs/proofnav/.gitignore @@ -0,0 +1,2 @@ +/dist/ +/node_modules/ diff --git a/doc/extensions/ecproofs/proofnav/easycrypt.ts b/doc/extensions/ecproofs/proofnav/easycrypt.ts new file mode 100644 index 000000000..4680cd7c9 --- /dev/null +++ b/doc/extensions/ecproofs/proofnav/easycrypt.ts @@ -0,0 +1,114 @@ +import { StreamLanguage } from "@codemirror/language" +import type { StreamParser } from "@codemirror/language" + +type KeywordGroups = Record +type TagMap = Record + +const keywords: KeywordGroups = { + bytac : ['exact', 'assumption', 'smt', 'coq', 'check', 'edit', 'fix', 'by', 'reflexivity', 'done', 'solve'], + dangerous : ['admit', 'admitted'], + global : ['axiom', 'axiomatized', 'lemma', 'realize', 'proof', 'qed', 'abort', 'goal', 'end', 'from', 'import', 'export', 'include', 'local', 'global', 'declare', 'hint', 'module', 'of', 'const', 'op', 'pred', 'inductive', 'notation', 'abbrev', 'require', 'theory', 'abstract', 'section', 'subtype', 'type', 'class', 'instance', 'print', 'search', 'locate', 'as', 'Pr', 'clone', 'with', 'rename', 'prover', 'timeout', 'why3', 'dump', 'remove', 'exit', 'Top', 'Self'], + internal : ['fail', 'time', 'undo', 'debug', 'pragma'], + prog : ['forall', 'exists', 'fun', 'glob', 'let', 'in', 'for', 'var', 'proc', 'if', 'is', 'match', 'then', 'else', 'elif', 'match', 'for', 'while', 'assert', 'return', 'res', 'equiv', 'hoare', 'ehoare', 'phoare', 'islossless', 'async'], + tactic : ['beta', 'iota', 'zeta', 'eta', 'logic', 'delta', 'simplify', 'cbv', 'congr', 'change', 'split', 'left', 'right', 'case', 'pose', 'gen', 'have', 'suff', 'elim', 'exlim', 'ecall', 'clear', 'wlog', 'idassign', 'apply', 'rewrite', 'rwnormal', 'subst', 'progress', 'trivial', 'auto', 'idtac', 'move', 'modpath', 'field', 'fieldeq', 'ring', 'ringeq', 'algebra', 'replace', 'transitivity', 'symmetry', 'seq', 'wp', 'sp', 'sim', 'skip', 'call', 'rcondt', 'rcondf', 'swap', 'cfold', 'rnd', 'rndsem', 'pr_bounded', 'bypr', 'byphoare', 'byehoare', 'byequiv', 'byupto', 'fel', 'conseq', 'exfalso', 'inline', 'outline', 'interleave', 'alias', 'weakmem', 'fission', 'fusion', 'unroll', 'splitwhile', 'kill', 'eager'], + tactical : ['try', 'first', 'last', 'do', 'expect'], +} + +const tags: TagMap = { + bytac : "annotation", + dangerous : "invalid", + global : "namespace", + internal : "invalid", + prog : "keyword", + tactic : "controlKeyword", + tactical : "controlOperator", +} + +function buildKeywordTagMap( + keywords: KeywordGroups, + tags: TagMap +): Record { + const result: Record = {} + + for (const [group, words] of Object.entries(keywords)) { + const tag = tags[group] + if (!tag) continue + + for (const word of words) { + result[word] = tag + } + } + + return result +} + +const keywordToTag = buildKeywordTagMap(keywords, tags) + +const identRE = /^[a-zA-Z_][A-Za-z0-9_']*/ +const numberRE = /^\d+/ +const punctRE = /^[()\[\]{};,.:]/ + +type State = { commentDepth: number } + +function eatNestedComment(stream: any, state: State): void { + while (!stream.eol()) { + if (stream.match("(*")) { + state.commentDepth++ + continue + } + if (stream.match("*)")) { + state.commentDepth-- + if (state.commentDepth <= 0) { + state.commentDepth = 0 + break + } + continue + } + stream.next() + } +} + +const parser: StreamParser = { + name: "easycrypt", + startState(): State { + return {commentDepth: 0} + }, + token(stream: any, state: State): string | null { + // Nested comment continuation + if (state.commentDepth > 0) { + eatNestedComment(stream, state) + return "comment" + } + + if (stream.eatSpace()) return null + + // Nested comment start + if (stream.match("(*")) { + state.commentDepth = 1 + eatNestedComment(stream, state) + return "comment" + } + + // Numbers + if (stream.match(numberRE)) { + return "number" + } + + // Identifiers / keywords + if (stream.match(identRE)) { + const word: string = stream.current() + return keywordToTag[word] ?? "variableName" + } + + // Punctuation + if (stream.match(punctRE)) { + return "punctuation" + } + + // Always make progress + stream.next() + return null + } +} + +export const easycryptHighlight = StreamLanguage.define(parser) diff --git a/doc/extensions/ecproofs/proofnav/esbuild.mjs b/doc/extensions/ecproofs/proofnav/esbuild.mjs new file mode 100644 index 000000000..61cbf24b4 --- /dev/null +++ b/doc/extensions/ecproofs/proofnav/esbuild.mjs @@ -0,0 +1,22 @@ +import esbuild from "esbuild"; + +const watch = process.argv.includes("--watch"); + +const ctx = await esbuild.context({ + entryPoints: ["index.ts"], + bundle: true, + format: "iife", + target: ["es2019"], + outfile: "dist/proofnav.bundle.js", + sourcemap: true, + minify: true +}); + +if (watch) { + await ctx.watch(); + console.log("proofnav: watching..."); +} else { + await ctx.rebuild(); + await ctx.dispose(); + console.log("proofnav: built"); +} diff --git a/doc/extensions/ecproofs/proofnav/index.ts b/doc/extensions/ecproofs/proofnav/index.ts new file mode 100644 index 000000000..414e0110a --- /dev/null +++ b/doc/extensions/ecproofs/proofnav/index.ts @@ -0,0 +1,46 @@ +import { createProofNavigator } from "./widget"; + +type ProofNavData = { + source: string; + sentenceEnds: number[]; + sentences: Array<{ goals?: string[]; message?: string | null }>; + initialSentence?: number; + title?: string; +}; + +function mountOne(mount: HTMLElement) { + const id = mount.id; + const dataEl = document.getElementById(id + "-data"); + if (!dataEl) return; + + let data: ProofNavData; + try { + data = JSON.parse(dataEl.textContent || "{}"); + } catch (e) { + mount.innerHTML = `
proofnav: invalid JSON
`; + return; + } + + const initialSentence = typeof data.initialSentence === "number" ? data.initialSentence : -1; + const title = typeof data.title === "string" ? data.title : undefined; + + createProofNavigator({ + parent: mount, + source: data.source, + sentenceEnds: data.sentenceEnds, + sentences: data.sentences, + initialSentence, + title, + }); +} + +function mountAll() { + const mounts = document.querySelectorAll(".proofnav-sphinx .proofnav-mount"); + mounts.forEach(mountOne); +} + +if (document.readyState === "loading") { + document.addEventListener("DOMContentLoaded", mountAll); +} else { + mountAll(); +} diff --git a/doc/extensions/ecproofs/proofnav/package-lock.json b/doc/extensions/ecproofs/proofnav/package-lock.json new file mode 100644 index 000000000..900f7747b --- /dev/null +++ b/doc/extensions/ecproofs/proofnav/package-lock.json @@ -0,0 +1,614 @@ +{ + "name": "proofnav", + "lockfileVersion": 3, + "requires": true, + "packages": { + "": { + "name": "proofnav", + "dependencies": { + "@codemirror/commands": "~6.10", + "@codemirror/language": "~6.12", + "@codemirror/state": "~6.5", + "@codemirror/view": "~6.39", + "@lezer/highlight": "~1.2" + }, + "devDependencies": { + "esbuild": "~0.27", + "typescript": "~5" + } + }, + "node_modules/@codemirror/commands": { + "version": "6.10.1", + "resolved": "https://registry.npmjs.org/@codemirror/commands/-/commands-6.10.1.tgz", + "integrity": "sha512-uWDWFypNdQmz2y1LaNJzK7fL7TYKLeUAU0npEC685OKTF3KcQ2Vu3klIM78D7I6wGhktme0lh3CuQLv0ZCrD9Q==", + "license": "MIT", + "dependencies": { + "@codemirror/language": "^6.0.0", + "@codemirror/state": "^6.4.0", + "@codemirror/view": "^6.27.0", + "@lezer/common": "^1.1.0" + } + }, + "node_modules/@codemirror/language": { + "version": "6.12.1", + "resolved": "https://registry.npmjs.org/@codemirror/language/-/language-6.12.1.tgz", + "integrity": "sha512-Fa6xkSiuGKc8XC8Cn96T+TQHYj4ZZ7RdFmXA3i9xe/3hLHfwPZdM+dqfX0Cp0zQklBKhVD8Yzc8LS45rkqcwpQ==", + "license": "MIT", + "dependencies": { + "@codemirror/state": "^6.0.0", + "@codemirror/view": "^6.23.0", + "@lezer/common": "^1.5.0", + "@lezer/highlight": "^1.0.0", + "@lezer/lr": "^1.0.0", + "style-mod": "^4.0.0" + } + }, + "node_modules/@codemirror/state": { + "version": "6.5.4", + "resolved": "https://registry.npmjs.org/@codemirror/state/-/state-6.5.4.tgz", + "integrity": "sha512-8y7xqG/hpB53l25CIoit9/ngxdfoG+fx+V3SHBrinnhOtLvKHRyAJJuHzkWrR4YXXLX8eXBsejgAAxHUOdW1yw==", + "license": "MIT", + "dependencies": { + "@marijn/find-cluster-break": "^1.0.0" + } + }, + "node_modules/@codemirror/view": { + "version": "6.39.11", + "resolved": "https://registry.npmjs.org/@codemirror/view/-/view-6.39.11.tgz", + "integrity": "sha512-bWdeR8gWM87l4DB/kYSF9A+dVackzDb/V56Tq7QVrQ7rn86W0rgZFtlL3g3pem6AeGcb9NQNoy3ao4WpW4h5tQ==", + "license": "MIT", + "dependencies": { + "@codemirror/state": "^6.5.0", + "crelt": "^1.0.6", + "style-mod": "^4.1.0", + "w3c-keyname": "^2.2.4" + } + }, + "node_modules/@esbuild/aix-ppc64": { + "version": "0.27.2", + "resolved": "https://registry.npmjs.org/@esbuild/aix-ppc64/-/aix-ppc64-0.27.2.tgz", + "integrity": "sha512-GZMB+a0mOMZs4MpDbj8RJp4cw+w1WV5NYD6xzgvzUJ5Ek2jerwfO2eADyI6ExDSUED+1X8aMbegahsJi+8mgpw==", + "cpu": [ + "ppc64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "aix" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/android-arm": { + "version": "0.27.2", + "resolved": "https://registry.npmjs.org/@esbuild/android-arm/-/android-arm-0.27.2.tgz", + "integrity": "sha512-DVNI8jlPa7Ujbr1yjU2PfUSRtAUZPG9I1RwW4F4xFB1Imiu2on0ADiI/c3td+KmDtVKNbi+nffGDQMfcIMkwIA==", + "cpu": [ + "arm" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "android" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/android-arm64": { + "version": "0.27.2", + "resolved": "https://registry.npmjs.org/@esbuild/android-arm64/-/android-arm64-0.27.2.tgz", + "integrity": "sha512-pvz8ZZ7ot/RBphf8fv60ljmaoydPU12VuXHImtAs0XhLLw+EXBi2BLe3OYSBslR4rryHvweW5gmkKFwTiFy6KA==", + "cpu": [ + "arm64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "android" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/android-x64": { + "version": "0.27.2", + "resolved": "https://registry.npmjs.org/@esbuild/android-x64/-/android-x64-0.27.2.tgz", + "integrity": "sha512-z8Ank4Byh4TJJOh4wpz8g2vDy75zFL0TlZlkUkEwYXuPSgX8yzep596n6mT7905kA9uHZsf/o2OJZubl2l3M7A==", + "cpu": [ + "x64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "android" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/darwin-arm64": { + "version": "0.27.2", + "resolved": "https://registry.npmjs.org/@esbuild/darwin-arm64/-/darwin-arm64-0.27.2.tgz", + "integrity": "sha512-davCD2Zc80nzDVRwXTcQP/28fiJbcOwvdolL0sOiOsbwBa72kegmVU0Wrh1MYrbuCL98Omp5dVhQFWRKR2ZAlg==", + "cpu": [ + "arm64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "darwin" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/darwin-x64": { + "version": "0.27.2", + "resolved": "https://registry.npmjs.org/@esbuild/darwin-x64/-/darwin-x64-0.27.2.tgz", + "integrity": "sha512-ZxtijOmlQCBWGwbVmwOF/UCzuGIbUkqB1faQRf5akQmxRJ1ujusWsb3CVfk/9iZKr2L5SMU5wPBi1UWbvL+VQA==", + "cpu": [ + "x64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "darwin" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/freebsd-arm64": { + "version": "0.27.2", + "resolved": "https://registry.npmjs.org/@esbuild/freebsd-arm64/-/freebsd-arm64-0.27.2.tgz", + "integrity": "sha512-lS/9CN+rgqQ9czogxlMcBMGd+l8Q3Nj1MFQwBZJyoEKI50XGxwuzznYdwcav6lpOGv5BqaZXqvBSiB/kJ5op+g==", + "cpu": [ + "arm64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "freebsd" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/freebsd-x64": { + "version": "0.27.2", + "resolved": "https://registry.npmjs.org/@esbuild/freebsd-x64/-/freebsd-x64-0.27.2.tgz", + "integrity": "sha512-tAfqtNYb4YgPnJlEFu4c212HYjQWSO/w/h/lQaBK7RbwGIkBOuNKQI9tqWzx7Wtp7bTPaGC6MJvWI608P3wXYA==", + "cpu": [ + "x64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "freebsd" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/linux-arm": { + "version": "0.27.2", + "resolved": "https://registry.npmjs.org/@esbuild/linux-arm/-/linux-arm-0.27.2.tgz", + "integrity": "sha512-vWfq4GaIMP9AIe4yj1ZUW18RDhx6EPQKjwe7n8BbIecFtCQG4CfHGaHuh7fdfq+y3LIA2vGS/o9ZBGVxIDi9hw==", + "cpu": [ + "arm" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "linux" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/linux-arm64": { + "version": "0.27.2", + "resolved": "https://registry.npmjs.org/@esbuild/linux-arm64/-/linux-arm64-0.27.2.tgz", + "integrity": "sha512-hYxN8pr66NsCCiRFkHUAsxylNOcAQaxSSkHMMjcpx0si13t1LHFphxJZUiGwojB1a/Hd5OiPIqDdXONia6bhTw==", + "cpu": [ + "arm64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "linux" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/linux-ia32": { + "version": "0.27.2", + "resolved": "https://registry.npmjs.org/@esbuild/linux-ia32/-/linux-ia32-0.27.2.tgz", + "integrity": "sha512-MJt5BRRSScPDwG2hLelYhAAKh9imjHK5+NE/tvnRLbIqUWa+0E9N4WNMjmp/kXXPHZGqPLxggwVhz7QP8CTR8w==", + "cpu": [ + "ia32" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "linux" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/linux-loong64": { + "version": "0.27.2", + "resolved": "https://registry.npmjs.org/@esbuild/linux-loong64/-/linux-loong64-0.27.2.tgz", + "integrity": "sha512-lugyF1atnAT463aO6KPshVCJK5NgRnU4yb3FUumyVz+cGvZbontBgzeGFO1nF+dPueHD367a2ZXe1NtUkAjOtg==", + "cpu": [ + "loong64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "linux" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/linux-mips64el": { + "version": "0.27.2", + "resolved": "https://registry.npmjs.org/@esbuild/linux-mips64el/-/linux-mips64el-0.27.2.tgz", + "integrity": "sha512-nlP2I6ArEBewvJ2gjrrkESEZkB5mIoaTswuqNFRv/WYd+ATtUpe9Y09RnJvgvdag7he0OWgEZWhviS1OTOKixw==", + "cpu": [ + "mips64el" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "linux" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/linux-ppc64": { + "version": "0.27.2", + "resolved": "https://registry.npmjs.org/@esbuild/linux-ppc64/-/linux-ppc64-0.27.2.tgz", + "integrity": "sha512-C92gnpey7tUQONqg1n6dKVbx3vphKtTHJaNG2Ok9lGwbZil6DrfyecMsp9CrmXGQJmZ7iiVXvvZH6Ml5hL6XdQ==", + "cpu": [ + "ppc64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "linux" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/linux-riscv64": { + "version": "0.27.2", + "resolved": "https://registry.npmjs.org/@esbuild/linux-riscv64/-/linux-riscv64-0.27.2.tgz", + "integrity": "sha512-B5BOmojNtUyN8AXlK0QJyvjEZkWwy/FKvakkTDCziX95AowLZKR6aCDhG7LeF7uMCXEJqwa8Bejz5LTPYm8AvA==", + "cpu": [ + "riscv64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "linux" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/linux-s390x": { + "version": "0.27.2", + "resolved": "https://registry.npmjs.org/@esbuild/linux-s390x/-/linux-s390x-0.27.2.tgz", + "integrity": "sha512-p4bm9+wsPwup5Z8f4EpfN63qNagQ47Ua2znaqGH6bqLlmJ4bx97Y9JdqxgGZ6Y8xVTixUnEkoKSHcpRlDnNr5w==", + "cpu": [ + "s390x" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "linux" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/linux-x64": { + "version": "0.27.2", + "resolved": "https://registry.npmjs.org/@esbuild/linux-x64/-/linux-x64-0.27.2.tgz", + "integrity": "sha512-uwp2Tip5aPmH+NRUwTcfLb+W32WXjpFejTIOWZFw/v7/KnpCDKG66u4DLcurQpiYTiYwQ9B7KOeMJvLCu/OvbA==", + "cpu": [ + "x64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "linux" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/netbsd-arm64": { + "version": "0.27.2", + "resolved": "https://registry.npmjs.org/@esbuild/netbsd-arm64/-/netbsd-arm64-0.27.2.tgz", + "integrity": "sha512-Kj6DiBlwXrPsCRDeRvGAUb/LNrBASrfqAIok+xB0LxK8CHqxZ037viF13ugfsIpePH93mX7xfJp97cyDuTZ3cw==", + "cpu": [ + "arm64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "netbsd" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/netbsd-x64": { + "version": "0.27.2", + "resolved": "https://registry.npmjs.org/@esbuild/netbsd-x64/-/netbsd-x64-0.27.2.tgz", + "integrity": "sha512-HwGDZ0VLVBY3Y+Nw0JexZy9o/nUAWq9MlV7cahpaXKW6TOzfVno3y3/M8Ga8u8Yr7GldLOov27xiCnqRZf0tCA==", + "cpu": [ + "x64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "netbsd" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/openbsd-arm64": { + "version": "0.27.2", + "resolved": "https://registry.npmjs.org/@esbuild/openbsd-arm64/-/openbsd-arm64-0.27.2.tgz", + "integrity": "sha512-DNIHH2BPQ5551A7oSHD0CKbwIA/Ox7+78/AWkbS5QoRzaqlev2uFayfSxq68EkonB+IKjiuxBFoV8ESJy8bOHA==", + "cpu": [ + "arm64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "openbsd" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/openbsd-x64": { + "version": "0.27.2", + "resolved": "https://registry.npmjs.org/@esbuild/openbsd-x64/-/openbsd-x64-0.27.2.tgz", + "integrity": "sha512-/it7w9Nb7+0KFIzjalNJVR5bOzA9Vay+yIPLVHfIQYG/j+j9VTH84aNB8ExGKPU4AzfaEvN9/V4HV+F+vo8OEg==", + "cpu": [ + "x64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "openbsd" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/openharmony-arm64": { + "version": "0.27.2", + "resolved": "https://registry.npmjs.org/@esbuild/openharmony-arm64/-/openharmony-arm64-0.27.2.tgz", + "integrity": "sha512-LRBbCmiU51IXfeXk59csuX/aSaToeG7w48nMwA6049Y4J4+VbWALAuXcs+qcD04rHDuSCSRKdmY63sruDS5qag==", + "cpu": [ + "arm64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "openharmony" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/sunos-x64": { + "version": "0.27.2", + "resolved": "https://registry.npmjs.org/@esbuild/sunos-x64/-/sunos-x64-0.27.2.tgz", + "integrity": "sha512-kMtx1yqJHTmqaqHPAzKCAkDaKsffmXkPHThSfRwZGyuqyIeBvf08KSsYXl+abf5HDAPMJIPnbBfXvP2ZC2TfHg==", + "cpu": [ + "x64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "sunos" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/win32-arm64": { + "version": "0.27.2", + "resolved": "https://registry.npmjs.org/@esbuild/win32-arm64/-/win32-arm64-0.27.2.tgz", + "integrity": "sha512-Yaf78O/B3Kkh+nKABUF++bvJv5Ijoy9AN1ww904rOXZFLWVc5OLOfL56W+C8F9xn5JQZa3UX6m+IktJnIb1Jjg==", + "cpu": [ + "arm64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "win32" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/win32-ia32": { + "version": "0.27.2", + "resolved": "https://registry.npmjs.org/@esbuild/win32-ia32/-/win32-ia32-0.27.2.tgz", + "integrity": "sha512-Iuws0kxo4yusk7sw70Xa2E2imZU5HoixzxfGCdxwBdhiDgt9vX9VUCBhqcwY7/uh//78A1hMkkROMJq9l27oLQ==", + "cpu": [ + "ia32" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "win32" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/win32-x64": { + "version": "0.27.2", + "resolved": "https://registry.npmjs.org/@esbuild/win32-x64/-/win32-x64-0.27.2.tgz", + "integrity": "sha512-sRdU18mcKf7F+YgheI/zGf5alZatMUTKj/jNS6l744f9u3WFu4v7twcUI9vu4mknF4Y9aDlblIie0IM+5xxaqQ==", + "cpu": [ + "x64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "win32" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@lezer/common": { + "version": "1.5.0", + "resolved": "https://registry.npmjs.org/@lezer/common/-/common-1.5.0.tgz", + "integrity": "sha512-PNGcolp9hr4PJdXR4ix7XtixDrClScvtSCYW3rQG106oVMOOI+jFb+0+J3mbeL/53g1Zd6s0kJzaw6Ri68GmAA==", + "license": "MIT" + }, + "node_modules/@lezer/highlight": { + "version": "1.2.3", + "resolved": "https://registry.npmjs.org/@lezer/highlight/-/highlight-1.2.3.tgz", + "integrity": "sha512-qXdH7UqTvGfdVBINrgKhDsVTJTxactNNxLk7+UMwZhU13lMHaOBlJe9Vqp907ya56Y3+ed2tlqzys7jDkTmW0g==", + "license": "MIT", + "dependencies": { + "@lezer/common": "^1.3.0" + } + }, + "node_modules/@lezer/lr": { + "version": "1.4.7", + "resolved": "https://registry.npmjs.org/@lezer/lr/-/lr-1.4.7.tgz", + "integrity": "sha512-wNIFWdSUfX9Jc6ePMzxSPVgTVB4EOfDIwLQLWASyiUdHKaMsiilj9bYiGkGQCKVodd0x6bgQCV207PILGFCF9Q==", + "license": "MIT", + "dependencies": { + "@lezer/common": "^1.0.0" + } + }, + "node_modules/@marijn/find-cluster-break": { + "version": "1.0.2", + "resolved": "https://registry.npmjs.org/@marijn/find-cluster-break/-/find-cluster-break-1.0.2.tgz", + "integrity": "sha512-l0h88YhZFyKdXIFNfSWpyjStDjGHwZ/U7iobcK1cQQD8sejsONdQtTVU+1wVN1PBw40PiiHB1vA5S7VTfQiP9g==", + "license": "MIT" + }, + "node_modules/crelt": { + "version": "1.0.6", + "resolved": "https://registry.npmjs.org/crelt/-/crelt-1.0.6.tgz", + "integrity": "sha512-VQ2MBenTq1fWZUH9DJNGti7kKv6EeAuYr3cLwxUWhIu1baTaXh4Ib5W2CqHVqib4/MqbYGJqiL3Zb8GJZr3l4g==", + "license": "MIT" + }, + "node_modules/esbuild": { + "version": "0.27.2", + "resolved": "https://registry.npmjs.org/esbuild/-/esbuild-0.27.2.tgz", + "integrity": "sha512-HyNQImnsOC7X9PMNaCIeAm4ISCQXs5a5YasTXVliKv4uuBo1dKrG0A+uQS8M5eXjVMnLg3WgXaKvprHlFJQffw==", + "dev": true, + "hasInstallScript": true, + "license": "MIT", + "bin": { + "esbuild": "bin/esbuild" + }, + "engines": { + "node": ">=18" + }, + "optionalDependencies": { + "@esbuild/aix-ppc64": "0.27.2", + "@esbuild/android-arm": "0.27.2", + "@esbuild/android-arm64": "0.27.2", + "@esbuild/android-x64": "0.27.2", + "@esbuild/darwin-arm64": "0.27.2", + "@esbuild/darwin-x64": "0.27.2", + "@esbuild/freebsd-arm64": "0.27.2", + "@esbuild/freebsd-x64": "0.27.2", + "@esbuild/linux-arm": "0.27.2", + "@esbuild/linux-arm64": "0.27.2", + "@esbuild/linux-ia32": "0.27.2", + "@esbuild/linux-loong64": "0.27.2", + "@esbuild/linux-mips64el": "0.27.2", + "@esbuild/linux-ppc64": "0.27.2", + "@esbuild/linux-riscv64": "0.27.2", + "@esbuild/linux-s390x": "0.27.2", + "@esbuild/linux-x64": "0.27.2", + "@esbuild/netbsd-arm64": "0.27.2", + "@esbuild/netbsd-x64": "0.27.2", + "@esbuild/openbsd-arm64": "0.27.2", + "@esbuild/openbsd-x64": "0.27.2", + "@esbuild/openharmony-arm64": "0.27.2", + "@esbuild/sunos-x64": "0.27.2", + "@esbuild/win32-arm64": "0.27.2", + "@esbuild/win32-ia32": "0.27.2", + "@esbuild/win32-x64": "0.27.2" + } + }, + "node_modules/style-mod": { + "version": "4.1.3", + "resolved": "https://registry.npmjs.org/style-mod/-/style-mod-4.1.3.tgz", + "integrity": "sha512-i/n8VsZydrugj3Iuzll8+x/00GH2vnYsk1eomD8QiRrSAeW6ItbCQDtfXCeJHd0iwiNagqjQkvpvREEPtW3IoQ==", + "license": "MIT" + }, + "node_modules/typescript": { + "version": "5.9.3", + "resolved": "https://registry.npmjs.org/typescript/-/typescript-5.9.3.tgz", + "integrity": "sha512-jl1vZzPDinLr9eUt3J/t7V6FgNEw9QjvBPdysz9KfQDD41fQrC2Y4vKQdiaUpFT4bXlb1RHhLpp8wtm6M5TgSw==", + "dev": true, + "license": "Apache-2.0", + "bin": { + "tsc": "bin/tsc", + "tsserver": "bin/tsserver" + }, + "engines": { + "node": ">=14.17" + } + }, + "node_modules/w3c-keyname": { + "version": "2.2.8", + "resolved": "https://registry.npmjs.org/w3c-keyname/-/w3c-keyname-2.2.8.tgz", + "integrity": "sha512-dpojBhNsCNN7T82Tm7k26A6G9ML3NkhDsnw9n/eoxSRlVBB4CEtIQ/KTCLI2Fwf3ataSXRhYFkQi3SlnFwPvPQ==", + "license": "MIT" + } + } +} diff --git a/doc/extensions/ecproofs/proofnav/package.json b/doc/extensions/ecproofs/proofnav/package.json new file mode 100644 index 000000000..421434db0 --- /dev/null +++ b/doc/extensions/ecproofs/proofnav/package.json @@ -0,0 +1,20 @@ +{ + "name": "proofnav", + "private": true, + "type": "module", + "scripts": { + "build": "node esbuild.mjs", + "watch": "node esbuild.mjs --watch" + }, + "dependencies": { + "@codemirror/commands": "~6.10", + "@codemirror/state": "~6.5", + "@codemirror/view": "~6.39", + "@codemirror/language": "~6.12", + "@lezer/highlight": "~1.2" + }, + "devDependencies": { + "esbuild": "~0.27", + "typescript": "~5" + } +} diff --git a/doc/extensions/ecproofs/proofnav/proofnav.css b/doc/extensions/ecproofs/proofnav/proofnav.css new file mode 100644 index 000000000..cea082ad0 --- /dev/null +++ b/doc/extensions/ecproofs/proofnav/proofnav.css @@ -0,0 +1,233 @@ +/* Scope everything under the directive wrapper to avoid theme conflicts */ +.proofnav-sphinx .proofnav-rtd{ + --pn-panel: #fcfcfc; + --pn-border: #e1e4e5; + --pn-text: #404040; + --pn-muted: #6a6a6a; + + /* more visible highlights */ + --pn-doneBg: #e6edf3; + --pn-curBg: #cfe3ff; + --pn-hoverBg:#e8f2ff; + + --pn-radius: 4px; + --pn-mono: ui-monospace, SFMono-Regular, Menlo, Monaco, Consolas, + "Liberation Mono", "Courier New", monospace; + + font: inherit; + color: var(--pn-text); +} + +.proofnav-sphinx .proofnav-rtd.proofnav { + display: grid; + grid-template-rows: auto auto; + gap: 12px; + box-sizing: border-box; + min-width: 0; +} + +.proofnav-sphinx .proofnav-rtd .panel{ + border: 1px solid var(--pn-border); + border-radius: var(--pn-radius); + overflow: hidden; + background: var(--pn-panel); + min-width: 0; +} + +.proofnav-sphinx .proofnav-rtd .proofnav__body{ + display: grid; + grid-template-rows: auto auto; + gap: 12px; +} + +.proofnav-sphinx .proofnav-rtd.pn-collapsed .proofnav__body{ + display: none; +} + +.proofnav-sphinx .proofnav-rtd .proofnav__btnToggle{ + display: inline-flex; + align-items: center; + gap: 6px; +} + +.proofnav-sphinx .proofnav-rtd .proofnav__btnToggle{ + padding: 4px 6px; + border-radius: 3px; + line-height: 1; +} + +.proofnav-sphinx .proofnav-rtd .proofnav__sr{ + position: absolute; + width: 1px; + height: 1px; + padding: 0; + margin: -1px; + overflow: hidden; + clip: rect(0,0,0,0); + white-space: nowrap; + border: 0; +} + +.proofnav-sphinx .proofnav-rtd .proofnav__chev{ + transition: transform 120ms ease; +} + +.proofnav-sphinx .proofnav-rtd.pn-collapsed .proofnav__chev{ + transform: rotate(-90deg); +} + +.proofnav-sphinx .proofnav-rtd .proofnav__sentencebar{ + display: flex; + align-items: center; + justify-content: space-between; + gap: 10px; + padding: 8px 10px; + border-bottom: 1px solid var(--pn-border); + background: #fff; +} + +.proofnav-sphinx .proofnav-rtd .proofnav__header{ + display:flex; + align-items:center; + justify-content: space-between; + padding: 8px 10px; + border-bottom: 1px solid var(--pn-border); + background: #fff; +} + +.proofnav-sphinx .proofnav-rtd .proofnav__title{ + font-weight: 600; + font-size: 14px; + color: #2d2d2d; + white-space: nowrap; + overflow: hidden; + text-overflow: ellipsis; +} + +.proofnav-sphinx .proofnav-rtd .proofnav__title{ + display: flex; + align-items: center; + gap: 8px; +} + +.proofnav-sphinx .proofnav-rtd .proofnav__subtitle{ + font-size: 12px; + color: var(--pn-muted); + margin-left: 10px; + font-weight: 500; +} + +.proofnav-sphinx .proofnav-rtd .proofnav__controls{ + display:flex; + gap: 8px; + flex-shrink: 0; +} + +.proofnav-sphinx .proofnav-rtd .proofnav__btn{ + appearance: none; + border: 1px solid var(--pn-border); + background: #fff; + color: var(--pn-text); + padding: 6px 9px; + border-radius: 3px; + cursor: pointer; + font-weight: 600; + font-size: 12px; +} +.proofnav-sphinx .proofnav-rtd .proofnav__btn:hover{ background: #f7f7f7; } + +.proofnav-sphinx .proofnav-rtd .proofnav__editor{ + height: auto; + background: #fff; + overflow: hidden; +} + +.proofnav-sphinx .proofnav-rtd .infoBody{ + padding: 10px; + display: grid; + grid-template-rows: auto auto; + gap: 10px; + box-sizing: border-box; +} + +.proofnav-sphinx .proofnav-rtd .box{ + border: 1px solid var(--pn-border); + border-radius: var(--pn-radius); + padding: 8px 10px; + background: #fff; + min-width: 0; +} + +.proofnav-sphinx .proofnav-rtd .tabs{ + display:flex; + gap: 6px; + flex-wrap: wrap; + margin-bottom: 6px; +} + +.proofnav-sphinx .proofnav-rtd .tab{ + border: 1px solid var(--pn-border); + background: #fff; + color: var(--pn-text); + padding: 4px 8px; + border-radius: 999px; + cursor: pointer; + font-weight: 600; + font-size: 12px; +} + +.proofnav-sphinx .proofnav-rtd .tab[aria-selected="true"]{ + background: #e8f0ff; + border-color: #c9d7ff; +} + +.proofnav-sphinx .proofnav-rtd .goal-sep{ + border-top: 1px solid var(--pn-border); + margin: 6px 0 8px 0; +} + +.proofnav-sphinx .proofnav-rtd pre{ + margin: 0; + white-space: pre-wrap; + word-break: break-word; + font-family: var(--pn-mono); + font-size: 11.5px; + color: var(--pn-text); +} + +.proofnav-sphinx .proofnav-rtd .empty{ + color: var(--pn-muted); + font-size: 13px; + font-weight: 600; +} + +/* sentence highlights */ +.proofnav-sphinx .proofnav-rtd .cm-sentenceDone{ background: var(--pn-doneBg); } +.proofnav-sphinx .proofnav-rtd .cm-sentenceHover{ background: var(--pn-hoverBg); } +.proofnav-sphinx .proofnav-rtd .cm-sentenceCurrent{ + background: var(--pn-curBg) !important; + box-shadow: inset 3px 0 0 rgba(32,94,255,.35); +} + +/* active sentence gutter */ +.proofnav-sphinx .proofnav-rtd .cm-activeSentenceGutter{ + background: #fbfbfb; + border-right: 1px solid var(--pn-border); + color: #2d2d2d; +} + +.proofnav-sphinx .proofnav-rtd .cm-activeSentenceMarker{ + width: 10px; + display: inline-flex; + align-items: center; + justify-content: center; + font-size: 12px; + user-select: none; +} + +/* pointer cursor only when hovering a sentence */ +.proofnav-sphinx .proofnav-rtd.pn-hovering .cm-content, +.proofnav-sphinx .proofnav-rtd.pn-hovering .cm-line, +.proofnav-sphinx .proofnav-rtd.pn-hovering .cm-gutters{ + cursor: pointer; +} diff --git a/doc/extensions/ecproofs/proofnav/widget.ts b/doc/extensions/ecproofs/proofnav/widget.ts new file mode 100644 index 000000000..3f7675b44 --- /dev/null +++ b/doc/extensions/ecproofs/proofnav/widget.ts @@ -0,0 +1,452 @@ +import { + EditorState, + StateEffect, + StateField, + Range, + RangeSet, +} from "@codemirror/state"; + +import { + EditorView, + Decoration, + keymap, + gutter, + GutterMarker, + lineNumbers, +} from "@codemirror/view"; + +import { defaultKeymap } from "@codemirror/commands"; +import { syntaxHighlighting, HighlightStyle } from "@codemirror/language"; +import { tags as t } from "@lezer/highlight" + +import { easycryptHighlight } from "./easycrypt"; + +export type ProofSentence = { + goals?: string[]; + message?: string | null; +}; + +export type CreateProofNavigatorOptions = { + parent: HTMLElement; + source: string; + sentenceEnds: number[]; + sentences: ProofSentence[]; + initialSentence?: number; // allow -1 (before first) + collapsible?: boolean; // default true + initialCollapsed?: boolean; // default true + title?: string; // default "Proof Navigator" +}; + +export type ProofNavigatorHandle = { + view: EditorView; + setSentence: (idx: number, opts?: { scroll?: boolean }) => void; + getSentence: () => number; + collapse: () => void; + expand: () => void; + toggleCollapsed: () => void; + isCollapsed: () => boolean; +}; + +const rtdHighlight: HighlightStyle = HighlightStyle.define([ + { tag: t.keyword, color: "#005a9c", fontWeight: "600" }, + { tag: t.annotation, color: "#a10d2b", fontWeight: "600" }, + { tag: t.invalid, color: "#ff0000", fontWeight: "600" }, + { tag: t.namespace, color: "#b61295", fontWeight: "600" }, + { tag: t.keyword, color: "#005a9c", fontWeight: "600" }, + { tag: t.controlKeyword, color: "#005a9c", fontWeight: "600" }, + { tag: t.controlOperator, color: "#108401", fontWeight: "600" }, + { tag: [t.string, t.special(t.string)], color: "#1a7f37" }, + { tag: t.comment, color: "#6a737d", fontStyle: "italic" }, + { tag: t.number, color: "#b31d28" }, + { tag: t.variableName, color: "#24292f" }, + { tag: [t.operator, t.punctuation], color: "#57606a" }, +]); + +export function createProofNavigator(opts: CreateProofNavigatorOptions): ProofNavigatorHandle { + const { + parent, + source, + sentenceEnds, + sentences, + initialSentence = -1, + collapsible = true, + initialCollapsed = true, + title = "Proof Navigator", + } = opts; + + if (!parent) throw new Error("parent is required"); + if (!Array.isArray(sentenceEnds) || sentenceEnds.length === 0) { + throw new Error("sentenceEnds must be non-empty"); + } + if (!Array.isArray(sentences) || sentences.length !== sentenceEnds.length) { + throw new Error("sentences length mismatch"); + } + + const sentenceStarts = sentenceEnds.map((_, i) => (i === 0 ? 0 : sentenceEnds[i - 1])); + + const clamp = (x: number, lo: number, hi: number) => Math.max(lo, Math.min(hi, x)); + + function sentenceIndexAtPos(pos: number): number { + let lo = 0; + let hi = sentenceEnds.length - 1; + while (lo < hi) { + const mid = (lo + hi) >> 1; + if (sentenceEnds[mid] >= pos) hi = mid; + else lo = mid + 1; + } + return lo; + } + + const root = document.createElement("div"); + root.className = "proofnav proofnav-rtd"; + root.innerHTML = ` +
+
+
+ ${collapsible ? ` + + ` : ""} + +
+
+ +
+
+
+
+ + +
+
+ +
+ +
+
+
+
+
+
+
+
+
+
+
+
+
+
+ `; + parent.appendChild(root); + + const elTitle = root.querySelector("[data-title]") as HTMLElement; + elTitle.textContent = title; + + const elEditor = root.querySelector("[data-editor]") as HTMLElement; + const elTabs = root.querySelector("[data-tabs]") as HTMLElement; + const elGoalContent = root.querySelector("[data-goalcontent]") as HTMLElement; + const elMessage = root.querySelector("[data-message]") as HTMLElement; + const elSentInfo = root.querySelector("[data-sentinfo]") as HTMLElement; + const elGoalSep = root.querySelector(".goal-sep") as HTMLElement; + const btnPrev = root.querySelector("[data-prev]") as HTMLButtonElement; + const btnNext = root.querySelector("[data-next]") as HTMLButtonElement; + + const btnToggle = root.querySelector("[data-toggle]") as HTMLButtonElement | null; + const elToggleLabel = root.querySelector("[data-toggle-label]") as HTMLElement | null; + + const setSentenceEffect = StateEffect.define(); + const setHoverEffect = StateEffect.define(); // number | null + + const sentenceField = StateField.define({ + create() { + return clamp(initialSentence, -1, sentenceEnds.length - 1); + }, + update(v, tr) { + for (const e of tr.effects) { + if (e.is(setSentenceEffect)) return e.value; + } + return v; + }, + }); + + const hoverField = StateField.define({ + create() { + return null; + }, + update(v, tr) { + for (const e of tr.effects) { + if (e.is(setHoverEffect)) return e.value; + } + return v; + }, + }); + + const sentenceHighlightField = StateField.define>({ + create(state) { + return buildDecorations(state.field(sentenceField), state.field(hoverField)); + }, + update(deco, tr) { + const changed = + tr.docChanged || + tr.effects.some((e) => e.is(setSentenceEffect) || e.is(setHoverEffect)); + if (changed) { + return buildDecorations(tr.state.field(sentenceField), tr.state.field(hoverField)); + } + return deco.map(tr.changes); + }, + provide: (f) => EditorView.decorations.from(f), + }); + + function buildDecorations(activeIdx: number, hoverIdx: number | null) { + const d: Range[] = []; + + if (hoverIdx != null && hoverIdx >= 0 && hoverIdx < sentenceEnds.length) { + const hs = sentenceStarts[hoverIdx]; + const he = sentenceEnds[hoverIdx]; + if (he > hs) d.push(Decoration.mark({ class: "cm-sentenceHover" }).range(hs, he)); + } + + if (activeIdx >= 0) { + const start = sentenceStarts[activeIdx]; + const end = sentenceEnds[activeIdx]; + + if (start > 0) d.push(Decoration.mark({ class: "cm-sentenceDone" }).range(0, start)); + if (end > start) d.push(Decoration.mark({ class: "cm-sentenceCurrent" }).range(start, end)); + } + + return Decoration.set(d, true); + } + + const hoverAndClick = EditorView.domEventHandlers({ + mousemove(e, view) { + const pos = view.posAtCoords({ x: e.clientX, y: e.clientY }); + if (pos == null) { + root.classList.remove("pn-hovering"); + if (view.state.field(hoverField) != null) { + view.dispatch({ effects: setHoverEffect.of(null) }); + } + return false; + } + + const idx = sentenceIndexAtPos(pos); + root.classList.add("pn-hovering"); + if (view.state.field(hoverField) !== idx) { + view.dispatch({ effects: setHoverEffect.of(idx) }); + } + return false; + }, + + mouseleave(_e, view) { + root.classList.remove("pn-hovering"); + if (view.state.field(hoverField) != null) { + view.dispatch({ effects: setHoverEffect.of(null) }); + } + return false; + }, + + mousedown(e, view) { + if (e.button !== 0) return false; + const pos = view.posAtCoords({ x: e.clientX, y: e.clientY }); + if (pos == null) return false; + setSentence(sentenceIndexAtPos(pos), { scroll: false }); + return true; + }, + }); + + class ActiveSentenceMarker extends GutterMarker { + toDOM() { + const span = document.createElement("span"); + span.className = "cm-activeSentenceMarker"; + span.textContent = "▶"; + return span; + } + } + const activeMarker = new ActiveSentenceMarker(); + + const activeSentenceGutter = gutter({ + class: "cm-activeSentenceGutter", + markers: (view) => { + const idx = view.state.field(sentenceField); + if (idx < 0) return RangeSet.empty; + const line = view.state.doc.lineAt(sentenceStarts[idx]).from; + return RangeSet.of([activeMarker.range(line)]); + }, + initialSpacer: () => activeMarker, + }); + + const rtdTheme = EditorView.theme({ + "&": { + backgroundColor: "#fff", + color: "#404040", + fontSize: "11px", + }, + ".cm-content": { + fontFamily: "var(--pn-mono)", + fontSize: "11px", + }, + ".cm-gutters": { + backgroundColor: "#fbfbfb", + borderRight: "1px solid #e1e4e5", + fontSize: "11px", + }, + ".cm-lineNumbers .cm-gutterElement": { + padding: "0 8px 0 10px", + fontSize: "11px", + } + }); + + const view = new EditorView({ + parent: elEditor, + state: EditorState.create({ + doc: source, + extensions: [ + easycryptHighlight, + syntaxHighlighting(rtdHighlight), + activeSentenceGutter, + lineNumbers(), + keymap.of(defaultKeymap), + EditorView.editable.of(false), + EditorState.readOnly.of(true), + sentenceField, + hoverField, + sentenceHighlightField, + hoverAndClick, + rtdTheme, + ], + }), + }); + + // autosize editor to content + function autosizeEditor() { + view.requestMeasure({ + read() { + return view.contentDOM.scrollHeight; + }, + write(height) { + // Small padding to avoid clipping descenders + elEditor.style.height = `${height + 6}px`; + } + }); + } + + requestAnimationFrame(() => requestAnimationFrame(autosizeEditor)); + + let activeGoalTab = 0; + + function render(idx: number) { + if (idx < 0) { + elSentInfo.textContent = "Before first sentence"; + elTabs.innerHTML = ""; + elGoalContent.innerHTML = `
No goals.
`; + elMessage.innerHTML = `
No message.
`; + elGoalSep.style.display = "none"; + return; + } + + elSentInfo.textContent = `Sentence ${idx + 1} / ${sentenceEnds.length}`; + const info = sentences[idx] || {}; + const goals = Array.isArray(info.goals) ? info.goals : []; + const msg = String(info.message ?? ""); + + elTabs.innerHTML = ""; + elGoalContent.innerHTML = ""; + elGoalSep.style.display = goals.length ? "block" : "none"; + + if (goals.length === 0) { + elGoalContent.innerHTML = `
No goals.
`; + activeGoalTab = 0; + } else { + activeGoalTab = clamp(activeGoalTab, 0, goals.length - 1); + goals.forEach((_, i) => { + const b = document.createElement("button"); + b.className = "tab"; + b.textContent = `Goal ${i + 1}`; + b.setAttribute("aria-selected", i === activeGoalTab ? "true" : "false"); + b.onclick = () => { + activeGoalTab = i; + render(getSentence()); + }; + elTabs.appendChild(b); + }); + const pre = document.createElement("pre"); + pre.textContent = goals[activeGoalTab] ?? ""; + elGoalContent.appendChild(pre); + } + + if (msg.trim()) { + const pre = document.createElement("pre"); + pre.textContent = msg; + elMessage.innerHTML = ""; + elMessage.appendChild(pre); + } else { + elMessage.innerHTML = `
No message.
`; + } + } + + function scrollTo(idx: number) { + if (idx < 0) return; + view.dispatch({ selection: { anchor: sentenceStarts[idx] }, scrollIntoView: true }); + } + + function setSentence(idx: number, { scroll = true }: { scroll?: boolean } = {}) { + const i = clamp(idx, -1, sentenceEnds.length - 1); + + const effects: StateEffect[] = [setSentenceEffect.of(i)]; + + if (i < 0) { + effects.push(setHoverEffect.of(null)); + root.classList.remove("pn-hovering"); + } + + view.dispatch({ effects }); + render(i); + if (scroll) scrollTo(i); + } + + function getSentence(): number { + return view.state.field(sentenceField); + } + + btnPrev.onclick = () => setSentence(getSentence() - 1); + btnNext.onclick = () => setSentence(getSentence() + 1); + + function isCollapsed(): boolean { + return root.classList.contains("pn-collapsed"); + } + + function setCollapsed(collapsed: boolean) { + if (!collapsible) return; + if (collapsed) root.classList.add("pn-collapsed"); + else root.classList.remove("pn-collapsed"); + + if (btnToggle) btnToggle.setAttribute("aria-expanded", collapsed ? "false" : "true"); + if (elToggleLabel) elToggleLabel.textContent = collapsed ? "Expand" : "Collapse"; + if (btnToggle) btnToggle.title = collapsed ? "Expand" : "Collapse"; + + // When expanding, CodeMirror may need a layout refresh + correct height. + if (!collapsed) { + requestAnimationFrame(() => { + autosizeEditor(); + view.requestMeasure(); + }); + } + } + + function collapse() { setCollapsed(true); } + function expand() { setCollapsed(false); } + function toggleCollapsed() { setCollapsed(!isCollapsed()); } + + if (btnToggle) { + btnToggle.onclick = () => toggleCollapsed(); + } + + setSentence(initialSentence); + + if (collapsible && initialCollapsed) { + setCollapsed(true); + } + + return { view, setSentence, getSentence, collapse, expand, toggleCollapsed, isCollapsed }; +} diff --git a/doc/extensions/ecpygment/ecpygment.py b/doc/extensions/ecpygment/ecpygment.py new file mode 100644 index 000000000..7fb05381b --- /dev/null +++ b/doc/extensions/ecpygment/ecpygment.py @@ -0,0 +1,15 @@ +# -------------------------------------------------------------- +import sphinx.application as sa +import sphinx.util as su + +from lexers.easycrypt import EasyCryptLexer + +# -------------------------------------------------------------- +def setup(app: sa.Sphinx) -> su.typing.ExtensionMetadata: + app.add_lexer("easycrypt", EasyCryptLexer) + + return { + 'version': '0.1', + 'parallel_read_safe': True, + 'parallel_write_safe': True, + } diff --git a/doc/extensions/ecpygment/lexers/easycrypt.py b/doc/extensions/ecpygment/lexers/easycrypt.py new file mode 100644 index 000000000..732013b9b --- /dev/null +++ b/doc/extensions/ecpygment/lexers/easycrypt.py @@ -0,0 +1,78 @@ +# ------------------------------------------------------------------------ +import pygments.lexer as pylex +import pygments.token as pytok + +import itertools as it + +# ------------------------------------------------------------------------ +# Generated by `scripts/srctx/keywords -m python < src/ecLexer.mll` +keywords = dict( + bytac = ['exact', 'assumption', 'smt', 'coq', 'check', 'edit', 'fix', 'by', 'reflexivity', 'done', 'solve'], + dangerous = ['admit', 'admitted'], + global_ = ['axiom', 'axiomatized', 'lemma', 'realize', 'proof', 'qed', 'abort', 'goal', 'end', 'from', 'import', 'export', 'include', 'local', 'global', 'declare', 'hint', 'module', 'of', 'const', 'op', 'pred', 'inductive', 'notation', 'abbrev', 'require', 'theory', 'abstract', 'section', 'subtype', 'type', 'class', 'instance', 'print', 'search', 'locate', 'as', 'Pr', 'clone', 'with', 'rename', 'prover', 'timeout', 'why3', 'dump', 'remove', 'exit', 'Top', 'Self'], + internal = ['fail', 'time', 'undo', 'debug', 'pragma'], + prog = ['forall', 'exists', 'fun', 'glob', 'let', 'in', 'for', 'var', 'proc', 'if', 'is', 'match', 'then', 'else', 'elif', 'match', 'for', 'while', 'assert', 'return', 'res', 'equiv', 'hoare', 'ehoare', 'phoare', 'islossless', 'async'], + tactic = ['beta', 'iota', 'zeta', 'eta', 'logic', 'delta', 'simplify', 'cbv', 'congr', 'change', 'split', 'left', 'right', 'case', 'pose', 'gen', 'have', 'suff', 'elim', 'exlim', 'ecall', 'clear', 'wlog', 'idassign', 'apply', 'rewrite', 'rwnormal', 'subst', 'progress', 'trivial', 'auto', 'idtac', 'move', 'modpath', 'field', 'fieldeq', 'ring', 'ringeq', 'algebra', 'replace', 'transitivity', 'symmetry', 'seq', 'wp', 'sp', 'sim', 'skip', 'call', 'rcondt', 'rcondf', 'swap', 'cfold', 'rnd', 'rndsem', 'pr_bounded', 'bypr', 'byphoare', 'byehoare', 'byequiv', 'byupto', 'fel', 'conseq', 'exfalso', 'inline', 'outline', 'interleave', 'alias', 'weakmem', 'fission', 'fusion', 'unroll', 'splitwhile', 'kill', 'eager'], + tactical = ['try', 'first', 'last', 'do', 'expect'], +) + +# ------------------------------------------------------------------------ +kwclasses = dict( + bytac = pytok.Name.Exception, + dangerous = pytok.Name.Exception, + global_ = pytok.Keyword.Declaration, + internal = pytok.Keyword.Declaration, + prog = pytok.Keyword.Reserved, + tactic = pytok.Keyword.Reserved, + tactical = pytok.Keyword.Pseudo, +) + +# ------------------------------------------------------------------------ +class EasyCryptLexer(pylex.RegexLexer): + name = "EasyCrypt" + filenames = ["*.ec", "*.eca"] + mimetypes = ["text/x-easycrypt"] + + tokens = { + "root": [ + # Whitespace + (r"[ \t]+", pytok.Whitespace), + (r"\n+", pytok.Whitespace), + + # Comments + (r"\(\*", pytok.Comment.Multiline, "comment"), + ] + [ + # Keywords + (pylex.words(keywords[ids], suffix=r"\b"), cls) + for ids, cls in kwclasses.items() + ] + [ + # Strings (simple single/double quoted) + (r'"([^"\\]|\\.)*"', pytok.String.Double), + + # Numbers + (r"\b\d+\b", pytok.Number.Integer), + + # Identifiers + (r"[A-Za-z_]\w*", pytok.Name), + + # Operators + (r"[+\-*/%=<>&|!]+", pytok.Operator), + + # Punctuation + (r"[()\[\]{},.;:]", pytok.Punctuation), + + # Anything else + (r".", pytok.Text), + ], + + "comment": [ + (r"\(\*", pytok.Comment.Multiline, "#push"), + + # If we see a closer, pop one nesting level + (r"\*\)", pytok.Comment.Multiline, "#pop"), + + # Otherwise consume content (keep it as Comment) + (r"[^()*]+", pytok.Comment.Multiline), + (r"[()*]", pytok.Comment.Multiline), + ], + } diff --git a/doc/index.rst b/doc/index.rst new file mode 100644 index 000000000..8b6c7d9b2 --- /dev/null +++ b/doc/index.rst @@ -0,0 +1,7 @@ +EasyCrypt reference manual +======================================================================== + +.. toctree:: + :maxdepth: 2 + + tactics diff --git a/doc/package-lock.json b/doc/package-lock.json new file mode 100644 index 000000000..012938edf --- /dev/null +++ b/doc/package-lock.json @@ -0,0 +1,6 @@ +{ + "name": "doc", + "lockfileVersion": 3, + "requires": true, + "packages": {} +} diff --git a/doc/requirements.txt b/doc/requirements.txt new file mode 100644 index 000000000..a496b96f3 --- /dev/null +++ b/doc/requirements.txt @@ -0,0 +1,3 @@ +Sphinx==8.2.* +sphinx_rtd_theme==3.1.* +sphinx_design==0.6.* diff --git a/doc/tactics.rst b/doc/tactics.rst new file mode 100644 index 000000000..5b954bbad --- /dev/null +++ b/doc/tactics.rst @@ -0,0 +1,8 @@ +Proof tactics reference +======================================================================== + +.. toctree:: + :maxdepth: 1 + :glob: + + tactics/* diff --git a/doc/tactics/skip.rst b/doc/tactics/skip.rst new file mode 100644 index 000000000..257de4e7a --- /dev/null +++ b/doc/tactics/skip.rst @@ -0,0 +1,95 @@ +======================================================================== +Tactic: `skip` +======================================================================== + +The `skip` tactic applies to program-logic goals where the program(s) under +consideration are empty. In this situation, program execution performs +no computation and produces no state changes. + +Applying `skip` eliminates the program component of the goal and reduces +the proof obligation to a pure logical goal. Concretely, the remaining +task is to prove that the precondition implies the postcondition. + +The `skip` tactic does not attempt to solve this logical obligation itself. + +.. contents:: + :local: + +------------------------------------------------------------------------ +In Hoare logic +------------------------------------------------------------------------ + +.. ecproof:: + :title: Hoare logic example + + require import AllCore. + + module M = { + proc f(x : int) = { + return x; + } + }. + + pred p : int. + pred q : int. + + lemma L : hoare[M.f : p x ==> q res]. + proof. + proc. (*$*) skip. + abort. + +------------------------------------------------------------------------ +In Relational Hoare logic +------------------------------------------------------------------------ + +In the relational Hoare logic setting, the `skip`` tactic applies only +when both programs are empty, in which case it reduces the relational +judgment to obligations on the preconditions and postconditions alone. + +.. ecproof:: + :title: Relational Hoare logic example + + require import AllCore. + + module M = { + proc f(x : int) = { + return x; + } + }. + + pred p : int & int. + pred q : int & int. + + lemma L : equiv[M.f ~ M.f : p x{1} x{2} ==> q res{1} res{2}]. + proof. + proc. (*$*) skip. + abort. + +------------------------------------------------------------------------ +In Probabilistic Hoare logic +------------------------------------------------------------------------ + +In the probabilistic Hoare logic setting, applying `skip` generates an +additional proof obligation compared to the pure Hoare case. Besides the +logical implication between the precondition and the postcondition, one +must also prove that the probability weight of the empty program, namely +`1%r`, satisfies the bound specified in the judgment. + +.. ecproof:: + :title: Probabilistic Hoare logic example + + require import AllCore. + + module M = { + proc f(x : int) = { + return x; + } + }. + + pred p : int. + pred q : int. + + lemma L : phoare[M.f : p x ==> q res] >= (1%r / 2%r). + proof. + proc. (*$*) skip. + abort. diff --git a/src/ec.ml b/src/ec.ml index 48da43b80..8c29fdd98 100644 --- a/src/ec.ml +++ b/src/ec.ml @@ -407,15 +407,36 @@ let main () = (* Initialize I/O + interaction module *) let module State = struct type t = { - prvopts : prv_options; - input : string option; - terminal : T.terminal lazy_t; - interactive : bool; - eco : bool; - gccompact : int option; - docgen : bool; - outdirp : string option; + (*---*) prvopts : prv_options; + (*---*) input : string option; + (*---*) terminal : T.terminal lazy_t; + (*---*) interactive : bool; + (*---*) eco : bool; + (*---*) gccompact : int option; + (*---*) docgen : bool; + (*---*) outdirp : string option; + mutable trace : trace1 list option; } + + and trace1 = + { position : int + ; goals : string list option + ; messages : (EcGState.loglevel * string) list } + + module Trace = struct + let trace0 : trace1 = + { position = 0; goals = None; messages = []; } + + let push1_message (trace1 : trace1) (msg, lvl) : trace1 = + { trace1 with messages = (msg, lvl) :: trace1.messages } + + let push_message (trace : trace1 list) msg = + match trace with + | [] -> + [push1_message trace0 msg] + | trace1 :: trace -> + push1_message trace1 msg :: trace + end end in let state : State.t = @@ -471,7 +492,8 @@ let main () = ; eco = false ; gccompact = None ; docgen = false - ; outdirp = None } + ; outdirp = None + ; trace = None } end @@ -493,6 +515,8 @@ let main () = lazy (T.from_channel ~name ~gcstats ~progress (open_in name)) in + let trace0 = State.{ position = 0; goals = None; messages = [] } in + { prvopts = {cmpopts.cmpo_provers with prvo_iterate = true} ; input = Some name ; terminal = terminal @@ -500,7 +524,8 @@ let main () = ; eco = cmpopts.cmpo_noeco ; gccompact = cmpopts.cmpo_compact ; docgen = false - ; outdirp = None } + ; outdirp = None + ; trace = Some [trace0] } end @@ -543,7 +568,8 @@ let main () = ; eco = true ; gccompact = None ; docgen = true - ; outdirp = docopts.doco_outdirp } + ; outdirp = docopts.doco_outdirp + ; trace = None } end in @@ -571,7 +597,20 @@ let main () = assert (nameo <> input); - let eco = EcEco.{ + let eco = + let mktrace (trace : State.trace1 list) : EcEco.ecotrace = + let mktrace1 (trace1 : State.trace1) : int * EcEco.ecotrace1 = + let goals = Option.value ~default:[] trace1.goals in + let messages = + let for1 (lvl, msg) = + Format.sprintf "%s: %s" + (EcGState.string_of_loglevel lvl) + msg in + String.concat "\n" (List.rev_map for1 trace1.messages) in + (trace1.position, EcEco.{ goals; messages; }) + in List.rev_map mktrace1 trace in + + EcEco.{ eco_root = EcEco.{ eco_digest = Digest.file input; eco_kind = kind; @@ -584,6 +623,7 @@ let main () = eco_kind = x.rqd_kind; } in (x.rqd_name, (ecr, x.rqd_direct))) (EcScope.Theory.required scope)); + eco_trace = Option.map mktrace state.trace; } in let out = open_out nameo in @@ -665,7 +705,10 @@ let main () = EcScope.hierror "invalid pragma: `%s'\n%!" x); let notifier (lvl : EcGState.loglevel) (lazy msg) = - T.notice ~immediate:true lvl msg terminal + state.trace <- state.trace |> Option.map (fun trace -> + State.Trace.push_message trace (lvl, msg) + ); + T.notice ~immediate:true lvl msg terminal; in EcCommands.addnotifier notifier; @@ -694,8 +737,25 @@ let main () = let timed = p.EP.gl_debug = Some `Timed in let break = p.EP.gl_debug = Some `Break in let ignore_fail = ref false in + + state.trace <- state.trace |> Option.map (fun trace -> + { State.Trace.trace0 with position = loc.loc_echar } :: trace + ); + try let tdelta = EcCommands.process ~src ~timed ~break p.EP.gl_action in + + state.trace <- state.trace |> Option.map (fun trace -> + match trace with + | [] -> assert false + | trace1 :: trace -> + assert (Option.is_none trace1.State.goals); + let goals = EcCommands.pp_all_goals () in + let goals = if List.is_empty goals then None else Some goals in + let trace1 = { trace1 with goals } in + trace1 :: trace + ); + if p.EP.gl_fail then begin ignore_fail := true; raise (EcScope.HiScopeError (None, "this command is expected to fail")) @@ -713,10 +773,10 @@ let main () = raise (EcScope.toperror_of_exn ~gloc:loc e) end; if T.interactive terminal then begin - let error = - Format.asprintf - "The following error has been ignored:@.@.@%a" - EcPException.exn_printer e in + let error = + Format.asprintf + "The following error has been ignored:@.@.@%a" + EcPException.exn_printer e in T.notice ~immediate:true `Info error terminal end end) diff --git a/src/ecCommands.ml b/src/ecCommands.ml index 9f647c52b..135a2b3de 100644 --- a/src/ecCommands.ml +++ b/src/ecCommands.ml @@ -912,6 +912,11 @@ let addnotifier (notifier : notifier) = let gstate = EcScope.gstate (oget !context).ct_root in ignore (EcGState.add_notifier notifier gstate) +(* -------------------------------------------------------------------- *) +let notify (level : EcGState.loglevel) fmt = + assert (EcUtils.is_some !context); + EcScope.notify (oget !context).ct_root level fmt + (* -------------------------------------------------------------------- *) let current () = (oget !context).ct_current @@ -1017,7 +1022,36 @@ let pp_current_goal ?(all = false) stream = end end +(* -------------------------------------------------------------------- *) let pp_maybe_current_goal stream = match (Pragma.get ()).pm_verbose with | true -> pp_current_goal ~all:(Pragma.get ()).pm_g_prall stream | false -> () + +(* -------------------------------------------------------------------- *) +let pp_all_goals () = + let scope = current () in + + match S.xgoal scope with + | Some { S.puc_active = Some ({ puc_jdg = S.PSCheck pf }, _) } -> begin + match EcCoreGoal.opened pf with + | None -> + [] + + | Some _ -> + let get_hc { EcCoreGoal.g_hyps; EcCoreGoal.g_concl } = + (EcEnv.LDecl.tohyps g_hyps, g_concl) + in + + let ppe = EcPrinting.PPEnv.ofenv (S.env scope) in + let goals = List.map get_hc (EcCoreGoal.all_opened pf) in + + List.map (fun goal -> + let buffer = Buffer.create 0 in + Format.fprintf + (Format.formatter_of_buffer buffer) + "%a@?" (EcPrinting.pp_goal1 ppe) goal; + Buffer.contents buffer) goals + end + + | _ -> [] diff --git a/src/ecCommands.mli b/src/ecCommands.mli index f61a313f3..a72d31a43 100644 --- a/src/ecCommands.mli +++ b/src/ecCommands.mli @@ -36,6 +36,7 @@ val initialize : val current : unit -> EcScope.scope val addnotifier : notifier -> unit +val notify : EcGState.loglevel -> ('a, Format.formatter, unit, unit) format4 -> 'a (* -------------------------------------------------------------------- *) val process_internal : @@ -60,6 +61,7 @@ val doc_comment : [`Global | `Item] * string -> unit (* -------------------------------------------------------------------- *) val pp_current_goal : ?all:bool -> Format.formatter -> unit val pp_maybe_current_goal : Format.formatter -> unit +val pp_all_goals : unit -> string list (* -------------------------------------------------------------------- *) val pragma_verbose : bool -> unit diff --git a/src/ecCorePrinting.ml b/src/ecCorePrinting.ml index d906a61e3..29051f0a0 100644 --- a/src/ecCorePrinting.ml +++ b/src/ecCorePrinting.ml @@ -112,6 +112,8 @@ module type PrinterAPI = sig val pp_hyps : PPEnv.t -> EcEnv.LDecl.hyps pp val pp_goal : PPEnv.t -> prpo_display -> ppgoal pp + val pp_goal1 : PPEnv.t -> (EcBaseLogic.hyps * form) pp + (* ------------------------------------------------------------------ *) val pp_by_theory : PPEnv.t -> (PPEnv.t -> (EcPath.path * 'a) pp) -> ((EcPath.path * 'a) list) pp diff --git a/src/ecEco.ml b/src/ecEco.ml index cd80c8020..fc8f41c98 100644 --- a/src/ecEco.ml +++ b/src/ecEco.ml @@ -5,7 +5,7 @@ module Json = Yojson (* -------------------------------------------------------------------- *) module Version = struct - let current : int = 3 + let current : int = 4 end (* -------------------------------------------------------------------- *) @@ -16,9 +16,16 @@ type ecoroot = { eco_digest : digest; } +type ecorange = int + +type ecotrace1 = { goals: string list; messages: string; } + +type ecotrace = (ecorange * ecotrace1) list + type eco = { eco_root : ecoroot; eco_depends : ecodepend Mstr.t; + eco_trace : ecotrace option; } and ecodepend = @@ -36,6 +43,24 @@ let flag_of_json (data : Json.t) : bool = let flag_to_json (flag : bool) : Json.t = `Bool flag +(* -------------------------------------------------------------------- *) +let int_of_json (data : Json.t) : int = + match data with + | `Int i -> i + | _ -> raise InvalidEco + +(* -------------------------------------------------------------------- *) +let string_of_json (data : Json.t) : string = + match data with + | `String s -> s + | _ -> raise InvalidEco + +(* -------------------------------------------------------------------- *) +let list_of_json (tx : Json.t -> 'a) (data : Json.t) : 'a list = + match data with + | `List data -> List.map tx data + | _ -> raise InvalidEco + (* -------------------------------------------------------------------- *) let kind_to_json (k : EcLoader.kind) = match k with @@ -71,9 +96,9 @@ let ecoroot_to_map (ecor : ecoroot) : (string * Json.t) list = "digest", digest_to_json ecor.eco_digest ] let ecoroot_of_map (data : Json.t Mstr.t) : ecoroot = - let kd = kind_of_json (Mstr.find_exn InvalidEco "kind" data) in - let dg = digest_of_json (Mstr.find_exn InvalidEco "digest" data) in - { eco_kind = kd; eco_digest = dg; } + let eco_kind = kind_of_json (Mstr.find_exn InvalidEco "kind" data) in + let eco_digest = digest_of_json (Mstr.find_exn InvalidEco "digest" data) in + { eco_kind; eco_digest; } (* -------------------------------------------------------------------- *) let ecoroot_to_json (ecor : ecoroot) : Json.t = @@ -86,6 +111,43 @@ let ecoroot_of_json (data : Json.t) : ecoroot = | _ -> raise InvalidEco +(* -------------------------------------------------------------------- *) +let trace_to_json (trace : ecotrace option) : Json.t = + match trace with + | None -> + `Null + + | Some trace -> + let for1 ((position, { goals; messages; })) = + `Assoc [ + ("position", `Int position); + ("goals" , `List (List.map (fun goal -> `String goal) goals)); + ("messages", `String messages); + ] + in `List (List.map for1 trace) + +let trace_of_json (data : Json.t) : ecotrace option = + match data with + | `Null -> + None + + | `List data -> + let for1 (data : Json.t) = + match data with + | `Assoc data -> + let data = Mstr.of_list data in + let position = Mstr.find_exn InvalidEco "position" data |> int_of_json in + let goals = Mstr.find_exn InvalidEco "goals" data |> list_of_json string_of_json in + let messages = Mstr.find_exn InvalidEco "messages" data |> string_of_json in + (position, { goals; messages; }) + | _ -> + raise InvalidEco + + in Some (List.map for1 data) + + | _ -> + raise InvalidEco + (* -------------------------------------------------------------------- *) let ecodepend_to_json ((ecor, direct) : ecodepend) : Json.t = `Assoc ([ "direct", flag_to_json direct] @ (ecoroot_to_map ecor)) @@ -119,6 +181,7 @@ let to_json (eco : eco) : Json.t = [ "version", `Int Version.current; "echash" , `String EcVersion.hash; "root" , ecoroot_to_json eco.eco_root; + "trace" , trace_to_json eco.eco_trace; "depends", `Assoc depends ] (* -------------------------------------------------------------------- *) @@ -135,10 +198,11 @@ let of_json (data : Json.t) : eco = if echash <> `String EcVersion.hash then raise InvalidEco; - let root = ecoroot_of_json (Mstr.find_exn InvalidEco "root" data) in - let depends = depends_of_json (Mstr.find_exn InvalidEco "depends" data) in + let eco_root = ecoroot_of_json (Mstr.find_exn InvalidEco "root" data) in + let eco_depends = depends_of_json (Mstr.find_exn InvalidEco "depends" data) in + let eco_trace = trace_of_json (Mstr.find_exn InvalidEco "trace" data) in - { eco_root = root; eco_depends = depends; } + { eco_root; eco_depends; eco_trace; } | _ -> raise InvalidEco diff --git a/src/ecOptions.ml b/src/ecOptions.ml index 499773796..f012e8e8d 100644 --- a/src/ecOptions.ml +++ b/src/ecOptions.ml @@ -25,6 +25,7 @@ and cmp_option = { cmpo_tstats : string option; cmpo_noeco : bool; cmpo_script : bool; + cmpo_trace : bool; } and cli_option = { @@ -347,6 +348,7 @@ let specs = { `Spec ("tstats" , `String, "Save timing statistics to "); `Spec ("script" , `Flag , "Computer-friendly output"); `Spec ("no-eco" , `Flag , "Do not cache verification results"); + `Spec ("trace" , `Flag , "Save all goals & messages in .eco"); `Spec ("compact", `Int , "")]); ("cli", "Run EasyCrypt top-level", [ @@ -516,7 +518,8 @@ let cmp_options_of_values ini values input = cmpo_compact = get_int "compact" values; cmpo_tstats = get_string "tstats" values; cmpo_noeco = get_flag "no-eco" values; - cmpo_script = get_flag "script" values; } + cmpo_script = get_flag "script" values; + cmpo_trace = get_flag "trace" values; } let runtest_options_of_values ini values (input, scenarios) = { runo_input = input; diff --git a/src/ecOptions.mli b/src/ecOptions.mli index 5ba1d0f63..59009718a 100644 --- a/src/ecOptions.mli +++ b/src/ecOptions.mli @@ -21,6 +21,7 @@ and cmp_option = { cmpo_tstats : string option; cmpo_noeco : bool; cmpo_script : bool; + cmpo_trace : bool; } and cli_option = { diff --git a/src/ecPrinting.ml b/src/ecPrinting.ml index c320e7186..a9f63997d 100644 --- a/src/ecPrinting.ml +++ b/src/ecPrinting.ml @@ -3314,6 +3314,10 @@ let pp_goal (ppe : PPEnv.t) (prpo : prpo_display) fmt (g, extra) = (PPGoal.pp_goal1 ~pphyps:false ~prpo ~idx:(i+2) ppe) g) gs +(* -------------------------------------------------------------------- *) +let pp_goal1 (ppe : PPEnv.t) (fmt : Format.formatter) (g : EcBaseLogic.hyps * form) = + PPGoal.pp_goal1 ppe fmt g + (* -------------------------------------------------------------------- *) let pp_ovdecl ppe fmt ov = Format.fprintf fmt "%s : %a" (odfl "_" ov.ov_name) (pp_type ppe) ov.ov_type