perf(prover): verify continuation proofs in place via rkyv #105
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: Profile Recursion (PR) | |
| # Runs the recursion-guest PC histogram diagnostics (single-query and | |
| # multi-query, in parallel via a matrix) and posts a combined per-function | |
| # profile as a PR comment. Triggered by a `/profile_recursion` comment from a | |
| # repo member, or manually via workflow_dispatch. | |
| on: | |
| workflow_dispatch: | |
| issue_comment: | |
| types: [created] | |
| permissions: | |
| contents: read | |
| pull-requests: write | |
| concurrency: | |
| # See bench-verify.yml. workflow_dispatch (no comment) falls to the unique run_id group. | |
| group: ${{ startsWith(github.event.comment.body, '/profile_recursion') && format('profile-recursion-{0}', github.event.issue.number) || format('profile-recursion-{0}', github.run_id) }} | |
| cancel-in-progress: false | |
| jobs: | |
| # One job per configuration; they run in parallel and each uploads a Markdown | |
| # fragment artifact. The `comment` job stitches them into one PR comment. | |
| profile: | |
| # Skip unless: workflow_dispatch, or "/profile_recursion" comment on a PR by a member. | |
| if: >- | |
| github.event_name == 'workflow_dispatch' || | |
| (github.event_name == 'issue_comment' && | |
| github.event.issue.pull_request && | |
| startsWith(github.event.comment.body, '/profile_recursion') && | |
| contains(fromJSON('["MEMBER","OWNER","COLLABORATOR"]'), github.event.comment.author_association)) | |
| runs-on: [self-hosted, bench] | |
| timeout-minutes: 90 | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| include: | |
| - name: single-query | |
| test: single | |
| title: "Single query (blowup=2, 1 query)" | |
| - name: multi-query | |
| test: multi | |
| title: "Multi query (blowup=8, 128-bit)" | |
| steps: | |
| - name: React to comment | |
| if: github.event_name == 'issue_comment' && matrix.name == 'single-query' | |
| uses: actions/github-script@v7 | |
| with: | |
| script: | | |
| await github.rest.reactions.createForIssueComment({ | |
| owner: context.repo.owner, | |
| repo: context.repo.repo, | |
| comment_id: context.payload.comment.id, | |
| content: 'eyes' | |
| }); | |
| - name: Get PR head ref | |
| id: pr-ref | |
| if: github.event_name == 'issue_comment' | |
| env: | |
| GH_TOKEN: ${{ github.token }} | |
| PR_NUM: ${{ github.event.issue.number }} | |
| run: | | |
| SHA=$(gh pr view "$PR_NUM" --repo "$GITHUB_REPOSITORY" --json headRefOid -q .headRefOid) | |
| echo "sha=$SHA" >> "$GITHUB_OUTPUT" | |
| - name: Checkout | |
| uses: actions/checkout@v4 | |
| with: | |
| ref: ${{ steps.pr-ref.outputs.sha || github.sha }} | |
| - name: Setup Rust Environment | |
| uses: ./.github/actions/setup-rust | |
| - name: Add cargo to PATH | |
| run: echo "$HOME/.cargo/bin" >> "$GITHUB_PATH" | |
| - name: Run recursion PC histogram (${{ matrix.name }}) | |
| env: | |
| TEST: ${{ matrix.test }} | |
| run: | | |
| # Self-provision the RISC-V sysroot in a user-writable dir (the default | |
| # /opt path on the bench runner is root-owned); the guest ELF build the | |
| # test triggers picks this up via the Makefile's `SYSROOT_DIR ?=`. | |
| export SYSROOT_DIR="$HOME/.lambda-vm-sysroot" | |
| set -o pipefail | |
| make test-profile-recursion-$TEST 2>&1 | tee /tmp/hist.log | |
| - name: Aggregate into a per-function fragment | |
| if: always() | |
| env: | |
| TITLE: ${{ matrix.title }} | |
| run: | | |
| python3 .github/scripts/aggregate_recursion_histogram.py \ | |
| /tmp/hist.log --title "$TITLE" --out "/tmp/fragment-${{ matrix.name }}.md" | |
| cat "/tmp/fragment-${{ matrix.name }}.md" >> "$GITHUB_STEP_SUMMARY" | |
| - name: Upload fragment | |
| if: always() | |
| uses: actions/upload-artifact@v4 | |
| with: | |
| name: profile-fragment-${{ matrix.name }} | |
| path: /tmp/fragment-${{ matrix.name }}.md | |
| retention-days: 7 | |
| # Stitch the matrix fragments into a single PR comment. | |
| comment: | |
| needs: profile | |
| # always() so partial-matrix failures still post; skip when `profile` was | |
| # skipped (non-/profile_recursion or non-member comment) so this job — and | |
| # the self-hosted bench runner it spins up — doesn't fire on every comment. | |
| if: always() && github.event_name == 'issue_comment' && needs.profile.result != 'skipped' | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Get PR head ref | |
| id: pr-ref | |
| env: | |
| GH_TOKEN: ${{ github.token }} | |
| PR_NUM: ${{ github.event.issue.number }} | |
| run: | | |
| SHA=$(gh pr view "$PR_NUM" --repo "$GITHUB_REPOSITORY" --json headRefOid -q .headRefOid) | |
| echo "sha=$SHA" >> "$GITHUB_OUTPUT" | |
| - name: Download fragments | |
| uses: actions/download-artifact@v4 | |
| with: | |
| path: fragments | |
| pattern: profile-fragment-* | |
| merge-multiple: true | |
| - name: Assemble comment body | |
| env: | |
| COMMIT_SHA: ${{ steps.pr-ref.outputs.sha }} | |
| run: | | |
| { | |
| echo "## Recursion guest profile" | |
| echo | |
| # Single-query first, then multi-query, then any others. | |
| for frag in fragments/fragment-single-query.md \ | |
| fragments/fragment-multi-query.md; do | |
| [ -f "$frag" ] && { cat "$frag"; echo; } | |
| done | |
| echo "<sub>Commit: ${COMMIT_SHA:0:8} · Runner: self-hosted bench</sub>" | |
| } > /tmp/profile_comment.md | |
| cat /tmp/profile_comment.md | |
| - name: Comment on PR | |
| uses: actions/github-script@v7 | |
| with: | |
| script: | | |
| const fs = require('fs'); | |
| const body = fs.readFileSync('/tmp/profile_comment.md', 'utf8'); | |
| const { data: comments } = await github.rest.issues.listComments({ | |
| owner: context.repo.owner, | |
| repo: context.repo.repo, | |
| issue_number: context.issue.number, | |
| }); | |
| // Reuse our own marker comment so repeated /profile_recursion runs update in place. | |
| const existing = comments.find(c => | |
| c.user.type === 'Bot' && | |
| c.body.includes('Recursion guest profile') | |
| ); | |
| if (existing) { | |
| await github.rest.issues.updateComment({ | |
| owner: context.repo.owner, | |
| repo: context.repo.repo, | |
| comment_id: existing.id, | |
| body, | |
| }); | |
| } else { | |
| await github.rest.issues.createComment({ | |
| owner: context.repo.owner, | |
| repo: context.repo.repo, | |
| issue_number: context.issue.number, | |
| body, | |
| }); | |
| } |