Algebruh

Bouwen

Algebruh vereist Rust 1.85 of later, Cargo, pkg-config en de Z3-ontwikkelbibliotheek. Als alternatief biedt de meegeleverde Nix shell deze afhankelijkheden en alle optionele checkers:

nix-shell

Bouw het release-binary en kopieer dit naar de wortel van de repository:

cargo build --release
cp target/release/algebruh .

Gebruik

Het programma kan als volgt worden gebruikt:

./algebruh [--all] [--json] [--interpret LIST] [--assume EXPR]... [--injective NAME]... [--ai-command CMD] [--emit PREFIX] CLAIM

Om de status van het systeem te controleren:

./algebruh doctor [--json]

Voorbeelden:

• ./algebruh "2 = 3"
• ./algebruh --assume "a = c" --assume "c = b" "a = b"
• ./algebruh --interpret int,real,bv8,mod:1 "2 = 3"
• ./algebruh --injective f --assume "f(a) = f(b)" "a = b"
• ./algebruh --interpret f32 "16777216 + 1 = 16777216"
• ./algebruh --all --json "a = b"

Opties:

• --all: Voert aanvullende checkers uit, probeert extra solver-seeds, zoekt naar voldoende premissen en print elke poging.
• --json: Print het volledige rapport als JSON.
• --ai-command CMD: Verstuurt het probleem als JSON naar CMD. De output hiervan moet een Lean-tactic zijn, die Algebruh alleen accepteert na verificatie door de Lean-kernel.

Expressies

Expressies ondersteunen gehele getallen, variabelenamen, unaire functieaanroepen zoals f(x), haakjes, een minteken (unair), +, -, *, /, %, =, == en !=.

Gebruik herhaalbare --injective NAME opties om unaire functies als injectief te declareren. Functieaanroepen zonder deze optie blijven oninterpreteerd.

Vermenigvuldiging, deling en modulo hebben een hogere prioriteit dan optelling en aftrekking. De semantiek van de operatoren volgt de geselecteerde interpretatie.

Elke claim of aanname moet één gelijkheid of ongelijkheid bevatten. Vergelijkingen zoals < en >= worden niet ondersteund.

Interpretaties

De optie --interpret accepteert een komma-gescheiden lijst:

Waarde	Betekenis
int	Z3 integers. Dit is de standaardinstelling.
real	Exacte reële rekenkunde. De % operator wordt niet ondersteund.
bvN of sbvN	Een signed N-bit vector, waarbij N tussen 1 en 256 ligt.
ubvN	Een unsigned N-bit vector.
mod:N	Gehele getalexpressies vergeleken modulo een positief getal N.
quot:N	De quotiëntring $\mathbb{Z}/N\mathbb{Z}$.
equiv:N	Gebruikersgedefinieerde gelijkheid $x \sim y$ wanneer $x$ en $y$ hetzelfde residu hebben modulo N.
f32, f64	IEEE-754 rekenkunde; integer literals worden gecast met round-to-nearest, ties-to-even.
singleton	Een domein waar alle waarden gelijk zijn.

Algebruh evalueert de integer-interpretatie altijd als basislijn. Er wordt REINTERPRETED gerapporteerd wanneer een geselecteerde alternatieve interpretatie een claim bewijst die integers niet bewijzen. Signed en unsigned bit-vector runs worden automatisch gekoppeld; verschillen ten opzichte van integers of ten opzichte van elkaar worden geprint als semantische waarschuwingen.

Resultaten

Resultaat	Betekenis	Exit code
PROVED	De aannames bewijzen de claim.	0
REFUTED	De aannames bewijzen de negatie van de claim.	0
CONTINGENT	Zowel de claim als de negatie ervan hebben modellen.	1
CONDITIONAL	Aanvullende premissen gevonden door --all bewijzen de claim.	1
VACUOUS	De aannames zijn inconsistent.	1
REINTERPRETED	Een geselecteerde alternatieve interpretatie bewijst de claim.	0
UNKNOWN	Geen enkel kandidaatresultaat is door onafhankelijke verificatie gekomen.	1
UNSAFE_AXIOM	Een Lean-kandidaat gebruikt of is afhankelijk van een onveilig axioma.	1
CHECKERBUGCANDIDATE	Solvers of proof checkers zijn het oneens.	1

Fouten bij invoer, artefacten, sandbox en solvers maken gebruik van exit code 2.

Checkers

De standaardrun maakt gebruik van de gekoppelde Z3-bibliotheek. Deze controleert kandidaten onafhankelijk met exacte evaluatie, equality saturation, bounded model search en LRAT replay waar van toepassing. De --all optie probeert daarnaast cvc5, Carcara, Lean met Mathlib, Vampire en E.

Voor bewezen of weerlegde integer-claims legt --all één differentieel resultaat vast over Z3, cvc5, Carcara en de Lean-kernel. Meningsverschillen in de uitkomst tussen Z3/cvc5 en replay-fouten bij Carcara resulteren in CHECKERBUGCANDIDATE. Algebruh minimaliseert deze meningsverschillen zolang ze reproduceerbaar zijn.

Externe tools worden uitgevoerd via Bubblewrap en prlimit. Algebruh vindt deze op de PATH.

Controleer de beschikbaarheid van tools met: ./algebruh doctor

Dit commando stopt met code 1 als een van de vermelde tools niet beschikbaar is.

Bewijsartefacten

Voor een resultaat met een geselecteerd Z3-bewijs kan --emit PREFIX worden gebruikt om het SMT-LIB script en bewijs op te slaan:

./algebruh --emit result "x + 0 = x"

Dit commando maakt result.smt2 en result.proof aan zonder bestaande bestanden te overschrijven. Als het z3 commando is geïnstalleerd, kan de controle opnieuw worden uitgevoerd met:

z3 result.smt2

Beperkingen

Algebruh ondersteunt rekenkundige gelijkheden en ongelijkheden over ingebouwde interpretaties. Gebruikersgedefinieerde gelijkheid is beperkt tot de modulaire equivalentiefamilie equiv:N. Niet-lineaire rekenkunde kan leiden tot UNKNOWN.

Deling en modulo gebruiken de geselecteerde Z3-interpretatie. Deling of modulo door nul volgt de Z3-semantiek. Bewijsbestanden maken gebruik van het Z3-bewijsformaat.