# CryptoLine - ecp_nistz256_add

> [Academia Sinica IIS Intern [Learning] - CryptoLine](/tCNMWzNhQleOWtHmMwgE4w)

## ecp_nistz256_add.gas

#! $1c(%rdi) = %%EA
#! (%rdi) = %%EA
#! $1c(%rsi) = %%EA
#! (%rsi) = %%EA
#! $1c(%rdx) = %%EA
#! (%rdx) = %%EA
#! %r$1c = %%r$1c
#! %rax = %%rax
#! %rcx = %%rcx
#! %rdx = %%rdx

#! add $1ea, $2v -> adds carry $2v $2v $1ea
#! adc $1ea, $2v -> adcs carry $2v $2v $1ea carry
#! adc \$0x0, $1v -> adc $1v $1v 0@uint64 carry
#! cmovb $1v, $2v -> cmov $2v carry $1v $2v
#! mov $1v, $2v -> mov $2v $1v
#! mov $1ea, $2v -> mov $2v $1ea
#! mov $1v, $2ea -> mov $2ea $1v
#! sub $1ea, $2v -> subb carry $2v $2v $1ea
#! sbb $1ea, $2v -> sbbs carry $2v $2v $1ea carry
#! sbb \$0x0, $1v -> sbbs carry $1v $1v 0@uint64 carry
#! xor $1v, $1v -> mov $1v 0@uint64


#ecp_nistz256_add:
# %rdi = 0x7fffffffda00
# %rsi = 0x7fffffffd9c0
# %rdx = 0x7fffffffd9e0
# %rcx = 0x7fffffffd9c0
# %r8  = 0x555555580c70
# %r9  = 0x7ffef3ff00000000
	#! -> SP = 0x7fffffffd9b8
	#push   %r12                                     #! EA = L0x7fffffffd9b0; PC = 0x55555557c320
	#push   %r13                                     #! EA = L0x7fffffffd9a8; PC = 0x55555557c322
	mov    (%rsi),%r8                               #! EA = L0x7fffffffd9c0; Value = 0x0000000000000008; PC = 0x55555557c324
	xor    %r13,%r13                                #! PC = 0x55555557c327
	mov    0x8(%rsi),%r9                            #! EA = L0x7fffffffd9c8; Value = 0x0000000000000001; PC = 0x55555557c32a
	mov    0x10(%rsi),%r10                          #! EA = L0x7fffffffd9d0; Value = 0x00007fffffffdb28; PC = 0x55555557c32e
	mov    0x18(%rsi),%r11                          #! EA = L0x7fffffffd9d8; Value = 0x00007fffffffdb38; PC = 0x55555557c332
	#lea    -0x33d(%rip),%rsi        # 0x55555557c000#! PC = 0x55555557c336
	add    (%rdx),%r8                               #! EA = L0x7fffffffd9e0; Value = 0x0000555555582d98; PC = 0x55555557c33d
	adc    0x8(%rdx),%r9                            #! EA = L0x7fffffffd9e8; Value = 0x000055555555501b; PC = 0x55555557c340
	mov    %r8,%rax                                 #! PC = 0x55555557c344
	adc    0x10(%rdx),%r10                          #! EA = L0x7fffffffd9f0; Value = 0x00007fffffffda16; PC = 0x55555557c347
	adc    0x18(%rdx),%r11                          #! EA = L0x7fffffffd9f8; Value = 0x0000555555580cbd; PC = 0x55555557c34b
	mov    %r9,%rdx                                 #! PC = 0x55555557c34f
	adc    $0x0,%r13                                #! PC = 0x55555557c352
	sub    (%rsi),%r8                               #! EA = L0x55555557c000; Value = 0xffffffffffffffff; PC = 0x55555557c356
	mov    %r10,%rcx                                #! PC = 0x55555557c359
	sbb    0x8(%rsi),%r9                            #! EA = L0x55555557c008; Value = 0x00000000ffffffff; PC = 0x55555557c35c
	sbb    0x10(%rsi),%r10                          #! EA = L0x55555557c010; Value = 0x0000000000000000; PC = 0x55555557c360
	mov    %r11,%r12                                #! PC = 0x55555557c364
	sbb    0x18(%rsi),%r11                          #! EA = L0x55555557c018; Value = 0xffffffff00000001; PC = 0x55555557c367
	sbb    $0x0,%r13                                #! PC = 0x55555557c36b
	cmovb  %rax,%r8                                 #! PC = 0x55555557c36f
	cmovb  %rdx,%r9                                 #! PC = 0x55555557c373
	mov    %r8,(%rdi)                               #! EA = L0x7fffffffda00; PC = 0x55555557c377
	cmovb  %rcx,%r10                                #! PC = 0x55555557c37a
	mov    %r9,0x8(%rdi)                            #! EA = L0x7fffffffda08; PC = 0x55555557c37e
	cmovb  %r12,%r11                                #! PC = 0x55555557c382
	mov    %r10,0x10(%rdi)                          #! EA = L0x7fffffffda10; PC = 0x55555557c386
	mov    %r11,0x18(%rdi)                          #! EA = L0x7fffffffda18; PC = 0x55555557c38a
	#mov    (%rsp),%r13                              #! EA = L0x7fffffffd9a8; Value = 0x00007fffffffdb20; PC = 0x55555557c38e
	#mov    0x8(%rsp),%r12                           #! EA = L0x7fffffffd9b0; Value = 0x0000555555556000; PC = 0x55555557c392
	#lea    0x10(%rsp),%rsp                          #! PC = 0x55555557c397
	#! <- SP = 0x7fffffffd9b8
	#repz retq                                      #! PC = 0x55555557c39c

