andres-erbsen/rfc8439.v

## rfc8439.v
Require Coq.Init.Byte Coq.Strings.String. Import Init.Byte(byte(..)) String.
Require Import coqutil.Datatypes.List. Import Lists.List List.ListNotations.
Require Import Coq.ZArith.BinInt. Import Zdiv. Local Open Scope Z_scope.
Require Import coqutil.Byte coqutil.Word.LittleEndianList.

(* reference: https://datatracker.ietf.org/doc/html/rfc8439 *)
(* perl -ne 'BEGIN{$/=""} print unless /^Example /' < rfc8439.v *)

Definition poly1305 (p:=2^130-5) (k : list byte) (m : list byte) : list byte :=
  let r := Z.land (le_combine (firstn 16 k)) 0x0ffffffc0ffffffc0ffffffc0fffffff in
  let t := fold_left (fun a n => (a+le_combine(n++[x01]))*r mod p) (chunk 16 m) 0 in
  le_split 16 (t + le_combine (skipn 16 k)).

Example Poly1305_Example_and_Test_Vector :
  let k := [x85;xd6;xbe;x78;x57;x55;x6d;x33;x7f;x44;x52;xfe;x42;xd5;x06;xa8;
            x01;x03;x80;x8a;xfb;x0d;xb2;xfd;x4a;xbf;xf6;xaf;x41;x49;xf5;x1b] in
  let m := list_byte_of_string "Cryptographic Forum Research Group" in
  poly1305 k m = [xa8;x06;x1d;xc1;x30;x51;x36;xc6;xc2;x2b;x8b;xaf;x0c;x01;x27;xa9].
Proof. vm_compute; exact eq_refl. Qed.

Local Notation "a + b" := (Z.land (a+b) (Z.ones 32)).
Local Notation "a ^ b" := (Z.lxor a b).
Local Notation "a <<< b" := (Z.shiftl a b + Z.shiftr a (32-b))
  (at level 30).

Definition quarter '(a, b, c, d) :=
  let a := a + b in  let d := d ^ a in  let d := d <<< 16 in
  let c := c + d in  let b := b ^ c in  let b := b <<< 12 in
  let a := a + b in  let d := d ^ a in  let d := d <<< 8 in
  let c := c + d in  let b := b ^ c in  let b := b <<< 7 in
  (a, b, c, d).

Example Test_Vector_for_the_ChaCha_Quarter_Round :
 quarter (0x11111111, 0x01020304, 0x9b8d6f43, 0x01234567) =
         (0xea2a92f4, 0xcb1cf8ce, 0x4581472e, 0x5881c4bb) := eq_refl.

Definition quarterround x y z t (st : list Z) :=
  let '(a,b,c,d) := quarter (nth x st 0, nth y st 0, nth z st 0, nth t st 0) in
  upd (upd (upd (upd st x a) y b) z c) t d.

Example Test_Vector_for_the_Quarter_Round_on_the_ChaCha_State :
  quarterround 2 7 8 13 [
    0x879531e0; 0xc5ecf37d; 0x516461b1; 0xc9a62f8a;
    0x44c20ef3; 0x3390af7f; 0xd9fc690b; 0x2a5f714c;
    0x53372767; 0xb00a5631; 0x974c541a; 0x359e9963;
    0x5c971061; 0x3d631689; 0x2098d9d6; 0x91dbd320]
    = [
    0x879531e0; 0xc5ecf37d; 0xbdb886dc; 0xc9a62f8a;
    0x44c20ef3; 0x3390af7f; 0xd9fc690b; 0xcfacafd2;
    0xe46bea80; 0xb00a5631; 0x974c541a; 0x359e9963;
    0x5c971061; 0xccc07c79; 0x2098d9d6; 0x91dbd320] := eq_refl.

Definition chacha20_block (*256bit*)key (*32bit+96bit*)nonce :=
  let st := (*512bit*)
    map le_combine (chunk 4 (list_byte_of_string"expand 32-byte k"))
    ++ map le_combine (chunk 4 key)
    ++ map le_combine (chunk 4 nonce) in
  let ss := Nat.iter 10 (fun ss =>
    let ss := quarterround  0  4  8 12  ss in
    let ss := quarterround  1  5  9 13  ss in
    let ss := quarterround  2  6 10 14  ss in
    let ss := quarterround  3  7 11 15  ss in
    let ss := quarterround  0  5 10 15  ss in
    let ss := quarterround  1  6 11 12  ss in
    let ss := quarterround  2  7  8 13  ss in
    let ss := quarterround  3  4  9 14  ss in
    ss) st in
  let st := map (fun '(s, t) => s + t) (combine ss st) in
  flat_map (le_split 4) st.

Example Test_Vector_for_the_ChaCha20_Block_Function:
  let key := map Byte.byte.of_Z (map Z.of_nat (seq 0 32)) in
  let nonce := [x00;x00;x00;x09;x00;x00;x00;x4a;x00;x00;x00;x00] in
  let counter := 1 in
  chacha20_block key (le_split 4 counter ++ nonce) = [
    x10;xf1;xe7;xe4;xd1;x3b;x59;x15;x50;x0f;xdd;x1f;xa3;x20;x71;xc4;
    xc7;xd1;xf4;xc7;x33;xc0;x68;x03;x04;x22;xaa;x9a;xc3;xd4;x6c;x4e;
    xd2;x82;x64;x46;x07;x9f;xaa;x09;x14;xc2;xd7;x05;xd9;x8b;x02;xa2;
    xb5;x12;x9c;xd1;xde;x16;x4e;xb9;xcb;xd0;x83;xe8;xa2;x50;x3c;x4e].
Proof. vm_compute. exact eq_refl. Qed.

Definition chacha20_encrypt key start nonce plaintext :=
  flat_map (fun '(counter, ck) =>
    zip byte.xor (chacha20_block key (le_split 4 (Z.of_nat counter) ++ nonce)) ck)
  (enumerate start (chunk 64 plaintext)).

Example Example_and_Test_Vector_for_the_ChaCha20_Cipher :
  let key := map Byte.byte.of_Z (map Z.of_nat (seq 0 32)) in
  let nonce := [x00;x00;x00;x00;x00;x00;x00;x4a;x00;x00;x00;x00] in
  let plaintext := list_byte_of_string "Ladies and Gentlemen of the class of '99: If I could offer you only one tip for the future, sunscreen would be it." in
  chacha20_encrypt key 1 nonce plaintext = [
    x6e;x2e;x35;x9a;x25;x68;xf9;x80;x41;xba;x07;x28;xdd;x0d;x69;x81;
    xe9;x7e;x7a;xec;x1d;x43;x60;xc2;x0a;x27;xaf;xcc;xfd;x9f;xae;x0b;
    xf9;x1b;x65;xc5;x52;x47;x33;xab;x8f;x59;x3d;xab;xcd;x62;xb3;x57;
    x16;x39;xd6;x24;xe6;x51;x52;xab;x8f;x53;x0c;x35;x9f;x08;x61;xd8;
    x07;xca;x0d;xbf;x50;x0d;x6a;x61;x56;xa3;x8e;x08;x8a;x22;xb6;x5e;
    x52;xbc;x51;x4d;x16;xcc;xf8;x06;x81;x8c;xe9;x1a;xb7;x79;x37;x36;
    x5a;xf9;x0b;xbf;x74;xa3;x5b;xe6;xb4;x0b;x8e;xed;xf2;x78;x5e;x42;
    x87;x4d].
Proof. vm_compute. exact eq_refl. Qed.

Definition chacha20poly1305_aead_encrypt aad key iv constant plaintext :=
  let pad16 xs := repeat x00 (Nat.div_up (length xs) 16 * 16 - length xs) in
  let nonce := constant ++ iv in
  let otk := firstn 32 (chacha20_block key (le_split 4 0 ++ nonce)) in
  let ciphertext := chacha20_encrypt key 1 nonce plaintext in
  let mac_data := aad ++ pad16 aad in
  let mac_data := mac_data ++ ciphertext ++ pad16 ciphertext in
  let mac_data := mac_data ++ le_split 8 (Z.of_nat (length aad)) in
  let mac_data := mac_data ++ le_split 8 (Z.of_nat (length ciphertext)) in
  let tag := poly1305 otk mac_data in
  (ciphertext, tag).

Example Example_and_Test_Vector_for_AEAD_CHACHA20_POLY1305 :
  let constant := [x07;x00;x00;x00] in
  let key := map Byte.byte.of_Z (map Z.of_nat (seq 0x80 32)) in
  let iv := map Byte.byte.of_Z (map Z.of_nat (seq 0x40 8)) in
  let aad := [x50;x51;x52;x53;xc0;xc1;xc2;xc3;xc4;xc5;xc6;xc7] in
  let plaintext := list_byte_of_string "Ladies and Gentlemen of the class of '99: If I could offer you only one tip for the future, sunscreen would be it." in
  chacha20poly1305_aead_encrypt aad key iv constant plaintext = ([
    xd3;x1a;x8d;x34;x64;x8e;x60;xdb;x7b;x86;xaf;xbc;x53;xef;x7e;xc2;
    xa4;xad;xed;x51;x29;x6e;x08;xfe;xa9;xe2;xb5;xa7;x36;xee;x62;xd6;
    x3d;xbe;xa4;x5e;x8c;xa9;x67;x12;x82;xfa;xfb;x69;xda;x92;x72;x8b;
    x1a;x71;xde;x0a;x9e;x06;x0b;x29;x05;xd6;xa5;xb6;x7e;xcd;x3b;x36;
    x92;xdd;xbd;x7f;x2d;x77;x8b;x8c;x98;x03;xae;xe3;x28;x09;x1b;x58;
    xfa;xb3;x24;xe4;xfa;xd6;x75;x94;x55;x85;x80;x8b;x48;x31;xd7;xbc;
    x3f;xf4;xde;xf0;x8e;x4b;x7a;x9d;xe5;x76;xd2;x65;x86;xce;xc6;x4b;
    x61;x16], [x1a;xe1;x0b;x59;x4f;x09;xe2;x6a;x7e;x90;x2e;xcb;xd0;x60;x06;x91]).
Proof. vm_compute; exact eq_refl. Qed.
	Require Coq.Init.Byte Coq.Strings.String. Import Init.Byte(byte(..)) String.
	Require Import coqutil.Datatypes.List. Import Lists.List List.ListNotations.
	Require Import Coq.ZArith.BinInt. Import Zdiv. Local Open Scope Z_scope.
	Require Import coqutil.Byte coqutil.Word.LittleEndianList.

	(* reference: https://datatracker.ietf.org/doc/html/rfc8439 *)
	(* perl -ne 'BEGIN{$/=""} print unless /^Example /' < rfc8439.v *)

	Definition poly1305 (p:=2^130-5) (k : list byte) (m : list byte) : list byte :=
	let r := Z.land (le_combine (firstn 16 k)) 0x0ffffffc0ffffffc0ffffffc0fffffff in
	let t := fold_left (fun a n => (a+le_combine(n++[x01]))*r mod p) (chunk 16 m) 0 in
	le_split 16 (t + le_combine (skipn 16 k)).

	Example Poly1305_Example_and_Test_Vector :
	let k := [x85;xd6;xbe;x78;x57;x55;x6d;x33;x7f;x44;x52;xfe;x42;xd5;x06;xa8;
	x01;x03;x80;x8a;xfb;x0d;xb2;xfd;x4a;xbf;xf6;xaf;x41;x49;xf5;x1b] in
	let m := list_byte_of_string "Cryptographic Forum Research Group" in
	poly1305 k m = [xa8;x06;x1d;xc1;x30;x51;x36;xc6;xc2;x2b;x8b;xaf;x0c;x01;x27;xa9].
	Proof. vm_compute; exact eq_refl. Qed.

	Local Notation "a + b" := (Z.land (a+b) (Z.ones 32)).
	Local Notation "a ^ b" := (Z.lxor a b).
	Local Notation "a <<< b" := (Z.shiftl a b + Z.shiftr a (32-b))
	(at level 30).

	Definition quarter '(a, b, c, d) :=
	let a := a + b in let d := d ^ a in let d := d <<< 16 in
	let c := c + d in let b := b ^ c in let b := b <<< 12 in
	let a := a + b in let d := d ^ a in let d := d <<< 8 in
	let c := c + d in let b := b ^ c in let b := b <<< 7 in
	(a, b, c, d).

	Example Test_Vector_for_the_ChaCha_Quarter_Round :
	quarter (0x11111111, 0x01020304, 0x9b8d6f43, 0x01234567) =
	(0xea2a92f4, 0xcb1cf8ce, 0x4581472e, 0x5881c4bb) := eq_refl.

	Definition quarterround x y z t (st : list Z) :=
	let '(a,b,c,d) := quarter (nth x st 0, nth y st 0, nth z st 0, nth t st 0) in
	upd (upd (upd (upd st x a) y b) z c) t d.

	Example Test_Vector_for_the_Quarter_Round_on_the_ChaCha_State :
	quarterround 2 7 8 13 [
	0x879531e0; 0xc5ecf37d; 0x516461b1; 0xc9a62f8a;
	0x44c20ef3; 0x3390af7f; 0xd9fc690b; 0x2a5f714c;
	0x53372767; 0xb00a5631; 0x974c541a; 0x359e9963;
	0x5c971061; 0x3d631689; 0x2098d9d6; 0x91dbd320]
	= [
	0x879531e0; 0xc5ecf37d; 0xbdb886dc; 0xc9a62f8a;
	0x44c20ef3; 0x3390af7f; 0xd9fc690b; 0xcfacafd2;
	0xe46bea80; 0xb00a5631; 0x974c541a; 0x359e9963;
	0x5c971061; 0xccc07c79; 0x2098d9d6; 0x91dbd320] := eq_refl.

	Definition chacha20_block (256bit)key (32bit+96bit)nonce :=
	let st := (512bit)
	map le_combine (chunk 4 (list_byte_of_string"expand 32-byte k"))
	++ map le_combine (chunk 4 key)
	++ map le_combine (chunk 4 nonce) in
	let ss := Nat.iter 10 (fun ss =>
	let ss := quarterround 0 4 8 12 ss in
	let ss := quarterround 1 5 9 13 ss in
	let ss := quarterround 2 6 10 14 ss in
	let ss := quarterround 3 7 11 15 ss in
	let ss := quarterround 0 5 10 15 ss in
	let ss := quarterround 1 6 11 12 ss in
	let ss := quarterround 2 7 8 13 ss in
	let ss := quarterround 3 4 9 14 ss in
	ss) st in
	let st := map (fun '(s, t) => s + t) (combine ss st) in
	flat_map (le_split 4) st.

	Example Test_Vector_for_the_ChaCha20_Block_Function:
	let key := map Byte.byte.of_Z (map Z.of_nat (seq 0 32)) in
	let nonce := [x00;x00;x00;x09;x00;x00;x00;x4a;x00;x00;x00;x00] in
	let counter := 1 in
	chacha20_block key (le_split 4 counter ++ nonce) = [
	x10;xf1;xe7;xe4;xd1;x3b;x59;x15;x50;x0f;xdd;x1f;xa3;x20;x71;xc4;
	xc7;xd1;xf4;xc7;x33;xc0;x68;x03;x04;x22;xaa;x9a;xc3;xd4;x6c;x4e;
	xd2;x82;x64;x46;x07;x9f;xaa;x09;x14;xc2;xd7;x05;xd9;x8b;x02;xa2;
	xb5;x12;x9c;xd1;xde;x16;x4e;xb9;xcb;xd0;x83;xe8;xa2;x50;x3c;x4e].
	Proof. vm_compute. exact eq_refl. Qed.

	Definition chacha20_encrypt key start nonce plaintext :=
	flat_map (fun '(counter, ck) =>
	zip byte.xor (chacha20_block key (le_split 4 (Z.of_nat counter) ++ nonce)) ck)
	(enumerate start (chunk 64 plaintext)).

	Example Example_and_Test_Vector_for_the_ChaCha20_Cipher :
	let key := map Byte.byte.of_Z (map Z.of_nat (seq 0 32)) in
	let nonce := [x00;x00;x00;x00;x00;x00;x00;x4a;x00;x00;x00;x00] in
	let plaintext := list_byte_of_string "Ladies and Gentlemen of the class of '99: If I could offer you only one tip for the future, sunscreen would be it." in
	chacha20_encrypt key 1 nonce plaintext = [
	x6e;x2e;x35;x9a;x25;x68;xf9;x80;x41;xba;x07;x28;xdd;x0d;x69;x81;
	xe9;x7e;x7a;xec;x1d;x43;x60;xc2;x0a;x27;xaf;xcc;xfd;x9f;xae;x0b;
	xf9;x1b;x65;xc5;x52;x47;x33;xab;x8f;x59;x3d;xab;xcd;x62;xb3;x57;
	x16;x39;xd6;x24;xe6;x51;x52;xab;x8f;x53;x0c;x35;x9f;x08;x61;xd8;
	x07;xca;x0d;xbf;x50;x0d;x6a;x61;x56;xa3;x8e;x08;x8a;x22;xb6;x5e;
	x52;xbc;x51;x4d;x16;xcc;xf8;x06;x81;x8c;xe9;x1a;xb7;x79;x37;x36;
	x5a;xf9;x0b;xbf;x74;xa3;x5b;xe6;xb4;x0b;x8e;xed;xf2;x78;x5e;x42;
	x87;x4d].
	Proof. vm_compute. exact eq_refl. Qed.

	Definition chacha20poly1305_aead_encrypt aad key iv constant plaintext :=
	let pad16 xs := repeat x00 (Nat.div_up (length xs) 16 * 16 - length xs) in
	let nonce := constant ++ iv in
	let otk := firstn 32 (chacha20_block key (le_split 4 0 ++ nonce)) in
	let ciphertext := chacha20_encrypt key 1 nonce plaintext in
	let mac_data := aad ++ pad16 aad in
	let mac_data := mac_data ++ ciphertext ++ pad16 ciphertext in
	let mac_data := mac_data ++ le_split 8 (Z.of_nat (length aad)) in
	let mac_data := mac_data ++ le_split 8 (Z.of_nat (length ciphertext)) in
	let tag := poly1305 otk mac_data in
	(ciphertext, tag).

	Example Example_and_Test_Vector_for_AEAD_CHACHA20_POLY1305 :
	let constant := [x07;x00;x00;x00] in
	let key := map Byte.byte.of_Z (map Z.of_nat (seq 0x80 32)) in
	let iv := map Byte.byte.of_Z (map Z.of_nat (seq 0x40 8)) in
	let aad := [x50;x51;x52;x53;xc0;xc1;xc2;xc3;xc4;xc5;xc6;xc7] in
	let plaintext := list_byte_of_string "Ladies and Gentlemen of the class of '99: If I could offer you only one tip for the future, sunscreen would be it." in
	chacha20poly1305_aead_encrypt aad key iv constant plaintext = ([
	xd3;x1a;x8d;x34;x64;x8e;x60;xdb;x7b;x86;xaf;xbc;x53;xef;x7e;xc2;
	xa4;xad;xed;x51;x29;x6e;x08;xfe;xa9;xe2;xb5;xa7;x36;xee;x62;xd6;
	x3d;xbe;xa4;x5e;x8c;xa9;x67;x12;x82;xfa;xfb;x69;xda;x92;x72;x8b;
	x1a;x71;xde;x0a;x9e;x06;x0b;x29;x05;xd6;xa5;xb6;x7e;xcd;x3b;x36;
	x92;xdd;xbd;x7f;x2d;x77;x8b;x8c;x98;x03;xae;xe3;x28;x09;x1b;x58;
	xfa;xb3;x24;xe4;xfa;xd6;x75;x94;x55;x85;x80;x8b;x48;x31;xd7;xbc;
	x3f;xf4;xde;xf0;x8e;x4b;x7a;x9d;xe5;x76;xd2;x65;x86;xce;xc6;x4b;
	x61;x16], [x1a;xe1;x0b;x59;x4f;x09;xe2;x6a;x7e;x90;x2e;xcb;xd0;x60;x06;x91]).
	Proof. vm_compute; exact eq_refl. Qed.