#lang rosette ; int32? is a shorthand for the type (bitvector 32). (define int32? (bitvector 32)) ; int32 takes as input an integer literal and returns ; the corresponding 32-bit bitvector value. (define (int32 i) (bv i int32?)) ; bvudiv2 performs unsigned 32-bit division by 2. (define (bvudiv2 x) (bvudiv x (int32 2))) ; x / 2 ; bvudiv2-a performs unsigned 32-bit division by 2 ; using shifting. (define (bvudiv2-a x) (bvashr x (int32 1))) ; x >> 1 ; Verification: we find that bvudiv2-a is not correct on all values. (define-symbolic x int32?) (define cex (verify (assert (equal? (bvudiv2 x) (bvudiv2-a x))))) cex (evaluate (bvudiv2 x) cex) (evaluate (bvudiv2-a x) cex) ; Angelic execution: is there some input on which bvudiv2-a is correct? (define guess (solve (assert (equal? (bvudiv2 x) (bvudiv2-a x))))) guess ; It turns out that bvudiv2-a is correct for all non-negative values. (verify (begin (assume (bvsge x (int32 0))) (assert (equal? (bvudiv2 x) (bvudiv2-a x))))) (require rosette/lib/synthax) ; Synthesis: how can we implement bvudiv2-b so that it is correct on all values? (define (bvudiv2-b x) ((choose bvashr bvlshr bvshl) x (?? int32?))) ; x [>> | << | >>>] ?? (define sol (synthesize #:forall (list x) #:guarantee (assert (equal? (bvudiv2 x) (bvudiv2-b x))))) (generate-forms sol)