diff --git a/examples/ChaChaPoly/chacha_poly.ec b/examples/ChaChaPoly/chacha_poly.ec
index ece92fab5..95f18263b 100644
--- a/examples/ChaChaPoly/chacha_poly.ec
+++ b/examples/ChaChaPoly/chacha_poly.ec
@@ -213,8 +213,9 @@ hint solve 0 random : dpoly_out_ll dpoly_out_funi dpoly_out_fu.
 
 clone import GenBlock as TPoly with 
   op block_size = poly_in_size + poly_out_size 
-  proof ge0_block_size by smt (ge0_poly_in_size ge0_poly_out_size) 
+  proof *
   rename "block" as "poly".
+realize ge0_poly_size by smt (ge0_poly_in_size ge0_poly_out_size).
 hint solve 0 random : dpoly_ll dpoly_funi dpoly_fu. 
 
 clone import GenBlock as Extra_block
@@ -1385,6 +1386,22 @@ module EncRnd = {
    
 }.
 
+(* The ideal AEAD: encryption returns random bytes of the length of the *)
+(* message and a random tag, decryption only accepts the ciphertexts    *)
+(* returned by encryption.                                              *)
+module IdealAEAD : Oracles = {
+  proc init () = { Mem.log <- empty; }
+
+  proc enc (p : plaintext) = {
+    var c;
+    c <@ EncRnd.enc(p);
+    Mem.log.[c] <- p;
+    return c;
+  }
+
+  proc dec (c : ciphertext) = { return Mem.log.[c]; }
+}.
+
 section PROOFS.
   declare module A <: CCA_Adv { -BNR, -Mem, -IndBlock, -RO, -FRO}.
 
@@ -2778,4 +2795,143 @@ section PROOFS.
      by have /# := step4_bad2 &m.
    qed.
 
+  lemma CCA_CPA_IdealAEAD &m :
+    Pr[CCA_game(CCA_CPA_Adv(BNR_Adv(A)), EncRnd).main() @ &m : res] =
+    Pr[CCA_game(BNR_Adv(A), IdealAEAD).main() @ &m : res].
+  proof.
+  byequiv (: ={glob A} ==> ={res}) => //; proc; inline *; wp.
+  call (: ={Mem.log, glob BNR}); 1,2: by sim.
+  by auto.
+  qed.
+
+  lemma conclusion_ideal &m :
+    Pr[CCA_game(BNR_Adv(A), RealOrcls(ChaChaPoly)).main() @ &m : res] <=
+      Pr[CCA_game(BNR_Adv(A), IdealAEAD).main() @ &m : res] +
+      (Pr[Indist.Distinguish(D(BNR_Adv(A)), IndBlock).game() @ &m : res] -
+       Pr[Indist.Distinguish(D(BNR_Adv(A)), IndRO).game() @ &m : res]) +
+       qdec%r * (maxr pr_zeropol pr1_poly_out) +
+       qdec%r * pr1_poly_out.
+  proof. by rewrite -CCA_CPA_IdealAEAD; apply: conclusion. qed.
+
 end section PROOFS.
