Tracking issue: document bitvector rules

This tracks the documentation of the bitvector rules to the specification document.

Rough TODOs:

• Collect all note documents about bitvector rules
• Add bitvector section to "concepts" section of the specification
• Add all bitvector rules
• Add examples

Bitvector rules:

• bitblast_var
• bitblast_const
• bitblast_and
• bitblast_or
• bitblast_xor
• bitblast_xnor
• bitblast_not
• bitblast_add
• bitblast_neg
• bitblast_mult
• bitblast_extract
• bitblast_concat
• bitblast_eq
• bitblast_ult
• bitblast_slt
• bitblast_sext

This branch contains the preliminary work that was done in 2023: https://gitlab.uliege.be/verit/alethe/-/tree/devel/bitblasting?ref_type=heads

However, this was done with the motivation of eventually creating a not cvc5 specific calculus. Hence, it might be necessary to "undo" some design ideas implemented there.

This PDF defines the semantics of (most of) the rules with a legacy notation that hopefully is clear enough:bitblasting.pdf

This PDF was based on how cvc5 specifically does bit-blasting. However, it's kind of standard stuff (Daniel Kroening's Decision Procedure book for example describes something really similar).

I started extending the Alethe spec to phrase the inferences above in Alethe, in this branch: https://gitlab.uliege.be/verit/alethe/-/tree/bv?ref_type=heads

Carcara has been extended to support the inferences as cvc5 does them: https://github.com/HanielB/carcara/tree/bvSupport (see https://github.com/HanielB/carcara/blob/bvSupport/carcara/src/checker/rules/bitvectors.rs)

One detail is that cvc5 produces n-ary versions of some of these rules (for bvmult, bvadd, bvand etc I forget now which ones exactly but in the checking in Carcara this is spelled out).

The rules above do not cover: shifts, division, mod/rem.

I dislike the names in the cvc5 proofs at the moment, for the new operators and for the bit-blasting proofs. In this commit I changed the branch in Carcara to use the cvc5 names rather than other names I thought were nicer: https://github.com/HanielB/carcara/commit/3f84d0606307ee4257db588d79e0137956e71e7f

This was motivated to use Carcara in the cvc5 regressions. I did not want to change the names used by cvc5 because this will impact Isabelle's reconstruction.

I propose that we converge on which names to use now. So that how it'll be in Alethe is defined, and that cvc5, Carcara, and Isabelle follow along. I personally prefer the names that were removed in the commit above in the Carcara branch.

@Lachnitt

added cvc5 rules labels

I agree on the names. Another issue is potential name clashes if bbT is a user defined symbol. In AletheLF we handle this with adding @ in front of those symbols. I think we should do the same.

Regarding the naming issue, I propose that for now we document the status-quo names, and if we agree to rename, we meet on Zoom for a renaming "ceremony" where we change the names everywhere at the same time. Then we celebrate over some Blubberlutsch.

marked the checklist item Collect all note documents about bitvector rules as completed

marked the checklist item Add bitvector section to "concepts" section of the specification as completed

mentioned in merge request !4 (merged)

So we now have a first version of the general description section and three proof rules (taken from @hbarbosa 's branch). The format of these rules will serve as a prototype for the other rules.

changed the description

added todo-specification label