/seL4-l4v-master/HOL4/Manual/Description/ |
H A D | HolBdd.tex | 876 Encoding is done with the least significant bits first in the BDD ordering. For example, if variables
|
/seL4-l4v-master/HOL4/Manual/Translations/IT/Description/ |
H A D | HolBdd.tex | 876 Encoding is done with the least significant bits first in the BDD ordering. For example, if variables
|
H A D | theories.tex | 2461 \holtxt{word\_slice} & \holtxt{''} & \num\rarr\num\rarr\worda\rarr\worda & Set bits outside field to zero \\
|
/seL4-l4v-master/HOL4/examples/ARM/v4/ |
H A D | arm_evalLib.sml | 651 fun bits h l n = (n mod pow(two,plus1 h)) div (pow(two,l)) function 655 map (fn (i,j) => num2byte (bits (fromInt i) (fromInt j) w))
|
H A D | assemblerML.sml | 68 fun bits h l (n:bool list) = List.take(List.drop(n,l),h + 1 - l); function 69 fun bit b n = (bits b b n = [true]); 149 val Rn = list2register o bits 19 16; 150 val Rd = list2register o bits 15 12; 151 val Rs = list2register o bits 11 8; 152 val Rm = list2register o bits 3 0; 165 mk_immediate (list2int (bits 11 8 l)) (list2num (bits 7 0 l)) 169 let val imm = list2int (bits 11 7 l) in 170 {Rm = Rm l, Imm = imm, Sh = list2shift (bits [all...] |
/seL4-l4v-master/HOL4/examples/ARM/v7/ |
H A D | arm_opsemScript.sml | 2964 where <spec_reg> is APSR_<bits>, CPSR_<fields> or SPSR_<fields> 2965 <bits> is nzcvq, g, or nzcvqg 2982 where <spec_reg> is APSR_<bits>, CPSR_<fields> or SPSR_<fields> 2983 <bits> is nzcvq, g, or nzcvqg
|
/seL4-l4v-master/HOL4/examples/ARM/v7/eval/ |
H A D | emit_eval.sml | 280 | armML.DataProcessing (armML.Reverse_Bits _) => "reverse bits"
|
/seL4-l4v-master/HOL4/examples/ARM_security_properties/model/ |
H A D | arm_opsemScript.sml | 2988 where <spec_reg> is APSR_<bits>, CPSR_<fields> or SPSR_<fields> 2989 <bits> is nzcvq, g, or nzcvqg 3006 where <spec_reg> is APSR_<bits>, CPSR_<fields> or SPSR_<fields> 3007 <bits> is nzcvq, g, or nzcvqg
|
/seL4-l4v-master/HOL4/examples/Crypto/MARS/ |
H A D | MARS_keyExpansionScript.sml | 142 (* Record the two lowest bits of K[i], by setting j = K[i] & 3, and then 143 consider the word with these two bits set to 1, w = K[i] | 3 *)
|
/seL4-l4v-master/HOL4/examples/Crypto/Serpent/Reference/ |
H A D | Serpent_Reference_TransformationScript.sml | 560 (* compute the parity on select bits *)
|
/seL4-l4v-master/HOL4/examples/Crypto/TEA/ |
H A D | teaScript.sml | 6 (* causes all bits of the key and data to be mixed repeatedly.The number of *) 9 (* authors suggest 32. The key is set at 128 bits. *)
|
/seL4-l4v-master/HOL4/examples/Crypto/TWOFISH/ |
H A D | twofishScript.sml | 5 up to 256 bits. The cipher is a 16-round Feistel network with a 290 (* argument, with an extra rotate over 8 bits. The values Ai and Bi are *) 291 (* combined in a PHT. One of the results is further rotated by 9 bits. *)
|
/seL4-l4v-master/HOL4/examples/HolCheck/ |
H A D | bddTools.sml | 38 (* and it would be inefficient to unwind the higher order bits *)
|
/seL4-l4v-master/HOL4/examples/HolCheck/examples/ |
H A D | alu.sml | 25 val aw = 1; (* address space width in bits *) 26 val d = 1; (* datapath width in bits *) 49 (* where the address space is wsize bits wide *) 58 (* generates bitwise conjunction of equality tests for registers r1 and r2, each w bits wide *) 91 (* width d, and with an address space of aw bits. The ctl_wff's are CTL formulae expressing the *)
|
H A D | amba_ahbScript.sml | 402 (* decoder, decodes higher order address bits to figure out which slave is being targeted *)
|
H A D | amba_apbScript.sml | 16 (* note: psel_x is a family signals, where x identifies the slave, so the x is not bits e.g. psel_2 is a valid signal *)
|
/seL4-l4v-master/HOL4/examples/acl2/examples/M1/ |
H A D | hol_defaxiomsScript.sml | 3498 |- signed_byte_p bits x = 3500 [integerp bits; less (nat 0) bits; 3501 integer_range_p (unary_minus (expt (nat 2) (add (int ~1) bits))) 3502 (expt (nat 2) (add (int ~1) bits)) x], 3507 |- unsigned_byte_p bits x = 3509 [integerp bits; not (less bits (nat 0)); 3510 integer_range_p (nat 0) (expt (nat 2) bits) x],
|
/seL4-l4v-master/HOL4/examples/acl2/examples/acl2-hol-ltl-paper-example/ |
H A D | hol_defaxiomsScript.sml | 3460 |- signed_byte_p bits x = 3462 [integerp bits; less (nat 0) bits; 3463 integer_range_p (unary_minus (expt (nat 2) (add (int ~1) bits))) 3464 (expt (nat 2) (add (int ~1) bits)) x], 3469 |- unsigned_byte_p bits x = 3471 [integerp bits; not (less bits (nat 0)); 3472 integer_range_p (nat 0) (expt (nat 2) bits) x],
|
/seL4-l4v-master/HOL4/examples/acl2/ml/ |
H A D | hol_defaxiomsScript.sml | 3456 |- signed_byte_p bits x = 3458 [integerp bits; less (nat 0) bits; 3459 integer_range_p (unary_minus (expt (nat 2) (add (int ~1) bits))) 3460 (expt (nat 2) (add (int ~1) bits)) x], 3465 |- unsigned_byte_p bits x = 3467 [integerp bits; not (less bits (nat 0)); 3468 integer_range_p (nat 0) (expt (nat 2) bits) x],
|
H A D | signedintScript.sml | 297 (* extend r l : Sign extend an integer i to fit in l bits *)
|
/seL4-l4v-master/HOL4/examples/dev/AES/curried/ |
H A D | word8Script.sml | 11 (* 8 bits per byte, represented as an 8-tuple of truth values. *) 26 (* variables, or as 256 tuples of bits. The former is useful for symbolic *) 197 Compare bits and bytes as if they were numbers. Not currently used
|
/seL4-l4v-master/HOL4/examples/dev/AES/tupled/ |
H A D | word8Script.sml | 11 (* 8 bits per byte, represented as an 8-tuple of truth values. *) 23 (* variables, or as 256 tuples of bits. The former is useful for symbolic *) 173 Compare bits and bytes as if they were numbers. Not currently used
|
/seL4-l4v-master/HOL4/examples/dev/sw/ |
H A D | preARMScript.sml | 28 (* CPSR, In user programs only the top 4 bits of the CPSR are relevant *)
|
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/ |
H A D | preARMScript.sml | 25 (* CPSR, In user programs only the top 4 bits of the CPSR are relevant *)
|
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/ |
H A D | preARMScript.sml | 24 (* CPSR, In user programs only the top 4 bits of the CPSR are relevant *)
|