Add a tour of the RawVec proof #907

	name: VeriFast

	on:
	workflow_dispatch:
	merge_group:
	pull_request:
	branches: [ main ]
	push:
	paths:
	- 'library/**'
	- '.github/workflows/verifast.yml'
	- 'verifast-proofs/**'

	defaults:
	run:
	shell: bash

	jobs:
	check-verifast-on-std:
	name: Verify std library
	runs-on: ubuntu-latest

	steps:
	- name: Checkout Repository
	uses: actions/checkout@v4

	- name: Install VeriFast
	run: \|
	cd ~
	curl -OL https://github.com/verifast/verifast/releases/download/25.08/verifast-25.08-linux.tar.gz
	# https://github.com/verifast/verifast/attestations/10123891
	echo '1e40019d6add91bf72141c86f4007f2fe1eef67f453cb7fb8f1f5ab7d31d509f verifast-25.08-linux.tar.gz' \| shasum -a 256 -c
	tar xf verifast-25.08-linux.tar.gz

	- name: Install the Rust toolchain used by VeriFast
	run: rustup toolchain install nightly-2025-04-09

	- name: Run VeriFast Verification
	run: \|
	export PATH=~/verifast-25.08/bin:$PATH
	cd verifast-proofs
	bash check-verifast-proofs.sh

	notify-btj:
	name: Notify @btj
	runs-on: ubuntu-latest
	needs: check-verifast-on-std
	if: failure()
	permissions:
	id-token: write

	steps:
	- name: Get GitHub OIDC token
	id: get_token
	uses: actions/github-script@v7
	with:
	script: \|
	const audience = 'notify-bart-jacobs';
	return await core.getIDToken(audience);
	result-encoding: string

	- name: Call notification endpoint
	run: \|
	curl -X POST "https://verify-rust-std-verifast-monitor.bart-jacobs.workers.dev/" \
	-H "Authorization: Bearer ${{ steps.get_token.outputs.result }}" \
	-H "Content-Type: application/json" \
	-d '{}'

Provide feedback