#lang rosette ; The bitvector datatype we'll use: 128 bits. (define BV? (bitvector 128)) ; Takes an integer constant and returns ; the corresponding bitvector. (define (BV v) (bv v BV?)) ; The absolute value function for bitvectors. (define (bvabs v) (if (bvslt v (BV 0)) (bvneg v) v)) ; Returns the square of y. (define (sq y) (bvmul y y)) ; Returns the square of the absolute value of y. (define (sqabs y) (bvmul (bvabs y) (bvabs y))) ; Are sq and sqabs equal on all inputs? (define-symbolic y BV?) (time (verify (assert (equal? (sq y) (sqabs y)))))