## ecp_nistz256_add.cl - [Before]

proc main (L0x55555557c000, L0x55555557c008, L0x55555557c010, L0x55555557c018, L0x7fffffffd9c0, L0x7fffffffd9c8, L0x7fffffffd9d0, L0x7fffffffd9d8, L0x7fffffffd9e0, L0x7fffffffd9e8, L0x7fffffffd9f0, L0x7fffffffd9f8) =
{
  true
  &&
  true
}

(* #! -> SP = 0x7fffffffd9b8 *)
#! 0x7fffffffd9b8 = 0x7fffffffd9b8;
(* #push   %r12                                     #! EA = L0x7fffffffd9b0; PC = 0x55555557c320 *)
#push   %%r12                                     #! L0x7fffffffd9b0 = L0x7fffffffd9b0; 0x55555557c320 = 0x55555557c320;
(* #push   %r13                                     #! EA = L0x7fffffffd9a8; PC = 0x55555557c322 *)
#push   %%r13                                     #! L0x7fffffffd9a8 = L0x7fffffffd9a8; 0x55555557c322 = 0x55555557c322;
(* mov    (%rsi),%r8                               #! EA = L0x7fffffffd9c0; Value = 0x0000000000000008; PC = 0x55555557c324 *)
mov r8 L0x7fffffffd9c0;
(* xor    %r13,%r13                                #! PC = 0x55555557c327 *)
mov r13 0@uint64;
(* mov    0x8(%rsi),%r9                            #! EA = L0x7fffffffd9c8; Value = 0x0000000000000001; PC = 0x55555557c32a *)
mov r9 L0x7fffffffd9c8;
(* mov    0x10(%rsi),%r10                          #! EA = L0x7fffffffd9d0; Value = 0x00007fffffffdb28; PC = 0x55555557c32e *)
mov r10 L0x7fffffffd9d0;
(* mov    0x18(%rsi),%r11                          #! EA = L0x7fffffffd9d8; Value = 0x00007fffffffdb38; PC = 0x55555557c332 *)
mov r11 L0x7fffffffd9d8;
(* #lea    -0x33d(%rip),%rsi        # 0x55555557c000#! PC = 0x55555557c336 *)
#lea    -0x33d(%rip),%rsi        # 0x55555557c000#! 0x55555557c336 = 0x55555557c336;
(* add    (%rdx),%r8                               #! EA = L0x7fffffffd9e0; Value = 0x0000555555582d98; PC = 0x55555557c33d *)
adds carry r8 r8 L0x7fffffffd9e0;
(* adc    0x8(%rdx),%r9                            #! EA = L0x7fffffffd9e8; Value = 0x000055555555501b; PC = 0x55555557c340 *)
adcs carry r9 r9 L0x7fffffffd9e8 carry;
(* mov    %r8,%rax                                 #! PC = 0x55555557c344 *)
mov rax r8;
(* adc    0x10(%rdx),%r10                          #! EA = L0x7fffffffd9f0; Value = 0x00007fffffffda16; PC = 0x55555557c347 *)
adcs carry r10 r10 L0x7fffffffd9f0 carry;
(* adc    0x18(%rdx),%r11                          #! EA = L0x7fffffffd9f8; Value = 0x0000555555580cbd; PC = 0x55555557c34b *)
adcs carry r11 r11 L0x7fffffffd9f8 carry;
(* mov    %r9,%rdx                                 #! PC = 0x55555557c34f *)
mov rdx r9;
(* adc    $0x0,%r13                                #! PC = 0x55555557c352 *)
adc r13 r13 0@uint64 carry;
(* sub    (%rsi),%r8                               #! EA = L0x55555557c000; Value = 0xffffffffffffffff; PC = 0x55555557c356 *)
subb carry r8 r8 L0x55555557c000;
(* mov    %r10,%rcx                                #! PC = 0x55555557c359 *)
mov rcx r10;
(* sbb    0x8(%rsi),%r9                            #! EA = L0x55555557c008; Value = 0x00000000ffffffff; PC = 0x55555557c35c *)
sbbs carry r9 r9 L0x55555557c008 carry;
(* sbb    0x10(%rsi),%r10                          #! EA = L0x55555557c010; Value = 0x0000000000000000; PC = 0x55555557c360 *)
sbbs carry r10 r10 L0x55555557c010 carry;
(* mov    %r11,%r12                                #! PC = 0x55555557c364 *)
mov r12 r11;
(* sbb    0x18(%rsi),%r11                          #! EA = L0x55555557c018; Value = 0xffffffff00000001; PC = 0x55555557c367 *)
sbbs carry r11 r11 L0x55555557c018 carry;
(* sbb    $0x0,%r13                                #! PC = 0x55555557c36b *)
sbbs carry r13 r13 0@uint64 carry;
(* cmovb  %rax,%r8                                 #! PC = 0x55555557c36f *)
cmov r8 carry rax r8;
(* cmovb  %rdx,%r9                                 #! PC = 0x55555557c373 *)
cmov r9 carry rdx r9;
(* mov    %r8,(%rdi)                               #! EA = L0x7fffffffda00; PC = 0x55555557c377 *)
mov L0x7fffffffda00 r8;
(* cmovb  %rcx,%r10                                #! PC = 0x55555557c37a *)
cmov r10 carry rcx r10;
(* mov    %r9,0x8(%rdi)                            #! EA = L0x7fffffffda08; PC = 0x55555557c37e *)
mov L0x7fffffffda08 r9;
(* cmovb  %r12,%r11                                #! PC = 0x55555557c382 *)
cmov r11 carry r12 r11;
(* mov    %r10,0x10(%rdi)                          #! EA = L0x7fffffffda10; PC = 0x55555557c386 *)
mov L0x7fffffffda10 r10;
(* mov    %r11,0x18(%rdi)                          #! EA = L0x7fffffffda18; PC = 0x55555557c38a *)
mov L0x7fffffffda18 r11;
(* #mov    (%rsp),%r13                              #! EA = L0x7fffffffd9a8; Value = 0x00007fffffffdb20; PC = 0x55555557c38e *)
#mov    (%rsp),%%r13                              #! L0x7fffffffd9a8 = L0x7fffffffd9a8; 0x00007fffffffdb20 = 0x00007fffffffdb20; 0x55555557c38e = 0x55555557c38e;
(* #mov    0x8(%rsp),%r12                           #! EA = L0x7fffffffd9b0; Value = 0x0000555555556000; PC = 0x55555557c392 *)
#mov    0x8(%rsp),%%r12                           #! L0x7fffffffd9b0 = L0x7fffffffd9b0; 0x0000555555556000 = 0x0000555555556000; 0x55555557c392 = 0x55555557c392;
(* #lea    0x10(%rsp),%rsp                          #! PC = 0x55555557c397 *)
#lea    0x10(%rsp),%rsp                          #! 0x55555557c397 = 0x55555557c397;
(* #! <- SP = 0x7fffffffd9b8 *)
#! 0x7fffffffd9b8 = 0x7fffffffd9b8;
(* #repz retq                                      #! PC = 0x55555557c39c *)
#repz retq                                      #! 0x55555557c39c = 0x55555557c39c;

{
  true
  &&
  true
}

## ecp_nistz256_add.cl - [After]

proc main (uint64 a0, uint64 a1, uint64 a2, uint64 a3,
           uint64 b0, uint64 b1, uint64 b2, uint64 b3,
           uint64 p0, uint64 p1, uint64 p2, uint64 p3) =

{
  true
  &&
  and [ p0 = 0xffffffffffffffff@64, p1 = 0x00000000ffffffff@64,
        p2 = 0x0000000000000000@64, p3 = 0xffffffff00000001@64,
        limbs 64 [a0, a1, a2, a3] <u limbs 64 [p0, p1, p2, p3],
        limbs 64 [b0, b1, b2, b3] <u limbs 64 [p0, p1, p2, p3]
  ]
}

mov L0x7fffffffd9c0 a0; mov L0x7fffffffd9c8 a1;
mov L0x7fffffffd9d0 a2; mov L0x7fffffffd9d8 a3;
mov L0x7fffffffd9e0 b0; mov L0x7fffffffd9e8 b1;
mov L0x7fffffffd9f0 b2; mov L0x7fffffffd9f8 b3;

mov L0x55555557c000 0xffffffffffffffff@uint64;
mov L0x55555557c008 0x00000000ffffffff@uint64;
mov L0x55555557c010 0x0000000000000000@uint64;
mov L0x55555557c018 0xffffffff00000001@uint64;

(* #! -> SP = 0x7fffffffd9b8 *)
#! 0x7fffffffd9b8 = 0x7fffffffd9b8;
(* #push   %r12                                     #! EA = L0x7fffffffd9b0; PC = 0x55555557c320 *)
#push   %%r12                                     #! L0x7fffffffd9b0 = L0x7fffffffd9b0; 0x55555557c320 = 0x55555557c320;
(* #push   %r13                                     #! EA = L0x7fffffffd9a8; PC = 0x55555557c322 *)
#push   %%r13                                     #! L0x7fffffffd9a8 = L0x7fffffffd9a8; 0x55555557c322 = 0x55555557c322;
(* mov    (%rsi),%r8                               #! EA = L0x7fffffffd9c0; Value = 0x0000000000000008; PC = 0x55555557c324 *)
mov r8 L0x7fffffffd9c0;
(* xor    %r13,%r13                                #! PC = 0x55555557c327 *)
mov r13 0@uint64;
(* mov    0x8(%rsi),%r9                            #! EA = L0x7fffffffd9c8; Value = 0x0000000000000001; PC = 0x55555557c32a *)
mov r9 L0x7fffffffd9c8;
(* mov    0x10(%rsi),%r10                          #! EA = L0x7fffffffd9d0; Value = 0x00007fffffffdb28; PC = 0x55555557c32e *)
mov r10 L0x7fffffffd9d0;
(* mov    0x18(%rsi),%r11                          #! EA = L0x7fffffffd9d8; Value = 0x00007fffffffdb38; PC = 0x55555557c332 *)
mov r11 L0x7fffffffd9d8;
(* #lea    -0x33d(%rip),%rsi        # 0x55555557c000#! PC = 0x55555557c336 *)
#lea    -0x33d(%rip),%rsi        # 0x55555557c000#! 0x55555557c336 = 0x55555557c336;
(* add    (%rdx),%r8                               #! EA = L0x7fffffffd9e0; Value = 0x0000555555582d98; PC = 0x55555557c33d *)
adds carry r8 r8 L0x7fffffffd9e0;
(* adc    0x8(%rdx),%r9                            #! EA = L0x7fffffffd9e8; Value = 0x000055555555501b; PC = 0x55555557c340 *)
adcs carry r9 r9 L0x7fffffffd9e8 carry;
(* mov    %r8,%rax                                 #! PC = 0x55555557c344 *)
mov rax r8;
(* adc    0x10(%rdx),%r10                          #! EA = L0x7fffffffd9f0; Value = 0x00007fffffffda16; PC = 0x55555557c347 *)
adcs carry r10 r10 L0x7fffffffd9f0 carry;
(* adc    0x18(%rdx),%r11                          #! EA = L0x7fffffffd9f8; Value = 0x0000555555580cbd; PC = 0x55555557c34b *)
adcs carry r11 r11 L0x7fffffffd9f8 carry;
(* mov    %r9,%rdx                                 #! PC = 0x55555557c34f *)
mov rdx r9;
(* adc    $0x0,%r13                                #! PC = 0x55555557c352 *)
adc r13 r13 0@uint64 carry;
(* sub    (%rsi),%r8                               #! EA = L0x55555557c000; Value = 0xffffffffffffffff; PC = 0x55555557c356 *)
subb carry r8 r8 L0x55555557c000;
(* mov    %r10,%rcx                                #! PC = 0x55555557c359 *)
mov rcx r10;
(* sbb    0x8(%rsi),%r9                            #! EA = L0x55555557c008; Value = 0x00000000ffffffff; PC = 0x55555557c35c *)
sbbs carry r9 r9 L0x55555557c008 carry;
(* sbb    0x10(%rsi),%r10                          #! EA = L0x55555557c010; Value = 0x0000000000000000; PC = 0x55555557c360 *)
sbbs carry r10 r10 L0x55555557c010 carry;
(* mov    %r11,%r12                                #! PC = 0x55555557c364 *)
mov r12 r11;
(* sbb    0x18(%rsi),%r11                          #! EA = L0x55555557c018; Value = 0xffffffff00000001; PC = 0x55555557c367 *)
sbbs carry r11 r11 L0x55555557c018 carry;
(* sbb    $0x0,%r13                                #! PC = 0x55555557c36b *)
sbbs carry r13 r13 0@uint64 carry;
(* cmovb  %rax,%r8                                 #! PC = 0x55555557c36f *)
cmov r8 carry rax r8;
(* cmovb  %rdx,%r9                                 #! PC = 0x55555557c373 *)
cmov r9 carry rdx r9;
(* mov    %r8,(%rdi)                               #! EA = L0x7fffffffda00; PC = 0x55555557c377 *)
mov L0x7fffffffda00 r8;
(* cmovb  %rcx,%r10                                #! PC = 0x55555557c37a *)
cmov r10 carry rcx r10;
(* mov    %r9,0x8(%rdi)                            #! EA = L0x7fffffffda08; PC = 0x55555557c37e *)
mov L0x7fffffffda08 r9;
(* cmovb  %r12,%r11                                #! PC = 0x55555557c382 *)
cmov r11 carry r12 r11;
(* mov    %r10,0x10(%rdi)                          #! EA = L0x7fffffffda10; PC = 0x55555557c386 *)
mov L0x7fffffffda10 r10;
(* mov    %r11,0x18(%rdi)                          #! EA = L0x7fffffffda18; PC = 0x55555557c38a *)
mov L0x7fffffffda18 r11;
(* #mov    (%rsp),%r13                              #! EA = L0x7fffffffd9a8; Value = 0x00007fffffffdb20; PC = 0x55555557c38e *)
#mov    (%rsp),%%r13                              #! L0x7fffffffd9a8 = L0x7fffffffd9a8; 0x00007fffffffdb20 = 0x00007fffffffdb20; 0x55555557c38e = 0x55555557c38e;
(* #mov    0x8(%rsp),%r12                           #! EA = L0x7fffffffd9b0; Value = 0x0000555555556000; PC = 0x55555557c392 *)
#mov    0x8(%rsp),%%r12                           #! L0x7fffffffd9b0 = L0x7fffffffd9b0; 0x0000555555556000 = 0x0000555555556000; 0x55555557c392 = 0x55555557c392;
(* #lea    0x10(%rsp),%rsp                          #! PC = 0x55555557c397 *)
#lea    0x10(%rsp),%rsp                          #! 0x55555557c397 = 0x55555557c397;
(* #! <- SP = 0x7fffffffd9b8 *)
#! 0x7fffffffd9b8 = 0x7fffffffd9b8;
(* #repz retq                                      #! PC = 0x55555557c39c *)
#repz retq                                      #! 0x55555557c39c = 0x55555557c39c;

mov c0 L0x7fffffffda00;
mov c1 L0x7fffffffda08;
mov c2 L0x7fffffffda10;
mov c3 L0x7fffffffda18;

{
  true
  &&
  and [eqmod (limbs 64 [c0, c1, c2, c3, 0@64])
             (limbs 64 [a0, a1, a2, a3, 0@64] + limbs 64 [b0, b1, b2, b3, 0@64])
             (limbs 64 [p0, p1, p2, p3, 0@64]),
      limbs 64 [c0, c1, c2, c3] <u limbs 64 [p0, p1, p2, p3]            
  ]
}

## 分析過程紀錄

| L0x7fffffffd9c0 | L0x7fffffffd9c8 | L0x7fffffffd9d0 | L0x7fffffffd9d8 |
| --------------- | --------------- | --------------- | --------------- |
| a0 | a1 | a2 | a3 |
| r8 | r9 | r10 | r11 |
| a~0~ + b~0~ | a~1~ + b~1~ | a~2~ + b~2~ | a~3~ + b~3~ |

| L0x7fffffffd9e0 | L0x7fffffffd9e8 | L0x7fffffffd9f0 | L0x7fffffffd9f8 |
| --------------- | --------------- | --------------- | --------------- |
| b0 | b1 | b2 | b3 |

| L0x55555557c000 | L0x55555557c008 | L0x55555557c010 | L0x55555557c018 |
| ------------------ | ------------------ | ------------------ | ------------------ |
| 0xffffffffffffffff | 0x00000000ffffffff | 0x0000000000000000 | 0xffffffff00000001 |

- 加法

adds carry r8 r8 L0x7fffffffd9e0;
adcs carry r9 r9 L0x7fffffffd9e8 carry;
adcs carry r10 r10 L0x7fffffffd9f0 carry;
adcs carry r11 r11 L0x7fffffffd9f8 carry;

> a~0~ + b~0~，結果放 r8
> a~1~ + b~1~ ，結果放在 r9
> a~2~ + b~2~ ，結果放在 r10
> a~3~ + b~3~ ，結果放在 r11

- 處理進位

mov r13 0@uint64;
adc r13 r13 0@uint64 carry;

> 將 carry 放置 r13

- 放置結果到暫存器

mov rax r8;
mov rdx r9;
mov rcx r10;
mov r12 r11;

- 處理 mod

subb carry r8 r8 L0x55555557c000;
sbbs carry r9 r9 L0x55555557c008 carry;
sbbs carry r10 r10 L0x55555557c010 carry;
sbbs carry r11 r11 L0x55555557c018 carry;
sbbs carry r13 r13 0@uint64 carry;

cmov r8 carry rax r8;
cmov r9 carry rdx r9;
cmov r10 carry rcx r10;
cmov r11 carry r12 r11;

- 結果

mov L0x7fffffffda00 r8;
mov L0x7fffffffda08 r9;
mov L0x7fffffffda10 r10;
mov L0x7fffffffda18 r11;

mov c0 L0x7fffffffda00;
mov c1 L0x7fffffffda08;
mov c2 L0x7fffffffda10;
mov c3 L0x7fffffffda18;

## 指令說明 與 操作
- precondition and postcondition
- 將變數設定他們的位址
- `mov L0x7fffffffd9c0 a0;`
- `mov L0x7fffffffd9e0 b0;`
- `mov L0x55555557c000 0xffffffffffffffff@uint64;`