search

microsoft / ivy

IVy is a research tool intended to allow interactive development of protocols and their proofs of correctness and to provide a platform for developing and experimenting with automated proof techniques. In particular, IVy provides interactive visualization of automated proofs, and supports a use model in which the human protocol designer and the automated tool interact to expose errors and prove correctness.
Other
223 stars 80 forks source link

Understanding BitFieldExtraction Operator bfe[][] #84

Open prpr2770 opened 4 years ago

prpr2770 commented 4 years ago

I'm trying to encode and decode information in the following data structure

instance packetload : bit_vector(16)
instance bv3 : bit_vector(3)

    object arbitload2 = {

        object brick = {
            type this = struct {
                brick1 : packetload,       
                brick2 : bv3
            }
            instance idx : unbounded_sequence
            instance arr : array(idx,this)
        }

        variant this of arbitload = struct {

            block1      : packetload,    
            block2      : brick.arr   

        }
}

And I believe i need to use the BFE-operator. I couldn't find proper documentation about this, and I was wondering if I could get some help in understanding it.

From the file language.md I obtained the following description: 

 `bfe[3][0]` is the bit field extraction operator the takes the low order 4 bits of a bit vector.

Further in an earlier issue here bfe[0][7](enc) was used. I'm confused about the indexing that's provided.

May I have a description of this operator, and how it needs to be used, to extract information from a byte of data? Should the byte be defined as bit_vector(8) or can it be described by bv[8]?