Searched refs:witness (Results 1 - 25 of 50) sorted by relevance

12

/seL4-l4v-10.1.1/HOL4/src/num/arith/src/
H A DExists_arith.sml76 (* a witness for the formula in the form of a variable-name/value binding. *)
89 (* witness : term list -> (string * int) list *)
91 (* Function to find a witness for a formula from the disjuncts of a *)
95 fun witness tml = function
97 then failwith "witness"
98 else Shostak (coeffs_of_leq_set (hd tml)) handle _ => (witness (tl tml));
122 in (let val binding = witness (strip_disj (rhs (concl th)))
/seL4-l4v-10.1.1/HOL4/examples/miller/miller/
H A Dmiller_rabinScript.sml106 val witness_def = Define `witness n a
116 in (~witness n (a + 2), s')`;
235 ``!n a. 0 < a /\ a < n /\ witness n a ==> ~prime n``,
237 >> Q.PAT_X_ASSUM `witness n a` MP_TAC
331 ``!n. 1 < n ==> ~witness n 1``,
341 1 < n /\ ODD n /\ 0 < a /\ a < n /\ ~witness n a ==>
357 1 < n /\ ODD n /\ 0 < a /\ a < n /\ ~witness n a /\ ODD s /\
377 1 < n /\ ODD n /\ 0 < a /\ a < n /\ ~witness n a ==>
388 (n - 1) <= 2 * CARD {a | 0 < a /\ a < n /\ witness n a}``,
390 >> Suff `2 * CARD (\a. 0 < a /\ a < n /\ ~witness
[all...]
/seL4-l4v-10.1.1/HOL4/examples/muddy/muddyC/buddy/src/
H A Dprime.c158 static int isWitness(unsigned int witness, unsigned int src) argument
174 d = u64_mulmod(d,witness,src);
187 unsigned int witness = Random(src-1); local
189 if (isWitness(witness,src))
/seL4-l4v-10.1.1/HOL4/examples/acl2/examples/acl2-hol-ltl-paper-example/
H A DLTLScript.sml243 2. Witness s1' as (c-bisimilar-transition-witness-m->n s s1 M s' M' vars)
245 c-bisimilar-witness-member-of-states-m->n
248 c-bisimilar-witness-produces-bisimilar-states-m->n
251 3. Witness s1 as (c-bisimilar-transition-witness-n->m s M s' s1' M' vars)
253 c-bisimilar-witness-member-of-states-n->m
256 c-bisimilar-witness-produces-bisimilar-states-n->m
302 2. s0' is (c-bisimilar-initial-state-witness-m->n s0 M M' vars);
310 3. s0 is (c-bisimilar-initial-state-witness-n->m M s0' M' vars)
H A DsexpScript.sml1173 (* pkg-witness *)
1176 (* (defun-*1* pkg-witness (pkg) *)
1180 (* (intern *pkg-witness-name* pkg) *)
1181 (* (throw-raw-ev-fncall (list 'pkg-witness-er pkg))) *)
1182 (* (gv pkg-witness (pkg) (intern *pkg-witness-name* "ACL2")) *)
1184 (* ; Here, we treat the ACL2 constant *pkg-witness-name* as its value, *)
1189 (* ; Note that ACL2 refuses to parse (pkg-witness pkg) unless pkg is an *)
1196 (* ; (where pkg-witness was introduced) up through 3.0.1. That bug has been *)
/seL4-l4v-10.1.1/HOL4/examples/acl2/examples/
H A Dmiller-rabin.sml257 `witness n a =
265 (exists_witness n (hd::tl) = witness n hd \/ exists_witness n tl)`;
268 ``!n l. EXISTS (witness n) l = exists_witness n l``,
277 else ~(EXISTS (witness n) l)`;
373 (miller_rabin_list n [x] = ~witness n x)``,
415 (BIND (miller_rabin_uniform n) (\a. UNIT (~witness n a))) T m)``,
423 (\a. UNIT (~witness n a))) (miller_rabin_list n q) m`
445 (many (BIND (miller_rabin_uniform n) (\a. UNIT (~witness n a))) m =
/seL4-l4v-10.1.1/HOL4/src/0/
H A DKernelTypes.sml58 datatype witness = TERM of term | THEOREM of thm type
/seL4-l4v-10.1.1/HOL4/examples/acl2/examples/LTL/
H A DLTLScript.sml420 2. Witness s1' as (c-bisimilar-transition-witness-m->n s s1 M s' M' vars)
422 c-bisimilar-witness-member-of-states-m->n
425 c-bisimilar-witness-produces-bisimilar-states-m->n
428 3. Witness s1 as (c-bisimilar-transition-witness-n->m s M s' s1' M' vars)
430 c-bisimilar-witness-member-of-states-n->m
433 c-bisimilar-witness-produces-bisimilar-states-n->m
479 2. s0' is (c-bisimilar-initial-state-witness-m->n s0 M M' vars);
487 3. s0 is (c-bisimilar-initial-state-witness-n->m M s0' M' vars)
772 s-expression witness for the existentially quantified variable B
/seL4-l4v-10.1.1/HOL4/src/coretypes/
H A DpairLib.sml172 val witness = mk_pselect (vs,body) value
173 val eqs = varstruct_to_eqs witness vs
/seL4-l4v-10.1.1/HOL4/src/HolQbf/
H A DQbfCertificate.sml248 replace references to v by references to v's witness (extension) variable.
249 If v has no witness, replace references to v by references to T,
251 For example, if v has no witness:
259 TFk is the continuation for when l has no witness.
262 vk is the continuation for when l has a witness.
263 vk is passed the literal of the witness,
264 and s with the index of the witness added *)
/seL4-l4v-10.1.1/HOL4/examples/acl2/ml/
H A DsexpScript.sml1173 (* pkg-witness *)
1176 (* (defun-*1* pkg-witness (pkg) *)
1180 (* (intern *pkg-witness-name* pkg) *)
1181 (* (throw-raw-ev-fncall (list 'pkg-witness-er pkg))) *)
1182 (* (gv pkg-witness (pkg) (intern *pkg-witness-name* "ACL2")) *)
1184 (* ; Here, we treat the ACL2 constant *pkg-witness-name* as its value, *)
1189 (* ; Note that ACL2 refuses to parse (pkg-witness pkg) unless pkg is an *)
1196 (* ; (where pkg-witness was introduced) up through 3.0.1. That bug has been *)
H A Dmake_sexp.ml899 (* pkg-witness *)
902 (* (defun-*1* pkg-witness (pkg) *)
906 (* (intern *pkg-witness-name* pkg) *)
907 (* (throw-raw-ev-fncall (list 'pkg-witness-er pkg))) *)
908 (* (gv pkg-witness (pkg) nil))) *)
910 (* ; Here, we treat the ACL2 constant *pkg-witness-name* as its value, *)
915 (* ; Note that ACL2 refuses to parse (pkg-witness pkg) unless pkg is an *)
/seL4-l4v-10.1.1/HOL4/src/datatype/mutrec/
H A DMutRecDef.sml72 is_closed determines whether there is a witness for each type in the
81 (fn {type_name, witness = {name,arg_info}} => type_name = tyname)
120 General Case: We need to try to find a witness for a type being defined.
123 world). If we find such a constructor, it is a witness, and so we put it
135 val witness = find value
141 case witness
154 {type_name = type_name,witness = constr} ::
420 {type_name, witness = {arg_info,name}}
434 val witness = value
437 val tac = (EXISTS_TAC witness) THE
[all...]
/seL4-l4v-10.1.1/HOL4/examples/acl2/examples/M1/
H A DsexpScript.sml1173 (* pkg-witness *)
1176 (* (defun-*1* pkg-witness (pkg) *)
1180 (* (intern *pkg-witness-name* pkg) *)
1181 (* (throw-raw-ev-fncall (list 'pkg-witness-er pkg))) *)
1182 (* (gv pkg-witness (pkg) (intern *pkg-witness-name* "ACL2")) *)
1184 (* ; Here, we treat the ACL2 constant *pkg-witness-name* as its value, *)
1189 (* ; Note that ACL2 refuses to parse (pkg-witness pkg) unless pkg is an *)
1196 (* ; (where pkg-witness was introduced) up through 3.0.1. That bug has been *)
/seL4-l4v-10.1.1/HOL4/src/datatype/
H A DEnumType.sml195 val witness = let value
206 (mk_eq(mk_comb(witness, constr), alphavar n)))
213 val clauses = subst [witness |-> f] (concl clauses_thm)
215 val exists_thm = EXISTS(mk_exists(f, clauses), witness) clauses_thm
H A Dind_typeScript.sml181 let val (pred, witness) = dest_comb(concl thm)
186 (mk_exists(x, mk_comb(pred, x)),witness) thm
/seL4-l4v-10.1.1/HOL4/examples/fsub/
H A Dkernel_subtypingScript.sml153 val witness = hd args value
154 val ex_thm = EXISTS (pattern, witness) th
H A Dfull_subtypingScript.sml468 val witness = hd args value
469 val ex_thm = EXISTS (pattern, witness) th
H A DfsubtypesScript.sml60 the witness *)
/seL4-l4v-10.1.1/HOL4/examples/imperative/
H A DreflectOnFailure.sml218 Finally, we need to provide a witness for s that proves the original specification is violated.
/seL4-l4v-10.1.1/HOL4/examples/ind_def/
H A DalgebraScript.sml224 (* proofs of TRANSIT P A Q and TERMINAL Q. The user supplies a witness *)
/seL4-l4v-10.1.1/HOL4/examples/theorem-prover/milawa-prover/
H A Dmilawa_logicScript.sml60 - witness function for a certain expression and variable name. *)
89 | (* expression, variable name, and semantic witness function *)
195 defining equation and witness functions must return a value that
544 (* User witness function definitions *)
545 (!f params exp var_name witness ctxt.
546 f IN FDOM ctxt /\ (ctxt ' f = (params,WITNESS_FUN exp var_name,witness)) ==>
1162 THEN1 (* user-defined witness function *)
2166 (Q.ABBREV_TAC `witness = \args. @v. isTrue (EvalTerm (FunVarBind (s::params) (v::args),ctxt) l)`
2187 \\ Q.UNABBREV_TAC `witness` \\ FULL_SIMP_TAC std_ss [] \\ METIS_TAC [])
/seL4-l4v-10.1.1/HOL4/src/postkernel/
H A DTheory.sml517 * declared in the current theory and its witness is up-to-date.
532 * to recursively examine its witness(es). We can't just accept a witness
538 * dynamic programming. It holds the value "true" when the witness is
/seL4-l4v-10.1.1/HOL4/Manual/Description/
H A DholCheck.tex143 The result is a list of triples, one triple per property checked. The first component contains the BDD representation of the set of states satisfying the property. The second component contains a theorem certifying that the property holds in the model i.e.\ it holds in the initial states. The third contains a witness trace that counts up to 4, at which point v2 goes high.
355 Each element is a triple of the form \( (term\_bdd,thm,trace) \).\footnote{A \(\textup{term\_bdd}\) is an ML value that contains a \HOL{} term together with its boolean semantics represented as a BDD (see the \texttt{HolBddLib} documentation for details).} These are the BDD semantics of the property, a theorem certifying the property holds (if it does) and a counterexample or witness trace, if one could be recovered.
371 This is the result corresponding to the first property (which described the set of initial states). The first component is the \(\textup{term\_bdd}\) that corresponds to the set of states of the model satsified by this property. As expected, the set of initial states is contained in the set of initial states and thus the second component is a success theorem attesting to this. The predicate \( \mathtt{CTL\_MODEL\_SAT} \)\index{holCheckLib!CTLMODELSAT@\ml{CTL\_MODEL\_SAT}} says that the property holds in the formal model \( \mathtt{ctlKS\_ttt}\). If the property had not held, the theorem derivation would have failed and the component would have been \( \mathtt{NONE}\). The third component is used to return the counterexample or witness associated with the property. Since we succeeded there is no counterexample, and witnesses are only returned for properties talking about paths, so this component is \( \mathtt{NONE}\). Note that the theorem has some assumptions associated with it. We shall return to these later.
402 This result corresponds to the fourth property, that stated that A has a winning strategy. This is true, and we get the success theorem, as well as a witness, which shows that there is such a path from the initial state.
556 The generation of witness traces for properties of the form \(\mathbf{EG} f \) (or dually, counterexamples for \(\mathbf{AF} f \) style properties) leaves much to be desired: it tries to give the shortest qualifying path which usually turns out to be just the initial state, whereas typically the user is interested in the longest one.
/seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Description/
H A DholCheck.tex143 The result is a list of triples, one triple per property checked. The first component contains the BDD representation of the set of states satisfying the property. The second component contains a theorem certifying that the property holds in the model i.e. it holds in the initial states. The third contains a witness trace that counts up to 4, at which point v2 goes high.
355 Each element is a triple of the form \( (term\_bdd,thm,trace) \).\footnote{A \(\textup{term\_bdd}\) is an ML value that contains a \HOL{} term together with its boolean semantics represented as a BDD (see the \texttt{HolBddLib} documentation for details).} These are the BDD semantics of the property, a theorem certifying the property holds (if it does) and a counterexample or witness trace, if one could be recovered.
371 This is the result corresponding to the first property (which described the set of initial states). The first component is the \(\textup{term\_bdd}\) that corresponds to the set of states of the model satsified by this property. As expected, the set of initial states is contained in the set of initial states and thus the second component is a success theorem attesting to this. The predicate \( \mathtt{CTL\_MODEL\_SAT} \)\index{holCheckLib!CTLMODELSAT@\ml{CTL\_MODEL\_SAT}} says that the property holds in the formal model \( \mathtt{ctlKS\_ttt}\). If the property had not held, the theorem derivation would have failed and the component would have been \( \mathtt{NONE}\). The third component is used to return the counterexample or witness associated with the property. Since we succeeded there is no counterexample, and witnesses are only returned for properties talking about paths, so this component is \( \mathtt{NONE}\). Note that the theorem has some assumptions associated with it. We shall return to these later.
402 This result corresponds to the fourth property, that stated that A has a winning strategy. This is true, and we get the success theorem, as well as a witness, which shows that there is such a path from the initial state.
556 The generation of witness traces for properties of the form \(\mathbf{EG} f \) (or dually, counterexamples for \(\mathbf{AF} f \) style properties) leaves much to be desired: it tries to give the shortest qualifying path which usually turns out to be just the initial state, whereas typically the user is interested in the longest one.

Completed in 362 milliseconds

12