Module bitvec

This module provides a specification-friendly bit vector type.

Modules

int_vec_interp

This module defines interpretation for bit vectors as vectors of machine integers of various size and signedness.

Structs

BitVec

A fixed-size bit vector type.

Constants

REWRITE_RULE

An F* attribute that indiquates a rewritting lemma should be applied

Functions

bitvec_postprocess_norm

This function is useful only for verification in F*. Used with postprocess_rewrite, this tactic: