| /seL4-l4v-master/HOL4/examples/Crypto/RC6/ |
| H A D | RC6Script.sml | 154 (* should make sure that corresponding Round and InvRound use the same keys *)
198 (* that PreWhitening and PostWhitening use the same key pair *)
|
| /seL4-l4v-master/HOL4/examples/HolCheck/ |
| H A D | stringBinTree.sml | 56 (* append a string of the minimum character, of the same length as the longest key (mxl), to all keys *)
97 (* chars at index i are all the same *)
|
| H A D | decompScript.sml | 72 (* basic idea is that if f holds in some model then it should hold in the same model with extra ap's thrown in,
74 (* note: the assumptions on L and T are very strong only because ks1 and ks2 are more or less the same
77 noting that all ap must have the same semantics *)
|
| /seL4-l4v-master/seL4/src/machine/ |
| H A D | io.c | 134 }, { /* 6: z- or t-prefixed (assumed to be same size) */
286 * unspecified for other forms, do the same. Stop immediately
|
| /seL4-l4v-master/HOL4/polyml/libpolyml/ |
| H A D | x86assembly_gas64.S | 187 /* This is exactly the same as raisex but seems to be needed to work round a PIC problem. */
267 # This implements atomic subtraction in the same way as atomic_decrement
|
| /seL4-l4v-master/HOL4/polyml/basis/ |
| H A D | String.sml | 21 are simply different views on the same underlying structure.
462 if test = 0 (* If the strings are the same up to the shorter length ... *)
882 three octal digits in the same way as conversion to
994 (* If the size is the same we can return the original string.
1100 of handling this. We could implement arrays in the same
1114 val maxLen = String.maxSize (* Use the same maximum as string. *)
1209 the same but in that case diW must be zero and the copy is a no-op. *)
1501 This definition is almost the same as String.tokens and String.fields. *)
1632 (* Copy a slice into an array. N.B. The arrays could be the same. *)
1641 on the index whether the source and destination are the same o
[all...] |
| H A D | Real32.sml | 159 the same sign as the number even if it is zero. *)
211 (* Scan input source for a valid number. The format is the same as
|
| H A D | LargeWord.sml | 176 same form as negative integers. *)
275 (* If int is fixed precision an int is the same size as a word and will always fit within a
|
| /seL4-l4v-master/HOL4/examples/algebra/group/ |
| H A D | groupActionScript.sml | 294 val _ = set_fixity "act" (Infix(NONASSOC, 450)); (* same as relation *)
388 val _ = set_fixity "~~" (Infix(NONASSOC, 450)); (* same as relation *)
727 then orbit is same size as the group.
1152 (* Alternative form of the same theorem. *)
1160 (* Theorem: stabilizers of points in same orbit:
1292 (* Another formulation of the same result. *)
1351 (3) same as (1)
1406 (3) same as (1)
1911 (* Theorem: For (g act X) f, sing_orbits is the same size as fixed_points f g X,
|
| /seL4-l4v-master/HOL4/examples/algebra/field/ |
| H A D | fieldMapScript.sml | 297 val _ = set_fixity "~~~" (Infix(NONASSOC, 450)); (* same as relation *)
298 val _ = set_fixity "===" (Infix(NONASSOC, 450)); (* same as relation *)
299 val _ = set_fixity "~^~" (Infix(NONASSOC, 450)); (* same as relation *)
300 val _ = set_fixity "=^=" (Infix(NONASSOC, 450)); (* same as relation *)
463 (* This is the same as field_homo_trans. *)
476 (* This is the same as field_homo_sym. *)
756 (* This is the same as field_iso_trans. *)
769 (* This is the same as field_iso_sym. *)
1118 val _ = set_fixity "<<=" (Infixl 500); (* same as + in arithmeticScript.sml *)
|
| /seL4-l4v-master/seL4/manual/parts/ |
| H A D | objects.tex | 157 If there are no other runnable threads with the same priority as the caller,
213 the kernel does the same operation as \apifunc{seL4\_Send}{sel4_send}. What
228 slot in the replying thread's TCB. It has exactly the same behaviour as
482 objects must be of the same type, specified by the \texttt{type} argument. In
483 the case of variable-sized objects, each object must also be of the same size.
|
| /seL4-l4v-master/HOL4/examples/acl2/examples/LTL/ |
| H A D | LTLScript.sml | 446 ; n has the same set of successor states (with respect to vars).
450 ; vice-versa, where we consider two states to be the same if
451 ; they are the same when restricted to vars.
|
| /seL4-l4v-master/HOL4/examples/fermat/twosq/ |
| H A D | iterateScript.sml | 705 (* Another proof of the same theorem. *)
706 (* This is 'elementary' in the sense that LINV is not used, but same concept. *)
842 (* Idea: all elements in the orbit have the same period. *)
|
| /seL4-l4v-master/isabelle/src/Doc/Tutorial/document/ |
| H A D | sets.tex | 32 all elements have the same type, say~$\tau$, and the set itself has type
99 This is the same example using \textsc{ascii} syntax, illustrating a pitfall:
121 same elements. This is
368 is displayed. For example, \isa{Collect\ P} is the same term as
369 \isa{\isacharbraceleft x.\ P\ x\isacharbraceright}. The same thing can
821 applying the introduction rules shown above. The same proof script handles
|
| /seL4-l4v-master/l4v/isabelle/src/Doc/Tutorial/document/ |
| H A D | sets.tex | 32 all elements have the same type, say~$\tau$, and the set itself has type
99 This is the same example using \textsc{ascii} syntax, illustrating a pitfall:
121 same elements. This is
368 is displayed. For example, \isa{Collect\ P} is the same term as
369 \isa{\isacharbraceleft x.\ P\ x\isacharbraceright}. The same thing can
821 applying the introduction rules shown above. The same proof script handles
|
| /seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/ParseTree/ |
| H A D | MATCH_COMPILER.sml | 251 (* A new wild card entry with the same defaults as a previous entry. *)
379 (* Two exceptions can only be considered the same if they are both
380 constants and the same value. *)
548 (* At the same time we have to get the equality function
752 (* Singleton tuple - this is just the same as the field. *)
816 (* We now process exception constructors in the same way as datatype constructors.
|
| /seL4-l4v-master/HOL4/examples/formal-languages/lambek/ |
| H A D | ExampleScript.sml | 69 (* same proof, done automatically *)
486 CONJ_TAC \\ (* 2 sub-goals, same tacticals *)
|
| /seL4-l4v-master/HOL4/src/1/ |
| H A D | Mutual.sml | 90 (* the same structure as the input term tm, will do a *)
156 (* then applying tac to the goal A,"!n. P[n] ==> P[SUC n] has the same *)
|
| H A D | dep_rewrite.sig | 67 (* remove duplicates; thus, several theorems with the same *)
68 (* hypothesis, or several uses of the same theorem, will generate *)
|
| /seL4-l4v-master/HOL4/src/integer/ |
| H A D | CooperSyntax.sml | 212 their free variables bound by binders higher in the same term
471 the same on the RHS of the theorem returned *)
|
| /seL4-l4v-master/HOL4/Manual/Description/ |
| H A D | holCheck.tex | 183 For our running example, we use \texttt{ttt.sml} from \texttt{src/HolCheck/examples}. Build this (and others\footnote{The AMBA examples are large and take a while to build. To skip them, see the README file in the same folder.}) by typing \texttt{Holmake} in \texttt{src/HolCheck/examples}. Now start \HOL{} from this directory (or use the -I command-line parameter).
201 The function takes a \hc{} model as an argument, and returns a model which is the same as the argument, but additionally contains the results of the model checking. We now describe how a \hc{} model is constructed.
254 \(\mathtt{nm}\) is an optional argument when constructing the model (hence it is stored internally as an option type). It is a string that names the formal model that is generated internally by \hc{}. Since the resulting theorems are stated in terms of this model, it is useful to have an abbreviation for the term representing the model to keep the theorem statement readable. \hc{} has a default name for models, but if the user expects to be using more than one model in the same session, then setting a name is required to avoid name clashes.
353 \(\mathtt{holCheck}\) returns another model. This model is exactly the same as \texttt{ttt1}, except that it now contains the results of the model checking. These are recovered via the function \texttt{holCheckLib.get\_results}, and return a list in which the n\({}^{th}\) element gives the results of model checking the n\({}^{th}\) property in the list returned by \texttt{holCheckLib.get\_props}. \texttt{holCheckLib.get\_results} returns an option type, since no results are known before model checking takes place.
379 The second result corresponds to a win position for A. Since the initial state is not a win position for A, there is no success theorem and as before counterexamples are only provided for properties talking about paths. The third result is exactly the same, since the initial state is not a win position for B either.
404 The last result is the same as the second and third, since B does not have a winning strategy, and counterexamples cannot be calculated for properties that assert the existence of specific paths (since the ``counterexample'' would effectively be the entire set of reachable states).\index{holCheckLib!traces}
415 This returns a model that is exactly the same as \texttt{ttt2}, except that any assumptions introduced due to the postponed proof have been discharged. We can confirm this by looking at say, the first property, again.
568 \texttt{prove\_model}\index{holCheckLib!ML bindings!prove\_model@\ml{prove\_model}} must be used in the same session in which the model checking was done, if the produced theorems are going to be written to permanent storage. This is because the lazy proof machinery is unable to persist lazy theorems, owing to Moscow ML's inability to persist closures.
|
| /seL4-l4v-master/HOL4/Manual/Translations/IT/Description/ |
| H A D | holCheck.tex | 183 For our running example, we use \texttt{ttt.sml} from \texttt{src/HolCheck/examples}. Build this (and others\footnote{The AMBA examples are large and take a while to build. To skip them, see the README file in the same folder.}) by typing \texttt{Holmake} in \texttt{src/HolCheck/examples}. Now start \HOL{} from this directory (or use the -I command-line parameter).
201 The function takes a \hc{} model as an argument, and returns a model which is the same as the argument, but additionally contains the results of the model checking. We now describe how a \hc{} model is constructed.
254 \(\mathtt{nm}\) is an optional argument when constructing the model (hence it is stored internally as an option type). It is a string that names the formal model that is generated internally by \hc{}. Since the resulting theorems are stated in terms of this model, it is useful to have an abbreviation for the term representing the model to keep the theorem statement readable. \hc{} has a default name for models, but if the user expects to be using more than one model in the same session, then setting a name is required to avoid name clashes.
353 \(\mathtt{holCheck}\) returns another model. This model is exactly the same as \texttt{ttt1}, except that it now contains the results of the model checking. These are recovered via the function \texttt{holCheckLib.get\_results}, and return a list in which the n\({}^{th}\) element gives the results of model checking the n\({}^{th}\) property in the list returned by \texttt{holCheckLib.get\_props}. \texttt{holCheckLib.get\_results} returns an option type, since no results are known before model checking takes place.
379 The second result corresponds to a win position for A. Since the initial state is not a win position for A, there is no success theorem and as before counterexamples are only provided for properties talking about paths. The third result is exactly the same, since the initial state is not a win position for B either.
404 The last result is the same as the second and third, since B does not have a winning strategy, and counterexamples cannot be calculated for properties that assert the existence of specific paths (since the ``counterexample'' would effectively be the entire set of reachable states).\index{holCheckLib!traces}
415 This returns a model that is exactly the same as \texttt{ttt2}, except that any assumptions introduced due to the postponed proof have been discharged. We can confirm this by looking at say, the first property, again.
568 \texttt{prove\_model}\index{holCheckLib!ML bindings!prove\_model@\ml{prove\_model}} must be used in the same session in which the model checking was done, if the produced theorems are going to be written to permanent storage. This is because the lazy proof machinery is unable to persist lazy theorems, owing to Moscow ML's inability to persist closures.
|
| /seL4-l4v-master/HOL4/examples/ARM_security_properties/ |
| H A D | MMU_SetupScript.sml | 276 (* lemma: same setup --> same access rights *)
|
| /seL4-l4v-master/HOL4/src/quantHeuristics/ |
| H A D | quantHeuristicsTools.sml | 330 * variables in fvL. Similar VARIANT_TAC does the same for
626 * [``x'``, ``x'``, ``y``] (both the same!!!)
|
| /seL4-l4v-master/HOL4/examples/algebra/polynomial/ |
| H A D | polynomialScript.sml | 180 val _ = set_fixity "||" (Infixl 500); (* same as + in arithmeticScript.sml *)
221 (* Power multiplication of a polynomial, i.e. x^n * (polynomial in x), same as shifting. *)
|