feat: generalize to arbitrary bitvec width `zeroextend_bigger_smaller` and `truncate_of_concat_is_lsb`

leanprover / LNSym

Armv8 Native Code Symbolic Simulator in Lean

Apache License 2.0

62 stars 18 forks source link

feat: generalize to arbitrary bitvec width `zeroextend_bigger_smaller` and `truncate_of_concat_is_lsb` #221

Closed luisacicolini closed 1 month ago

luisacicolini commented 1 month ago

Description:

This PR extends truncate_of_concat_is_lsb_64 to arbitrary-width bitvectors.

Testing:

What tests have been run? Did make all succeed for your changes? Yes Was conformance testing successful on an Aarch64 machine? yes

License:

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.

luisacicolini commented 1 month ago

thank you for reviewing this @shigoel! Everything should be fixed now. I removed zeroextend_bigger_smaller and added a comment pointing to the correct arbitrary-width version.

luisacicolini commented 1 month ago

thanks @alexkeizer! I updated the theorem with your suggestions