feat: Add basic definitions and proof sketch for rounding equivalence #288

	name: Golden testing
	on:
	push:
	branches:
	- "main"
	pull_request:
	merge_group:

	permissions:
	contents: read

	jobs:
	build:
	name: Golden testing against FloatX + SymFPU
	permissions:
	pull-requests: write
	runs-on: ubuntu-latest
	steps:
	- name: Checkout 🛎️
	uses: actions/checkout@v4

	- name: Build with lean-action
	uses: leanprover/lean-action@v1
	with:
	use-mathlib-cache: false
	use-github-cache: true
	build: true
	test: false

	- name: Install C++ build tools
	run: \|
	sudo apt-get update
	sudo apt-get install -y build-essential cmake

	- name: Set up Python
	uses: actions/setup-python@v5
	with:
	python-version: '3.10'

	- name: Cache Python dependencies
	uses: actions/cache@v4
	with:
	path: ~/.cache/pip
	key: ${{ runner.os }}-pip-${{ hashFiles('**/requirements.txt') }}
	restore-keys: \|
	${{ runner.os }}-pip-

	- name: Install Python dependencies
	run: pip install -r requirements.txt

	- name: Run golden test for FloatX
	run: ./test/ci/compare-floatx-fplean.sh

	- name: Run golden test for SymFPU
	run: ./test/ci/compare-symfpu-fplean.sh

Provide feedback