#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))

; The uninterpreted function we'll use instead of multiplication.
(define-symbolic umul (~> BV? BV? BV?))

; Returns the square of y.
(define (sq y)
  (umul y y))

; Returns the square of the absolute value of y.
(define (sqabs y)
  (umul (bvabs y) (bvabs y)))

; Are sq and sqabs equal on all inputs?
(define-symbolic y BV?)
(time
 (verify
  (assert (equal? (sq y) (sqabs y))))) 

(time
 (verify
  #:assume    (assert (equal? (umul y y) (umul (bvneg y) (bvneg y))))
  #:guarantee (assert (equal? (sq y) (sqabs y)))))