Add support for real, bv8, bv16, bv32, bv64#8
Conversation
atomb
requested review from
MikaelMayer,
andrewmwells-amazon,
joehendrix and
shigoel
|
LGTM, thanks! I'm curious about the scope of a possible full parameterization of the I'm guessing it's the former. The latter would require non-trivial changes to Lambda's type system, which -- like vanilla OCaml -- doesn't support type families. |
| { name := "Bv8.Add", | ||
| inputs := [("x", mty[bv8]), ("y", mty[bv8])], | ||
| output := mty[bv8], | ||
| denote := none }, |
There was a problem hiding this comment.
Perhaps out of scope for this PR, but would be good to add denotation functions for bitvecs to allow constant folding/concrete evaluation.
There was a problem hiding this comment.
Yeah, I definitely want to add those, but I figured I'd keep the first PR simple.
| | _ => none | ||
|
|
||
| /-- | ||
| If `e` is an `LExpr` real, then denote that into a Lean `String`. |
There was a problem hiding this comment.
Nit: worth noting this denotation into a String is intentional because we don't import reals from Mathlib (yet?).
There was a problem hiding this comment.
Yep, exactly. I suspect we should support reals more thoroughly, but I think we should have a design discussion about exactly how. For now, strings allow us to send constants through the verification pipeline.
Yeah, I mean the former primarily. The latter would be cool, but I expect more work than it's worth. |
A fully-parameterized bit vector type doesn't work well at all stages of the pipeline at the moment, but could potentially in the future. The Lambda dialect, at least, has a `.bitvec n` constructor in `LMonoTy`, but most of the rest of the pipeline treats each bit vector type entirely independently.
Also make sure other examples are included in the build.
…nat support) status Gap strata-org#6: mark BV→int (`e as_int`) as implemented; note int→BV and centralized coercion pass as remaining work. Gap strata-org#8: mark `type nat := int` synonym + auto non-negativity axioms as partially implemented; document the mixed-type datatype limitation and point to nat_axiom_discussion.lean for design alternatives. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
2 participants
A fully-parameterized bit vector type doesn't work well at all stages of the pipeline at the moment, but could potentially in the future. The Lambda dialect, at least, has a
.bitvec nconstructor inLMonoTy, but most of the rest of the pipeline treats each bit vector type entirely independently.By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.