From 5ec2bfd2a2381934845e1a8bd9183e77b0fadeb6 Mon Sep 17 00:00:00 2001 From: Alexander Hicks Date: Thu, 7 Aug 2025 16:22:26 +0100 Subject: [PATCH 01/44] add mathlib dependency, update lean version, todo: fix build errors --- lake-manifest.json | 82 ++++++++++++++++++++++++++++++++++++- lakefile.toml | 4 ++ lean-toolchain | 2 +- src/Iris/BI/BIBase.lean | 1 - src/Iris/Std/DelabRule.lean | 17 ++++++++ 5 files changed, 103 insertions(+), 3 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 195d8b30c..aef6d1fa9 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,7 +1,17 @@ {"version": "1.1.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/leanprover-community/quote4", + [{"url": "https://github.com/leanprover-community/mathlib4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "a03809fa069dd9b3722e8f2e27e586a39db695fb", + "name": "mathlib", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, "scope": "leanprover-community", @@ -10,6 +20,76 @@ "manifestFile": "lake-manifest.json", "inputRev": "stable", "inherited": false, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "c37191eba2da78393070da8c4367689d8c4276e4", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/LeanSearchClient", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "6c62474116f525d2814f0157bb468bf3a4f9f120", + "name": "LeanSearchClient", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/import-graph", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "4241928fd3ebae83a037a253e39d9b773e34c3b4", + "name": "importGraph", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/ProofWidgets4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "96c67159f161fb6bf6ce91a2587232034ac33d7e", + "name": "proofwidgets", + "manifestFile": "lake-manifest.json", + "inputRev": "v0.0.67", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/aesop", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "0a136f764a5dfedc4498e93ad8e297cff57ba2fc", + "name": "aesop", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/batteries", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "c4277d9bca1c4d366ae1d976175ff6c008e56ac2", + "name": "batteries", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "c682c91d2d4dd59a7187e2ab977ac25bd1f87329", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, "configFile": "lakefile.toml"}], "name": "iris", "lakeDir": ".lake"} diff --git a/lakefile.toml b/lakefile.toml index f1c790ac9..b110ebce4 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -7,6 +7,10 @@ name = "Qq" scope = "leanprover-community" version = "git#stable" +[[require]] +name = "mathlib" +scope = "leanprover-community" + [[lean_lib]] name = "Iris" diff --git a/lean-toolchain b/lean-toolchain index b9f9eea14..2c6e1c4ba 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.21.0 \ No newline at end of file +leanprover/lean4:v4.22.0-rc4 diff --git a/src/Iris/BI/BIBase.lean b/src/Iris/BI/BIBase.lean index 61d3bd3e5..e42a3414f 100644 --- a/src/Iris/BI/BIBase.lean +++ b/src/Iris/BI/BIBase.lean @@ -285,4 +285,3 @@ macro_rules delab_rule except0 | `($_ $P) => do ``(iprop(◇ $(← unpackIprop P))) - diff --git a/src/Iris/Std/DelabRule.lean b/src/Iris/Std/DelabRule.lean index f677b798f..0b04c17f4 100644 --- a/src/Iris/Std/DelabRule.lean +++ b/src/Iris/Std/DelabRule.lean @@ -32,3 +32,20 @@ macro_rules def unexpand : Lean.PrettyPrinter.Unexpander $[| $p => $s]* | _ => throw ()) + +/- Suggested fix +syntax "delab_rule" ident matchAlts' : command +macro_rules + | `(delab_rule $f $[| $p => $s]*) => do + let f := f.getId + if f.isAnonymous then + throwUnsupported + let f ← match ← Macro.resolveGlobalName f with + | [(name, [])] => pure name + | _ => throwUnsupported + + `(@[app_unexpander $(mkIdent f)] + def unexpand : Lean.PrettyPrinter.Unexpander + $[| $p => $s]* + | _ => throw ()) +-/ From 7b500b088aba6a4c55b8b5d1d985ae4a6f4ae6e3 Mon Sep 17 00:00:00 2001 From: Quang Dao Date: Thu, 7 Aug 2025 10:21:32 -0600 Subject: [PATCH 02/44] update README --- readme.md | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/readme.md b/readme.md index c224133ba..a19166662 100644 --- a/readme.md +++ b/readme.md @@ -1,8 +1,15 @@ -Lean 4 port of *Iris*, a higher-order concurrent separation logic framework. +# Verified-zkEVM Fork of Iris +This is a fork of [iris-lean](https://github.com/iris-project/iris-lean), a higher-order concurrent separation logic framework. We plan to develop the [Bluebell](https://arxiv.org/pdf/2402.18708) program logic on top of Iris. This repo adds mathlib as a dependency for probability theory and other math prerequisites. + +- [Verified-zkEVM Fork of Iris](#verified-zkevm-fork-of-iris) - [About Iris](#about-iris) - [Project](#project) - [Usage](#usage) + - [1. Instantiating the Separation Logic Interface](#1-instantiating-the-separation-logic-interface) + - [2. Adding Custom Notation](#2-adding-custom-notation) + - [3. Instantiating Existing Typeclasses](#3-instantiating-existing-typeclasses) + - [4. Writing Separation Logic Proofs](#4-writing-separation-logic-proofs) - [Structure](#structure) - [Tactics](#tactics) - [Type Classes](#type-classes) From 55f0cce60bbe3a88a9bd0deba5fcbbbb55567774 Mon Sep 17 00:00:00 2001 From: Quang Dao Date: Thu, 7 Aug 2025 10:27:35 -0600 Subject: [PATCH 03/44] pin mathlib to v4.21.0 --- lake-manifest.json | 38 ++++++++++++++++++------------------- lakefile.toml | 6 +----- lean-toolchain | 2 +- src/Iris/Std/DelabRule.lean | 17 ----------------- 4 files changed, 21 insertions(+), 42 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index aef6d1fa9..932d13d1a 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,27 +5,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "a03809fa069dd9b3722e8f2e27e586a39db695fb", + "rev": "308445d7985027f538e281e18df29ca16ede2ba3", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "v4.21.0", "inherited": false, "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/quote4", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "e9c65db4823976353cd0bb03199a172719efbeb7", - "name": "Qq", - "manifestFile": "lake-manifest.json", - "inputRev": "stable", - "inherited": false, - "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "c37191eba2da78393070da8c4367689d8c4276e4", + "rev": "c4aa78186d388e50a436e8362b947bae125a2933", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "4241928fd3ebae83a037a253e39d9b773e34c3b4", + "rev": "d07bd64f1910f1cc5e4cc87b6b9c590080e7a457", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -55,27 +45,37 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "96c67159f161fb6bf6ce91a2587232034ac33d7e", + "rev": "6980f6ca164de593cb77cd03d8eac549cc444156", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.67", + "inputRev": "v0.0.62", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "0a136f764a5dfedc4498e93ad8e297cff57ba2fc", + "rev": "8ff27701d003456fd59f13a9212431239d902aef", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", "inherited": true, "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/quote4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "e9c65db4823976353cd0bb03199a172719efbeb7", + "name": "Qq", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "c4277d9bca1c4d366ae1d976175ff6c008e56ac2", + "rev": "8d2067bf518731a70a255d4a61b5c103922c772e", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,7 +85,7 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "c682c91d2d4dd59a7187e2ab977ac25bd1f87329", + "rev": "7c6aef5f75a43ebbba763b44d535175a1b04c9e0", "name": "Cli", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/lakefile.toml b/lakefile.toml index b110ebce4..bb6a8fb32 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -2,14 +2,10 @@ name = "iris" srcDir = "./src/" defaultTargets = ["Iris", "IrisTest"] -[[require]] -name = "Qq" -scope = "leanprover-community" -version = "git#stable" - [[require]] name = "mathlib" scope = "leanprover-community" +version = "git#v4.21.0" [[lean_lib]] name = "Iris" diff --git a/lean-toolchain b/lean-toolchain index 2c6e1c4ba..980709bbb 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.22.0-rc4 +leanprover/lean4:v4.21.0 diff --git a/src/Iris/Std/DelabRule.lean b/src/Iris/Std/DelabRule.lean index 0b04c17f4..f677b798f 100644 --- a/src/Iris/Std/DelabRule.lean +++ b/src/Iris/Std/DelabRule.lean @@ -32,20 +32,3 @@ macro_rules def unexpand : Lean.PrettyPrinter.Unexpander $[| $p => $s]* | _ => throw ()) - -/- Suggested fix -syntax "delab_rule" ident matchAlts' : command -macro_rules - | `(delab_rule $f $[| $p => $s]*) => do - let f := f.getId - if f.isAnonymous then - throwUnsupported - let f ← match ← Macro.resolveGlobalName f with - | [(name, [])] => pure name - | _ => throwUnsupported - - `(@[app_unexpander $(mkIdent f)] - def unexpand : Lean.PrettyPrinter.Unexpander - $[| $p => $s]* - | _ => throw ()) --/ From 5c1d7a08010891a7ca73f4b31c8488d5dff88b49 Mon Sep 17 00:00:00 2001 From: Quang Dao Date: Thu, 7 Aug 2025 10:30:33 -0600 Subject: [PATCH 04/44] add sync upstream workflow --- .github/workflows/sync-upstream.yml | 150 ++++++++++++++++++++++++++++ 1 file changed, 150 insertions(+) create mode 100644 .github/workflows/sync-upstream.yml diff --git a/.github/workflows/sync-upstream.yml b/.github/workflows/sync-upstream.yml new file mode 100644 index 000000000..9a8545d6e --- /dev/null +++ b/.github/workflows/sync-upstream.yml @@ -0,0 +1,150 @@ +name: Sync with Upstream + +on: + schedule: + - cron: "0 9 */14 * *" # Every 14 days at 09:00 AM UTC + workflow_dispatch: # Allow manual triggering + +jobs: + sync_upstream: + runs-on: ubuntu-latest + permissions: + contents: write + pull-requests: write + steps: + - name: Checkout repository + uses: actions/checkout@v4 + with: + token: ${{ secrets.GITHUB_TOKEN }} + fetch-depth: 0 + + - name: Configure Git + run: | + git config --global user.name "github-actions[bot]" + git config --global user.email "github-actions[bot]@users.noreply.github.com" + + - name: Add upstream remote + run: | + git remote add upstream https://github.com/leanprover-community/iris-lean.git || true + git fetch upstream + + - name: Create sync branch + id: sync + run: | + BRANCH_NAME="sync-upstream-$(date +%Y-%m-%d)" + echo "branch_name=$BRANCH_NAME" >> $GITHUB_OUTPUT + + # Check if there are any differences between our master and upstream master + UPSTREAM_COMMITS=$(git rev-list --count HEAD..upstream/master 2>/dev/null || echo "0") + echo "upstream_commits=$UPSTREAM_COMMITS" >> $GITHUB_OUTPUT + + if [ "$UPSTREAM_COMMITS" -eq "0" ]; then + echo "No new commits from upstream. Skipping sync." + echo "needs_sync=false" >> $GITHUB_OUTPUT + exit 0 + fi + + echo "needs_sync=true" >> $GITHUB_OUTPUT + echo "Found $UPSTREAM_COMMITS new commits from upstream" + + # Create and switch to sync branch + git checkout -b "$BRANCH_NAME" + + # Attempt to merge upstream changes + if git merge upstream/master --no-edit; then + echo "merge_success=true" >> $GITHUB_OUTPUT + echo "Upstream changes merged successfully" + else + echo "merge_success=false" >> $GITHUB_OUTPUT + echo "Merge conflicts detected" + # Add all files (including conflicted ones) and commit + git add . + git commit -m "WIP: Sync with upstream - merge conflicts need resolution" + fi + + - name: Push sync branch + if: steps.sync.outputs.needs_sync == 'true' + run: | + git push origin ${{ steps.sync.outputs.branch_name }} + + - name: Create Pull Request + if: steps.sync.outputs.needs_sync == 'true' + uses: actions/github-script@v7 + with: + script: | + const branchName = '${{ steps.sync.outputs.branch_name }}'; + const mergeSuccess = '${{ steps.sync.outputs.merge_success }}' === 'true'; + const upstreamCommits = '${{ steps.sync.outputs.upstream_commits }}'; + + let title, body; + + if (mergeSuccess) { + title = `🔄 Sync with upstream (${upstreamCommits} commits)`; + body = `## Upstream Sync + + This PR automatically syncs changes from \`leanprover-community/iris-lean\`. + + ### Changes + - **${upstreamCommits}** new commits from upstream + - No merge conflicts detected ✅ + + ### Next Steps + - Review the changes + - Run tests to ensure compatibility + - Merge when ready + + --- + *This PR was created automatically by the sync-upstream workflow.*`; + } else { + title = `⚠️ Sync with upstream (${upstreamCommits} commits) - Conflicts Need Resolution`; + body = `## Upstream Sync - Manual Resolution Required + + This PR automatically syncs changes from \`leanprover-community/iris-lean\`, but **merge conflicts were detected** and need manual resolution. + + ### Changes + - **${upstreamCommits}** new commits from upstream + - ⚠️ Merge conflicts detected - manual resolution required + + ### Next Steps + 1. Check out this branch locally: \`git checkout ${branchName}\` + 2. Resolve merge conflicts in the affected files + 3. Commit the resolved changes + 4. Push the updates: \`git push origin ${branchName}\` + 5. Review and merge this PR + + ### Commands to resolve locally: + \`\`\`bash + git checkout ${branchName} + # Resolve conflicts in your editor + git add . + git commit -m "Resolve merge conflicts from upstream sync" + git push origin ${branchName} + \`\`\` + + --- + *This PR was created automatically by the sync-upstream workflow.*`; + } + + const { data: pr } = await github.rest.pulls.create({ + owner: context.repo.owner, + repo: context.repo.repo, + title: title, + head: branchName, + base: 'master', + body: body + }); + + console.log(`Created PR #${pr.number}: ${pr.html_url}`); + + // Add labels based on merge status + const labels = ['upstream-sync']; + if (!mergeSuccess) { + labels.push('merge-conflicts'); + } + + await github.rest.issues.addLabels({ + owner: context.repo.owner, + repo: context.repo.repo, + issue_number: pr.number, + labels: labels + }); \ No newline at end of file From 2e405eb9809ebf95fe8b013e1781629fcc738622 Mon Sep 17 00:00:00 2001 From: Quang Dao Date: Thu, 7 Aug 2025 10:35:03 -0600 Subject: [PATCH 05/44] add AI review workflow --- .github/workflows/build.yml | 9 +++++ .github/workflows/review.yml | 75 ++++++++++++++++++++++++++++++++++++ 2 files changed, 84 insertions(+) create mode 100644 .github/workflows/review.yml diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 68e58ae13..1e0baab28 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -8,6 +8,15 @@ on: workflow_dispatch: jobs: + cancel: + name: "Cancel Previous Runs" + runs-on: ubuntu-latest + steps: + - uses: styfle/cancel-workflow-action@0.12.1 + with: + all_but_latest: true + access_token: ${{ github.token }} + build: runs-on: ubuntu-latest diff --git a/.github/workflows/review.yml b/.github/workflows/review.yml new file mode 100644 index 000000000..789bafa46 --- /dev/null +++ b/.github/workflows/review.yml @@ -0,0 +1,75 @@ +name: AI Code Review with External Context + +on: + issue_comment: + types: [created] + +# This job will only run on pull request comments that start with '/review' +jobs: + review: + # UPDATED LINE: Added a check for author association + if: >- + github.event.issue.pull_request && + startsWith(github.event.comment.body, '/review') && + ( + github.event.comment.author_association == 'OWNER' || + github.event.comment.author_association == 'MEMBER' + ) + runs-on: ubuntu-latest + permissions: + contents: read + pull-requests: write + + steps: + - name: Checkout repository + uses: actions/checkout@v4 + + - name: Set up Python + uses: actions/setup-python@v5 + with: + python-version: '3.11' + + - name: Install dependencies + run: pip install -r ./scripts/requirements.txt + + - name: Extract URL and Files from comment + id: get_args + run: | + BODY="${{ github.event.comment.body }}" + URL=$(echo "$BODY" | grep -o 'https://[^ ]*') + FILES=$(echo "$BODY" | sed -n 's/.*and-files \([^ ]*\).*/\1/p') + echo "url=$URL" >> $GITHUB_OUTPUT + echo "files=$FILES" >> $GITHUB_OUTPUT + + - name: Run AI Review Script + id: ai_review + env: + # The GitHub token is automatically available to the runner + GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} + GEMINI_API_KEY: ${{ secrets.GEMINI_API_KEY }} + run: | + # Run the script and capture its output to post as a comment later + # We use a special "end of file" marker to handle multiline output + EOF_MARKER=$(head /dev/urandom | tr -dc A-Za-z0-9 | head -c 16) + echo "review_text<<$EOF_MARKER" >> $GITHUB_OUTPUT + python ./scripts/review.py \ + --pr-number ${{ github.event.issue.number }} \ + --context-url ${{ steps.get_args.outputs.url }} \ + --context-files "${{ steps.get_args.outputs.files }}" >> $GITHUB_OUTPUT + echo "$EOF_MARKER" >> $GITHUB_OUTPUT + + - name: Post Review Comment + uses: actions/github-script@v7 + env: + REVIEW_TEXT: ${{ steps.ai_review.outputs.review_text }} + with: + script: | + const header = '### 🤖 AI Review (with external context)\\n\\n'; + const reviewBody = process.env.REVIEW_TEXT; + + github.rest.issues.createComment({ + issue_number: context.issue.number, + owner: context.repo.owner, + repo: context.repo.repo, + body: header + reviewBody + }); \ No newline at end of file From db00e9689a24b798266a87452929325fd12f61f2 Mon Sep 17 00:00:00 2001 From: Quang Dao Date: Thu, 7 Aug 2025 11:06:43 -0600 Subject: [PATCH 06/44] add review python file and requirements text file --- scripts/requirements.txt | 6 ++ scripts/review.py | 159 +++++++++++++++++++++++++++++++++++++++ 2 files changed, 165 insertions(+) create mode 100644 scripts/requirements.txt create mode 100644 scripts/review.py diff --git a/scripts/requirements.txt b/scripts/requirements.txt new file mode 100644 index 000000000..6951201c3 --- /dev/null +++ b/scripts/requirements.txt @@ -0,0 +1,6 @@ +# scripts/requirements.txt + +google-generativeai +requests +beautifulsoup4 +PyMuPDF \ No newline at end of file diff --git a/scripts/review.py b/scripts/review.py new file mode 100644 index 000000000..f67100fed --- /dev/null +++ b/scripts/review.py @@ -0,0 +1,159 @@ +import os +import argparse +import subprocess +import requests +from bs4 import BeautifulSoup +import google.generativeai as genai +import fitz +import io + +# --- Helper Functions --- +# --- PR diff --- +def get_pr_diff(pr_number: str) -> str: + """Fetches the diff of the specified pull request.""" + try: + diff = subprocess.check_output(["gh", "pr", "diff", pr_number], text=True).strip() + if not diff: return "Could not retrieve PR diff." + return diff + except subprocess.CalledProcessError as e: return f"Error fetching PR diff: {e}" + +# --- Reference document --- +def get_document_content(urls_str: str) -> str: + """Fetches and extracts text content from a comma-separated string of URLs.""" + if not urls_str: + return "No external references were provided." + + all_docs_content = "" + urls = [url.strip() for url in urls_str.split(',')] + + for url in urls: + if not url: continue + try: + headers = {'User-Agent': 'Mozilla/5.0 (Windows NT 10.0; Win64; x64)'} + response = requests.get(url, timeout=30, headers=headers) + response.raise_for_status() + content_type = response.headers.get("Content-Type", "") + content = "" + if "application/pdf" in content_type or url.lower().endswith('.pdf'): + with fitz.open(stream=io.BytesIO(response.content), filetype="pdf") as doc: + content = "".join(page.get_text() for page in doc) + else: + soup = BeautifulSoup(response.content, "html.parser") + for element in soup(["script", "style", "nav", "footer", "header"]): element.decompose() + text = soup.get_text() + lines = (line.strip() for line in text.splitlines()) + content = "\n".join(chunk for line in lines for chunk in line.split(" ") if chunk) + all_docs_content += f"--- Start of content from {url} ---\n{content}\n--- End of content from {url} ---\n\n" + except Exception as e: + all_docs_content += f"--- Error processing document '{url}': {e} ---\n\n" + return all_docs_content + +# --- Relevant files from the repository --- +def get_repo_files_content(paths_str: str) -> str: + """Reads content from a comma-separated string of file and directory paths.""" + if not paths_str: + return "No ArkLib references were provided." + + all_files_content = "" + paths = [path.strip() for path in paths_str.split(',')] + + expanded_files = [] + for path in paths: + if not path: continue + if os.path.isdir(path): + for root, _, files in os.walk(path): + for name in files: + expanded_files.append(os.path.join(root, name)) + elif os.path.isfile(path): + expanded_files.append(path) + else: + all_files_content += f"--- Error: Could not find file or directory {path} ---\n\n" + + unique_files = sorted(list(set(expanded_files))) + + for file_path in unique_files: + try: + with open(file_path, 'r', encoding='utf-8') as f: + content = f.read() + all_files_content += f"--- Start of content from {file_path} ---\n{content}\n--- End of content from {file_path} ---\n\n" + except Exception as e: + all_files_content += f"--- Error reading file {file_path}: {e} ---\n\n" + + return all_files_content + +def analyze_code_with_context(diff: str, external_context: str, repo_context: str, additional_comments: str) -> str: + """Generates a code review using the Gemini 2.5 Pro.""" + api_key = os.getenv("GEMINI_API_KEY") + if not api_key: return "Error: GEMINI_API_KEY environment variable not set." + + genai.configure(api_key=api_key) + model = genai.GenerativeModel('gemini-2.5-pro') + + additional_comments_section = "" + if additional_comments and additional_comments.strip(): + additional_comments_section = f""" + **4. Additional Reviewer Comments:** + --- + {additional_comments} + --- + """ + + prompt = f""" + You are an expert code reviewer. Your task is to review a pull request. You have been given the following information: + 1. The content of external reference documents. + 2. The full content of other relevant files from the repository. + 3. The code changes ("diff") from the pull request. + {additional_comments_section} + **1. External Reference Documents:** + --- + {external_context} + --- + + **2. Additional Repository Context Files:** + --- + {repo_context} + --- + + **3. Pull Request Diff:** + --- + {diff} + --- + + **Your Instructions:** + 1. Carefully analyze the "Pull Request Diff" paying attention to the logic, correctness, and style of the changes. + 2. Take into account the additional context provided by other files in the repository. + 3. Compare the formalization against the information and specifications described in the "Reference Document Content". + 4. If "Additional Reviewer Comments" are provided, pay close attention to them as they give specific instructions or focus areas for your review. + 5. Provide a concise, high-level summary of the changes. + 6. Check that the code correctly formalizes the relevant material from the reference document. + 7. Provide specific, actionable feedback. If you find issues, suggest what changes are required, explaining why, and illustrate this with code. + 8. Structure your review clearly. Use markdown for formatting. + """ + try: + response = model.generate_content(prompt) + return response.text + except Exception as e: return f"An error occurred while calling the Gemini API: {e}" + +def main(): + parser = argparse.ArgumentParser(description="AI Code Reviewer") + parser.add_argument("--pr-number", required=True) + parser.add_argument("--external-refs", required=False, default="") + parser.add_argument("--arklib-refs", required=False, default="") + parser.add_argument("--additional-comments", required=False, default="") + args = parser.parse_args() + + diff = get_pr_diff(args.pr_number) + external_context = get_document_content(args.external_refs) + repo_context = get_repo_files_content(args.arklib_refs) + + # Basic checks for errors + if "Error" in diff[:60] or "Error" in external_context[:60]: + print(f"Aborting due to error fetching context:\nDiff: {diff}\nExternal Doc: {external_context}") + return + + print("Generating AI review...") + review = analyze_code_with_context(diff, external_context, repo_context, args.additional_comments) + print(review) + +if __name__ == "__main__": + main() \ No newline at end of file From 572cc3b51eb005d7a811d521196c5f3056da82e6 Mon Sep 17 00:00:00 2001 From: Quang Dao Date: Thu, 7 Aug 2025 12:36:30 -0600 Subject: [PATCH 07/44] port over bluebell stuff from VCV-io (#2) --- lakefile.toml | 5 + src/Bluebell.lean | 1 + src/Bluebell/Basic.lean | 612 ++++++++++++++++++ src/Bluebell/ProbabilityTheory/Coupling.lean | 118 ++++ .../ProbabilityTheory/IndepProduct.lean | 129 ++++ 5 files changed, 865 insertions(+) create mode 100644 src/Bluebell.lean create mode 100644 src/Bluebell/Basic.lean create mode 100644 src/Bluebell/ProbabilityTheory/Coupling.lean create mode 100644 src/Bluebell/ProbabilityTheory/IndepProduct.lean diff --git a/lakefile.toml b/lakefile.toml index bb6a8fb32..107e929f5 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -9,6 +9,11 @@ version = "git#v4.21.0" [[lean_lib]] name = "Iris" +globs = ["Iris.*"] + +[[lean_lib]] +name = "Bluebell" +globs = ["Bluebell.*"] [[lean_lib]] name = "IrisTest" diff --git a/src/Bluebell.lean b/src/Bluebell.lean new file mode 100644 index 000000000..18a017fea --- /dev/null +++ b/src/Bluebell.lean @@ -0,0 +1 @@ +import Bluebell.Basic diff --git a/src/Bluebell/Basic.lean b/src/Bluebell/Basic.lean new file mode 100644 index 000000000..bae8a8ae4 --- /dev/null +++ b/src/Bluebell/Basic.lean @@ -0,0 +1,612 @@ +import Iris +import Iris.Algebra.CMRA +import Bluebell.ProbabilityTheory.Coupling +import Bluebell.ProbabilityTheory.IndepProduct + +/-! # Formalizing the Bluebell paper + +This is a copy from an initial attempt in VCV-io. We comment out most of this since there are lots of errors due to updates in Iris. -/ + +open Iris ProbabilityTheory MeasureTheory + +-- Indexed tuples +def indexedTuple (α : Type*) (I : Finset ℕ) := I → α + +def indexedTuple.remove (α : Type*) (I : Finset ℕ) (J : Finset ℕ) (_ : J ⊆ I) : + indexedTuple α I → indexedTuple α (I \ J) := + fun x i => x ⟨i.1, by aesop⟩ + +-- /-- A typeclass for expressing that a type `M` has a validity predicate `✓` -/ +-- class Valid (M : Type*) where +-- valid : M → Prop + +-- export Valid (valid) + +-- prefix:50 "✓" => Valid.valid + +-- instance {α : Type*} [Valid α] (p : α → Prop) : Valid (Subtype p) where +-- valid := fun x => Valid.valid x.1 + +-- instance {α β : Type*} [Valid α] [Valid β] : Valid (α × β) where +-- valid := fun x => Valid.valid x.1 ∧ Valid.valid x.2 + +-- /-- The class of **discrete** cameras, which do not care about step-indexing + +-- TODO: use `Discrete` instance from `CMRA` -/ +-- class DiscreteCMRA (α : Type*) extends CommSemigroup α, Valid α where +-- equiv : α → α → Prop +-- pcore : α → Option α + +-- is_equiv : Equivalence equiv + +-- mul_equiv {x y z} : equiv y z → equiv (x * y) (x * z) +-- pcore_equiv {x y cx} : equiv x y → pcore x = some cx → ∃ cy, pcore y = some cy ∧ equiv cx cy + +-- pcore_left {x cx} : pcore x = some cx → equiv (cx * x) x +-- pcore_idem {x cx} : pcore x = some cx → equiv x cx +-- pcore_mono' {x y cx} : pcore x = some cx → ∃ cy, pcore (x * y) = some (cx * cy) + +-- -- TODO: check whether these are stated correctly +-- valid_equiv {x y} : equiv x y → valid x → valid y +-- valid_mul {x y} : valid (x * y) → valid x + +-- section DiscreteCMRA + +-- variable {α : Type*} [DiscreteCMRA α] {x y₁ y₂ : α} +-- open DiscreteCMRA + +-- lemma valid_extend : valid x → equiv x (y₁ * y₂) → ∃ z₁ z₂, equiv x (z₁ * z₂) := by tauto + +-- lemma valid_l_of_equiv_mul (h₁ : valid x) (h₂ : equiv x (y₁ * y₂)) : valid y₁ := +-- valid_mul (valid_equiv h₂ h₁) + +-- lemma valid_r_of_equiv_mul (h₁ : valid x) (h₂ : equiv x (y₁ * y₂)) : valid y₂ := +-- valid_mul (valid_equiv (mul_comm y₁ y₂ ▸ h₂) h₁) + +-- example : valid x → equiv x (y₁ * y₂) → ∃ z₁ z₂, equiv x (z₁ * z₂) ∧ valid z₁ ∧ valid z₂ := +-- λ h₁ h₂ ↦ let ⟨z₁, z₂, h⟩ := valid_extend h₁ h₂ +-- ⟨z₁, z₂, h, valid_l_of_equiv_mul h₁ h, valid_r_of_equiv_mul h₁ h⟩ + +-- end DiscreteCMRA + +-- instance DiscreteCMRA.instOFE (α : Type*) [DiscreteCMRA α] : OFE α where +-- Equiv := equiv +-- Dist := fun _ ↦ equiv +-- dist_eqv := by simp [DiscreteCMRA.is_equiv] +-- equiv_dist := by simp +-- dist_lt := fun h _ ↦ h + +-- /-- A discrete CMRA can be converted to a regular CMRA -/ +-- instance DiscreteCMRA.instCMRA {α : Type*} [DiscreteCMRA α] : CMRA α := +-- { +-- pcore := pcore +-- op := (·*·) +-- ValidN := fun _ x ↦ valid x +-- Valid := valid +-- op_ne := ⟨fun _ _ _ h ↦ mul_equiv h⟩ +-- pcore_ne := pcore_equiv +-- validN_ne := valid_equiv +-- valid_iff_validN := by simp +-- validN_succ := by simp +-- assoc := by simp [mul_assoc] +-- comm := by simp [mul_comm] +-- pcore_op_left := pcore_left +-- pcore_idem := λ h ↦ by obtain ⟨_, h₁, h₂⟩ := pcore_equiv (pcore_idem h) h +-- exact h₁ ▸ OFE.Equiv.symm h₂ +-- pcore_op_mono := pcore_mono' +-- validN_op_left := valid_mul +-- extend {_ _ y₁ y₂ _ _} := by use y₁, y₂; simpa +-- } + +-- -- class DiscreteUnitalCMRA (α : Type*) extends DiscreteCMRA α, One α where + +-- /-- Typeclass for expressing that a type `M` with multiplication and a one satisfies +-- `1 * a = a` on the left. + +-- This is a unbundled version of `MulOneClass` where we don't require `a * 1 = a` on the right. -/ +-- class MulOneLeftClass (M : Type*) extends One M, Mul M where +-- /-- One is a left neutral element for multiplication -/ +-- protected one_mul : ∀ a : M, 1 * a = a + +-- attribute [simp] MulOneLeftClass.one_mul + +-- instance {M : Type*} [MulOneClass M] : MulOneLeftClass M where +-- one_mul := one_mul + +-- /-- An ordered unital resource algebra is a type with a multiplication, a one, a preorder `≤`, +-- and a validity predicate `✓`, such that: + +-- - `1` is valid +-- - validity is downward closed: `a ≤ b → ✓ b → ✓ a` +-- - validity of multiplication cancels on the right: `✓ (a * b) → ✓ a` +-- - multiplication on the right is monotone: `a ≤ b → a * c ≤ b * c` -/ +-- class OrderedUnitalResourceAlgebra (M : Type*) extends +-- MulOneLeftClass M, Valid M, Preorder M, MulRightMono M where +-- valid_one : ✓ (1 : M) +-- valid_mono {a b} : a ≤ b → ✓ b → ✓ (a : M) +-- valid_mul {a b} : ✓ (a * b : M) → ✓ a + +-- export OrderedUnitalResourceAlgebra (valid_one valid_mono valid_mul) + +-- attribute [simp] valid_one + +-- namespace OrderedUnitalResourceAlgebra + +-- variable {I M : Type*} [OrderedUnitalResourceAlgebra M] + +-- instance : MulRightMono M := ⟨fun _ _ _ h ↦ mul_right_mono h⟩ + +-- /-- Lifting the validity predicate to indexed tuples by requiring all elements to be valid -/ +-- @[simp] +-- instance [Valid M] : Valid (I → M) where +-- valid := fun x => ∀ i, ✓ x i + +-- /-- A resource algebra on `M` is lifted pointwise to a resource algebra on `I → M` -/ +-- instance {I : Type*} : OrderedUnitalResourceAlgebra (I → M) where +-- one_mul := by intro a; funext i; simp only [Pi.mul_apply, Pi.one_apply, MulOneLeftClass.one_mul] +-- valid_one := by intro i; exact valid_one +-- valid_mono := by intro _ _ hab hb i; exact valid_mono (hab i) (hb i) +-- valid_mul := by intro _ _ hab i; exact valid_mul (hab i) +-- elim := by intro _ _ _ h; exact fun i => mul_right_mono (h i) + +-- /-- Define a discrete `CMRA` instance given an `OrderedUnitalResourceAlgebra` instance -/ +-- instance instCMRA : DiscreteCMRA M := sorry + +-- end OrderedUnitalResourceAlgebra + + +-- /-! ## Permissions -/ + +-- /-- A permission on type `α` is a map from `α` to the non-negative rationals `ℚ≥0`. + +-- We need to have the `Multiplicative` tag in order to specify that multiplication is pointwise +-- addition, and unit is the constant zero map. -/ +-- @[reducible] def Permission (α : Type*) := Multiplicative (α → ℚ≥0) + +-- variable {α : Type*} + +-- -- instance : Preorder (Permission α) := inferInstanceAs (Preorder (Multiplicative (α → ℚ≥0))) +-- -- instance : MulOneClass (Permission α) := inferInstanceAs (MulOneClass (Multiplicative (α → ℚ≥0))) +-- -- instance : MulLeftMono (Permission α) := inferInstanceAs (MulLeftMono (Multiplicative (α → ℚ≥0))) + +-- /-- Permissions form an `OrderedUnitalResourceAlgebra` where `≤` is defined pointwise, a resource is valid iff it's below `1` pointwise, and composition is pointwise multiplication -/ +-- instance : OrderedUnitalResourceAlgebra (Permission α) where +-- valid := fun p => p ≤ 1 +-- valid_one := by simp +-- valid_mul := by intro a b hab; simp_all only [le_one_iff_eq_one, LeftCancelMonoid.mul_eq_one, +-- le_refl] +-- valid_mono := by intro a b h h'; simp_all only [le_one_iff_eq_one] +-- -- mul_right_mono := by intro a b c h i; sorry + +-- /-! ## Probability spaces -/ + +-- variable {Ω : Type*} + +-- noncomputable section + +-- -- We want the trivial `{∅, Ω}` sigma algebra, upon which the measure is defined to be `0` on `∅` +-- -- and `1` on `Ω` +-- instance [inst : Nonempty Ω] : One (ProbabilitySpace Ω) where +-- one := @ProbabilitySpace.mk Ω (@MeasureSpace.mk Ω ⊥ (@Measure.dirac _ ⊥ (Classical.choice inst))) +-- (by constructor; simp [Measure.dirac]) + +-- abbrev PSp (Ω : Type*) := WithTop (ProbabilitySpace Ω) + +-- @[simp] +-- instance : Valid (PSp Ω) where +-- valid := fun x => match x with | some _ => True | none => False + +-- instance [inst : Nonempty Ω] : OrderedUnitalResourceAlgebra (PSp Ω) where +-- mul := fun x y => match x, y with +-- | some x, some y => if h : (x.indepProduct y).isSome then (x.indepProduct y).get h else none +-- | _, _ => none +-- valid_one := by simp +-- valid_mul := by intro a b hab; cases a <;> cases b <;> simp_all +-- valid_mono := by +-- intro a b h h'; cases a <;> cases b <;> simp_all +-- have h' : (⊤ : PSp Ω) ≤ WithTop.some _ := h +-- contrapose! h' +-- simp +-- one_mul := sorry +-- elim := sorry +-- -- mul_right_mono := sorry + +-- variable {V : Type*} + +-- -- Needs to encode the term `P = P' ⊗ 𝟙_ (p.support → V)` in the paper +-- /-- Compatibility of a probability space with a permission, defined as the existence of a splitting between: + +-- - the trivial probability space on the zero part of the permission `𝟙_ ({a // p a = 0} → V)` +-- - another probability space `P'` on the non-zero part of the permission -/ +-- def ProbabilityTheory.ProbabilitySpace.compatiblePerm (_P : ProbabilitySpace (α → V)) (p : Permission α) : Prop := +-- ∃ _P' : ProbabilitySpace ({a // p a > 0} → V), True + +-- /-- Generalize compatibility of `ProbabilitySpace` with `Permission` to `PSp` by letting `⊤` be +-- compatible with all permission maps -/ +-- def PSp.compatiblePerm (P : PSp (α → V)) (p : Permission α) : Prop := match P with +-- | some P => ProbabilitySpace.compatiblePerm P p +-- | none => True + +-- /-- The joint structure of a probability space and a permission that are compatible. + +-- This is given a resource algebra structure by pointwise product of the underlying probability space +-- and permission RAs, up to compatibility. -/ +-- @[reducible] +-- def PSpPm (α : Type*) (V : Type*) := +-- {Pp : PSp (α → V) × Permission α // Pp.1.compatiblePerm Pp.2} + +-- namespace PSpPm + +-- /-- Lift a probability space to a probability space-permission pair, via coupling it with the +-- all-one permission -/ +-- def liftProb (μ : ProbabilitySpace (α → V)) : PSpPm α V := +-- ⟨⟨μ, 1⟩, by sorry⟩ + +-- @[simp] +-- instance [Nonempty V] : One (PSpPm α V) where +-- one := ⟨⟨One.one, One.one⟩, by simp [One.one, PSp.compatiblePerm, ProbabilitySpace.compatiblePerm]⟩ + +-- /-- Multiplication is pointwise product of the probability space and the permission -/ +-- @[simp] +-- instance [Nonempty V] : Mul (PSpPm α V) where +-- -- TODO: need to prove product preserves compatibility +-- mul Pp₁ Pp₂ := ⟨⟨Pp₁.1.1 * Pp₂.1.1, Pp₁.1.2 * Pp₂.1.2⟩, by sorry⟩ + +-- -- instance : Valid (PSpPm α V) := inferInstanceAs <| +-- -- Valid (Subtype (fun Pp : PSp (α → V) × Permission α => Pp.1.compatiblePerm Pp.2)) + +-- /-- The resource algebra instance on `PSpPm α V` -/ +-- instance [Nonempty V] : OrderedUnitalResourceAlgebra (PSpPm α V) where +-- one_mul := by simp; intro P p h; sorry +-- valid_one := by simp [Valid.valid, One.one]; sorry +-- valid_mul := by sorry +-- valid_mono := by sorry +-- elim := by sorry + +-- end PSpPm + +-- end + +-- /-- The main model of Bluebell is a function type `I → PSpPm α V`, where `I` is the index set of (independent) program executions. The resource algebra structure is lifted pointwise from `PSpPm`. + +-- To handle multiple programs drawn from index set `I`, we use the RA `I → PSpPm` where +-- operations are lifted pointwise -/ +-- abbrev IndexedPSpPm (I α V : Type*) := I → PSpPm α V + +-- namespace IndexedPSpPm + +-- variable {I α V : Type*} + +-- /-- Lift an indexed set of probability spaces to an indexed set of probability space-permission +-- pairs, via pointwise lifting -/ +-- def liftProb (μ : I → ProbabilitySpace (α → V)) : IndexedPSpPm I α V := +-- fun i => PSpPm.liftProb (μ i) + +-- instance : FunLike (IndexedPSpPm I α V) I (PSpPm α V) where +-- coe := fun x => x +-- coe_injective' := by intro x y h; simp [h] + +-- noncomputable instance [Nonempty V] : OrderedUnitalResourceAlgebra (IndexedPSpPm I α V) := +-- inferInstanceAs (OrderedUnitalResourceAlgebra (I → PSpPm α V)) + +-- end IndexedPSpPm + +-- /-- A hyper-assertion is an upward closed predicate on `IndexedPSpPm I α V`. + +-- We re-use the existing Lean structure `UpperSet`, so an element of this type has: + +-- - a carrier (a `Set`, equivalent to a predicate) +-- - a proof that the set is upward closed -/ +-- abbrev HyperAssertion (I α V : Type*) := UpperSet (IndexedPSpPm I α V) +-- -- {ha : IndexedPSpPm I α V → Prop // ∀ x y, x ≤ y → ha x → ha y} + +-- /-- `FunLike` instance for `HyperAssertion` so that we can write `P a` instead of `a ∈ P` -/ +-- instance {I α V : Type*} : FunLike (HyperAssertion I α V) (IndexedPSpPm I α V) Prop where +-- coe := fun P => P.carrier +-- coe_injective' := by intro P Q h; aesop + +-- namespace HyperAssertion + +-- variable {I α V : Type*} + +-- /-- The predicate underlying a hyper-assertion -/ +-- def pred (P : HyperAssertion I α V) : IndexedPSpPm I α V → Prop := (· ∈ P.carrier) + +-- /-- A hyper-assertion `P` is irrelevant for a finite set of indices `J` if it is entailed by the set +-- of all probability spaces that are compatible with the permission at each index. + +-- Note that there may be multiple such `J`. -/ +-- def isIrrelevant [DecidableEq I] [Fintype I] (J : Set I) (P : HyperAssertion I α V) : Prop := +-- ∀ a, (∃ a' : IndexedPSpPm I α V, +-- -- The paper writes `a = a' \ J`, but it's not clear what this operation is (should there be a +-- -- "default" value for all unused indices?) +-- valid a' ∧ (a = a') ∧ P a') → P a + +-- /-- The relevant indices `idx(P)` of a hyper-assertion `P` is the smallest subset of `I` whose +-- complement is irrelevant for `P`. -/ +-- def relevantIndices [DecidableEq I] [Fintype I] (P : HyperAssertion I α V) : Set I := +-- sInf (setOf (fun J : Set I => isIrrelevant J.compl P)) + +-- /-- The empty hyper-assertion -/ +-- def emp : HyperAssertion I α V := ⟨setOf (fun _ => False), fun _ _ _ h => h⟩ + +-- /-- The entailment relation on hyper-assertions: +-- `P ⊢ Q` if for any valid resource `a`, if `P` holds for `a`, then `Q` holds for `a`. -/ +-- def entails (P Q : HyperAssertion I α V) : Prop := +-- ∀ a, ✓ a → P a → Q a + +-- /-- Equivalence between hyper-assertions is defined as mutual entailment, denoted `P ⊣⊢ Q` -/ +-- def equiv (P Q : HyperAssertion I α V) : Prop := +-- entails P Q ∧ entails Q P + +-- /-- Lift a proposition to a hyper-assertion, `⌜ φ ⌝` -/ +-- def pure (φ : Prop) : HyperAssertion I α V := ⟨setOf (fun _ => φ), fun _ _ _ ha => ha⟩ + +-- alias lift := pure + +-- /-- Conjunction of two hyper-assertions, defined pointwise -/ +-- def and (P Q : HyperAssertion I α V) : HyperAssertion I α V := +-- ⟨setOf (fun a => P a ∧ Q a), fun _ _ hab ⟨hP, hQ⟩ => ⟨P.upper' hab hP, Q.upper' hab hQ⟩⟩ + +-- /-- Disjunction of two hyper-assertions, defined pointwise -/ +-- def or (P Q : HyperAssertion I α V) : HyperAssertion I α V := +-- ⟨setOf (fun a => P a ∨ Q a), fun _ _ hab h => match h with +-- | Or.inl hP => Or.inl (P.upper' hab hP) +-- | Or.inr hQ => Or.inr (Q.upper' hab hQ)⟩ + +-- -- Note: don't think we can define implication `→` or negation `¬`, since upward closedness gives the +-- -- wrong direction + +-- -- Not sure how to define these either +-- def sForall (P : HyperAssertion I α V → Prop) : HyperAssertion I α V := sorry +-- -- ⟨setOf (fun a => P (fun b => a ≤ b)), fun _ _ hab h b hb => P.upper' (hab b) hb⟩ + +-- def sExists (P : HyperAssertion I α V → Prop) : HyperAssertion I α V := sorry + +-- /-- Existential quantification over hyper-assertions -/ +-- def «exists» {β : Sort*} (P : β → HyperAssertion I α V) : HyperAssertion I α V := +-- ⟨setOf (fun a => ∃ b, P b a), fun _ _ hab ⟨b, h⟩ => ⟨b, (P b).upper' hab h⟩⟩ + +-- /-- Universal quantification over hyper-assertions -/ +-- def «forall» {β : Sort*} (P : β → HyperAssertion I α V) : HyperAssertion I α V := +-- ⟨setOf (fun a => ∀ b, P b a), fun _ _ hab h b => (P b).upper' hab (h b)⟩ + +-- /-- Separating conjunction of two hyper-assertions, `P ∗ Q`, defined for every `a` as the existence of elements +-- `b₁ ∈ P` and `b₂ ∈ Q` respectively, such that `b₁ * b₂ ≤ a`. -/ +-- def sep (P : HyperAssertion I α V) (Q : HyperAssertion I α V) : HyperAssertion I α V := +-- ⟨setOf (fun a => ∀ b, valid (a * b) → P b → Q (a * b)), fun a a' ha h b hb₁ hb₂ => by +-- simp_all; sorry⟩ + +-- /-- Separating implication of two hyper-assertions, `P -∗ Q`, defined for every `a` as the existence of elements +-- `b₁ ∈ P` and `b₂ ∈ Q` respectively, such that `b₁ * b₂ ≤ a`. -/ +-- def wand (P : HyperAssertion I α V) (Q : HyperAssertion I α V) : HyperAssertion I α V := +-- ⟨setOf (fun a => ∃ b₁ b₂, (b₁ * b₂) ≤ a ∧ b₁ ∈ P ∧ b₂ ∈ Q), +-- fun _ _ hab ⟨b₁, b₂, h, hb₁, hb₂⟩ => ⟨b₁, b₂, le_trans h hab, hb₁, hb₂⟩⟩ + +-- open Iris.BI in +-- instance : BIBase (HyperAssertion I α V) where +-- Entails := entails +-- emp := emp +-- pure := pure +-- and := and +-- or := or +-- imp := sorry +-- sForall := sorry +-- sExists := sorry +-- sep := sep +-- wand := wand +-- persistently := sorry +-- later := sorry + +-- section Ownership + +-- /-! ### Ownership-related hyper-assertions -/ + +-- /-- Ownership of a resource `b : IndexedPSpPm I α V`, defined for every `a` as the predicate `b ≤ a`. -/ +-- def own (b : IndexedPSpPm I α V) : HyperAssertion I α V := +-- ⟨setOf (fun a => b ≤ a), fun _ _ hab ha => le_trans ha hab⟩ + +-- /-- Ownership of an indexed tuple of probability spaces `P : I → PSp (α → V)` and permissions +-- `p : I → Permission α`, defined as the existence of compatibility proofs `h` for each element, such +-- that we have ownership of the overall tuple (with the compatibility proof). -/ +-- def ownIndexedTuple (P : I → ProbabilitySpace (α → V)) (p : I → Permission α) : HyperAssertion I α V := +-- «exists» (fun h : ∀ i, (P i).compatiblePerm (p i) => own (fun i => ⟨⟨P i, p i⟩, h i⟩)) + +-- variable [DecidableEq I] [Nonempty V] {β : Type*} [MeasurableSpace β] + +-- /-- Ownership of an indexed probability spaces `P : I → PSp (α → V)`, defined as the +-- existence of a compatible indexed permission `p : I → Permission α` such that we have +-- ownership of the overall tuple. -/ +-- def ownIndexedProb (P : I → ProbabilitySpace (α → V)) : HyperAssertion I α V := +-- «exists» (fun p : I → Permission α => ownIndexedTuple P p) + +-- /-- The hyper-assertion `E⟨i⟩ ∼ μ`, for some expression `E : (α → V) → β`, index `i : I`, +-- and discrete probability distribution `μ : PMF β`, is defined as +-- `∃ P, Own P ∗ lift ((E⟨i⟩ is a.e. measurable for (P i)) ∧ μ = (P i).μ.map E)`-/ +-- def assertSampledFrom (i : I) (E : (α → V) → β) (μ : PMF β) : HyperAssertion I α V := +-- «exists» (fun P : I → ProbabilitySpace (α → V) => +-- sep (ownIndexedProb P) +-- (lift (@AEMeasurable _ _ _ (P i).σAlg E (P i).μ ∧ μ.toMeasure = @Measure.map _ _ (P i).σAlg _ E (P i).μ))) + +-- /-- Assertion that the expected value of `E` at index `i` is `ev` -/ +-- def assertExpectation [TopologicalSpace β] [AddCommMonoid β] [SMul ENNReal β] +-- (i : I) (E : (α → V) → β) (ev : β) : HyperAssertion I α V := +-- «exists» (fun μ => sep (assertSampledFrom i E μ) (lift (ev = ∑' b, (μ b) • b))) + +-- /-- Assertion that the probability of a Boolean-valued expression `E` at index `i` is `prob` -/ +-- def assertProbability (i : I) (E : (α → V) → Bool) (prob : ENNReal) : HyperAssertion I α V := +-- «exists» (fun μ => sep (assertSampledFrom i E μ) (lift (prob = μ true))) + +-- /-- Assertion that `E` is true almost surely -/ +-- noncomputable def assertTrue (i : I) (E : (α → V) → Bool) : HyperAssertion I α V := +-- assertSampledFrom i E (PMF.pure true) + +-- /-- Assertion that we own `E` (but its distribution is not known) -/ +-- def assertOwn (i : I) (E : (α → V) → β) : HyperAssertion I α V := +-- «exists» (fun μ => assertSampledFrom i E μ) + +-- /-- Assertion that the variable `x : α` at index `i` has permission `q : ℚ≥0` -/ +-- def assertPermissionVar (i : I) (x : α) (q : ℚ≥0) : HyperAssertion I α V := +-- «exists» (fun Pp : IndexedPSpPm I α V => sep (own Pp) (lift ((Pp i).1.2 x = q))) + +-- /-- Assertion that a hyper-assertion `P` holds alongside an ownership of an indexed permission `p` + +-- This is useful when defining pre-conditions at the beginning of the program (where we have a +-- precondition `P` and all variables have permission `1`) -/ +-- def assertPermission (P : HyperAssertion I α V) (p : I → Permission α) : HyperAssertion I α V := +-- and P <| +-- «exists» (fun compatP : {P : I → ProbabilitySpace (α → V) // ∀ i, (P i).compatiblePerm (p i)} => +-- own (fun i => ⟨⟨compatP.1 i, p i⟩, compatP.2 i⟩)) + +-- end Ownership + +-- def isPermissionAbstract (X : Set (I × α)) (P : HyperAssertion I α V) : Prop := sorry +-- -- ∀ Pp : IndexedPSpPm I α V, ∀ q : ℚ≥0, ∀ n : ℕ+, P Pp ≤ P → ∃ Pp' : IndexedPSpPm I α V, Pp' ≤ P ∧ Pp = Pp' ∧ True + +-- /-- The joint conditioning modality -/ +-- def jointCondition {β : Type*} [MeasurableSpace β] [MeasurableSpace V] (μ : PMF β) (K : β → HyperAssertion I α V) : +-- HyperAssertion I α V := sorry +-- -- «exists» (fun P : I → ProbabilitySpace (α → V) => sorry) +-- -- ⟨setOf (fun a => ∃ P : I → ProbabilitySpace (α → V), +-- -- ∃ p : I → Permission α, +-- -- ∃ h : ∀ i, (P i).compatiblePerm (p i), +-- -- ∃ κ : (i : I) → β → @Measure (α → V) (P i).σAlg, +-- -- (fun i => ⟨⟨P i, p i⟩, h i⟩ : IndexedPSpPm I α V) ≤ a ∧ ∀ i, (P i).μ = μ.toMeasure.bind (κ i) ∧ +-- -- ∀ v ∈ μ.support, K v (fun j => ⟨⟨@ProbabilitySpace.mk _ (P j).σAlg (κ j v) sorry, p j⟩, h j⟩)), by sorry⟩ + +-- notation "𝑪_" => jointCondition + +-- /-- The lifting of a relation `R : Set (s → V)`, where `s : Set (I × α)`, to a hyper-assertion -/ +-- noncomputable def liftRelation [DecidableEq V] [MeasurableSpace V] +-- (s : Set (I × α)) (R : Set (s → V)) : HyperAssertion I α V := +-- «exists» (fun μ : PMF (s → V) => +-- sep (lift (∑' x : R, μ x = 1)) +-- (𝑪_ μ (fun v : s → V => +-- «forall» (fun x : s => assertTrue x.1.1 (fun y => v x = y x.1.2))))) + +-- /-- Weakest precondition of a program -/ +-- def wp (t : IndexedPSpPm I α V → IndexedPSpPm I α V) (Q : HyperAssertion I α V) : HyperAssertion I α V := +-- ⟨setOf (fun a => ∀ μ₀ c, (a * c) ≤ IndexedPSpPm.liftProb μ₀ → +-- ∃ b, (b * c) ≤ t (IndexedPSpPm.liftProb μ₀) ∧ Q b), by sorry⟩ + +-- section ProgramLogic + +-- /-! ### The program logic of Bluebell -/ + +-- -- TODO: we also need to state the regular rules of separation logic, so stuff like +-- theorem and_comm {P Q : HyperAssertion I α V} : P ∧ Q ⊣⊢ Q ∧ P := sorry + +-- /-- If `P` and `Q` affect disjoint sets of indices, then `P ∧ Q` entails `P ∗ Q` -/ +-- theorem sep_of_and [DecidableEq I] [Fintype I] {P Q : HyperAssertion I α V} +-- (h : relevantIndices P ∩ relevantIndices Q = ∅) : (P ∧ Q) ⊢ (P ∗ Q) := by +-- sorry + +-- /-- If `E⟨i⟩` is sampled from both `μ` and `μ'`, then `⌜ μ = μ' ⌝` holds as a proposition -/ +-- theorem sampledFrom_inj {β : Type*} [MeasurableSpace β] {i : I} {E : (α → V) → β} {μ μ' : PMF β} : +-- (assertSampledFrom i E μ) ∧ (assertSampledFrom i E μ') ⊢ ⌜ μ = μ' ⌝ := by +-- sorry + +-- /-- `E₁⟨i⟩` and `E₂⟨i⟩` are both true if and only if `E₁⟨i⟩ ∧ E₂⟨i⟩` is true -/ +-- theorem sep_assertTrue_iff {i : I} {E₁ E₂ : (α → V) → Bool} : +-- (assertTrue i E₁) ∗ (assertTrue i E₂) ⊣⊢ assertTrue i (fun x => E₁ x ∧ E₂ x) := by +-- sorry + +-- /-- If `pabs(𝑃, pvar(𝐸⟨𝑖⟩))` (need to define this), then `assertTrue i E ∧ P` entails `assertTrue i E ∗ P` -/ +-- theorem sep_of_and_assertTrue {i : I} {E : (α → V) → Bool} {P : HyperAssertion I α V} +-- (h : True) : (assertTrue i E) ∗ P ⊢ (assertTrue i E) ∧ P := by +-- sorry + +-- /-- Sampling hyper-assertions `(E₁⟨i⟩, E₂⟨i⟩) ∼ (μ₁, μ₂)` for a product space can be split +-- into sampling `E₁⟨i⟩ ∼ μ₁` and `E₂⟨i⟩ ∼ μ₂` -/ +-- theorem sampledFrom_prod {β₁ β₂ : Type _} [MeasurableSpace β₁] [MeasurableSpace β₂] {i : I} +-- (E₁ : (α → V) → β₁) (E₂ : (α → V) → β₂) (μ₁ : PMF β₁) (μ₂ : PMF β₂) : +-- assertSampledFrom i (fun x => (E₁ x, E₂ x)) (Prod.mk <$> μ₁ <*> μ₂) ⊢ +-- (assertSampledFrom i E₁ μ₁) ∗ (assertSampledFrom i E₂ μ₂) := by +-- sorry + +-- section JointConditioning + +-- variable {β : Type*} [MeasurableSpace β] {μ : PMF β} {K K₁ K₂ : β → HyperAssertion I α V} +-- [MeasurableSpace V] + +-- theorem C_conseq (h : ∀ v, K₁ v ⊢ K₂ v) : 𝑪_ μ K₁ ⊢ 𝑪_ μ K₂ := by +-- sorry + +-- theorem C_frame {P : HyperAssertion I α V} : P ∗ 𝑪_ μ K ⊢ 𝑪_ μ (fun v => sep P (K v)) := by +-- sorry + +-- theorem C_unit_left [Countable β] [MeasurableSingletonClass β] {v₀ : β} : +-- 𝑪_ (Measure.dirac v₀).toPMF K ⊣⊢ K v₀ := by +-- sorry + +-- theorem C_unit_right [DecidableEq β] {i : I} {E : (α → V) → β} {μ : PMF β} : +-- assertSampledFrom i E μ ⊣⊢ 𝑪_ μ (fun v => assertTrue i (fun x => E x = v)) := by +-- sorry + +-- theorem C_assoc {β₁ β₂ : Type _} [MeasurableSpace β₁] [MeasurableSpace β₂] +-- {μ : PMF β₁} {κ : β₁ → PMF β₂} {K : β₁ × β₂ → HyperAssertion I α V} : +-- 𝑪_ μ (fun v => 𝑪_ (κ v) (fun w => K (v, w))) ⊢ +-- 𝑪_ (do let v ← μ; let w ← κ v; return (v, w)) K := by +-- sorry + +-- theorem C_unassoc {β₁ β₂ : Type _} [MeasurableSpace β₁] [MeasurableSpace β₂] +-- {μ : PMF β₁} {κ : β₁ → PMF β₂} {K : β₂ → HyperAssertion I α V} : +-- 𝑪_ (μ.bind κ) (fun w => K w) ⊢ 𝑪_ μ (fun v => 𝑪_ (κ v) (fun w => K w)) := by +-- sorry + +-- theorem C_and [DecidableEq I] [Fintype I] (h : ∀ v, relevantIndices (K₁ v) ∩ relevantIndices (K₂ v) = ∅) : +-- 𝑪_ μ K₁ ∧ 𝑪_ μ K₂ ⊢ 𝑪_ μ (fun v => and (K₁ v) (K₂ v)) := by +-- sorry + +-- /-- Also requires that the measurable space on `β` is the top one -/ +-- theorem C_exists {γ : Type*} {Q : β × γ → HyperAssertion I α V} : +-- 𝑪_ μ (fun v => ∃ x, Q (v, x)) ⊢ ∃ f : β → γ, 𝑪_ μ (fun v => Q (v, f v)) := by +-- sorry + +-- theorem C_forall {γ : Type*} {Q : β × γ → HyperAssertion I α V} : +-- 𝑪_ μ (fun v => «forall» (fun x => Q (v, x))) ⊢ ∀ x, 𝑪_ μ (fun v => Q (v, x)) := by +-- sorry + +-- theorem C_transfer {β' : Type*} [MeasurableSpace β'] {μ' : PMF β'} (f : μ'.support ≃ μ.support) +-- (h : ∀ b, (hb : b ∈ μ'.support) → μ' b = μ (f ⟨b, hb⟩).1) : +-- 𝑪_ μ K ⊢ 𝑪_ μ' (fun b => K (f ⟨b, sorry⟩)) := by +-- sorry + +-- theorem C_sep_assertTrue {i : I} {E : (α → V) → Bool} : +-- 𝑪_ μ (fun v => sep (K v) (assertTrue i E)) ⊢ assertTrue i E ∗ 𝑪_ μ K := by +-- sorry + +-- theorem C_pure {s : Set β} : +-- ⌜ ∑' x : s, μ x = 1 ⌝ ∗ 𝑪_ μ K ⊣⊢ 𝑪_ μ (fun v => sep (pure (v ∈ s)) (K v)) := by +-- sorry + +-- end JointConditioning + +-- section WeakestPrecondition + +-- variable {I α V : Type*} [MeasurableSpace V] {t t₁ t₂ : IndexedPSpPm I α V → IndexedPSpPm I α V} +-- {P Q Q' Q₁ Q₂ : HyperAssertion I α V} + +-- theorem wp_conseq (h : Q ⊢ Q') : (wp t Q) ⊢ (wp t Q') := by sorry + +-- theorem wp_frame : P ∗ (wp t Q) ⊢ (wp t (sep P Q)) := by sorry + +-- theorem wp_comp : (wp t₁ (wp t₂ Q)) ⊣⊢ (wp (t₁ ∘ t₂) Q) := by sorry + +-- -- TODO: need to express `|t|`, the set of relevant indices of a program `t`, and `t₁ + t₂`, the +-- -- combined execution of `t₁` and `t₂` if they affect disjoint sets of indices (so we must model `t` +-- -- as an AST which is then interpreted into a function) +-- -- Required conditions: `(h1 : relevantIndices Q₁ ∩ |t₂| ⊆ |t₁|) (h2 : relevantIndices Q₂ ∩ |t₁| ⊆ |t₂|)` +-- theorem wp_conj : (wp t₁ Q₁) ∧ (wp t₂ Q₂) ⊣⊢ (wp (sorry) (and Q₁ Q₂)) := by sorry + +-- -- TODO: what is `own_α` exactly (`own_𝕏` in the paper)? +-- theorem C_wp_swap {β : Type*} [MeasurableSpace β] {μ : PMF β} {K : β → HyperAssertion I α V} : +-- 𝑪_ μ (fun v => wp t (K v)) ∧ sorry ⊢ wp t (𝑪_ μ K) := by sorry + +-- -- Add wp rules for the program syntax + +-- end WeakestPrecondition + +-- end ProgramLogic + +-- end HyperAssertion diff --git a/src/Bluebell/ProbabilityTheory/Coupling.lean b/src/Bluebell/ProbabilityTheory/Coupling.lean new file mode 100644 index 000000000..95c680711 --- /dev/null +++ b/src/Bluebell/ProbabilityTheory/Coupling.lean @@ -0,0 +1,118 @@ +/- +Copyright (c) 2025 Verified zkEVM contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Quang Dao +-/ + +import Mathlib.Probability.ProbabilityMassFunction.Constructions + +/-! +# Coupling for probability distributions + +-/ + +universe u + +noncomputable section + +namespace PMF + +variable {α β : Type*} + +class IsCoupling (c : PMF (α × β)) (p : PMF α) (q : PMF β) where + map_fst : c.map Prod.fst = p + map_snd : c.map Prod.snd = q + +def Coupling (p : PMF α) (q : PMF β) := + { c : PMF (α × β) // IsCoupling c p q } + +end PMF + +/-- Subprobability distribution. -/ +@[reducible] +def SPMF : Type u → Type u := OptionT PMF + +namespace SPMF + +variable {α β : Type u} + +instance : Monad SPMF := inferInstance + +instance : LawfulMonad SPMF := inferInstance + +-- instance : Alternative SPMF := inferInstance + +instance : FunLike (SPMF α) (Option α) ENNReal := + inferInstanceAs (FunLike (PMF (Option α)) (Option α) ENNReal) + +-- instance : MonadLift PMF SPMF := inferInstance + +-- instance : LawfulMonadLift PMF SPMF := inferInstance + +-- instance : LawfulFailure SPMF := inferInstance + +theorem pure_eq_pmf_pure {a : α} : (pure a : SPMF α) = PMF.pure a := by + simp [pure, liftM, OptionT.pure, monadLift, MonadLift.monadLift, OptionT.lift, PMF.instMonad] + +theorem bind_eq_pmf_bind {p : SPMF α} {f : α → SPMF β} : + (p >>= f) = PMF.bind p (fun a => match a with | some a' => f a' | none => PMF.pure none) := by + simp [bind, liftM, OptionT.bind, monadLift, MonadLift.monadLift, OptionT.lift, + PMF.instMonad, OptionT.mk] + rfl + +@[ext] +class IsCoupling (c : SPMF (α × β)) (p : SPMF α) (q : SPMF β) : Prop where + map_fst : Prod.fst <$> c = p + map_snd : Prod.snd <$> c = q + +def Coupling (p : SPMF α) (q : SPMF β) := + { c : SPMF (α × β) // IsCoupling c p q } + +-- Interaction between `Coupling` and `pure` / `bind` + +example (f g : α → β) (h : f = g) : ∀ x, f x = g x := by exact fun x ↦ congrFun h x + +/-- The coupling of two pure values must be the pure pair of those values -/ +theorem IsCoupling.pure_iff {α β : Type u} {a : α} {b : β} {c : SPMF (α × β)} : + IsCoupling c (pure a) (pure b) ↔ c = pure (a, b) := by + constructor + · intro ⟨h1, h2⟩ + simp [pure_eq_pmf_pure, liftM, monadLift, OptionT.instMonadLift, OptionT.lift, OptionT.mk] at h1 h2 + have : (x : Option α) → (Prod.fst <$> c) x = (some <$> PMF.pure a) x := by + rw [h1]; intro x; congr + sorry + · intro h; constructor <;> simp [h, ← liftM_map] + +theorem IsCoupling.none_iff {α β : Type u} {c : SPMF (α × β)} : + IsCoupling c (failure : SPMF α) (failure : SPMF β) ↔ c = failure := by + simp [failure] + constructor + · intro h; sorry + · intro h; constructor <;> simp [h] <;> sorry + +/-- Main theorem about coupling and bind operations -/ +theorem IsCoupling.bind {α₁ α₂ β₁ β₂ : Type u} + {p : SPMF α₁} {q : SPMF α₂} {f : α₁ → SPMF β₁} {g : α₂ → SPMF β₂} + (c : Coupling p q) (d : (a₁ : α₁) → (a₂ : α₂) → SPMF (β₁ × β₂)) + (h : ∀ (a₁ : α₁) (a₂ : α₂), c.1.1 (some (a₁, a₂)) ≠ 0 → IsCoupling (d a₁ a₂) (f a₁) (g a₂)) : + IsCoupling (c.1 >>= λ (p : α₁ × α₂) => d p.1 p.2) (p >>= f) (q >>= g) := by + obtain ⟨hc₁, hc₂⟩ := c.2 + constructor + · simp [← hc₁]; congr; funext ⟨a₁, a₂⟩; have := h a₁ a₂; sorry + · simp [← hc₂]; sorry + +/-- Existential version of `IsCoupling.bind` -/ +theorem IsCoupling.exists_bind {α₁ α₂ β₁ β₂ : Type u} + {p : SPMF α₁} {q : SPMF α₂} {f : α₁ → SPMF β₁} {g : α₂ → SPMF β₂} + (c : Coupling p q) + (h : ∀ (a₁ : α₁) (a₂ : α₂), ∃ (d : SPMF (β₁ × β₂)), IsCoupling d (f a₁) (g a₂)) : + ∃ (d : SPMF (β₁ × β₂)), IsCoupling d (p >>= f) (q >>= g) := + let d : (a₁ : α₁) → (a₂ : α₂) → SPMF (β₁ × β₂) := + fun a₁ a₂ => Classical.choose (h a₁ a₂) + let hd : ∀ (a₁ : α₁) (a₂ : α₂), c.1.1 (some (a₁, a₂)) ≠ 0 → IsCoupling (d a₁ a₂) (f a₁) (g a₂) := + fun a₁ a₂ _ => Classical.choose_spec (h a₁ a₂) + ⟨c.1 >>= λ (p : α₁ × α₂) => d p.1 p.2, IsCoupling.bind c d hd⟩ + +end SPMF + +end diff --git a/src/Bluebell/ProbabilityTheory/IndepProduct.lean b/src/Bluebell/ProbabilityTheory/IndepProduct.lean new file mode 100644 index 000000000..e30b84c9f --- /dev/null +++ b/src/Bluebell/ProbabilityTheory/IndepProduct.lean @@ -0,0 +1,129 @@ +import Mathlib.Probability.Independence.Conditional +import Mathlib.Probability.ProbabilityMassFunction.Basic + +/-! ## Independent product of probability measures -/ + +open ProbabilityTheory MeasureTheory + +alias MeasureTheory.MeasureSpace.σAlg := MeasureSpace.toMeasurableSpace +alias MeasureTheory.MeasureSpace.μ := MeasureSpace.volume + +variable {Ω : Type*} + +/-- We define `(ℱ, μ) ≤ (𝒢, ν)` if `ℱ ≤ 𝒢` and `μ` is the restriction of `ν` to `ℱ` -/ +instance : Preorder (MeasureSpace Ω) where + -- TODO: double-check if we are supposed to use `map` or `comap` + le m₁ m₂ := (m₁.σAlg ≤ m₂.σAlg) ∧ m₁.μ = (@Measure.map _ _ m₂.σAlg m₁.σAlg id m₂.μ) + le_refl m := by simp only [LE.le, imp_self, implies_true, Measure.map_id, and_self] + le_trans := by + rintro ⟨ℱ₁, μ₁⟩ ⟨ℱ₂, μ₂⟩ ⟨ℱ₃, μ₃⟩ ⟨hℱ₁₂, hμ₁₂⟩ ⟨hℱ₂₃, hμ₂₃⟩ + simp_all + refine ⟨le_trans hℱ₁₂ hℱ₂₃, ?_⟩ + · rw [Measure.map_map] <;> aesop + +/-- The sum of two measurable spaces on the same space `Ω` is the measurable space generated by the + union of the two spaces -/ +def MeasurableSpace.sum (m₁ : MeasurableSpace Ω) (m₂ : MeasurableSpace Ω) : MeasurableSpace Ω := + MeasurableSpace.generateFrom (MeasurableSet[m₁] ∪ MeasurableSet[m₂]) + +namespace ProbabilityTheory + +/-- A probability space is a `MeasureSpace` where the measure is a probability measure (i.e. has + total measure `1`) -/ +class ProbabilitySpace (Ω : Type*) extends MeasureSpace Ω where + [is_prob : IsProbabilityMeasure volume] + +def ProbabilitySpace.σAlg [P : ProbabilitySpace Ω] : MeasurableSpace Ω := + ProbabilitySpace.toMeasureSpace.toMeasurableSpace +def ProbabilitySpace.μ [P : ProbabilitySpace Ω] : Measure[P.σAlg] Ω := + ProbabilitySpace.toMeasureSpace.volume + +/-- A probability mass function, under some measurable space, induces a probability space -/ +noncomputable def ProbabilitySpace.ofPMF [MeasurableSpace Ω] (μ : PMF Ω) : ProbabilitySpace Ω := + { toMeasurableSpace := inferInstance, + volume := μ.toMeasure, + is_prob := PMF.toMeasure.isProbabilityMeasure μ } + +@[simp] +instance ProbabilitySpace.instProbabilityMeasure [P : ProbabilitySpace Ω] : + IsProbabilityMeasure (P.μ) := + ProbabilitySpace.is_prob + +@[simp] +lemma ProbabilitySpace.σAlg_apply [P : ProbabilitySpace Ω] : + P.σAlg = P.toMeasureSpace.toMeasurableSpace := rfl +@[simp] +lemma ProbabilitySpace.μ_apply [P : ProbabilitySpace Ω] : + P.μ = P.toMeasureSpace.volume := rfl + +/-- We define `(ℱ, μ) ≤ (𝒢, ν)` if `ℱ ≤ 𝒢` and `μ` is the restriction of `ν` to `ℱ` -/ +instance : Preorder (ProbabilitySpace Ω) where + le m₁ m₂ := (m₁.σAlg ≤ m₂.σAlg) ∧ m₁.μ = (@Measure.map _ _ m₂.σAlg m₁.σAlg id m₂.μ) + le_refl m := by simp only [LE.le, imp_self, implies_true, Measure.map_id, and_self] + le_trans := by + rintro ⟨ℱ₁, μ₁, _⟩ ⟨ℱ₂, μ₂, _⟩ ⟨ℱ₃, μ₃, _⟩ ⟨hℱ₁₂, hμ₁₂⟩ ⟨hℱ₂₃, hμ₂₃⟩ + simp_all + refine ⟨le_trans hℱ₁₂ hℱ₂₃, ?_⟩ + · rw [Measure.map_map] <;> aesop + +end ProbabilityTheory + +section IndependentProduct + +variable {m₁ : MeasurableSpace Ω} {m₂ : MeasurableSpace Ω} + +/-- An independent product of measures `μ₁` and `μ₂` (on measurable spaces `m₁` and `m₂`, + respectively) is a measure `μ` on the sum of `m₁` and `m₂` that satisfies the product formula -/ +@[ext] +class Measure.IndependentProduct (μ₁ : Measure[m₁] Ω) (μ₂ : Measure[m₂] Ω) where + μ : Measure[MeasurableSpace.sum m₁ m₂] Ω + inter_eq_prod {X Y} (hX : MeasurableSet[m₁] X) (hY : MeasurableSet[m₂] Y) : + μ (X ∩ Y) = μ₁ X * μ₂ Y + +/-- The independent product of two measures is unique, if it exists -/ +instance {μ₁ : Measure[m₁] Ω} {μ₂ : Measure[m₂] Ω} : Subsingleton (Measure.IndependentProduct μ₁ μ₂) := by + constructor + intro ⟨μ, hμ⟩ ⟨μ', hμ'⟩ + ext + simp + sorry + -- To prove this, [Li et al. 2023] requires the Dynkin π-λ theorem, which is + -- `MeasurableSpace.induction_on_inter`. + +#check IsPiSystem +#check MeasurableSpace.induction_on_inter + +noncomputable section + +/-- The partial operation of independent product on `MeasureSpace`s, when it exists -/ +def MeasureTheory.MeasureSpace.indepProduct (m₁ : MeasureSpace Ω) (m₂ : MeasureSpace Ω) : Option (MeasureSpace Ω) := by + classical + by_cases h : Nonempty (Measure.IndependentProduct m₁.2 m₂.2) + · exact some (@MeasureSpace.mk Ω (m₁.1.sum m₂.1) (Classical.choice h).μ) + · exact none + +/-- The partial operation of independent product on `ProbabilitySpace`s, when it exists -/ +def ProbabilityTheory.ProbabilitySpace.indepProduct (m₁ : ProbabilitySpace Ω) (m₂ : ProbabilitySpace Ω) : Option (ProbabilitySpace Ω) := by + classical + by_cases h : (m₁.toMeasureSpace.indepProduct m₂.toMeasureSpace).isSome + · exact some (@ProbabilitySpace.mk Ω ((m₁.toMeasureSpace.indepProduct m₂.toMeasureSpace).get h) (by + sorry)) + · exact none + +end + +end IndependentProduct + +#check MeasureSpace + +#check MeasureTheory.Measure.IsComplete + +/-- A set `s` is almost measurable with respect to a measure space `μ` if it is sandwiched between + two measurable sets that have the same measure -/ +def almostMeasurableSet [μ : MeasureSpace Ω] (s : Set Ω) := + ∃ t₁ t₂, MeasurableSet t₁ ∧ MeasurableSet t₂ ∧ t₁ ⊆ s ∧ s ⊆ t₂ ∧ μ.volume t₁ = μ.volume t₂ + +-- I think this is the same as `toMeasurable`, and also `almost measurable` functions in the paper +-- should coincide with the `AEMeasurable` class + +#check AEMeasurable From f3bf259d530e93e46055d20f20de63b57ef20c65 Mon Sep 17 00:00:00 2001 From: Quang Dao Date: Thu, 4 Sep 2025 18:48:58 -0600 Subject: [PATCH 08/44] feat: add original paper (#3) * add bluebell paper * update gitignore --- .gitignore | 14 + paper/ACM-Reference-Format.bst | 3081 +++++++ paper/Bluebell.pdf | Bin 0 -> 1724320 bytes paper/acmart.cls | 3567 +++++++++ paper/comment.cut | 22 + paper/paper.pdf | Bin 0 -> 1277987 bytes paper/paper.tex | 13226 +++++++++++++++++++++++++++++++ paper/style/appendix.sty | 96 + paper/style/notation.sty | 1576 ++++ 9 files changed, 21582 insertions(+) create mode 100644 paper/ACM-Reference-Format.bst create mode 100644 paper/Bluebell.pdf create mode 100644 paper/acmart.cls create mode 100644 paper/comment.cut create mode 100644 paper/paper.pdf create mode 100644 paper/paper.tex create mode 100644 paper/style/appendix.sty create mode 100644 paper/style/notation.sty diff --git a/.gitignore b/.gitignore index bfb30ec8c..09c0d156f 100644 --- a/.gitignore +++ b/.gitignore @@ -1 +1,15 @@ /.lake +/.notes +/.claude +/.cursor + +# LaTeX compilation files +*.aux +*.bbl +*.blg +*.fdb_latexmk +*.fls +*.log +*.out +*.synctex.gz +*.synctex(busy) diff --git a/paper/ACM-Reference-Format.bst b/paper/ACM-Reference-Format.bst new file mode 100644 index 000000000..c47cb4c0f --- /dev/null +++ b/paper/ACM-Reference-Format.bst @@ -0,0 +1,3081 @@ +%%% -*-BibTeX-*- +%%% ==================================================================== +%%% @BibTeX-style-file{ +%%% author = "Nelson H. F. Beebe, Boris Veytsman and Gerald Murray", +%%% version = "2.1", +%%% acmart-version = "1.90", +%%% date = "Mar 26 2023", +%%% filename = "ACM-Reference-Format.bst", +%%% email = "borisv@lk.net, boris@varphi.com", +%%% codetable = "ISO/ASCII", +%%% keywords = "ACM Transactions bibliography style; BibTeX", +%%% license = "public domain", +%%% supported = "yes", +%%% abstract = "", +%%% } +%%% ==================================================================== + +%%% Revision history: see source in git + +ENTRY + { address + advisor + archiveprefix + author + booktitle + chapter + city + date + edition + editor + eprint + eprinttype + eprintclass + howpublished + institution + journal + key + location + month + note + number + organization + pages + primaryclass + publisher + school + series + title + type + volume + year + % New keys recognized + issue % UTAH: used in, e.g., ACM SIGSAM Bulletin and ACM Communications in Computer Algebra + articleno + eid + day % UTAH: needed for newspapers, weeklies, bi-weeklies + doi % UTAH + url % UTAH + bookpages % UTAH + numpages + lastaccessed % UTAH: used only for @Misc{...} + coden % UTAH + isbn % UTAH + isbn-13 % UTAH + issn % UTAH + lccn % UTAH + distinctURL % whether to print url if doi is present + } + {} + { label.year extra.label sort.year sort.label basic.label.year} + +INTEGERS { output.state before.all mid.sentence after.sentence after.block } + +INTEGERS { show-isbn-10-and-13 } % initialized below in begin.bib + +INTEGERS { nameptr namesleft numnames } + +INTEGERS { multiresult } + +INTEGERS { len } + +INTEGERS { last.extra.num } + +STRINGS { s t t.org u } + +STRINGS { last.label next.extra } + +STRINGS { p1 p2 p3 page.count } + + +FUNCTION { not } +{ + { #0 } + { #1 } + if$ +} + +FUNCTION { and } +{ + 'skip$ + { pop$ #0 } + if$ +} + +FUNCTION { or } +{ + { pop$ #1 } + 'skip$ + if$ +} + + +FUNCTION { dump.stack.1 } +{ + duplicate$ "STACK[top] = [" swap$ * "]" * warning$ +} + +FUNCTION { dump.stack.2 } +{ + duplicate$ "STACK[top ] = [" swap$ * "]" * warning$ + swap$ + duplicate$ "STACK[top-1] = [" swap$ * "]" * warning$ + swap$ +} + +FUNCTION { empty.or.unknown } +{ + %% Examine the top stack entry, and push 1 if it is empty, or + %% consists only of whitespace, or is a string beginning with two + %% queries (??), and otherwise, push 0. + %% + %% This function provides a replacement for empty$, with the + %% convenient feature that unknown values marked by two leading + %% queries are treated the same as missing values, and thus, do not + %% appear in the output .bbl file, and yet, their presence in .bib + %% file(s) serves to mark values which are temporarily missing, but + %% are expected to be filled in eventually once more data is + %% obtained. The TeX User Group and BibNet bibliography archives + %% make extensive use of this practice. + %% + %% An empty string cannot serve the same purpose, because just as in + %% statistics data processing, an unknown value is not the same as an + %% empty value. + %% + %% At entry: stack = ... top:[string] + %% At exit: stack = ... top:[0 or 1] + + duplicate$ empty$ + { pop$ #1 } + { #1 #2 substring$ "??" = } + if$ +} + +FUNCTION { empty.or.zero } +{ + %% Examine the top entry and push 1 if it is empty, or is zero + duplicate$ empty$ + { pop$ #1 } + { "0" = } + if$ +} + + +FUNCTION { writeln } +{ + %% In BibTeX style files, the sequences + %% + %% ... "one" "two" output + %% ... "one" "two" output.xxx + %% + %% ship "one" to the output file, possibly following by punctuation, + %% leaving the stack with + %% + %% ... "two" + %% + %% There is thus a one-string lag in output processing that must be + %% carefully handled to avoid duplicating a string in the output + %% file. Unless otherwise noted, all output.xxx functions leave + %% just one new string on the stack, and that model should be born + %% in mind when reading or writing function code. + %% + %% BibTeX's asynchronous buffering of output from strings from the + %% stack is confusing because newline$ bypasses the buffer. It + %% would have been so much easier for newline to be a character + %% rather than a state of the output-in-progress. + %% + %% The documentation in btxhak.dvi is WRONG: it says + %% + %% newline$ Writes onto the bbl file what's accumulated in the + %% output buffer. It writes a blank line if and only + %% if the output buffer is empty. Since write$ does + %% reasonable line breaking, you should use this + %% function only when you want a blank line or an + %% explicit line break. + %% + %% write$ Pops the top (string) literal and writes it on the + %% output buffer (which will result in stuff being + %% written onto the bbl file when the buffer fills + %% up). + %% + %% Examination of the BibTeX source code shows that write$ does + %% indeed behave as claimed, but newline$ sends a newline character + %% directly to the output file, leaving the stack unchanged. The + %% first line "Writes onto ... buffer." is therefore wrong. + %% + %% The original BibTeX style files almost always use "write$ newline$" + %% in that order, so it makes sense to hide that pair in a private + %% function like this one, named after a statement in Pascal, + %% the programming language embedded in the BibTeX Web program. + + write$ % output top-of-stack string + newline$ % immediate write of newline (not via stack) +} + +FUNCTION { init.state.consts } +{ + #0 'before.all := + #1 'mid.sentence := + #2 'after.sentence := + #3 'after.block := +} + +FUNCTION { output.nonnull } +{ % Stack in: ... R S T Stack out: ... R T File out: S + 's := + output.state mid.sentence = + { + ", " * write$ + } + { + output.state after.block = + { + add.period$ writeln + "\newblock " write$ + } + { + output.state before.all = + { + write$ + } + { + add.period$ " " * write$ + } + if$ + } + if$ + mid.sentence 'output.state := + } + if$ + s +} + +FUNCTION { output.nonnull.dot.space } +{ % Stack in: ... R S T Stack out: ... R T File out: S + 's := + output.state mid.sentence = % { ". " * write$ } + { + ". " * write$ + } + { + output.state after.block = + { + add.period$ writeln "\newblock " write$ + } + { + output.state before.all = + { + write$ + } + { + add.period$ " " * write$ + } + if$ + } + if$ + mid.sentence 'output.state := + } + if$ + s +} + +FUNCTION { output.nonnull.remove } +{ % Stack in: ... R S T Stack out: ... R T File out: S + 's := + output.state mid.sentence = + { + " " * write$ + } + { + output.state after.block = + { + add.period$ writeln "\newblock " write$ + } + { + output.state before.all = + { + write$ + } + { + add.period$ " " * write$ + } + if$ + } + if$ + mid.sentence 'output.state := + } + if$ + s +} + +FUNCTION { output.nonnull.removenospace } +{ % Stack in: ... R S T Stack out: ... R T File out: S + 's := + output.state mid.sentence = + { + "" * write$ + } + { + output.state after.block = + { + add.period$ writeln "\newblock " write$ + } + { + output.state before.all = + { + write$ + } + { + add.period$ " " * write$ + } + if$ + } + if$ + mid.sentence 'output.state := + } + if$ + s +} + +FUNCTION { output } +{ % discard top token if empty, else like output.nonnull + duplicate$ empty.or.unknown + 'pop$ + 'output.nonnull + if$ +} + +FUNCTION { output.dot.space } +{ % discard top token if empty, else like output.nonnull.dot.space + duplicate$ empty.or.unknown + 'pop$ + 'output.nonnull.dot.space + if$ +} + +FUNCTION { output.removenospace } +{ % discard top token if empty, else like output.nonnull.removenospace + duplicate$ empty.or.unknown + 'pop$ + 'output.nonnull.removenospace + if$ +} + +FUNCTION { output.check } +{ % like output, but warn if key name on top-of-stack is not set + 't := + duplicate$ empty.or.unknown + { pop$ "empty " t * " in " * cite$ * warning$ } + 'output.nonnull + if$ +} + +FUNCTION { bibinfo.output.check } +{ % like output.check, adding bibinfo field + 't := + duplicate$ empty.or.unknown + { pop$ "empty " t * " in " * cite$ * warning$ } + { "\bibinfo{" t "}{" * * swap$ * "}" * + output.nonnull } + if$ +} + +FUNCTION { output.check.dot.space } +{ % like output.dot.space, but warn if key name on top-of-stack is not set + 't := + duplicate$ empty.or.unknown + { pop$ "empty " t * " in " * cite$ * warning$ } + 'output.nonnull.dot.space + if$ +} + +FUNCTION { fin.block } +{ % functionally, but not logically, identical to fin.entry + add.period$ + writeln +} + +FUNCTION { fin.entry } +{ + add.period$ + writeln +} + +FUNCTION { new.sentence } +{ % update sentence state, with neither output nor stack change + output.state after.block = + 'skip$ + { + output.state before.all = + 'skip$ + { after.sentence 'output.state := } + if$ + } + if$ +} + +FUNCTION { fin.sentence } +{ + add.period$ + write$ + new.sentence + "" +} + +FUNCTION { new.block } +{ + output.state before.all = + 'skip$ + { after.block 'output.state := } + if$ +} + +FUNCTION { output.coden } % UTAH +{ % output non-empty CODEN as one-line sentence (stack untouched) + coden empty.or.unknown + { } + { "\showCODEN{" coden * "}" * writeln } + if$ +} + +% +% Sometimes articleno starts with the word 'Article' or 'Paper. +% (this is a bug of acmdl, sigh) +% We strip them. We assume eid or articleno is already on stack +% + +FUNCTION { strip.articleno.or.eid } +{ + 't := + t #1 #7 substring$ "Article" = + {t #8 t text.length$ substring$ 't :=} + { } + if$ + t #1 #7 substring$ "article" = + {t #8 t text.length$ substring$ 't :=} + { } + if$ + t #1 #5 substring$ "Paper" = + {t #6 t text.length$ substring$ 't :=} + { } + if$ + t #1 #5 substring$ "paper" = + {t #6 t text.length$ substring$ 't :=} + { } + if$ + % Strip any left trailing space or ~ + t #1 #1 substring$ " " = + {t #2 t text.length$ substring$ 't :=} + { } + if$ + t #1 #1 substring$ "~" = + {t #2 t text.length$ substring$ 't :=} + { } + if$ + t +} + + +FUNCTION { format.articleno } +{ + articleno empty.or.unknown not eid empty.or.unknown not and + { "Both articleno and eid are defined for " cite$ * warning$ } + 'skip$ + if$ + articleno empty.or.unknown eid empty.or.unknown and + { "" } + { + numpages empty.or.unknown + { "articleno or eid field, but no numpages field, in " + cite$ * warning$ } + { } + if$ + eid empty.or.unknown + { "Article \bibinfo{articleno}{" articleno strip.articleno.or.eid * "}" * } + { "Article \bibinfo{articleno}{" eid strip.articleno.or.eid * "}" * } + if$ + } + if$ +} + +FUNCTION { format.year } +{ % push year string or "[n.\,d.]" onto output stack + %% Because year is a mandatory field, we always force SOMETHING + %% to be output + "\bibinfo{year}{" + year empty.or.unknown + { "[n.\,d.]" } + { year } + if$ + * "}" * +} + +FUNCTION { format.day.month } +{ % push "day month " or "month " or "" onto output stack + day empty.or.unknown + { + month empty.or.unknown + { "" } + { "\bibinfo{date}{" month * "} " *} + if$ + } + { + month empty.or.unknown + { "" } + { "\bibinfo{date}{" day * " " * month * "} " *} + if$ + } + if$ +} + +FUNCTION { format.day.month.year } % UTAH +{ % if month is empty, push "" else push "(MON.)" or "(DD MON.)" + % Needed for frequent periodicals: 2008. ... New York Times C-1, C-2, C-17 (23 Oct.) + % acm-*.bst addition: prefix parenthesized date string with + % ", Article nnn " + articleno empty.or.unknown eid empty.or.unknown and + { "" } + { output.state after.block = + {", " format.articleno * } + { format.articleno } + if$ + } + if$ + " (" * format.day.month * format.year * ")" * +} + +FUNCTION { output.day.month.year } % UTAH +{ % if month is empty value, do nothing; else output stack top and + % leave with new top string "(MON.)" or "(DD MON.)" + % Needed for frequent periodicals: 2008. ... New York Times C-1, C-2, C-17 (23 Oct.) + format.day.month.year + output.nonnull.remove +} + +FUNCTION { strip.doi } % UTAH +{ % Strip any Web address prefix to recover the bare DOI, leaving the + % result on the output stack, as recommended by CrossRef DOI + % documentation. + % For example, reduce "http://doi.acm.org/10.1145/1534530.1534545" to + % "10.1145/1534530.1534545". A suitable URL is later typeset and + % displayed as the LAST item in the reference list entry. Publisher Web + % sites wrap this with a suitable link to a real URL to resolve the DOI, + % and the master https://doi.org/ address is preferred, since publisher- + % specific URLs can disappear in response to economic events. All + % journals are encouraged by the DOI authorities to use that typeset + % format and link procedures for uniformity across all publications that + % include DOIs in reference lists. + % The numeric prefix is guaranteed to start with "10.", so we use + % that as a test. + % 2017-02-04 Added stripping of https:// (Boris) + doi #1 #3 substring$ "10." = + { doi } + { + doi 't := % get modifiable copy of DOI + + % Change https:// to http:// to strip both prefixes (BV) + + t #1 #8 substring$ "https://" = + { "http://" t #9 t text.length$ #8 - substring$ * 't := } + { } + if$ + + t #1 #7 substring$ "http://" = + { + t #8 t text.length$ #7 - substring$ 't := + + "INTERNAL STYLE-FILE ERROR" 's := + + % search for next "/" and assign its suffix to s + + { t text.length$ } + { + t #1 #1 substring$ "/" = + { + % save rest of string as true DOI (should be 10.xxxx/yyyy) + t #2 t text.length$ #1 - substring$ 's := + "" 't := % empty string t terminates the loop + } + { + % discard first character and continue loop: t <= substring(t,2,last) + t #2 t text.length$ #1 - substring$ 't := + } + if$ + } + while$ + + % check for valid DOI (should be 10.xxxx/yyyy) + s #1 #3 substring$ "10." = + { } + { "unrecognized DOI substring " s * " in DOI value [" * doi * "]" * warning$ } + if$ + + s % push the stripped DOI on the output stack + + } + { + "unrecognized DOI value [" doi * "]" * warning$ + doi % push the unrecognized original DOI on the output stack + } + if$ + } + if$ +} + +% +% Change by BV: added standard prefix to URL +% +FUNCTION { output.doi } % UTAH +{ % output non-empty DOI as one-line sentence (stack untouched) + doi empty.or.unknown + { } + { + %% Use \urldef here for the same reason it is used in output.url, + %% see output.url for further discussion. + "\urldef\tempurl%" writeln + "\url{https://doi.org/" strip.doi * "}" * writeln + "\showDOI{\tempurl}" writeln + } + if$ +} + +FUNCTION { output.isbn } % UTAH +{ % output non-empty ISBN-10 and/or ISBN-13 as one-line sentences (stack untouched) + show-isbn-10-and-13 + { + %% show both 10- and 13-digit ISBNs + isbn empty.or.unknown + { } + { + "\showISBNx{" isbn * "}" * writeln + } + if$ + isbn-13 empty.or.unknown + { } + { + "\showISBNxiii{" isbn-13 * "}" * writeln + } + if$ + } + { + %% show 10-digit ISBNs only if 13-digit ISBNs not available + isbn-13 empty.or.unknown + { + isbn empty.or.unknown + { } + { + "\showISBNx{" isbn * "}" * writeln + } + if$ + } + { + "\showISBNxiii{" isbn-13 * "}" * writeln + } + if$ + } + if$ +} + +FUNCTION { output.issn } % UTAH +{ % output non-empty ISSN as one-line sentence (stack untouched) + issn empty.or.unknown + { } + { "\showISSN{" issn * "}" * writeln } + if$ +} + +FUNCTION { output.issue } +{ % output non-empty issue number as a one-line sentence (stack untouched) + issue empty.or.unknown + { } + { "Issue " issue * "." * writeln } + if$ +} + +FUNCTION { output.lccn } % UTAH +{ % return with stack untouched + lccn empty.or.unknown + { } + { "\showLCCN{" lccn * "}" * writeln } + if$ +} + +FUNCTION { output.note } % UTAH +{ % return with stack empty + note empty.or.unknown + { } + { "\shownote{" note * "}" add.period$ * writeln } + if$ +} + +FUNCTION { output.note.check } % UTAH +{ % return with stack empty + note empty.or.unknown + { "empty note in " cite$ * warning$ } + { "\shownote{" note * "}" add.period$ * writeln } + if$ +} + +FUNCTION { output.eprint } % +{ % return with stack empty + eprint empty.or.unknown + { } + { "\showeprint" + archiveprefix empty.or.unknown + { eprinttype empty.or.unknown + { } + { "[" eprinttype "]" * * * } + if$ + } + { "[" archiveprefix "l" change.case$ "]" * * * } + if$ + "{" eprint "}" * * * + primaryclass empty.or.unknown + { eprintclass empty.or.unknown + { } + { "~[" eprintclass "]" * * * } + if$ + } + { "~[" primaryclass "]" * * * } + if$ + writeln + } + if$ +} + + +% +% Changes by BV 2011/04/15. Do not output +% url if doi is defined +% +% +% Changes by BV 2021/11/26. Output url even if doi is defined +% if distinctURL is not zero. +% +FUNCTION { output.url } % UTAH +{ % return with stack untouched + % output URL and associated lastaccessed fields + doi empty.or.unknown distinctURL empty.or.zero not or + { + url empty.or.unknown + { } + { + %% Use \urldef, outside \showURL, so that %nn, #, etc in URLs work + %% correctly. Put the actual URL on its own line to reduce the + %% likelihood of BibTeX's nasty line wrapping after column 79. + %% \url{} can undo this, but if that doesn't work for some reason + %% the .bbl file would have to be repaired manually. + "\urldef\tempurl%" writeln + "\url{" url * "}" * writeln + + "\showURL{%" writeln + lastaccessed empty.or.unknown + { "" } + { "Retrieved " lastaccessed * " from " * } + if$ + "\tempurl}" * writeln + } + if$ + } + { } + if$ +} + +FUNCTION { output.year.check } +{ % warn if year empty, output top string and leave " YEAR