Thanks! That's a good one!
-
-
JFYI: I've now added this as clmul application to the current xbitmanip draft at https://raw.githubusercontent.com/cliffordwolf/xbitmanip/master/xbitmanip-draft.pdf … (you are now listed as contributor to xbitmanip, btw) and I've added the following invariant to my test cases.pic.twitter.com/zRtU4R5ztX
1 reply 0 retweets 4 likes -
This Tweet is unavailable.
-
Replying to @johnregehr @rygorous
I've done some exploration of this using SyGuS and quantified SMT. See for example http://svn.clifford.at/handicraft/2018/xbitpermsyn/ …. (Also submitted some SyGuS benchmarks.) A big unsolved problem seems to be generating programs that contain large (word-sized) magic constants.
0 replies 0 retweets 3 likes -
This Tweet is unavailable.
-
Replying to @johnregehr @rygorous
Oh, I'm very interested! Is any of that published?
0 replies 0 retweets 0 likes -
This Tweet is unavailable.
-
This Tweet is unavailable.
-
This Tweet is unavailable.
-
This Tweet is unavailable.
Thanks! I'll send a reply tomorrow. (Afk right now.) In a way I am already doing this in the svn link I shared above. (This one only deals with bit permutation operators, so it's trivial to pre-generate a perfect minimal set of sample constants.)
-
-
This Tweet is unavailable.
-
This Tweet is unavailable.
- Show replies
-
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.