Distributivity of exponentials

CLAUDE.md

@@ -85,8 +85,12 @@ Key dependencies (authoritative pins live in `rocq-cryptis.opam` — treat it as
 - `THash t` — hashes
 - `TNonFree pt of PreTerm.wf pt & is_non_free pt` — the Diffie–Hellman fragment (inverse / exponentiation / product), represented indirectly by a well-formed `PreTerm.pre_term`
 
+Underneath, `PreTerm.pre_term` is an *arity-indexed* datatype: `PT0 o`, `PT1 o pt`, `PT2 o pt1 pt2` and `PTN o ts`, where the operations of each arity live in their own inductive (`term_op0`, `term_op1`, `term_op2`, `term_opN`) with its own derived `eqType`/`choiceType`/`countType`/`orderType`. `term_opN` currently has the single constructor `ONMul`, and `PTMul ts` is a `Notation` for `PTN ONMul ts` — so `match`es and `case` patterns keep naming products directly, and adding a second n-ary operation turns every product-specific `match` into a non-exhaustiveness error rather than a silent wrong branch. Two habits follow: in `case`/`elim` intro patterns the n-ary branch destructs the operation (`case: pt => [o|o t|o t1 t2|[] ts]`, or `[|||[] ts]` when the other branches need no names) exactly as the op1/op2 branches already do (`[k| |]`, `[||]`); and structural functions that ignore the operation (`height`, `PreTerm.tsize`, `nonces_of_pre_term`) match on `PTN _ ts`, while product-specific ones (`is_mul`, `factors`, `wf`, `normalize`) match on `PTMul`. The HeapLang encoding mirrors the arities too: `(#TOpN_tag, (repr o, repr_list …))`, with `repr ONMul = #TMul_tag`.
+
 `TInv`, `TExp`, `TExpN`, `TMul`, `TMulN` are **smart constructors** (locked `Definition`s over `TNonFree`), *not* real constructors — so `case`/`elim` on them is not structural; use the custom induction principles (`term_ind`/`term_rect` in `core/term/base.v`, `term_lt_ind` in `core/term/tsize.v`). Typed key wrappers `aenc_key`/`sign_key`/`senc_key` sit on top of `TKey`, and the surface API lives in `Module Spec` (`core/term/spec.v`: `Spec.tag`, `Spec.of_list`, `Spec.pkey`, `Spec.to_list`, …).
 
+Exponentiation is an endomorphism of the multiplicative group: `(a·b)^x = a^x·b^x`, and hence also `1^x = 1` and `(a⁻¹)^x = (a^x)⁻¹`. `PreTerm.wf` therefore demands that the base of a normal-form exponential be an **atom** — neither product, nor inverse, nor exponential (`negb (is_non_free b)`); `PreTerm.exp` re-establishes this by spreading over `PreTerm.factors` (`exp b e := mul ((λ t, exp_aux t e) <$> factors b)`, with `exp_aux` handling the `PTInv` case and `mk_exp` the `e = 1` guard). Two consequences bite downstream: `TExp` is **not** injective in the exponent at the unit base, so `TExp_injr`, `base_TExp`, `expo_TExp`, `tsize_TExp`, `minted_TExp`, `public_TExpN` and friends carry `negb (is_mul b)` / `negb (is_inv b)` premises; and a protocol that exponentiates an attacker-supplied value must either reject the identity or reason factor-by-factor (`factors_TExp`, `public_TExp_factors`, `subterm_TExp_factors`).
+
 The term layer is split across `core/term/` and aggregated by `core/term.v`: `base.v` (the `term` inductive, the `unfold`/`fold` ↔ `pre_term` conjugation, smart constructors, instances, destructor defs, the `count` API (`count`, `count_inj`, `count_TMulN`, `count_TInv`, …), and the structural `term_rect`/`term_ind` eliminators), `algebra.v` (multiplicative-group + DH-exponentiation laws), `tsize.v` (the `tsize` measure, its termination lemmas, and the well-founded `term_lt_rect`/`term_lt_ind`), `repr.v` (`val_of_term`/`repr`), `nonces.v`, `subterms.v`, `spec.v`. Downstream imports `cryptis.core.term`, so the split is transparent — but **module-qualified references (`base.foo`) break when a lemma moves file**; prefer unqualified names. Each split file must re-declare the file-local `Implicit Types (t k : term) (ts : list term).` and `Set Implicit Arguments.` block (those do not cross a `Require` boundary).
 
 **The Public Predicate** (`core/public.v`): Central to the framework. `public t` (an Iris proposition) holds when term `t` is known to the attacker. Protocol proofs establish invariants about which terms are and are not public.
@@ -116,7 +120,7 @@ examples/*
 
 The `_CoqProject` file specifies the exact file ordering for compilation.
 
-**mathcomp ↔ stdpp boundary:** `core/pre_term/base.v` is implemented in mathcomp (`seq`, `%O` order, `~~`, `sort <=%O`, bigops, `deriving`); `core/pre_term/normalize.v` (normal forms + the `wf`/`normalize` machinery) is already stdpp-only. `core/pre_term/with_stdpp.v` is *the* bridge, and is where any new mathcomp→stdpp translation belongs: it packages the deriving-generated order both as `pt_order` (a stdpp `relation` with `RelDecision`/`Transitive`/`Total`/`AntiSymm`) and as a global `Lexico PreTerm.pre_term` instance (with `StrictOrder`/`TrichotomyT`, which is what makes `bool_decide (x = y ∨ lexico x y)` decidable), and proves `pt_order_lexico`, `pt_order_mul` (the derived order on `PTMul ts` *is* stdpp's `lexico` on `ts`) and `pt_orderE` (the structural comparison equation, stated with `bool_decide` and `op0_le`/`op1_le`/`op2_le` instead of `<=%O`). Because of that bridge, `primitives/pre_term.v` — which implements the `normalize.v` operations in HeapLang — needs no mathcomp beyond `ssreflect`. Everything from `core/term/` upward is stdpp (`Forall`, `≡ₚ`, `∈`, `merge_sort`). The active boolean→Prop coercion above `pre_term` is stdpp's `Is_true`, **not** ssreflect's `is_true` (bridged by `is_trueP` in `lib/mathcomp_compat.v`); mixing the two silently breaks `rewrite`/`apply`.
+**mathcomp ↔ stdpp boundary:** `core/pre_term/base.v` is implemented in mathcomp (`seq`, `%O` order, `~~`, `sort <=%O`, bigops, `deriving`); `core/pre_term/normalize.v` (normal forms + the `wf`/`normalize` machinery) is already stdpp-only. `core/pre_term/with_stdpp.v` is *the* bridge, and is where any new mathcomp→stdpp translation belongs: it packages the deriving-generated order both as `pt_order` (a stdpp `relation` with `RelDecision`/`Transitive`/`Total`/`AntiSymm`) and as a global `Lexico PreTerm.pre_term` instance (with `StrictOrder`/`TrichotomyT`, which is what makes `bool_decide (x = y ∨ lexico x y)` decidable), and proves `pt_order_lexico`, `pt_order_N` (the derived order on `PTN o ts` *is* stdpp's `lexico` on `ts`) and `pt_orderE` (the structural comparison equation, stated with `bool_decide` and `op0_le`/`op1_le`/`op2_le`/`opN_le` instead of `<=%O`). Because of that bridge, `primitives/pre_term.v` — which implements the `normalize.v` operations in HeapLang — needs no mathcomp beyond `ssreflect`. Everything from `core/term/` upward is stdpp (`Forall`, `≡ₚ`, `∈`, `merge_sort`). The active boolean→Prop coercion above `pre_term` is stdpp's `Is_true`, **not** ssreflect's `is_true` (bridged by `is_trueP` in `lib/mathcomp_compat.v`); mixing the two silently breaks `rewrite`/`apply`.
 
 ### Case Studies
 

cryptis/core/minted.v

@@ -57,11 +57,12 @@ Lemma minted_TInv t : minted (TInv t) ⊣⊢ minted t.
 Proof. by rewrite unlock nonces_of_termE. Qed.
 
 Lemma minted_TExpN t ts :
-  negb (is_exp t) -> invs_canceled ts ->
+  negb (is_exp t) -> negb (is_mul t) -> negb (is_inv t) ->
+  invs_canceled ts ->
   minted (TExpN t ts) ⊣⊢ minted t ∧ [∗ list] t' ∈ ts, minted t'.
 Proof.
-move => nx ic.
-rewrite unlock (nonces_of_term_TExpN nx ic) big_sepS_union_pers.
+move => nx nm ni ic.
+rewrite unlock (nonces_of_term_TExpN nx nm ni ic) big_sepS_union_pers.
 by rewrite big_sepS_union_list_pers big_sepL_fmap.
 Qed.
 
@@ -74,11 +75,13 @@ rewrite unlock (nonces_of_term_TMulN ic).
 by rewrite big_sepS_union_list_pers big_sepL_fmap.
 Qed.
 
+(* Unconditional: [nonces_of_term_base_exps] holds for every [t], including a
+   product, where [base t = t] and [exps t = []]. *)
 Lemma minted_base_exps t :
   minted t ⊣⊢ minted (base t) ∧ [∗ list] t' ∈ exps t, minted t'.
 Proof.
-by rewrite -{1}[t]base_expsK
-  (minted_TExpN (base_Nexp t) (invs_canceled_factors (expo t))).
+rewrite unlock (nonces_of_term_base_exps t) big_sepS_union_pers.
+by rewrite big_sepS_union_list_pers big_sepL_fmap.
 Qed.
 
 Lemma all_minted_TExpN t ts :
@@ -103,12 +106,12 @@ by rewrite big_sepS_union_list_pers big_sepL_fmap.
 Qed.
 
 Lemma minted_TExp t1 t2 :
-  negb (is_exp t1) ->
+  negb (is_exp t1) -> negb (is_mul t1) -> negb (is_inv t1) ->
   minted (TExp t1 t2) ⊣⊢ minted t1 ∧ minted t2.
 Proof.
-move => nx.
+move => nx nm ni.
 have -> : TExp t1 t2 = TExpN t1 (factors t2) by rewrite /TExpN factorsK.
-rewrite (minted_TExpN nx (invs_canceled_factors t2)).
+rewrite (minted_TExpN nx nm ni (invs_canceled_factors t2)).
 by rewrite -minted_factors.
 Qed.
 
@@ -132,7 +135,7 @@ Lemma minted_to_list t ts :
   minted t -∗ [∗ list] t' ∈ ts, minted t'.
 Proof.
 elim/term_ind': t ts => //=.
-  by case=> // ts [<-] /=; iIntros "?".
+  by case=> // [] ts [<-] /=; iIntros "?".
 move=> t _ tl IH ts.
 case e: (Spec.to_list tl) => [ts'|] // [<-] /=.
 rewrite minted_TPair /=; iIntros "[??]"; iFrame.

cryptis/core/pre_term.v

@@ -15,7 +15,7 @@ Fixpoint tsize (pt : pre_term) : nat :=
   | PT0 _ => 1
   | PT1 _ pt => S (tsize pt)
   | PT2 _ t1 t2 => S (tsize t1 + tsize t2)
-  | PTMul ts => S (sum_list_with tsize ts)
+  | PTN _ ts => S (sum_list_with tsize ts)
   end.
 
 End PreTerm.

cryptis/core/pre_term/base.v

@@ -104,10 +104,29 @@ HB.instance Definition _ := term_op2_isCountable.
 Definition term_op2_isOrder := [derive isOrder for term_op2].
 HB.instance Definition _ := term_op2_isOrder.
 
+Inductive term_opN :=
+| ONMul.
+
+Notation TMul_tag := 0%Z.
+
+Canonical term_opN_indDef := [indDef for term_opN_rect].
+Canonical term_opN_indType := IndType term_opN term_opN_indDef.
+Definition term_opN_hasDecEq := [derive hasDecEq for term_opN].
+#[warnings="-projection-no-head-constant"]
+HB.instance Definition _ := term_opN_hasDecEq.
+Definition term_opN_hasChoice := [derive hasChoice for term_opN].
+#[warnings="-projection-no-head-constant"]
+HB.instance Definition _ := term_opN_hasChoice.
+Definition term_opN_isCountable := [derive isCountable for term_opN].
+#[warnings="-projection-no-head-constant"]
+HB.instance Definition _ := term_opN_isCountable.
+Definition term_opN_isOrder := [derive isOrder for term_opN].
+HB.instance Definition _ := term_opN_isOrder.
+
 Notation TOp0_tag := 0%Z.
 Notation TOp1_tag := 1%Z.
 Notation TOp2_tag := 2%Z.
-Notation TMul_tag := 3%Z.
+Notation TOpN_tag := 3%Z.
 
 Module PreTerm.
 
@@ -116,34 +135,35 @@ Inductive pre_term :=
 | PT0 of term_op0
 | PT1 of term_op1 & pre_term
 | PT2 of term_op2 & pre_term & pre_term
-| PTMul of list pre_term.
+| PTN of term_opN & list pre_term.
 Set Elimination Schemes.
 
 (** Convenient shorthands for some operations *)
 Notation PTInv e := (PT1 O1Inv e).
 Notation PTExp b e := (PT2 O2Exp b e).
+Notation PTMul ts := (PTN ONMul ts).
 
 Definition pre_term_rect'
   (T1 : pre_term -> Type)
   (T2 : list pre_term -> Type)
   (H1 : forall o, T1 (PT0 o))
   (H2 : forall o t1, T1 t1 -> T1 (PT1 o t1))
   (H3 : forall o t1, T1 t1 -> forall t2, T1 t2 -> T1 (PT2 o t1 t2))
-  (Hmul : forall ts, T2 ts -> T1 (PTMul ts))
+  (HN : forall o ts, T2 ts -> T1 (PTN o ts))
   (H5 : T2 [::])
   (H6 : forall t, T1 t -> forall ts, T2 ts -> T2 (t :: ts)) :=
   fix loop1 t {struct t} : T1 t :=
     match t with
     | PT0 o => H1 o
     | PT1 o t => H2 o t (loop1 t)
     | PT2 o t1 t2 => H3 o t1 (loop1 t1) t2 (loop1 t2)
-    | PTMul ts =>
+    | PTN o ts =>
       let fix loop2 ts {struct ts} : T2 ts :=
           match ts with
           | [::] => H5
           | t :: ts => H6 t (loop1 t) ts (loop2 ts)
           end in
-      Hmul ts (loop2 ts)
+      HN o ts (loop2 ts)
     end.
 
 Definition list_pre_term_rect'
@@ -152,14 +172,14 @@ Definition list_pre_term_rect'
   (H1 : forall o, T1 (PT0 o))
   (H2 : forall o t1, T1 t1 -> T1 (PT1 o t1))
   (H3 : forall o t1, T1 t1 -> forall t2, T1 t2 -> T1 (PT2 o t1 t2))
-  (Hmul : forall ts, T2 ts -> T1 (PTMul ts))
+  (HN : forall o ts, T2 ts -> T1 (PTN o ts))
   (H5 : T2 [::])
   (H6 : forall t, T1 t -> forall ts, T2 ts -> T2 (t :: ts)) :=
   fix loop2 ts {struct ts} : T2 ts :=
     match ts with
     | [::] => H5
     | t :: ts =>
-      H6 t (@pre_term_rect' T1 T2 H1 H2 H3 Hmul H5 H6 t) ts (loop2 ts)
+      H6 t (@pre_term_rect' T1 T2 H1 H2 H3 HN H5 H6 t) ts (loop2 ts)
     end.
 
 Combined Scheme pre_term_list_pre_term_rect
@@ -181,8 +201,8 @@ Definition pre_term_rect (T : pre_term -> Type)
   (H1 : forall o, T (PT0 o))
   (H2 : forall o t1, T t1 -> T (PT1 o t1))
   (H3 : forall o t1, T t1 -> forall t2, T t2 -> T (PT2 o t1 t2))
-  (Hmul : forall ts, foldr (fun t R => T t * R)%type unit ts ->
-          T (PTMul ts)) t : T t.
+  (HN : forall o ts, foldr (fun t R => T t * R)%type unit ts ->
+          T (PTN o ts)) t : T t.
 Proof.
 exact: (@pre_term_rect' T (foldr (fun t R => T t * R)%type unit)).
 Defined.
@@ -199,7 +219,7 @@ Definition cons_num pt : Z :=
   | PT0 _ => TOp0_tag
   | PT1 _ _ => TOp1_tag
   | PT2 _ _ _ => TOp2_tag
-  | PTMul _ => TMul_tag
+  | PTN _ _ => TOpN_tag
   end.
 
 Open Scope order_scope.
@@ -248,15 +268,16 @@ Lemma leqE pt1 pt2 :
       if o1 == o2 then
         if t11 == t21 then (t12 <= t22)%O else (t11 <= t21)%O
       else (o1 <= o2)%O
-    | PTMul ts1, PTMul ts2 =>
-      ((ts1 : seqlexi_with Order.default_display _) <= ts2)%O
+    | PTN o1 ts1, PTN o2 ts2 =>
+      if o1 == o2 then ((ts1 : seqlexi_with Order.default_display _) <= ts2)%O
+      else (o1 <= o2)%O
     | _, _ => false
     end
   else (cons_num pt1 <=? cons_num pt2)%Z.
 Proof.
 case: pt1 pt2
-    => [o1|o1 t1|o1 t11 t12|ts1]
-       [o2|o2 t2|o2 t21 t22|ts2] //=.
+    => [o1|o1 t1|o1 t11 t12|o1 ts1]
+       [o2|o2 t2|o2 t21 t22|o2 ts2] //=.
 - by rewrite [RHS]le_alt.
 - by rewrite [(t1 <= t2)%O]le_alt.
 - by rewrite (le_alt t12).