/seL4-l4v-master/HOL4/examples/elliptic/ |
H A D | ellipticScript.sml | 1511 fun compilable_multiword_operations words bits = 1517 fun compilable_curve_operations prime words bits = 1519 val {inject,add,mod,...} = compilable_multiword_operations words bits
|
/seL4-l4v-master/HOL4/examples/simple_complexity/lib/ |
H A D | bitsizeScript.sml | 409 (* Define number of bits of a number, recursively. *) 579 For powers of 2, say, n = 8 = 2 ** 3, 3 bits can represent 8 binaries, from 000 to 111, or 0 to 7. 580 The number 8 itself in binary is 1000, with 4 bits, 1 bit more than what the exponent indicates.
|
/seL4-l4v-master/HOL4/src/n-bit/ |
H A D | alignmentScript.sml | 453 Theorems for standard alignment lengths of 1, 2 and 3 bits
|
/seL4-l4v-master/HOL4/src/simp/src/ |
H A D | Cache.sml | 109 irrelevants bits of the assumptions.
|
/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/HolCheck/ |
H A D | bddTools.sml | 38 (* and it would be inefficient to unwind the higher order bits *)
|
/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],
|
/seL4-l4v-master/HOL4/polyml/mlsource/extra/Win/ |
H A D | DeviceBase.sml | 286 (* These bits indicate the valid fields in the structure. *)
|
H A D | DeviceContext.sml | 472 val BITSPIXEL = W (12 (* Number of bits per pixel *))
|
/seL4-l4v-master/HOL4/polyml/basis/ |
H A D | Real32.sml | 24 on the X87 is set to 64-bits which is correct for the Real.real operations
|
H A D | LargeWord.sml | 162 val wordSize = bitsInWord - 1 (* 31 or 63 bits *)
|
H A D | Real.sml | 169 32-bits). That will convert all the bits of the mantissa
|
/seL4-l4v-master/HOL4/polyml/ |
H A D | config.guess | 666 long bits = sysconf(_SC_KERNEL_BITS); 676 switch (bits)
|
/seL4-l4v-master/seL4/manual/parts/ |
H A D | threads.tex | 343 For some registers, the kernel will silently mask certain bits or ranges of bits off, and force them to contain certain 570 occured. & \ipcbloc{seL4\_TimeoutFault\_Data} \\ Upper 32-bits of 572 \ipcbloc{seL4\_TimeoutFault\_Consumed} \\ Lower 32-bits of microseconds
|
/seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/arm/ |
H A D | prog_armLib.sml | 67 val bits = collect_term_of_type ``:arm_bit`` g value 110 val pre_post = map mk_pre_post_assertion (regs @ bits @ mems)
|
/seL4-l4v-master/l4v/isabelle/src/Doc/Nitpick/document/ |
H A D | root.tex | 457 binary notation, the number of bits to use can be specified using 458 the \textit{bits} option. For example: 461 \textbf{nitpick} [\textit{binary\_ints}, \textit{bits}${} = 16$] 1893 is specified by the \textit{bits} (\S\ref{scope-of-search}) option. By default, 1902 {\small See also \textit{bits} (\S\ref{scope-of-search}) and 1905 \opdefault{bits}{int\_seq}{\upshape 1--10} 1906 Specifies the number of bits to use to represent natural numbers and integers in
|
/seL4-l4v-master/isabelle/src/Doc/Nitpick/document/ |
H A D | root.tex | 457 binary notation, the number of bits to use can be specified using 458 the \textit{bits} option. For example: 461 \textbf{nitpick} [\textit{binary\_ints}, \textit{bits}${} = 16$] 1893 is specified by the \textit{bits} (\S\ref{scope-of-search}) option. By default, 1902 {\small See also \textit{bits} (\S\ref{scope-of-search}) and 1905 \opdefault{bits}{int\_seq}{\upshape 1--10} 1906 Specifies the number of bits to use to represent natural numbers and integers in
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/common/ |
H A D | stateLib.sml | 1618 val bits = List.map bitstringSyntax.mk_b o value 1625 | NONE => bits (wordsSyntax.uint_of_word tm) 1629 SOME i => bits i
|
/seL4-l4v-master/HOL4/examples/dev/ |
H A D | vsynth.sml | 405 (* Default: 32-bits wide, initial value = 1. *)
|
/seL4-l4v-master/HOL4/src/metis/ |
H A D | mlibClause.sml | 207 type bits = {parm : parameters, id : int, thm : thm, order : termorder}; type
|
/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/diningcryptos/ |
H A D | basic_leakage_examplesScript.sml | 202 (* 2 BITS: match of bits of h1 and h2 *)
|
/seL4-l4v-master/HOL4/examples/AKS/theories/ |
H A D | AKSmapsScript.sml | 1819 Step 0: useful bits 2301 Step 0: some useful bits, show h <= t and 0 < t 2380 Step 0: some useful bits, show q <= t and 0 < t 2586 Step 0: some useful bits, show q <= t and 0 < t
|