Searched refs:a3 (Results 1 - 25 of 55) sorted by relevance

123

/seL4-l4v-master/seL4/src/arch/riscv/machine/
H A Dregisterset.c12 a2, a3, a4, a5
29 a0, a1, a2, a3, a4, a5, a6, a7,
/seL4-l4v-master/seL4/include/arch/riscv/arch/machine/
H A Dregisterset.h40 a3 = 12, enumerator in enum:_register
145 [seL4_UnknownSyscall_A3] = a3,\
172 [seL4_TimeoutReply_a3] = a3, \
/seL4-l4v-master/HOL4/examples/elliptic/
H A Delliptic_exampleScript.sml231 let a3 = ex1_field_elt example1_curve.a3
236 let y = ~y1 - a1 * x1 - a3
250 let a3 = ex1_field_elt example1_curve.a3 in
256 let d = & 2 * y1 + a1 * x1 + a3
260 let m = (~(x1 ** 3w) + a4 * x1 + & 2 * a6 - a3 * y1) / d in
262 let y = ~(l + a1) * x - m - a3
278 let a3 = ex1_field_elt example1_curve.a3 i
[all...]
H A DellipticScript.sml478 a3 : 'a;
502 let a3 = e.a3 in
504 a1 * a3 + & 2 * a4`;
513 let a3 = e.a3 in
515 a3 ** 2 + & 4 * a6`;
527 let a3 = e.a3 in
530 a1 ** 2 * a6 + & 4 * a2 * a6 - a1 * a3 * a
[all...]
/seL4-l4v-master/seL4/libsel4/arch_include/riscv/sel4/arch/
H A Dtypes.h50 seL4_Word a3; member in struct:seL4_UserContext_
/seL4-l4v-master/HOL4/examples/l3-machine-code/mips/step/
H A Dmips_stepScript.sml272 `!a0: word8 a1: word8 a2: word8 a3: word8 a4: word8 a5: word8 a6: word8
274 let w = a7 @@ a6 @@ a5 @@ a4 @@ a3 @@ a2 @@ a1 @@ a0
279 ((31 >< 0) w = (a3 @@ a2 @@ a1 @@ a0) : word32) /\
280 ((39 >< 0) w = (a4 @@ a3 @@ a2 @@ a1 @@ a0) : 40 word) /\
281 ((47 >< 0) w = (a5 @@ a4 @@ a3 @@ a2 @@ a1 @@ a0) : word48) /\
282 ((55 >< 0) w = (a6 @@ a5 @@ a4 @@ a3 @@ a2 @@ a1 @@ a0) : 56 word) /\
288 ((31 >< 8) w = (a3 @@ a2 @@ a1) : word24) /\
289 ((31 >< 16) w = (a3 @@ a2) : word16) /\
290 ((31 >< 24) w = a3) /\
291 ((63 >< 8) w = (a7 @@ a6 @@ a5 @@ a4 @@ a3
[all...]
/seL4-l4v-master/HOL4/examples/Crypto/IDEA/
H A DideaScript.sml55 `?a1 a2 a3 a4 a5 a6 a7 a8 a9.
56 x = (a1,a2,a3,a4,a5,a6,a7,a8,a9)`
64 `?a1 a2 a3 a4 a5 a6 a7 a8.
65 x = (a1,a2,a3,a4,a5,a6,a7,a8)`
82 `?a1 a2 a3 a4.
83 x = (a1,a2,a3,a4)`
/seL4-l4v-master/HOL4/examples/
H A Dtaut.sml4324 (car3 = (a3 \/ b3) /\ car2 \/ a3 /\ b3) /\
4327 (som3 = ~(a3 = ~(b3 = car2))) /\
4332 (cout3 = cout2 /\ b3 \/ cout2 /\ a3 \/ b3 /\ a3)
4338 ~((~a3 /\ ~b3 \/ a3 /\ b3) /\ ~cout2 \/
4339 cout2 /\ ~(~a3 /\ ~b3 \/ a3 /\ b3))) /\
4348 ~(a1 /\ a2 \/ ~a3 /\ (a
[all...]
/seL4-l4v-master/HOL4/examples/dev/AES/tupled/
H A Dword8Script.sml187 `BYTE_COMPARE (a7,a6,a5,a4,a3,a2,a1,a0)
197 (case BIT_COMPARE a3 b3
H A DRoundOpScript.sml74 `XOR_BLOCK ((a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15):block)
77 (a0 # b0, a1 # b1, a2 # b2, a3 # b3,
323 (a3 # b3 # c3 # d3) #
326 (a1 # a2 # a3 # a4) #
H A DaesScript.sml33 `?a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11.
34 x = (a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11)`
/seL4-l4v-master/HOL4/polyml/mlsource/extra/Win/
H A DRectangle.sml38 (* fun usercall_MII name CR (C1,C2,C3) (a1,a2,a3) =
45 val va3 = to3 a3
/seL4-l4v-master/seL4/src/arch/riscv/
H A Dtraps.S49 STORE a3, (12*REGBYTES)(t0)
/seL4-l4v-master/HOL4/examples/dev/AES/word8/
H A DRoundOpScript.sml75 `XOR_BLOCK ((a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15):block)
78 (a0 ?? b0, a1 ?? b1, a2 ?? b2, a3 ?? b3,
322 (a3 ?? b3 ?? c3 ?? d3) ??
325 (a1 ?? a2 ?? a3 ?? a4) ??
H A DaesScript.sml33 `?a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11.
34 x = (a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11)`
/seL4-l4v-master/HOL4/examples/Crypto/AES/
H A DRoundOpScript.sml75 `XOR_BLOCK ((a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15):block)
78 (a0 ?? b0, a1 ?? b1, a2 ?? b2, a3 ?? b3,
319 (a3 ?? b3 ?? c3 ?? d3) ??
322 (a1 ?? a2 ?? a3 ?? a4) ??
H A DaesScript.sml33 `?a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11.
34 x = (a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11)`
/seL4-l4v-master/HOL4/src/q/
H A Dselftest.sml83 [([a1,a2,a3], c)] =>
87 val _ = aconvdie "assumption #3" a3 expected_mat1a3
179 [([a1, a2, a3], c)] =>
182 aconvdie "assumption #3" a3 expected_a3;
/seL4-l4v-master/HOL4/examples/dev/AES/curried/
H A DRoundOpScript.sml74 `XOR_BLOCK ((a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15):block)
77 (a0 # b0, a1 # b1, a2 # b2, a3 # b3,
348 (a3 # b3 # c3 # d3) #
351 (a1 # a2 # a3 # a4) #
H A DaesScript.sml32 `?a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11.
33 x = (a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11)`
H A Dword8Script.sml211 `BYTE_COMPARE (BYTE a7 a6 a5 a4 a3 a2 a1 a0)
221 (case BIT_COMPARE a3 b3
/seL4-l4v-master/HOL4/src/quantHeuristics/
H A DquantHeuristicsLibParameters.sml146 val t = ``(\ (a1, a2, a3). P a1 a2 a3) (x:('a # 'b # 'c))``
/seL4-l4v-master/HOL4/examples/Crypto/TWOFISH/
H A DtwofishScript.sml75 val toLarge_def = Define`toLarge (a3:word8,a2:word8,a1:word8,a0:word8) =
76 a3 @@ a2 @@ a1 @@ a0`;
225 let (a3, b3) = (a2 ?? a2, a0 ?? ROR4(b2,1) ?? (8w*a2 && 0xfw)) in
226 let (a4, b4) = (t2(a3), t3(b3))
/seL4-l4v-master/isabelle/src/Tools/Metis/src/
H A Dproblems.sml1102 ~(a3 * b3 * c3 = a3 * (b3 * c3)) ==> F`},
1114 ~(a3 * b3 * c3 = a3 * (b3 * c3)) \/ ~(x * y = y * x)) ==> F`},
1134 ~(a3 * b3 * c3 = a3 * (b3 * c3)) \/ ~(x * y = y * x)) ==> F`},
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/
H A Dproblems.sml1102 ~(a3 * b3 * c3 = a3 * (b3 * c3)) ==> F`},
1114 ~(a3 * b3 * c3 = a3 * (b3 * c3)) \/ ~(x * y = y * x)) ==> F`},
1134 ~(a3 * b3 * c3 = a3 * (b3 * c3)) \/ ~(x * y = y * x)) ==> F`},

Completed in 210 milliseconds

123