+
+(* -------------------------------------------------------------------- *)
+(* The same bound on the absolute value of the advantage, obtained by    *)
+(* applying conclusion_ideal to the adversary that negates its output.   *)
+section Abs.
+  declare module A <: CCA_Adv { -BNR, -Mem, -IndBlock, -RO, -FRO}.
+
+  declare axiom A_ll : forall (O <: CCA_Oracles{-A}), islossless O.enc => islossless O.dec => islossless A(O).main.
+
+  declare axiom neq_w1_w2 : w1 <> w2.
+
+  local module NegA (O : CCA_Oracles) = {
+    proc main () = {
+      var b;
+      b <@ A(O).main();
+      return !b;
+    }
+  }.
+
+  local lemma NegA_ll (O <: CCA_Oracles{-NegA}) :
+    islossless O.enc => islossless O.dec => islossless NegA(O).main.
+  proof. by move=> enc_ll dec_ll; proc; call (A_ll O enc_ll dec_ll). qed.
+
+  local lemma cc_ll : islossless EncRnd.cc.
+  proof.
+  proc; wp; while (true) (size p); last by auto; smt(size_ge0 size_eq0).
+  move=> z; auto => /> &1 hp.
+  smt(dblock_ll size_drop gt0_block_size size_ge0 size_eq0).
+  qed.
+
+  local lemma chacha_enc_ll (O <: Indist.Oracle{-A}) :
+    islossless O.f => islossless D(BNR_Adv(A), O).O.ChaCha.enc.
+  proof.
+  move=> f_ll; proc; while (true) (size p); last by auto; smt(size_ge0 size_eq0).
+  move=> z; wp; call f_ll; auto => /> &1 hp.
+  smt(size_drop gt0_block_size size_ge0 size_eq0).
+  qed.
+
+  local lemma real_ll : islossless CCA_game(BNR_Adv(A), RealOrcls(ChaChaPoly)).main.
+  proof.
+  proc; inline *; wp.
+  call (A_ll (BNR(RealOrcls(ChaChaPoly))) _ _); 1,2: by islossless.
+  by auto; smt(dkey_ll).
+  qed.
+
+  local lemma ideal_ll : islossless CCA_game(BNR_Adv(A), IdealAEAD).main.
+  proof.
+  proc; inline *; wp.
+  call (A_ll (BNR(IdealAEAD)) _ _); 2: by islossless.
+  + proc; sp; if; last by auto.
+    inline IdealAEAD.enc EncRnd.enc; wp; rnd; call cc_ll; auto => /> &hr _.
+    by have := dpoly_out_ll; rewrite /is_lossless /predT => ->.
+  by auto.
+  qed.
+
+  local lemma dist_ll (O <: Indist.Function{-A, -BNR}) :
+    islossless O.init => islossless O.f =>
+    islossless Indist.Distinguish(D(BNR_Adv(A)), O).game.
+  proof.
+  move=> init_ll f_ll; proc; inline *; wp.
+  call (A_ll (<: BNR(D(BNR_Adv(A), O).O)) _ _).
+  + proc; sp; if; last by auto.
+    by inline 1; inline 4; wp; call f_ll; wp; call (chacha_enc_ll O f_ll); auto.
+  + proc; sp; if; last by auto.
+    inline 1; inline 4; wp; seq 9 : true => //; first by wp; call f_ll; auto.
+    by if; [wp; call (chacha_enc_ll O f_ll) | auto].
+  by wp; call init_ll.
+  qed.
+
+  local lemma Pr_real &m :
+    Pr[CCA_game(BNR_Adv(NegA), RealOrcls(ChaChaPoly)).main() @ &m : res] =
+    1%r - Pr[CCA_game(BNR_Adv(A), RealOrcls(ChaChaPoly)).main() @ &m : res].
+  proof.
+  have -> : Pr[CCA_game(BNR_Adv(NegA), RealOrcls(ChaChaPoly)).main() @ &m : res] =
+            Pr[CCA_game(BNR_Adv(A), RealOrcls(ChaChaPoly)).main() @ &m : !res].
+  + byequiv (: ={glob A} ==> res{1} = !res{2}) => //; proc; inline *; wp.
+    by call (: ={glob BNR, Mem.k}); 1,2: sim; auto.
+  by rewrite Pr[mu_not]; congr; byphoare real_ll.
+  qed.
+
+  local lemma Pr_ideal &m :
+    Pr[CCA_game(BNR_Adv(NegA), IdealAEAD).main() @ &m : res] =
+    1%r - Pr[CCA_game(BNR_Adv(A), IdealAEAD).main() @ &m : res].
+  proof.
+  have -> : Pr[CCA_game(BNR_Adv(NegA), IdealAEAD).main() @ &m : res] =
+            Pr[CCA_game(BNR_Adv(A), IdealAEAD).main() @ &m : !res].
+  + byequiv (: ={glob A} ==> res{1} = !res{2}) => //; proc; inline *; wp.
+    by call (: ={glob BNR, Mem.log}); 1,2: sim; auto.
+  by rewrite Pr[mu_not]; congr; byphoare ideal_ll.
+  qed.
+
+  local lemma Pr_dist (O <: Indist.Function{-A, -BNR}) &m :
+    islossless O.init => islossless O.f =>
+    Pr[Indist.Distinguish(D(BNR_Adv(NegA)), O).game() @ &m : res] =
+    1%r - Pr[Indist.Distinguish(D(BNR_Adv(A)), O).game() @ &m : res].
+  proof.
+  move=> init_ll f_ll.
+  have -> : Pr[Indist.Distinguish(D(BNR_Adv(NegA)), O).game() @ &m : res] =
+            Pr[Indist.Distinguish(D(BNR_Adv(A)), O).game() @ &m : !res].
+  + byequiv (: ={glob A, glob O} ==> res{1} = !res{2}) => //; proc; inline *; wp.
+    by call (: ={glob BNR, glob O}); 1,2: sim; wp; call (: true); auto.
+  by rewrite Pr[mu_not]; congr; byphoare (dist_ll O init_ll f_ll).
+  qed.
+
+  lemma conclusion_ideal_abs &m :
+    `|Pr[CCA_game(BNR_Adv(A), RealOrcls(ChaChaPoly)).main() @ &m : res] -
+      Pr[CCA_game(BNR_Adv(A), IdealAEAD).main() @ &m : res]| <=
+      `|Pr[Indist.Distinguish(D(BNR_Adv(A)), IndBlock).game() @ &m : res] -
+        Pr[Indist.Distinguish(D(BNR_Adv(A)), IndRO).game() @ &m : res]| +
+      qdec%r * (maxr pr_zeropol pr1_poly_out) +
+      qdec%r * pr1_poly_out.
+  proof.
+  have h1 := conclusion_ideal A A_ll neq_w1_w2 &m.
+  have h2 := conclusion_ideal NegA NegA_ll neq_w1_w2 &m.
+  move: h2; rewrite Pr_real Pr_ideal.
+  rewrite (Pr_dist IndBlock &m _ _); 1,2: by islossless; smt(dkey_ll).
+  rewrite (Pr_dist IndRO &m _ _); 1,2: by islossless; smt(dblock_ll).
+  smt().
+  qed.
+
+end section Abs.
diff --git a/examples/ChaChaPoly/chacha_poly_rfc.ec b/examples/ChaChaPoly/chacha_poly_rfc.ec
new file mode 100644
index 000000000..9a4c04915
--- /dev/null
+++ b/examples/ChaChaPoly/chacha_poly_rfc.ec
@@ -0,0 +1,334 @@
+(* -------------------------------------------------------------------- *)
+(* The generic ChaCha20-Poly1305 proof instantiated with the Poly1305   *)
+(* of RFC 8439.                                                         *)
+require import AllCore List IntDiv Real Distr DList StdOrder.
+require import Poly1305_prime Poly1305_field Poly1305_msg Poly1305_clamp.
+require Chacha_poly.
+import IntOrder Zp1305 P1305.
+
+(* -------------------------------------------------------------------- *)
+(* Bytes stay abstract, with their encoding into [0, 256).              *)
+type byte.
+
+op to_uint : byte -> int.
+op of_uint : int -> byte.
+
+axiom to_uint_rg (b : byte) : 0 <= to_uint b < 256.
+axiom to_uint_inj : injective to_uint.
+axiom of_uintK (n : int) : 0 <= n < 256 => to_uint (of_uint n) = n.
+
+(* The uniform distribution on bytes, shared by the Poly1305 clamping   *)
+(* (theory Clamp) and by the generic proof (theory Byte.Support below). *)
+lemma to_uintK (b : byte) : of_uint (to_uint b) = b.
+proof. by apply: to_uint_inj; rewrite of_uintK // to_uint_rg. qed.
+
+clone MFinite as ByteFin with
+  type t <- byte,
+  op Support.enum = map of_uint (range 0 256)
+  proof Support.enum_spec
+  rename "dunifin" as "dbyte".
+
+realize Support.enum_spec.
+proof.
+move=> b; rewrite count_uniq_mem.
+- rewrite map_inj_in_uniq ?range_uniq // => x y /mem_range hx /mem_range hy eq.
+  by rewrite -(of_uintK x hx) -(of_uintK y hy) eq.
+by rewrite b2i_eq1; apply/mapP; exists (to_uint b); rewrite mem_range to_uint_rg to_uintK.
+qed.
+
+lemma card_byte : ByteFin.Support.card = 256.
+proof. by rewrite /ByteFin.Support.card size_map size_range. qed.
+
+clone Clamp as CL with
+  type byte <- byte,
+  op to_uint <- to_uint,
+  op of_uint <- of_uint,
+  op dbyte <- ByteFin.dbyte
+proof to_uint_rg, to_uint_inj, of_uintK, dbyte1E.
+realize to_uint_rg by exact: to_uint_rg.
+realize to_uint_inj by exact: to_uint_inj.
+realize of_uintK by exact: of_uintK.
+realize dbyte1E.
+proof. by move=> b; rewrite ByteFin.dbyte1E card_byte. qed.
+
+(* -------------------------------------------------------------------- *)
+(* The Poly1305 key r and the tag are 16 bytes long.                    *)
+subtype poly_in as PolyIn = { l : byte list | size l = 16 }
+  rename "poly_in_of_bytes", "bytes_of_poly_in".
+
+realize inhabited.
+proof. by exists (nseq 16 witness); rewrite size_nseq. qed.
+import PolyIn.
+
+subtype poly_out as PolyOut = { l : byte list | size l = 16 }
+  rename "poly_out_of_bytes", "bytes_of_poly_out".
+
+realize inhabited.
+proof. by exists (nseq 16 witness); rewrite size_nseq. qed.
+import PolyOut.
+
+(* Tags are integers modulo 2^128, in little-endian.                    *)
+op int_of_poly_out (t : poly_out) = CL.le_int (bytes_of_poly_out t).
+op poly_out_of_int (n : int) = poly_out_of_bytesd (CL.le_bytes 16 (n %% 2 ^ 128)).
+
+op poly_out_add (t1 t2 : poly_out) =
+  poly_out_of_int (int_of_poly_out t1 + int_of_poly_out t2).
+
+op poly_out_sub (t1 t2 : poly_out) =
+  poly_out_of_int (int_of_poly_out t1 - int_of_poly_out t2).
+
+lemma e128 : 256 ^ 16 = 2 ^ 128.
+proof. by cbv hint {expr0 expr_pred}. qed.
+
+lemma gt0_e128 : 0 < 2 ^ 128.
+proof. by rewrite expr_gt0. qed.
+
+lemma int_of_poly_out_rg (t : poly_out) : 0 <= int_of_poly_out t < 2 ^ 128.
+proof. by have := CL.le_int_rg (bytes_of_poly_out t); rewrite bytes_of_poly_outP e128. qed.
+
+lemma int_of_poly_out_inj : injective int_of_poly_out.
+proof.
+move=> t1 t2 h; apply: bytes_of_poly_out_inj; apply: CL.le_int_inj => //.
+by rewrite !bytes_of_poly_outP.
+qed.
+
+lemma int_of_poly_outK (n : int) :
+  int_of_poly_out (poly_out_of_int n) = n %% 2 ^ 128.
+proof.
+rewrite /int_of_poly_out /poly_out_of_int poly_out_of_bytesdK ?CL.size_le_bytes //.
+by rewrite CL.le_bytesK // e128; smt(modz_ge0 ltz_pmod gt0_e128).
+qed.
+
+lemma poly_out_of_intK (t : poly_out) : poly_out_of_int (int_of_poly_out t) = t.
+proof.
+by apply: int_of_poly_out_inj; rewrite int_of_poly_outK modz_small; smt(int_of_poly_out_rg).
+qed.
+
+lemma eq_poly_out_of_int (n1 n2 : int) :
+  poly_out_of_int n1 = poly_out_of_int n2 <=> n1 %% 2 ^ 128 = n2 %% 2 ^ 128.
+proof.
+split=> [h|h]; first by rewrite -!int_of_poly_outK h.
+by rewrite /poly_out_of_int h.
+qed.
+
+lemma poly_out_subrK (t1 t2 : poly_out) :
+  t1 = poly_out_add (poly_out_sub t1 t2) t2.
+proof.
+rewrite /poly_out_add /poly_out_sub int_of_poly_outK -{1}(poly_out_of_intK t1).
+by rewrite eq_poly_out_of_int modzDml subrK.
+qed.
+
+lemma poly_out_addrK (t1 t2 : poly_out) :
+  t1 = poly_out_sub (poly_out_add t1 t2) t2.
+proof.
+rewrite /poly_out_add /poly_out_sub int_of_poly_outK -{1}(poly_out_of_intK t1).
+by rewrite eq_poly_out_of_int modzDml addrK.
+qed.
+
+lemma poly_out_addr_subrr (t1 t2 : poly_out) :
+  t1 = poly_out_add t1 (poly_out_sub t2 t2).
+proof.
+rewrite /poly_out_add /poly_out_sub int_of_poly_outK -{1}(poly_out_of_intK t1).
+by rewrite eq_poly_out_of_int modzDmr subrr addr0.
+qed.
+
+lemma poly_out_subr_addr (t t1 t2 : poly_out) :
+  poly_out_add (poly_out_sub t t1) t2 = poly_out_add t (poly_out_sub t2 t1).
+proof.
+rewrite /poly_out_add /poly_out_sub !int_of_poly_outK eq_poly_out_of_int.
+by rewrite modzDml modzDmr addrA addrAC.
+qed.
+
+(* The Poly1305 evaluation: the low 128 bits of m(r) with r clamped.    *)
+op poly1305_eval (r : poly_in) (p : poly) =
+  poly_out_of_int (asint (peval p (CL.r_of (bytes_of_poly_in r)))).
+
+(* Maximal sizes of the associated data and of the ciphertext accepted  *)
+(* in the security game, within the limits of RFC 8439. The bound of    *)
+(* the final theorem grows linearly with them.                          *)
+op max_ad : int.
+op max_cipher : int.
+
+axiom max_ad_rg : 0 <= max_ad <= 2 ^ 64 - 1.
+axiom max_cipher_rg : 0 <= max_cipher <= (2 ^ 32 - 1) * 64.
+
+(* Number of 16-byte blocks of the MAC input for maximal sizes.         *)
+op max_nblocks = (max_ad + 15) %/ 16 + (max_cipher + 15) %/ 16 + 1.
+
+op pr_zeropol = (8 * max_nblocks)%r / (2 ^ 106)%r.
+
+lemma ge0_pr_zeropol : 0%r <= pr_zeropol.
+proof.
+rewrite /pr_zeropol RealOrder.divr_ge0 le_fromint; last by rewrite expr_ge0.
+by rewrite /max_nblocks; smt(divz_ge0 max_ad_rg max_cipher_rg).
+qed.
+
+(* Sizes accepted in the security game.                                 *)
+op valid_sizes (a c : byte list) =
+  size a <= max_ad /\ size c <= max_cipher.
+
+lemma valid_sizes_size (a c : byte list) :
+  valid_sizes a c => CL.valid_size a /\ CL.valid_size c.
+proof.
+have e64 : 2 ^ 64 = 18446744073709551616 by cbv hint {expr0 expr_pred}.
+have e32 : 2 ^ 32 = 4294967296 by cbv hint {expr0 expr_pred}.
+by rewrite /valid_sizes /CL.valid_size e64; smt(max_ad_rg max_cipher_rg).
+qed.
+
+lemma nblocks_le (a c : byte list) : valid_sizes a c => CL.nblocks a c <= max_nblocks.
+proof.
+rewrite /valid_sizes /CL.nblocks /max_nblocks => -[ha hc].
+by rewrite ler_add2r ler_add leq_div2r // ler_add2r.
+qed.
+
+lemma pr_tag_diff_rfc (a1 c1 a2 c2 : byte list) (t1 t2 : poly_out) :
+  valid_sizes a1 c1 => valid_sizes a2 c2 =>
+  CL.topol a2 c2 <> CL.topol a1 c1 =>
+  mu (dmap (dlist ByteFin.dbyte 16) poly_in_of_bytesd)
+     (fun r => t2 = poly_out_add t1 (poly_out_sub (poly1305_eval r (CL.topol a2 c2))
+                                                 (poly1305_eval r (CL.topol a1 c1))))
+  <= pr_zeropol.
+proof.
+move=> v1 v2 neq; have [va1 vc1] := valid_sizes_size _ _ v1.
+have [va2 vc2] := valid_sizes_size _ _ v2.
+have neq' : (a1, c1) <> (a2, c2) by apply: contra neq => -[-> ->].
+pose d := int_of_poly_out t2 - int_of_poly_out t1.
+apply: (RealOrder.ler_trans (mu CL.dr (fun r =>
+  (CL.hpoly r a2 c2 - CL.hpoly r a1 c1) %% 2 ^ 128 = d %% 2 ^ 128))).
+- rewrite dmapE /CL.dr dmapE; apply: mu_le => bs; rewrite supp_dlist // => -[sz _].
+  rewrite /(\o) /= /poly_out_add /poly_out_sub /poly1305_eval poly_in_of_bytesdK //.
+  rewrite !int_of_poly_outK -{1}(poly_out_of_intK t2) eq_poly_out_of_int /d /CL.hpoly.
+  pose h2 := asint _; pose h1 := asint _; move=> eq_t.
+  rewrite -(modzDml (int_of_poly_out t2)) eq_t modzDml addrAC subrr add0r.
+  by rewrite modz_mod modzBm.
+apply: (RealOrder.ler_trans _ _ _ (CL.pr_tag_diff a1 c1 a2 c2 d va1 vc1 va2 vc2 neq')).
+rewrite /pr_zeropol RealOrder.ler_wpmul2r.
+- by rewrite RealOrder.invr_ge0 le_fromint expr_ge0.
+by rewrite le_fromint ler_wpmul2l // ler_maxrP !nblocks_le.
+qed.
+
+(* -------------------------------------------------------------------- *)
+clone Chacha_poly as RFC8439 with
+  type Byte.byte <- byte,
+  theory Byte.Support <- ByteFin.Support,
+  op Poly_in.poly_in_size <- 16,
+  type Poly_in.poly_in <- poly_in,
+  op Poly_in.poly_in_of_bytes <- poly_in_of_bytes,
+  op Poly_in.bytes_of_poly_in <- bytes_of_poly_in,
+  op Poly_out.poly_out_size <- 16,
+  type Poly_out.poly_out <- poly_out,
+  op Poly_out.poly_out_of_bytes <- poly_out_of_bytes,
+  op Poly_out.bytes_of_poly_out <- bytes_of_poly_out,
+  op Extra_block.extra_block_size <- 32,
+  op C.max_counter <- 2 ^ 32 - 1,
+  type polynomial <- poly,
+  op topol <- CL.topol,
+  op max_ad_size <- max_ad,
+  op max_cipher_size <- max_cipher,
+  op poly1305_eval <- poly1305_eval,
+  op (+) <- poly_out_add,
+  op (-) <- poly_out_sub,
+  op pr_zeropol <- pr_zeropol,
+  op w1 <- poly_out_of_int 0,
+  op w2 <- poly_out_of_int 1
+proof Poly_in.ge0_poly_in_size, Poly_out.ge0_poly_out_size,
+  Extra_block.ge0_extra_block_size,
+  Poly_in.poly_in_of_bytesN by exact: poly_in_of_bytesN,
+  Poly_in.poly_in_of_bytesT by exact: poly_in_of_bytesT,
+  Poly_in.bytes_of_poly_inP by exact: bytes_of_poly_inP,
+  Poly_in.bytes_of_poly_inK by exact: bytes_of_poly_inK,
+  Poly_out.poly_out_of_bytesN by exact: poly_out_of_bytesN,
+  Poly_out.poly_out_of_bytesT by exact: poly_out_of_bytesT,
+  Poly_out.bytes_of_poly_outP by exact: bytes_of_poly_outP,
+  Poly_out.bytes_of_poly_outK by exact: bytes_of_poly_outK,
+  C.gt0_max_counter, gt0_block_size, max_cipher_size_ok, topol_inj, poly_out_sub_add, poly_out_add_sub,
+  poly_out_add_sub', poly_out_swap, ge0_pr_zeropol, pr_zeropol_spec.
+realize Poly_in.ge0_poly_in_size by done.
+realize Poly_out.ge0_poly_out_size by done.
+realize Extra_block.ge0_extra_block_size by done.
+realize C.gt0_max_counter by rewrite subr_gt0 exprn_egt1.
+realize gt0_block_size by rewrite /Block.block_size.
+realize max_cipher_size_ok by rewrite /Block.block_size; smt(max_cipher_rg).
+realize topol_inj.
+proof.
+move=> a1 c1 a2 c2 /valid_sizes_size [va1 vc1] /valid_sizes_size [va2 vc2].
+exact: CL.topol_inj.
+qed.
+realize poly_out_sub_add by exact: poly_out_subrK.
+realize poly_out_add_sub by exact: poly_out_addrK.
+realize poly_out_add_sub' by exact: poly_out_addr_subrr.
+realize poly_out_swap by exact: poly_out_subr_addr.
+realize ge0_pr_zeropol by exact: ge0_pr_zeropol.
+realize pr_zeropol_spec.
+proof.
+move=> a1 a2 c1 c2 t1 t2 v1 v2 /=.
+exact: pr_tag_diff_rfc.
+qed.
+
+(* -------------------------------------------------------------------- *)
+lemma neq_w1_w2 : poly_out_of_int 0 <> poly_out_of_int 1.
+proof.
+by rewrite eq_poly_out_of_int mod0z modz_small //=; smt(expr_gt0 exprn_egt1).
+qed.
+
+lemma pr1_poly_outE : RFC8439.pr1_poly_out = 1%r / (2 ^ 128)%r.
+proof.
+rewrite /RFC8439.pr1_poly_out /RFC8439.Poly_out.dpoly_out.
+rewrite (dmap1E_can _ _ bytes_of_poly_out) 1:bytes_of_poly_outKd.
+- by move=> bs; rewrite supp_dlist // => -[sz _]; rewrite poly_out_of_bytesdK.
+rewrite dlist1E // bytes_of_poly_outP /=.
+rewrite (StdBigop.Bigreal.BRM.eq_big_seq _ (fun _ => 1%r / 256%r)) /=.
+- by move=> b _; rewrite ByteFin.dbyte1E card_byte.
+rewrite StdBigop.Bigreal.mulr_const bytes_of_poly_outP -e128.
+by rewrite RField.exprVn // RField.fromintXn.
+qed.
+
+lemma pr1_poly_out_le : RFC8439.pr1_poly_out <= pr_zeropol.
+proof.
+have h106 : 0%r < (2 ^ 106)%r by rewrite lt_fromint expr_gt0.
+have h22 : 1%r <= (2 ^ 22)%r by rewrite le_fromint exprn_ege1.
+have hN : 1%r <= (8 * max_nblocks)%r.
+- by rewrite le_fromint /max_nblocks; smt(divz_ge0 max_ad_rg max_cipher_rg).
+rewrite pr1_poly_outE /pr_zeropol (_ : 2 ^ 128 = 2 ^ 106 * 2 ^ 22).
+- by rewrite -exprD_nneg.
+rewrite RealOrder.ler_pdivl_mulr // fromintM RField.div1r RField.invfM.
+rewrite RField.mulrAC RField.mulVf 1:RealOrder.gtr_eqF // RField.mul1r.
+apply: (RealOrder.ler_trans 1%r _ _ _ hN).
+by rewrite RealOrder.invr_le1 //; smt().
+qed.
+
+(* -------------------------------------------------------------------- *)
+(* The security of ChaCha20-Poly1305 (RFC 8439): a nonce-respecting     *)
+(* adversary making at most qdec decryption queries, with associated    *)
+(* data of at most max_ad bytes and ciphertexts of at most max_cipher   *)
+(* bytes, distinguishes the real scheme from the ideal AEAD with        *)
+(* advantage at most the distance of ChaCha20 from a random oracle plus *)
+(* qdec * (8 * max_nblocks / 2^106 + 1 / 2^128), where max_nblocks is   *)
+(* the number of 16-byte blocks of the MAC input for maximal sizes.     *)
+section Security.
+
+declare module A <: RFC8439.SKE_RND.CCA_Adv {-RFC8439.SKE_RND.Mem,
+  -RFC8439.FullRO.RO, -RFC8439.FullRO.FRO, -RFC8439.IndBlock, -RFC8439.BNR}.
+
+declare axiom A_ll (O <: RFC8439.SKE_RND.CCA_Oracles{-A}) :
+  islossless O.enc => islossless O.dec => islossless A(O).main.
+
+lemma chacha_poly_rfc_security &m :
+  `|Pr[RFC8439.SKE_RND.CCA_game(RFC8439.BNR_Adv(A),
+        RFC8439.SKE_RND.RealOrcls(RFC8439.ChaChaPoly)).main() @ &m : res] -
+    Pr[RFC8439.SKE_RND.CCA_game(RFC8439.BNR_Adv(A),
+        RFC8439.IdealAEAD).main() @ &m : res]| <=
+    `|Pr[RFC8439.Indist.Distinguish(RFC8439.D(RFC8439.BNR_Adv(A)),
+          RFC8439.IndBlock).game() @ &m : res] -
+      Pr[RFC8439.Indist.Distinguish(RFC8439.D(RFC8439.BNR_Adv(A)),
+          RFC8439.IndRO).game() @ &m : res]| +
+    RFC8439.qdec%r * pr_zeropol +
+    RFC8439.qdec%r / (2 ^ 128)%r.
+proof.
+have h := RFC8439.conclusion_ideal_abs A A_ll neq_w1_w2 &m.
+have hm : RealOrder.maxr pr_zeropol RFC8439.pr1_poly_out = pr_zeropol.
+- by rewrite RealOrder.maxrE pr1_poly_out_le.
+by move: h; rewrite hm pr1_poly_outE RField.div1r.
+qed.
+
+end section Security.
diff --git a/examples/ChaChaPoly/poly1305_clamp.ec b/examples/ChaChaPoly/poly1305_clamp.ec
new file mode 100644
index 000000000..93acace94
--- /dev/null
+++ b/examples/ChaChaPoly/poly1305_clamp.ec
@@ -0,0 +1,196 @@
+(* -------------------------------------------------------------------- *)
+(* Poly1305 key clamping and the probability that a clamped key is a    *)
+(* root of the difference of two message polynomials.                   *)
+(* RFC 8439, section 2.5.1: r[3], r[7], r[11], r[15] &= 15 and          *)
+(* r[4], r[8], r[12] &= 252; 22 bits are cleared, so for r made of 16   *)
+(* uniform bytes, each value of the clamped r has probability at most  *)
+(* 2^-106.                                                              *)
+require import AllCore List IntDiv Distr DList StdOrder StdBigop.
+require import Poly1305_prime Poly1305_field Poly1305_msg.
+import IntOrder Bigreal Bigreal.BRM Zp1305 P1305.
+
+abstract theory Clamp.
+
+clone include MacData.
+
+op dbyte : byte distr.
+
+axiom dbyte1E (b : byte) : mu1 dbyte b = 1%r / 256%r.
+
+(* -------------------------------------------------------------------- *)
+(* Indices of the bytes whose top 4 bits, resp. bottom 2 bits, are cleared. *)
+op clampA (i : int) = i = 3 \/ i = 7 \/ i = 11 \/ i = 15.
+op clampB (i : int) = i = 4 \/ i = 8 \/ i = 12.
+
+op clamp_uint (i x : int) =
+  if clampA i then x %% 16 else if clampB i then x - x %% 4 else x.
+
+op clamp_byte (i : int) (b : byte) = of_uint (clamp_uint i (to_uint b)).
+
+op clamp (bs : byte list) =
+  mkseq (fun i => clamp_byte i (nth witness bs i)) 16.
+
+op r_of (bs : byte list) = inzmod (le_int (clamp bs)).
+
+op dr = dmap (dlist dbyte 16) r_of.
+
+(* Number of bytes with a given clamped value.                          *)
+op nfib (i : int) = if clampA i then 16 else if clampB i then 4 else 1.
+
+op cand (i : int) (w : byte) (j : int) =
+  if clampA i then 16 * j + to_uint w else to_uint w + j.
+
+(* -------------------------------------------------------------------- *)
+lemma to_uintK (b : byte) : of_uint (to_uint b) = b.
+proof. by apply: to_uint_inj; rewrite of_uintK // to_uint_rg. qed.
+
+lemma clamp_uint_rg (i x : int) : 0 <= x < 256 => 0 <= clamp_uint i x < 256.
+proof. by rewrite /clamp_uint; smt(modz_ge0 ltz_pmod). qed.
+
+lemma mu_clamp_byte (i : int) (w : byte) :
+  mu dbyte (fun b => clamp_byte i b = w) <= (nfib i)%r / 256%r.
+proof.
+pose s := map (fun j => of_uint (cand i w j)) (range 0 (nfib i)).
+apply: (RealOrder.ler_trans (mu dbyte (mem s))).
+- apply: mu_le => b _ /= hb; apply/mapP.
+  have hw : to_uint w = clamp_uint i (to_uint b).
+  - by rewrite -hb /clamp_byte of_uintK // clamp_uint_rg to_uint_rg.
+  have [ge0_b lt_b] := to_uint_rg b.
+  move: hw; rewrite /cand /nfib /clamp_uint.
+  case: (clampA i) => _ hw.
+  - exists (to_uint b %/ 16); rewrite mem_range hw; split.
+    + by rewrite divz_ge0 //= ltz_divLR.
+    by rewrite -{1}(to_uintK b) {1}(divz_eq (to_uint b) 16) mulrC.
+  move: hw; case: (clampB i) => _ hw.
+  - exists (to_uint b %% 4); rewrite mem_range hw; split.
+    + smt(modz_ge0 ltz_pmod).
+    by rewrite subrK to_uintK.
+  by exists 0; rewrite mem_range hw /= to_uintK.
+apply: (RealOrder.ler_trans _ _ _ (mu_mem_le_mu1 dbyte s (1%r / 256%r) _)).
+- by move=> x; rewrite dbyte1E.
+rewrite size_map size_range ler_maxr; first by rewrite /nfib; smt().
+smt().
+qed.
+
+lemma clamp_inj (bs1 bs2 : byte list) :
+  r_of bs1 = r_of bs2 => clamp bs1 = clamp bs2.
+proof.
+have hp : 256 ^ 16 < p1305.
+- by rewrite p1305E; cbv hint {expr0 expr_pred}.
+have sz : forall bs, size (clamp bs) = 16 by move=> bs; rewrite size_mkseq.
+have := le_int_rg (clamp bs1); have := le_int_rg (clamp bs2); rewrite !sz.
+move=> rg2 rg1; rewrite /r_of -eq_inzmod => h; apply: le_int_inj.
+- by rewrite !sz.
+by move: h; rewrite !modz_small //; smt().
+qed.
+
+lemma prod_nfib :
+  bigi predT (fun i => (nfib i)%r / 256%r) 0 16 = 1%r / (2 ^ 106)%r.
+proof.
+have -> : 2 ^ 106 = 81129638414606681695789005144064.
+- by cbv hint {expr0 expr_pred}.
+rewrite /nfib /clampA /clampB; do 16! (rewrite big_ltn 1:// /=).
+by rewrite big_geq.
+qed.
+
+lemma dr1E (x : zmod) : mu1 dr x <= 1%r / (2 ^ 106)%r.
+proof.
+have h106 : 0 < 2 ^ 106 by rewrite expr_gt0.
+rewrite /dr dmap1E /(\o) /pred1.
+case: (exists bs0, r_of bs0 = x) => [[bs0 <<-]|nx]; last first.
+- have -> : mu (dlist dbyte 16) (fun x0 => r_of x0 = x) = 0%r.
+  + by apply: mu0_false => bs _; apply: contra nx => h; exists bs.
+  by rewrite RField.div1r RealOrder.invr_ge0 le_fromint ltrW.
+pose w := clamp bs0.
+apply: (RealOrder.ler_trans (mu (dlist dbyte 16) (fun xs =>
+  forall i, (0 <= i) && (i < 16) => clamp_byte i (nth witness xs i) = nth witness w i))).
+- apply: mu_le => bs _ /= /clamp_inj h i [ge0_i lt_i].
+  by rewrite /w -h /clamp nth_mkseq.
+have /= -> := dlistE witness dbyte (fun i b => clamp_byte i b = nth witness w i) 16.
+rewrite -RField.div1r -prod_nfib; apply: ler_prod => i _ /=; split.
+- by apply: ge0_mu.
+by move=> _; apply: mu_clamp_byte.
+qed.
+
+(* -------------------------------------------------------------------- *)
+op nblocks (a c : byte list) = (size a + 15) %/ 16 + (size c + 15) %/ 16 + 1.
+
+lemma pr_topol_diff (a1 c1 a2 c2 : byte list) (t : zmod) :
+  valid_size a1 => valid_size c1 => valid_size a2 => valid_size c2 =>
+  (a1, c1) <> (a2, c2) =>
+  mu dr (fun r => peval (topol a2 c2) r - peval (topol a1 c1) r = t)
+  <= (max (nblocks a1 c1) (nblocks a2 c2))%r / (2 ^ 106)%r.
+proof.
+move=> va1 vc1 va2 vc2 neq.
+pose P := topol a2 c2 - topol a1 c1 - polyC t.
+have neq_t : topol a1 c1 <> topol a2 c2.
+- by apply: contra neq => /(topol_inj _ _ _ _ va1 vc1 va2 vc2) [-> ->].
+have c0 : forall a c, (topol a c).[0] = zero by move=> a c; rewrite /topol polyLE.
+have nz_P : P <> poly0.
+- apply: contra neq_t => hP; apply/poly_eqP => k ge0_k.
+  have := congr1 (fun p => p.[k]) _ _ hP => /=.
+  rewrite /P !(polyDE, polyNE) polyCE poly0E.
+  case: (k = 0) => [->> _|_]; first by rewrite !c0.
+  by rewrite ZModpField.oppr0 ZModpField.addr0 ZModpField.subr_eq0 => ->.
+have deg_P : deg P - 1 <= max (nblocks a1 c1) (nblocks a2 c2).
+- rewrite /P; have := degB (topol a2 c2 - topol a1 c1) (polyC t).
+  have := degB (topol a2 c2) (topol a1 c1).
+  have := degC_le t; rewrite !deg_topol /nblocks.
+  smt(divz_ge0 size_ge0).
+rewrite (mu_eq _ _ (root P)) => [r /=|].
+- by rewrite /P !pevalB pevalC ZModpField.subr_eq0.
+apply: (RealOrder.ler_trans _ _ _ (mu_root_le dr P (1%r / (2 ^ 106)%r) nz_P dr1E)).
+have h106 : 0%r < (2 ^ 106)%r by rewrite lt_fromint expr_gt0.
+rewrite RField.div1r; apply: RealOrder.ler_wpmul2r.
+- by rewrite RealOrder.invr_ge0 RealOrder.ltrW.
+by rewrite le_fromint.
+qed.
+
+(* -------------------------------------------------------------------- *)
+(* The Poly1305 tag keeps the low 128 bits of the evaluation, so tags   *)
+(* are compared modulo 2^128. Two field elements x1, x2 have            *)
+(* -p < x2 - x1 < p < 2^130, which leaves at most 8 differences in the  *)
+(* field for a given difference modulo 2^128.                           *)
+op hpoly (r : zmod) (a c : byte list) = asint (peval (topol a c) r).
+
+lemma modz_diff_small (x y d q : int) :
+  0 < q => 0 <= x < 4 * q => 0 <= y < 4 * q => (y - x) %% q = d %% q =>
+  exists k, (-4 <= k < 4) /\ y - x = d %% q + k * q.
+proof.
+move=> gt0_q rgx rgy h; exists ((y - x) %/ q).
+have := divz_eq (y - x) q; rewrite h => e; split; last by rewrite (addrC (d %% q)) -e.
+pose k := (y - x) %/ q.
+have h1 : k * q <= y - x by smt(modz_ge0).
+have h2 : y - x < (k + 1) * q by smt(ltz_pmod).
+split.
+- by rewrite -(ler_pmul2r q) //; smt().
+by rewrite -(ltr_pmul2r q) //; smt().
+qed.
+
+lemma pr_tag_diff (a1 c1 a2 c2 : byte list) (d : int) :
+  valid_size a1 => valid_size c1 => valid_size a2 => valid_size c2 =>
+  (a1, c1) <> (a2, c2) =>
+  mu dr (fun r => (hpoly r a2 c2 - hpoly r a1 c1) %% 2 ^ 128 = d %% 2 ^ 128)
+  <= (8 * max (nblocks a1 c1) (nblocks a2 c2))%r / (2 ^ 106)%r.
+proof.
+move=> va1 vc1 va2 vc2 neq.
+have hq : 0 < 2 ^ 128 by rewrite expr_gt0.
+have hp : p1305 <= 4 * 2 ^ 128.
+- by rewrite p1305E; cbv hint {expr0 expr_pred}.
+apply: (RealOrder.ler_trans (mu dr (fun r => has (fun k =>
+  peval (topol a2 c2) r - peval (topol a1 c1) r = inzmod (d %% 2 ^ 128 + k * 2 ^ 128))
+  (range (-4) 4)))).
+- apply: mu_le => r _ /= h; apply/hasP.
+  have := rg_asint (peval (topol a1 c1) r); have := rg_asint (peval (topol a2 c2) r).
+  move=> rg2 rg1.
+  have [k [rgk e]] := modz_diff_small _ _ d (2 ^ 128) hq _ _ h; 1,2: smt().
+  by exists k; rewrite mem_range rgk /= -e inzmodB !asintK.
+rewrite fromintM -RField.mulrA.
+have := mu_has_leM (fun r k => peval (topol a2 c2) r - peval (topol a1 c1) r
+  = inzmod (d %% 2 ^ 128 + k * 2 ^ 128)) dr (range (-4) 4)
+  ((max (nblocks a1 c1) (nblocks a2 c2))%r / (2 ^ 106)%r) _.
+- by move=> k _ /=; apply: pr_topol_diff.
+by rewrite size_range.
+qed.
+
+end Clamp.
diff --git a/examples/ChaChaPoly/poly1305_field.ec b/examples/ChaChaPoly/poly1305_field.ec
new file mode 100644
index 000000000..bb079eda4
--- /dev/null
+++ b/examples/ChaChaPoly/poly1305_field.ec
@@ -0,0 +1,13 @@
+(* -------------------------------------------------------------------- *)
+(* The field Z/(2^130 - 5) and the polynomials over it.                 *)
+require import AllCore IntDiv.
+require ZModP Poly.
+require import Poly1305_prime.
+
+clone import ZModP.ZModField as Zp1305 with
+  op p <- p1305
+  proof prime_p by exact: prime_p1305.
+
+clone import Poly.Poly as P1305 with
+  type coeff <- zmod,
+  theory IDCoeff <- ZModpField.
diff --git a/examples/ChaChaPoly/poly1305_msg.ec b/examples/ChaChaPoly/poly1305_msg.ec
new file mode 100644
index 000000000..d05f0f8ed
--- /dev/null
+++ b/examples/ChaChaPoly/poly1305_msg.ec
@@ -0,0 +1,213 @@
+(* -------------------------------------------------------------------- *)
+(* The Poly1305 message polynomial of the ChaCha20-Poly1305 AEAD        *)
+(* (RFC 8439, section 2.8): the MAC input                               *)
+(*   a || pad16(a) || c || pad16(c) || le64(|a|) || le64(|c|)           *)
+(* is cut into 16-byte blocks b_1, ..., b_q and gives the polynomial    *)
+(*   sum_i (le(b_i) + 2^128) X^(q - i + 1)                               *)
+(* over Z/(2^130 - 5). Different (a, c) give different polynomials.     *)
+require import AllCore List IntDiv BitEncoding StdOrder.
+require import Poly1305_prime Poly1305_field.
+import IntOrder BitChunking Zp1305 P1305.
+
+abstract theory MacData.
+
+type byte.
+
+op to_uint : byte -> int.
+op of_uint : int -> byte.
+
+axiom to_uint_rg b : 0 <= to_uint b < 256.
+axiom to_uint_inj : injective to_uint.
+axiom of_uintK n : 0 <= n < 256 => to_uint (of_uint n) = n.
+
+(* -------------------------------------------------------------------- *)
+(* Little-endian encoding.                                              *)
+op le_int (bs : byte list) =
+  foldr (fun b n => to_uint b + 256 * n) 0 bs.
+
+op le_bytes (k n : int) =
+  mkseq (fun i => of_uint (n %/ 256 ^ i %% 256)) k.
+
+lemma le_int_nil : le_int [] = 0.
+proof. by rewrite /le_int. qed.
+
+lemma le_int_cons (b : byte) (bs : byte list) :
+  le_int (b :: bs) = to_uint b + 256 * le_int bs.
+proof. by rewrite /le_int. qed.
+
+lemma le_int_rg (bs : byte list) : 0 <= le_int bs < 256 ^ size bs.
+proof.
+elim: bs => [|b bs [ge0 lt]]; first by rewrite le_int_nil expr0.
+rewrite le_int_cons /= exprD_nneg ?size_ge0 // expr1.
+smt(to_uint_rg).
+qed.
+
+lemma le_int_inj (b1 b2 : byte list) :
+  size b1 = size b2 => le_int b1 = le_int b2 => b1 = b2.
+proof.
+elim: b1 b2 => [|x1 b1 ih] [|x2 b2] //=; 1,2: smt(size_ge0).
+move=> eq_sz; rewrite !le_int_cons => h.
+have [h1 h2] : to_uint x1 = to_uint x2 /\ le_int b1 = le_int b2.
+- by smt(to_uint_rg).
+by rewrite (to_uint_inj _ _ h1) (ih b2 _ h2) // /#.
+qed.
+
+lemma le_bytes_cons (k n : int) : 0 <= k =>
+  le_bytes (k + 1) n = of_uint (n %% 256) :: le_bytes k (n %/ 256).
+proof.
+move=> ge0_k; rewrite /le_bytes mkseqSr //= expr0 divz1 /=.
+apply: eq_in_mkseq => i [ge0_i _] /=.
+by rewrite exprD_nneg // expr1 divzMr // expr_ge0.
+qed.
+
+lemma le_bytesK (k n : int) : 0 <= k => 0 <= n < 256 ^ k =>
+  le_int (le_bytes k n) = n.
+proof.
+move=> ge0_k; elim: k ge0_k n => [|k ge0_k ih] n.
+- by rewrite expr0 /le_bytes mkseq0 le_int_nil /#.
+rewrite exprD_nneg // expr1 => -[ge0_n lt_n].
+rewrite le_bytes_cons // le_int_cons of_uintK 1:/# ih; last by smt(divz_eq).
+by rewrite divz_ge0 //= ltz_divLR // mulrC.
+qed.
+
+lemma size_le_bytes (k n : int) : 0 <= k => size (le_bytes k n) = k.
+proof. by move=> ge0_k; rewrite /le_bytes size_mkseq /#. qed.
+
+(* -------------------------------------------------------------------- *)
+(* The MAC input.                                                       *)
+op pad16 (bs : byte list) =
+  nseq ((16 - size bs %% 16) %% 16) (of_uint 0).
+
+op mac_data (a c : byte list) =
+  a ++ pad16 a ++ c ++ pad16 c ++ le_bytes 8 (size a) ++ le_bytes 8 (size c).
+
+op valid_size (bs : byte list) = size bs < 2 ^ 64.
+
+lemma size_pad16 (bs : byte list) :
+  size bs + size (pad16 bs) = 16 * ((size bs + 15) %/ 16).
+proof.
+rewrite /pad16 size_nseq ler_maxr; first by smt(modz_ge0).
+have := divz_eq (size bs) 16; have := modz_ge0 (size bs) 16 _ => //.
+have := ltz_pmod (size bs) 16 _ => //.
+move: (size bs %% 16) (size bs %/ 16) => r q ge0_r lt_r ->.
+case: (r = 0) => [->> /=|nz_r].
+- by rewrite divzMDl // mulrC.
+rewrite modz_small 1:/# (_ : q * 16 + r + 15 = (q + 1) * 16 + (r - 1)) 1:/#.
+by rewrite divzMDl // (divz_small (r - 1)) 1:/#; ring.
+qed.
+
+lemma size_mac_data (a c : byte list) :
+  size (mac_data a c) = 16 * ((size a + 15) %/ 16 + (size c + 15) %/ 16 + 1).
+proof.
+rewrite /mac_data !size_cat !size_le_bytes //.
+smt(size_pad16).
+qed.
+
+lemma eqseq_catr (s1 s2 s3 s4 : 'a list) : size s3 = size s4 =>
+  (s1 ++ s3 = s2 ++ s4) <=> (s1 = s2) /\ (s3 = s4).
+proof.
+move=> eq_sz; split=> [h|[-> ->] //]; apply/eqseq_cat => //.
+by have := congr1 size _ _ h; rewrite !size_cat /#.
+qed.
+
+lemma le_bytes8_inj (n1 n2 : int) : 0 <= n1 < 2 ^ 64 => 0 <= n2 < 2 ^ 64 =>
+  le_bytes 8 n1 = le_bytes 8 n2 => n1 = n2.
+proof.
+have e : 2 ^ 64 = 256 ^ 8 by cbv hint {expr0 expr_pred}.
+rewrite e => h1 h2 h; rewrite -(le_bytesK 8 n1) // -(le_bytesK 8 n2) //.
+by rewrite h.
+qed.
+
+lemma mac_data_inj (a1 c1 a2 c2 : byte list) :
+  valid_size a1 => valid_size c1 => valid_size a2 => valid_size c2 =>
+  mac_data a1 c1 = mac_data a2 c2 => a1 = a2 /\ c1 = c2.
+proof.
+rewrite /valid_size => va1 vc1 va2 vc2; rewrite /mac_data.
+rewrite eqseq_catr ?size_le_bytes // => -[+ hc].
+rewrite eqseq_catr ?size_le_bytes // => -[+ ha].
+have eq_c : size c1 = size c2.
+- by apply: (le_bytes8_inj _ _ _ _ hc); smt(size_ge0).
+have eq_a : size a1 = size a2.
+- by apply: (le_bytes8_inj _ _ _ _ ha); smt(size_ge0).
+rewrite eqseq_catr ?(size_nseq, eq_c) // => -[+ _].
+rewrite eqseq_catr // => -[+ ->]; by rewrite eqseq_catr ?(size_nseq, eq_a).
+qed.
+
+(* -------------------------------------------------------------------- *)
+(* The message polynomial.                                              *)
+op coef (b : byte list) = inzmod (le_int b + 2 ^ 128).
+
+op blocks (a c : byte list) = chunk 16 (mac_data a c).
+
+op topol (a c : byte list) =
+  polyL (zero :: rev (map coef (blocks a c))).
+
+lemma coef_rg (b : byte list) : size b = 16 =>
+  asint (coef b) = le_int b + 2 ^ 128 /\ 2 ^ 128 <= asint (coef b).
+proof.
+move=> sz_b; have := le_int_rg b; rewrite sz_b.
+have -> : 256 ^ 16 = 2 ^ 128 by cbv hint {expr0 expr_pred}.
+have e128 : 2 ^ 128 = 340282366920938463463374607431768211456.
+- by cbv hint {expr0 expr_pred}.
+rewrite /coef inzmodK p1305E e128 => rg; rewrite modz_small /#.
+qed.
+
+lemma coef_inj (b1 b2 : byte list) : size b1 = 16 => size b2 = 16 =>
+  coef b1 = coef b2 => b1 = b2.
+proof.
+move=> sz1 sz2 eq; apply: le_int_inj; 1: by rewrite sz1 sz2.
+by have := coef_rg b1 sz1; have := coef_rg b2 sz2; rewrite eq /#.
+qed.
+
+lemma coef_neq0 (b : byte list) : size b = 16 => coef b <> zero.
+proof.
+move=> sz_b; rewrite -asint_eq zeroE; have [_] := coef_rg b sz_b.
+by move=> h; have /# := expr_gt0 128 2.
+qed.
+
+lemma size_blocks (a c : byte list) :
+  size (blocks a c) = (size a + 15) %/ 16 + (size c + 15) %/ 16 + 1.
+proof. by rewrite /blocks size_chunk // size_mac_data mulKz. qed.
+
+lemma size_in_blocks (a c b : byte list) : b \in blocks a c => size b = 16.
+proof. by apply: in_chunk_size. qed.
+
+lemma last_topol (a c : byte list) :
+  last zero (zero :: rev (map coef (blocks a c))) <> zero.
+proof.
+have : 0 < size (blocks a c) by rewrite size_blocks; smt(divz_ge0 size_ge0).
+have := size_in_blocks a c; case: (blocks a c) => //= b bs hb _.
+by rewrite rev_cons last_rcons; apply: coef_neq0; apply: hb.
+qed.
+
+lemma deg_topol (a c : byte list) :
+  deg (topol a c) = (size a + 15) %/ 16 + (size c + 15) %/ 16 + 2.
+proof.
+by rewrite /topol (degL _ (last_topol a c)) /= size_rev size_map size_blocks; ring.
+qed.
+
+lemma topol_inj (a1 c1 a2 c2 : byte list) :
+  valid_size a1 => valid_size c1 => valid_size a2 => valid_size c2 =>
+  topol a1 c1 = topol a2 c2 => a1 = a2 /\ c1 = c2.
+proof.
+move=> va1 vc1 va2 vc2 eq.
+have eq_sz : size (zero :: rev (map coef (blocks a1 c1)))
+           = size (zero :: rev (map coef (blocks a2 c2))).
+- have := congr1 deg _ _ eq.
+  by rewrite /topol (degL _ (last_topol a1 c1)) (degL _ (last_topol a2 c2)).
+move: eq => /(inj_polyL _ _ eq_sz) /= /rev_inj.
+move=> eq_m.
+have eq_b : blocks a1 c1 = blocks a2 c2.
+- apply: (in_inj_map coef (fun (b : byte list) => size b = 16) _ _ _ _ _ eq_m).
+  + by move=> x y; apply: coef_inj.
+  + by apply/allP => b /size_in_blocks.
+  + by apply/allP => b /size_in_blocks.
+apply: mac_data_inj => //.
+have h1 := chunkK 16 (mac_data a1 c1) _ _ => //.
+- by rewrite size_mac_data dvdz_mulr.
+have h2 := chunkK 16 (mac_data a2 c2) _ _ => //.
+- by rewrite size_mac_data dvdz_mulr.
+by rewrite -h1 -h2; congr; apply: eq_b.
+qed.
+
+end MacData.
diff --git a/examples/ChaChaPoly/poly1305_prime.ec b/examples/ChaChaPoly/poly1305_prime.ec
new file mode 100644
index 000000000..7516ef99d
--- /dev/null
+++ b/examples/ChaChaPoly/poly1305_prime.ec
@@ -0,0 +1,37 @@
+(* -------------------------------------------------------------------- *)
+(* The Poly1305 modulus 2^130 - 5 is prime: a chain of Pocklington      *)
+(* certificates (generated by factoring N - 1 and choosing witnesses).  *)
+require import AllCore List IntDiv Pocklington.
+
+op p1305 : int = 2 ^ 130 - 5.
+
+lemma p1305E : p1305 = 1361129467683753853853498429727072845819.
+proof. by rewrite /p1305; cbv hint {expr0 expr_pred}. qed.
+
+section.
+local lemma prime_5 : prime 5.
+proof. apply (pock_certif 5 [(2, 2); (2, 2)]); [by cbv delta hint +gcd +powmod | by rewrite /= prime2]. qed.
+local lemma prime_11 : prime 11.
+proof. apply (pock_certif 11 [(5, 2)]); [by cbv delta hint +gcd +powmod | by rewrite /= prime_5]. qed.
+local lemma prime_67 : prime 67.
+proof. apply (pock_certif 67 [(11, 2)]); [by cbv delta hint +gcd +powmod | by rewrite /= prime_11]. qed.
+local lemma prime_881 : prime 881.
+proof. apply (pock_certif 881 [(11, 2); (5, 2)]); [by cbv delta hint +gcd +powmod | by rewrite /= prime_11 prime_5]. qed.
+local lemma prime_37003 : prime 37003.
+proof. apply (pock_certif 37003 [(881, 2)]); [by cbv delta hint +gcd +powmod | by rewrite /= prime_881]. qed.
+local lemma prime_221101 : prime 221101.
+proof. apply (pock_certif 221101 [(67, 2); (11, 2)]); [by cbv delta hint +gcd +powmod | by rewrite /= prime_11 prime_67]. qed.
+local lemma prime_4024685905107147541 : prime 4024685905107147541.
+proof. apply (pock_certif 4024685905107147541 [(221101, 2); (37003, 2)]); [by cbv delta hint +gcd +powmod | by rewrite /= prime_221101 prime_37003]. qed.
+local lemma prime_897064739519922787230182993783 : prime 897064739519922787230182993783.
+proof. apply (pock_certif 897064739519922787230182993783 [(4024685905107147541, 2)]); [by cbv delta hint +gcd +powmod | by rewrite /= prime_4024685905107147541]. qed.
+
+lemma prime_p1305 : prime p1305.
+proof.
+rewrite p1305E.
+apply (pock_certif 1361129467683753853853498429727072845819
+                   [(897064739519922787230182993783, 2)]).
+- by cbv delta hint +gcd +powmod.
+by rewrite /= prime_897064739519922787230182993783.
+qed.
+end section.
diff --git a/theories/algebra/Poly.ec b/theories/algebra/Poly.ec
index 750e62e7a..930a5b9cd 100644
--- a/theories/algebra/Poly.ec
+++ b/theories/algebra/Poly.ec
@@ -1,6 +1,6 @@
 (* -------------------------------------------------------------------- *)
 require import AllCore Finite Distr DList List.
-require import Ring IntMin Bigalg StdBigop StdOrder.
+require import Ring IntMin Bigalg StdBigop StdOrder Ideal.
 require (*--*) Subtype.
 (*---*) import Bigint IntID IntOrder.
 
@@ -722,6 +722,16 @@ end BigPoly.
 
 import BigPoly.
 
+(* -------------------------------------------------------------------- *)
+clone import IdealComRing as PIdeal with
+    type t               <- poly,
+  theory IComRing        <- PolyComRing,
+      op BigDom.BAdd.big <- BigPoly.PCA.big<:'a>,
+      op BigDom.BMul.big <- BigPoly.PCM.big<:'a>
+
+  remove abbrev BigDom.BAdd.bigi
+  remove abbrev BigDom.BMul.bigi.
+
 (* -------------------------------------------------------------------- *)
 op peval (p : poly) (a : coeff) =
   BCA.bigi predT (fun i => p.[i] * exp a i) 0 (deg p + 1).
@@ -729,6 +739,156 @@ op peval (p : poly) (a : coeff) =
 (* -------------------------------------------------------------------- *)
 abbrev root p a = peval p a = Coeff.zeror.
 
+(* -------------------------------------------------------------------- *)
+lemma peval_degE p a :
+  peval p a = BCA.bigi predT (fun i => p.[i] * exp a i) 0 (deg p).
+proof.
+rewrite /peval (BCA.big_cat_int (deg p)) ?ge0_deg // 1:/#.
+by rewrite BCA.big_int1 /= gedeg_coeff // mul0r addr0.
+qed.
+
+lemma pevalwE n p a : deg p <= n =>
+  peval p a = BCA.bigi predT (fun i => p.[i] * exp a i) 0 n.
+proof.
+move=> le_pn; rewrite peval_degE (BCA.big_cat_int (deg p) 0 n) ?ge0_deg //.
+rewrite (BCA.big1_seq _ _ (range (deg p) n)) ?addr0 //=.
+by move=> i /mem_range [le_pi _]; rewrite gedeg_coeff // mul0r.
+qed.
+
+(* -------------------------------------------------------------------- *)
+lemma pevalC c a : peval (polyC c) a = c.
+proof.
+by rewrite (pevalwE 1) ?degC_le // BCA.big_int1 /= polyCE /= expr0 mulr1.
+qed.
+
+lemma peval0 a : peval poly0 a = Coeff.zeror.
+proof. by apply: pevalC. qed.
+
+lemma peval1 a : peval poly1 a = Coeff.oner.
+proof. by apply: pevalC. qed.
+
+lemma pevalX a : peval X a = a.
+proof.
+rewrite peval_degE degX (BCA.big_cat_int 1) // !BCA.big_int1 /=.
+by rewrite !polyXE /= mul0r add0r expr1 mul1r.
+qed.
+
+(* -------------------------------------------------------------------- *)
+lemma pevalD p q a : peval (p + q) a = peval p a + peval q a.
+proof.
+pose n := max (deg p) (deg q); rewrite (pevalwE n (p + q)) 1:degD //.
+rewrite (pevalwE n p) 1:/# (pevalwE n q) 1:/# BCA.sumrD.
+by apply: BCA.eq_bigr => i _ /=; rewrite polyDE mulrDl.
+qed.
+
+lemma pevalN p a : peval (-p) a = - peval p a.
+proof.
+rewrite /peval degN BCA.sumrN; apply: BCA.eq_bigr => i _ /=.
+by rewrite polyNE mulNr.
+qed.
+
+lemma pevalB p q a : peval (p - q) a = peval p a - peval q a.
+proof. by rewrite pevalD pevalN. qed.
+
+lemma pevalZ c p a : peval (c ** p) a = c * peval p a.
+proof.
+rewrite (pevalwE (deg p)) 1:degZ_le peval_degE BCA.mulr_sumr.
+by apply: BCA.eq_bigr => i _ /=; rewrite polyZE mulrA.
+qed.
+
+lemma peval_sum ['a] P F s a :
+  peval (PCA.big<:'a> P F s) a = BCA.big P (fun x => peval (F x) a) s.
+proof.
+elim: s => [|x s ih]; first by rewrite PCA.big_nil BCA.big_nil peval0.
+by rewrite PCA.big_cons BCA.big_cons; case: (P x); rewrite ?pevalD ih.
+qed.
+
+(* -------------------------------------------------------------------- *)
+lemma pevalMX p a : peval (p * X) a = peval p a * a.
+proof.
+rewrite (pevalwE (deg p + 1)).
+- apply: deg_leP => [|i le_i]; first by rewrite ler_paddl // ge0_deg.
+  by rewrite polyMXE gedeg_coeff //#.
+rewrite BCA.big_int_recl ?ge0_deg //= polyMXE lt0_coeff //= mul0r add0r.
+rewrite peval_degE BCA.mulr_suml !BCA.big_seq &(BCA.eq_bigr) /=.
+by move=> i /mem_range [ge0_i _]; rewrite polyMXE /= exprSr // mulrA.
+qed.
+
+lemma pevalMXn p a i : 0 <= i => peval (p * exp X i) a = peval p a * exp a i.
+proof.
+elim: i => [|i ge0_i ih]; first by rewrite !expr0 mulr1 Coeff.mulr1.
+by rewrite exprSr // mulrA pevalMX ih exprSr // mulrA.
+qed.
+
+lemma pevalXn a i : 0 <= i => peval (exp X i) a = exp a i.
+proof.
+by move=> ge0_i; rewrite -(mul1r (exp X i)) pevalMXn // peval1 mul1r.
+qed.
+
+lemma pevalM p q a : peval (p * q) a = peval p a * peval q a.
+proof.
+rewrite {1}(polyE q) PCA.mulr_sumr peval_sum (peval_degE q) BCA.mulr_sumr.
+rewrite !BCA.big_seq &(BCA.eq_bigr) => i /mem_range [ge0_i _] /=.
+by rewrite scalepE mulrCA -scalepE pevalZ pevalMXn // mulrCA.
+qed.
+
+lemma peval_exp p a i : 0 <= i => peval (exp p i) a = exp (peval p a) i.
+proof.
+elim: i => [|i ge0_i ih]; first by rewrite !expr0 peval1.
+by rewrite !exprS // pevalM ih.
+qed.
+
+lemma pevalXsubC a b : peval (X - polyC a) b = b - a.
+proof. by rewrite pevalB pevalX pevalC. qed.
+
+(* -------------------------------------------------------------------- *)
+(* Division by (X - a) leaves the remainder peval p a                  *)
+lemma peval_factor p a : exists q, p = q * (X - polyC a) + polyC (peval p a).
+proof.
+have hXn: forall i, 0 <= i =>
+  exists q, exp X i = (X - polyC a) * q + polyC (exp a i).
+- elim=> [|i ge0_i [q qE]]; first by exists poly0; rewrite !expr0 mulr0 add0r.
+  exists (X * q + polyC (exp a i)); rewrite exprS // qE Coeff.exprS // polyCM.
+  by rewrite !mulrDr -addrA -mulrDl subrK mulrCA.
+have: forall s, (forall i, i \in s => 0 <= i) => exists q,
+  PCA.big predT (fun i => p.[i] ** exp X i) s
+  = (X - polyC a) * q + polyC (BCA.big predT (fun i => p.[i] * exp a i) s).
+- elim=> [|i s ih] hs.
+  - by exists poly0; rewrite PCA.big_nil BCA.big_nil mulr0 add0r.
+  case: (ih _) => [j js|q qE]; first by apply: hs; rewrite /= js.
+  case: (hXn i _) => [|r rE]; first by apply: hs.
+  exists (p.[i] ** r + q); rewrite PCA.big_cons BCA.big_cons /= qE rE polyCD.
+  by rewrite scalepDr !scalepE polyCM mulrDr mulrCA addrACA.
+move/(_ (range 0 (deg p)) _); first by move=> i /mem_range [].
+by case=> q qE; exists q; rewrite peval_degE (mulrC q) -qE -polyE.
+qed.
+
+(* -------------------------------------------------------------------- *)
+lemma root0 x : root poly0 x.
+proof. by rewrite peval0. qed.
+
+lemma rootC c x : root (polyC c) x <=> c = Coeff.zeror.
+proof. by rewrite pevalC. qed.
+
+lemma rootX x : root X x <=> x = Coeff.zeror.
+proof. by rewrite pevalX. qed.
+
+lemma rootN p x : root (-p) x <=> root p x.
+proof. by rewrite pevalN oppr_eq0. qed.
+
+lemma root_XsubC a x : root (X - polyC a) x <=> x = a.
+proof. by rewrite pevalXsubC subr_eq0. qed.
+
+(* -------------------------------------------------------------------- *)
+lemma factor_theorem p a : root p a <=> exists q, p = q * (X - polyC a).
+proof.
+split=> [rt|[q ->]]; last by rewrite pevalM pevalXsubC subrr mulr0.
+by case: (peval_factor p a) => q; rewrite rt addr0 => qE; exists q.
+qed.
+
+lemma root_factor_theorem p a : root p a <=> (X - polyC a) %| p.
+proof. by rewrite factor_theorem dvdrP. qed.
+
 (* -------------------------------------------------------------------- *)
 op prepolyL (a : coeff list) = fun i => nth Coeff.zeror a i.
 
@@ -971,4 +1131,73 @@ proof.
 rewrite /polyV; case: (deg p = 1); last done.
 by case/deg_eq1=> c [nz_c ->>]; rewrite !degC polyCE /= invr_eq0.
 qed.
+
+(* -------------------------------------------------------------------- *)
+lemma deg_XsubC a : deg (X - polyC a) = 2.
+proof. by rewrite degDl ?degX // degN degC; case: (a = IDCoeff.zeror). qed.
+
+lemma rootM p q x : root (p * q) x <=> root p x \/ root q x.
+proof. by rewrite pevalM mulf_eq0. qed.
+
+lemma rootZ c p x : c <> IDCoeff.zeror => root (c ** p) x <=> root p x.
+proof. by move=> nz_c; rewrite pevalZ mulf_eq0 nz_c. qed.
+
+lemma factor_theorem_deg p a : p <> poly0 => root p a =>
+  exists q, deg q = deg p - 1 /\ p = q * (X - polyC a).
+proof.
+move=> nz_p /factor_theorem [q ->>]; exists q => /=.
+have nz_q: q <> poly0 by apply: contra nz_p => ->; rewrite mul0r.
+by rewrite degM // -?deg_eq0 deg_XsubC //; ring.
+qed.
+
+(* -------------------------------------------------------------------- *)
+(* A non-zero polynomial has finitely many roots, less than its degree *)
+lemma roots_finite p : p <> poly0 =>
+  exists rs, uniq rs /\ size rs < deg p /\ forall x, root p x <=> x \in rs.
+proof.
+have: forall n, 0 <= n => forall p, p <> poly0 => deg p <= n =>
+  exists rs, uniq rs /\ size rs < deg p /\ forall x, root p x <=> x \in rs.
+- elim=> [|n ge0_n ih] q nz_q le_qn.
+  - by move: le_qn; rewrite lerNgt deg_gt0 nz_q.
+  case: (exists x, root q x) => [[x rx]|nrq]; last first.
+  - exists []; rewrite /= deg_gt0 nz_q /= => y; apply/negP => ry.
+    by apply: nrq; exists y.
+  case: (factor_theorem_deg q x nz_q rx) => r [degr ->>].
+  have nz_r: r <> poly0 by apply: contra nz_q => ->; rewrite mul0r.
+  case: (ih r nz_r _) => [/#|rs [_ [sz_rs hrs]]].
+  exists (undup (x :: rs)); split; first by apply: undup_uniq.
+  split=> [|y]; last by rewrite mem_undup /= -hrs rootM root_XsubC orbC.
+  by apply: (ler_lt_trans (size (x :: rs))) => [|/#]; apply: size_undup.
+by move=> h nz_p; apply: (h (deg p)) => //; apply: ge0_deg.
+qed.
+
+lemma max_poly_roots p rs :
+  p <> poly0 => all (root p) rs => uniq rs => size rs < deg p.
+proof.
+move=> nz_p /allP rts uq_rs; case: (roots_finite p nz_p) => s [_ [sz hs]].
+apply: (ler_lt_trans _ _ _ _ sz); apply: uniq_leq_size => // x /rts /=.
+by rewrite hs.
+qed.
+
+(* -------------------------------------------------------------------- *)
+lemma mu_root_le (d : coeff distr) p m :
+     p <> poly0
+  => (forall x, mu1 d x <= m)
+  => mu d (root p) <= (deg p - 1)%r * m.
+proof.
+move=> nz_p le_m; case: (roots_finite p nz_p) => rs [_ [sz hrs]].
+rewrite (mu_eq d _ (mem rs)) => [x /=|]; first by rewrite hrs.
+apply: (RealOrder.ler_trans _ _ _ (mu_mem_le_mu1 d rs m le_m)).
+apply: RealOrder.ler_wpmul2r; last by rewrite le_fromint /#.
+by apply: (RealOrder.ler_trans _ _ _ (ge0_mu d (pred1 witness)) (le_m witness)).
+qed.
+
+lemma mu_root_uni (d : coeff distr) p :
+     p <> poly0 => is_lossless d => is_uniform d
+  => mu d (root p) <= (deg p - 1)%r / (size (to_seq (support d)))%r.
+proof.
+move=> nz_p d_ll d_uni; apply: mu_root_le => // x.
+rewrite mu1_uni_ll // RField.div1r; case: (x \in d) => // _.
+by rewrite RealOrder.invr_ge0 le_fromint size_ge0.
+qed.
 end Poly.
diff --git a/theories/algebra/PolyReduce.ec b/theories/algebra/PolyReduce.ec
index ea679bf93..bf4c85cbf 100644
--- a/theories/algebra/PolyReduce.ec
+++ b/theories/algebra/PolyReduce.ec
@@ -16,17 +16,7 @@ clone export PolyComRing as BasePoly
   with type   coeff <- coeff,
        theory Coeff <- Coeff.
 
-import Coeff BigPoly BigCf.
-
-(* -------------------------------------------------------------------- *)
-clone import IdealComRing as PIdeal with
-    type t               <- BasePoly.poly,
-  theory IComRing        <- BasePoly.PolyComRing,
-      op BigDom.BAdd.big <- BasePoly.BigPoly.PCA.big<:'a>,
-      op BigDom.BMul.big <- BasePoly.BigPoly.PCM.big<:'a>
-
-  remove abbrev BigDom.BAdd.bigi
-  remove abbrev BigDom.BMul.bigi.
+import Coeff BigPoly BigCf PIdeal.
 
 import PCA.