/seL4-l4v-10.1.1/HOL4/examples/formal-languages/regular/regular-play/test/data/ |
H A D | gen.py | 3 import random namespace 11 sys.stdout.write(random.choice(s)) #string.printable
|
/seL4-l4v-10.1.1/HOL4/examples/diningcryptos/ |
H A D | leakageScript.sml | 110 `unif_prog_dist high low random = 111 (\s. if s IN (high CROSS low) CROSS random then 112 1/(&(CARD ((high CROSS low) CROSS random))) else 0)`; 116 `unif_prog_space high low random = 117 ((high CROSS low) CROSS random, 118 POW ((high CROSS low) CROSS random), 119 (\s. SIGMA (unif_prog_dist high low random) s))`; 136 ``!high low random. FINITE high /\ FINITE low /\ FINITE random /\ 137 ~((high CROSS low) CROSS random [all...] |
H A D | basic_leakage_examplesScript.sml | 141 val random = Define value 142 `random = {(\s:string. (0:num))}`; 148 val example1_conv = SIMP_CONV arith_ss [high, low, random, lem1,lem2,lem3]; 152 ``leakage (unif_prog_space (high (SUC (SUC (SUC 0)))) (low (SUC (SUC (SUC 0)))) random) M1 = 2``, 156 ``random``) 157 [high, low, random, lem1, lem2, lem3] 181 val example2_input_conv = SIMP_CONV arith_ss [high, low, random, lem1,lem2,lem3]; 185 ``leakage (unif_prog_space (high (SUC (SUC (SUC 0)))) (low (SUC (SUC (SUC 0)))) random) M2 = 2``, 189 ``random``) 190 [high, low, random, lem 223 val random = Define value 327 val random = Define value 378 val random = Define value 415 val random = Define value [all...] |
H A D | leakageLib.sml | 73 val unif_prog_space_leakage_computation_reduce_COMPUTE = prove (``!high low random f. FINITE high /\ FINITE low /\ FINITE random /\ ~((high CROSS low) CROSS random={}) ==> (leakage (unif_prog_space high low random) f = (1/(&(CARD high * CARD low * CARD random)))* (SIGMA (\(out,h,l). (\x. x * lg (((1/(&(CARD random)))* x))) (SIGMA (\r. if (f((h,l),r)=out) then 1 else 0) random)) 74 (IMAGE (\s. (f s,FST s)) (high CROSS low CROSS random)) - 75 SIGMA (\(out,l). (\x. x * lg (((1/(&(CARD high * CARD random)))* x))) 76 (SIGMA (\(h,r). if (f((h,l),r)=out) then 1 else 0) (high CROSS random))) [all...] |
/seL4-l4v-10.1.1/HOL4/src/portableML/poly/ |
H A D | Random.sig | 1 (* Random -- random number generator *) 9 val random : generator -> real value 17 [generator] is the type of random number generators, here the 20 [newgenseed seed] returns a random number generator with the given seed. 22 [newgen ()] returns a random number generator, taking the seed from 25 [random gen] returns a random number in the interval [0..1). 27 [randomlist (n, gen)] returns a list of n random numbers in the 30 [range (min, max) gen] returns an integral random number in the 33 [rangelist (min, max) (n, gen)] returns a list of n integral random [all...] |
H A D | Random.sml | 7 (* Generating random numbers. Paulson, page 96 *) 38 fun random {seedref} = function
|
/seL4-l4v-10.1.1/HOL4/examples/miller/prob/ |
H A D | prob_pseudoScript.sml | 8 (* The definition of the pseudo-random number generator. *) 15 (* Theorems to allow pseudo-random bits to be computed. *)
|
H A D | prob_pseudoTools.sml | 2 (* Coversions for evaluating the pseudo-random number generator. *) 18 congruence pseudo-random bit generator.
|
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
H A D | Random.sml | 4 Simple generator for pseudo-random numbers, using unboxed word 12 (* random words: 0w0 <= result <= max_word *) 22 see http://random.mat.sbg.ac.at/~charly/server/server.html*) 30 (*NB: higher bits are more random than lower ones*) 34 (* random integers: 0 <= result < k *) 43 (* random reals: 0.0 <= result < 1.0 *)
|
H A D | Random.sig | 4 Simple generator for pseudo-random numbers, using unboxed word
|
H A D | Portable.sig | 28 (* Generating random values. *)
|
H A D | PortablePolyml.sml | 28 (* Generating random values. *)
|
H A D | PortableMosml.sml | 32 (* Generating random values. *) 40 fun randomReal () = Random.random gen;
|
H A D | Model.sig | 197 (* A type of random finite models. *) 229 (* Check whether random groundings of a formula are true in the model. *) 260 (* Choosing a random perturbation to make a formula true in the model. *)
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Random.sml | 4 Simple generator for pseudo-random numbers, using unboxed word 12 (* random words: 0w0 <= result <= max_word *) 22 see http://random.mat.sbg.ac.at/~charly/server/server.html*) 30 (*NB: higher bits are more random than lower ones*) 34 (* random integers: 0 <= result < k *) 43 (* random reals: 0.0 <= result < 1.0 *)
|
H A D | Random.sig | 4 Simple generator for pseudo-random numbers, using unboxed word
|
H A D | Portable.sig | 28 (* Generating random values. *)
|
H A D | PortablePolyml.sml | 28 (* Generating random values. *)
|
H A D | PortableMosml.sml | 32 (* Generating random values. *) 40 fun randomReal () = Random.random gen;
|
H A D | Model.sig | 197 (* A type of random finite models. *) 229 (* Check whether random groundings of a formula are true in the model. *) 260 (* Choosing a random perturbation to make a formula true in the model. *)
|
/seL4-l4v-10.1.1/HOL4/src/integer/testing/ |
H A D | gen_bc_problem.sml | 20 val r = Random.random gen 27 val r = Random.random gen
|
H A D | genproblem.sml | 10 val r = Random.random gen 19 val r = Random.random gen 29 val r = Random.random gen
|
/seL4-l4v-10.1.1/HOL4/src/1/ |
H A D | MakeBigTerm.sml | 7 val n = Random.random gen 19 if Random.random gen < 0.5 andalso not (null bvs) then 34 if Random.random gen < 0.5 then (sz1, sz2) else (sz2, sz1) 43 val n = Random.random gen 72 val n = Random.random gen
|
/seL4-l4v-10.1.1/HOL4/src/metis/ |
H A D | mlibModel.sig | 44 (* Check whether a random grounding of a formula is satisfied by the model *) 49 (* Try to make formulas true by applying random perturbations to the model *)
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm8/prog/ |
H A D | arm8_progLib.sml | 722 val random = random_hex o Option.valOf o arm8_stepLib.arm8_pattern 724 val hex = List.map random arm8_stepLib.arm8_names 745 arm8_spec_hex (random "AddSubShiftedRegister32-1") 746 arm8_spec_hex (random "BranchRegisterJMP") 747 arm8_spec_hex (random "LoadStoreImmediate-1-1") 748 arm8_spec_hex (random "LoadStoreImmediate-1-2") 749 arm8_spec_hex (random "LoadStoreImmediate-1-3") 750 arm8_spec_hex (random "LoadStoreImmediate-1-4") 751 arm8_spec_hex (random "LoadStoreImmediate-2-3") 752 arm8_spec_hex (random "LoadStoreImmediat [all...] |