/seL4-l4v-master/seL4/src/arch/riscv/machine/ |
H A D | registerset.c | 12 a2, a3, a4, a5 29 a0, a1, a2, a3, a4, a5, a6, a7,
|
/seL4-l4v-master/seL4/include/arch/riscv/arch/machine/ |
H A D | registerset.h | 40 a3 = 12, enumerator in enum:_register 145 [seL4_UnknownSyscall_A3] = a3,\ 172 [seL4_TimeoutReply_a3] = a3, \
|
/seL4-l4v-master/HOL4/examples/elliptic/ |
H A D | elliptic_exampleScript.sml | 231 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 D | ellipticScript.sml | 478 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 D | types.h | 50 seL4_Word a3; member in struct:seL4_UserContext_
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/mips/step/ |
H A D | mips_stepScript.sml | 272 `!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 D | ideaScript.sml | 55 `?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 D | taut.sml | 4324 (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 D | word8Script.sml | 187 `BYTE_COMPARE (a7,a6,a5,a4,a3,a2,a1,a0) 197 (case BIT_COMPARE a3 b3
|
H A D | RoundOpScript.sml | 74 `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 D | aesScript.sml | 33 `?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 D | Rectangle.sml | 38 (* 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 D | traps.S | 49 STORE a3, (12*REGBYTES)(t0)
|
/seL4-l4v-master/HOL4/examples/dev/AES/word8/ |
H A D | RoundOpScript.sml | 75 `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 D | aesScript.sml | 33 `?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 D | RoundOpScript.sml | 75 `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 D | aesScript.sml | 33 `?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 D | selftest.sml | 83 [([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 D | RoundOpScript.sml | 74 `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 D | aesScript.sml | 32 `?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 D | word8Script.sml | 211 `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 D | quantHeuristicsLibParameters.sml | 146 val t = ``(\ (a1, a2, a3). P a1 a2 a3) (x:('a # 'b # 'c))``
|
/seL4-l4v-master/HOL4/examples/Crypto/TWOFISH/ |
H A D | twofishScript.sml | 75 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 D | problems.sml | 1102 ~(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 D | problems.sml | 1102 ~(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`},
|