Add a few intrinsics contracts #25

	# This workflow is responsible for verifying the standard library with Kani.

	name: Kani
	on:
	workflow_dispatch:
	pull_request:
	branches: [ main ]
	push:
	paths:
	- 'library/**'
	- '.github/workflows/kani.yml'

	defaults:
	run:
	shell: bash

	jobs:
	build:
	runs-on: ${{ matrix.os }}
	strategy:
	matrix:
	# Kani does not support windows.
	os: [ubuntu-latest, macos-latest]
	include:
	- os: ubuntu-latest
	base: ubuntu
	- os: macos-latest
	base: macos
	steps:
	- name: Checkout Library
	uses: actions/checkout@v4
	with:
	path: verify-rust-std
	submodules: true

	# We currently build Kani from a branch that tracks a rustc version compatible with this library version.
	- name: Checkout `Kani`
	uses: actions/checkout@v4
	with:
	repository: model-checking/kani
	path: kani
	ref: features/verify-rust-std

	- name: Setup Dependencies
	working-directory: kani
	run: \|
	./scripts/setup/${{ matrix.base }}/install_deps.sh

	- name: Build `Kani`
	working-directory: kani
	run: \|
	cargo build-dev --release
	echo "$(pwd)/scripts" >> $GITHUB_PATH

	- name: Run tests
	working-directory: verify-rust-std
	env:
	RUST_BACKTRACE: 1
	run: \|
	kani verify-std -Z unstable-options ./library --target-dir ${{ runner.temp }} -Z function-contracts \
	-Z mem-predicates -Z ptr-to-ref-cast-checks

Provide feedback