Searched refs:random (Results 1 - 25 of 87) sorted by relevance

1234

/seL4-l4v-10.1.1/HOL4/examples/formal-languages/regular/regular-play/test/data/
H A Dgen.py3 import random namespace
11 sys.stdout.write(random.choice(s)) #string.printable
/seL4-l4v-10.1.1/HOL4/examples/diningcryptos/
H A DleakageScript.sml110 `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 Dbasic_leakage_examplesScript.sml141 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 DleakageLib.sml73 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 DRandom.sig1 (* 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 DRandom.sml7 (* Generating random numbers. Paulson, page 96 *)
38 fun random {seedref} = function
/seL4-l4v-10.1.1/HOL4/examples/miller/prob/
H A Dprob_pseudoScript.sml8 (* The definition of the pseudo-random number generator. *)
15 (* Theorems to allow pseudo-random bits to be computed. *)
H A Dprob_pseudoTools.sml2 (* 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 DRandom.sml4 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 DRandom.sig4 Simple generator for pseudo-random numbers, using unboxed word
H A DPortable.sig28 (* Generating random values. *)
H A DPortablePolyml.sml28 (* Generating random values. *)
H A DPortableMosml.sml32 (* Generating random values. *)
40 fun randomReal () = Random.random gen;
H A DModel.sig197 (* 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 DRandom.sml4 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 DRandom.sig4 Simple generator for pseudo-random numbers, using unboxed word
H A DPortable.sig28 (* Generating random values. *)
H A DPortablePolyml.sml28 (* Generating random values. *)
H A DPortableMosml.sml32 (* Generating random values. *)
40 fun randomReal () = Random.random gen;
H A DModel.sig197 (* 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 Dgen_bc_problem.sml20 val r = Random.random gen
27 val r = Random.random gen
H A Dgenproblem.sml10 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 DMakeBigTerm.sml7 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 DmlibModel.sig44 (* 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 Darm8_progLib.sml722 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...]

Completed in 132 milliseconds

1234