[JasonGross]

Represent Word.Naive words as stdlib bits width (that is, Zmod (2^width)) instead of the hand-rolled { unsigned ; proof } record, and use the stdlib Zmod operations for arithmetic, bitwise operations, shifts and division. Division by zero keeps the previous default semantics because Zmod.udiv/umod/squot/srem already agree with the old default handlers, so the div_by_zero and mod_by_zero handler fields are gone (special_cases keeps only adjust_too_big_shift_amount). All exported names that downstream code uses (rep, unsigned, signed, wrap, gen_word, gen_ok, word, ok, word8..word512) keep their names and arities; mk, _unsigned_in_range and minimize_eq_proof are removed. Naive.rep width is definitionally bits width, so destruct on a word no longer yields a { unsigned ; proof } pair.

The record fields are the stdlib operations themselves (Zmod.add, Zmod.udiv, ...), with the shift amount adjustment kept as before; no wrappers and no simpl never flags. One caveat for downstream proofs: cbn/simpl through Zmod.add/of_small_Z duplicates subterms at each nesting level, so a bare cbn on deeply nested word arithmetic is exponential; proofs about concrete words should rewrite with the word.unsigned_* interface lemmas or use a targeted reduction. Only three downstream sites needed that (two proofs in bedrock2's compiler, one hint in rupicola).

Zmod first ships in rocq-stdlib 9.1, so the opam bound moves to rocq-stdlib >= 9.1. Rocq 9.0 and 9.1 are dropped from CI: their rocq/rocq-prover docker images ship rocq-stdlib 9.0.0 (no Zmod), so CI tests 9.2 and dev; the opam bound stays rocq-stdlib >= 9.1, which does allow Rocq 9.1. Downstream adaptations: mit-plv/bedrock2 (one proof file in the compiler) and mit-plv/rupicola (two examples); those PRs are linked in a comment below once open.

Written by Claude Fable 5.1 from Andres Erbsen's feasibility sketch (https://gist.github.com/andres-erbsen/17b583447d29dc085714bb8e9c7cdc89).

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm

[JasonGross]

Downstream adaptations: mit-plv/bedrock2#561 and mit-plv/rupicola#225 (both draft until this merges); fiat-crypto PR to follow.

---

Written by Claude Fable 5.1 via Claude Code (session https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm).

[JasonGross]

fiat-crypto side: mit-plv/fiat-crypto#2434 (draft until the chain above merges).

---

Written by Claude Fable 5.1 via Claude Code (session https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm).

[JasonGross]

Kami side: mit-plv/kami#51 (Kami words as stdlib bits), with a bedrock2 bridge simplification to follow, stacked on mit-plv/bedrock2#561.

---

Written by Claude Fable 5.1 via Claude Code (session https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm).

[andres-erbsen]

Does this line update rocq to 9.2 even if matrix lists 9.1?

[JasonGross]

I believe it does not (and claude agrees). I am not sure if there is a way to make it error if there are incompatibilities

[andres-erbsen]

I still don't feel great about having the conditional opam install in every CI script, with a patch version of stdlib pinned in it even. I'd rather just drop 9.1 support on opam, I think. It's possible there is a neat alternative, but I can't think of it just now.

[JasonGross]

We can ask upstream to maintain docker images for all compatible Rocq*stdlib versions?

[andres-erbsen]

I'd rather not deal with upstream, but if you wish, we can try.

[JasonGross]

Done: the pin script is gone and Rocq 9.1 is out of the docker matrix here and in bedrock2/rupicola, so CI tests 9.2 and dev with the build step exactly as on master. The opam bound stays rocq-stdlib >= 9.1~ (rocq-stdlib 9.1.0 does allow Rocq 9.1; it is just not tested).

---

Written by Claude Fable 5.1 via Claude Code (session https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm).

[andres-erbsen]

Would abbreviations work here?

[JasonGross]

No, the purpose is specifically to control performance of cbn. simpl never is attached to constants, whereas abbreviations are only for parsing/printing/naming.

[andres-erbsen]

Yes, but is the control actually necessary? I see some unfoldings added for the wrappers in downstream PRs. Could we fix the runaway simpl/cbn calls instead?

[JasonGross]

You can replace them with manual change or some other tactic. You can also do local simplification control in each file, but Claude was claiming that runaway cbn is a foot gun. What's your preference?

[andres-erbsen]

I think we should avoid Definition wrappers. Maaybe some Zmod definitions should be globally simpl never, I think that'd still be preferable. But cbn without arguments is a footgun regardless, so idk, as long as the appropriate cbn calls don't look too bad without adding simpl never i'd still go with that. If we need to use change, that may be a sign that something is wrong.

[JasonGross]

Done: the wrappers are gone and nothing is simpl never any more, here or downstream. The record fields are the stdlib operations directly, and the ! flags at the end of the file are back to what master has. Downstream, three sites needed a targeted reduction instead of a bare one: the two NaiveRiscvWordProperties proofs in bedrock2 (cbv with a named list of projections), and in rupicola one hint that ran cbn; lia on every goal (now restricted to arithmetic goal shapes) plus one line reverted to master's text. The local simpl never declarations that bedrock2's KamiWord.v carried are removed too; the Kami cone builds in the same time without them. fiat-crypto needed two one-line adjustments. The three lemmas in this file that restated stdlib ones (unsigned_inj, of_Z_unsigned, signed_of_Z) are dropped as well.

---

Written by Claude Fable 5.1 via Claude Code (session https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm).

[andres-erbsen]

After consolidating word type in Kami, we should revisit whether these adjustments are still necessary for the lightbulb end2end proof to go through.

[JasonGross]

Claude claims the consolidation is done in mit-plv/kami#51 and mit-plv/bedrock2#562, and the shift division conventions were kept unchanged "on purpose". I have asked Fable what this means

[JasonGross]

Apparently it means "I didn't want to change the lightbulb theorem statement", I suspect this happened after it got shifted from Fable to Opus. I have asked it to investigate / fix

[JasonGross]

Checked this once the Kami side was on stdlib bits (mit-plv/kami#51, mit-plv/bedrock2#562): the Kami-side word instance and Naive.word agree on all 26 fields at widths 32 and 8 (lemmas, not just spot checks), so bedrock2's processor bridge now simply is Naive.word and its own riscv_ok file is gone (mit-plv/bedrock2#563). The adjustment itself is still needed, though: without it Naive.word violates riscv_ok's slu_ignores_hibits (counterexample y = 1, z = 32), so the compiler theorem could not be instantiated at Naive at all. Before, the lightbulb proof did not depend on it (the Kami-side instance masked shift amounts with mod width itself); after the unification it does, like every other Naive user. What is superfluous is only the generality of the special_cases record, since every user passes the default handler.

---

Written by Claude Fable 5.1 via Claude Code (session https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm).

[JasonGross]

Claude is pretending to be me, I need to tell it to stop posting without attaching a Claude footer

[andres-erbsen]

Let's consider alternatives that don't need adding ad-hoc scripts to every projects CI config. For example, would it work to test opam only on Rocq 9.2?

[andres-erbsen]

These changes look good. Let's wait with merging until other repos are also approved.

When preparing PRs for repos that depend on coqutil, update git submodules such that all PRs test the approved coqutil change and are strictly up to date with the appropriate repository's master branch. When the first set of PRs is approved and passing CI on all repos, I want to be able to fast-forward all master branches to the PR-proposed versions (atomically across all repos, without recomputing submodule hashes).

[JasonGross]

Re-pinned for the atomic fast-forward. Every branch is on its repository's current master with no merge commits, and each pins the tip listed here for its dependency:

repo	PR	tip	on master	pins
coqutil	#186	ac2f85a	6d8b171
bedrock2	mit-plv/bedrock2#561	257a21d2	06655844	deps/coqutil ac2f85a (deps/kami, deps/riscv-coq as on master)
rupicola	mit-plv/rupicola#225	09c05c1c	5d37f856	bedrock2 257a21d2
fiat-crypto	mit-plv/fiat-crypto#2434	07ca965a	96b11d5f	rupicola 09c05c1c (coqprime, rewriter, coq-scripts as on master)

mit-plv/fiat-crypto#2435 (186e533f) is #2434 plus one commit. The Kami set is a second wave on top of these: mit-plv/kami#51 (dbba41f), mit-plv/bedrock2#562 (61831cc2, pins coqutil ac2f85a and kami dbba41f) and #563 (207ec716).

---

Written by Claude Fable 5.1 via Claude Code (session https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm).

[andres-erbsen]

Now let's create another stack of PRs to remove the Word interface altogether, hardcoding stdlib bits everywhere!

[JasonGross]

Starting on it. Survey and plan, for the record before the code arrives:

Shape. bits width is the type everywhere, Bitwidth width stays as the only class (gaining width_pos), and inside the existing sections Context {word: word.word width} becomes Local Notation word := (bits width) so the thousands of x : word sites are untouched. Operations are the stdlib ones; lemmas at use sites are the stdlib ones (Zmod.unsigned_add, bits.unsigned_range x width_nonneg, bits.unsigned_of_Z_small, ...); word.ok and every instance proof (Naive, KamiWord, BasicCSemantics, the two RiscvWordProperties files) are deleted, as are Interface.v, Naive.v and DebugWordEq.v. stdlib's udiv/umod/squot/srem already have the RISC-V by-zero semantics, so word.riscv_ok disappears; the shift-amount masking that Naive did is a language fact and gets spelled out in Semantics.interp_binop (Zmod.slu a (Zmod.unsigned b mod 2 ^ Z.log2 width)), after which riscv-coq's sll is plain Zmod.slu. What coqutil keeps of Properties.v is only what the stdlib lacks (ring hooks for Zmod.ring_theory with the of_Z morphism, the Z.smodulo bridge, broadcast, a handful of if/bool lemmas, the Decidable instances; roughly 150-200 lines). ZnWords is rebuilt one-for-one on stdlib lemmas; LiveVerif's bottom_up_simpl/unzify patterns move from @word.unsigned ?wi ?wo to @Zmod.unsigned (2^?w). The processor width is a concrete 32, so Kami's word 32 is convertible to bits 32: the kami repo needs no change, KamiWord.v shrinks to the wordToN/split/combine transport lemmas, and (per the note on mit-plv/bedrock2#563) the unification lands inside this set.

Stack (each on its repo's master, pinning the previous tip, as in the first wave): 1 coqutil (17 files, about -1300/+450); 2 riscv-coq (31 files); 3 bedrock2 as one PR with commits per subproject (171 files; it cannot be split, the compiler instantiates Semantics' types); 4 rupicola (50 files); 5 fiat-crypto (52 files, Types.parameters loses its word fields). Direct route rather than an intermediate "word is a definition" state: the expensive edits are the same either way and the intermediate state breaks every Ltac pattern on word.unsigned a second time. Sizes: about 2100 of_Z sites need an explicit width (bits.of_Z width z; /[x] stays for type-determined positions), 290 context lines go, 37 downstream Add Ring sites keep their four-line form with new names.

Questions where the design forks (proceeding with the first option unless you say otherwise): (1) shift masking spelled out in interp_binop rather than a named coqutil helper; (2) generic coqutil files take an explicit 0 < width hypothesis, downstream files use Bitwidth (about 40 files currently assume word.ok without it and get the class added); (3) no coqutil duplicate of unsigned_range, use bits.unsigned_range x width_nonneg at the 170 sites; (4) bits.of_Z width z spelled explicitly rather than a per-section notation; (5) the Z.smodulo bridge and the of_Z ring morphism are stdlib-shaped and could go to rocq-stdlib afterwards, coqutil keeps copies until then.

---

Written by Claude Fable 5.1 via Claude Code (session https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm).

[andres-erbsen]

feel free to use bits.of_Z _ z and/or a numeral notation

[JasonGross]

PR 1 of the word-removal set is #187 (coqutil, stacked on this PR). Numerals: bits.of_Z _ z is used wherever the type fixes the width, and #187 adds a numeral notation for bits. riscv-coq is next.

---

Written by Claude Fable 5.1 via Claude Code (session https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm).

[andres-erbsen]

For further follow-ups, consider the following issues and either present analysis or propose a PR (or PR stack) if there is one clear way to resolve the issue:

• we seem to have a variety of word and Zmod-related notations across the submodule tree, and there is also one in stdlib. What would be a nice way to standardize?
• eradicating LittleEndian.combine #44
• Why is sextend a part of the word interface? #4
• hooking word into lia #56 - this one may require careful design and comparison of the existing unzify, F_lia, ZnWords, and recent Kami additions

[andres-erbsen]

One more Zmod-porting task: this lemma and dependencies should be work on top of fiat-crypto, right? andres-erbsen/stdlib@5bd6d0d#diff-9834d25e486dacac5c1bfdd0402f4681e28c2cad3293269c7e80cbb3c38f2201R1364-R1395 I mean the last lemma in ZmodSqrt.v

[JasonGross]

Notation standardization (first item of the list above). The sextend item (coqutil#4) is answered on that issue: it is resolved by #187.

I surveyed every word/Zmod notation in stdlib, coqutil, riscv-coq, bedrock2 (+compiler,
LiveVerif, processor), rupicola, fiat-crypto, Kami, quartz and granite, and tried the obvious
unifications against Rocq 9.2.

What is there: stdlib gives Zmod_scope with 0 1 + - * ^, bound to the type, and nothing
for unsigned, literals, bitwise ops, shifts or comparisons. coqutil adds decimal literals.
bedrock2 adds \[x], /[x], ^+ ^- ^* ^<< ^>> (about 1250 use lines) and re-declares
word_scope four more times with !n, #n, +, [/a]. rupicola has +w, <w, &w, ...
(about 100 lines) and opens its scope at import. Kami has global ^+, $n, #n. fiat-crypto
has local $n, .+, ^ for xor. granite has its own literal notation that overrides 0/1.
Same symbol, different meaning: ^ (pow vs xor), < (unsigned Prop, signed bool, word-valued),
$@ (map vs sep-logic bytes).

Proposal: one file coqutil.Word.WordNotations owning word_scope (%word), containing
bedrock2's /[ ], \[ ], ^+ ^- ^* ^<< ^>> unchanged. No infix for bitwise ops or
comparisons: | breaks Z.divide's (a | b) and match arms (tested), ^ is pow, and
\[a] < \[b] already reads fine. Keep stdlib Zmod_scope for pure field files only, since
opening it over Z_scope mis-parses 2 ^ width (tested). Then bedrock2 re-exports and deletes
its copies, rupicola and fiat-crypto drop their local spellings, Kami scopes its globals, granite
stops overriding 0/1. Full report with counts, file:line evidence and compiled checks in the
follow-up document.

Full report

Follow-up A: word / Zmod notations across the submodule tree

Answer to Andres Erbsen's question on #186 (2026-09-17): "we seem to have a
variety of word and Zmod-related notations across the submodule tree, and there is also one
in stdlib. What would be a nice way to standardize?"

Status: analysis only, no PR yet. Lane fu-a, 2026-09-17.

Clones surveyed (read-only, all already ported to stdlib Zmod/bits):

repo	clone	tip
stdlib (rocq-9.2 switch)	/data/jason/.opam/rocq-9.2/lib/coq/user-contrib/Stdlib/Zmod/	Rocq 9.2+rc2
coqutil	/data/jason/fiat-crypto-worktrees/wp-h-dedup/coqutil	8b40a6c
riscv-coq	/data/jason/fiat-crypto-worktrees/wp-g2/riscv-coq	a98896f
bedrock2 (+compiler, LiveVerif, processor)	/data/jason/fiat-crypto-worktrees/wp-j3/bedrock2	447b97df
rupicola	/data/jason/fiat-crypto-worktrees/wp-f1/rupicola	4764adf
fiat-crypto	/data/jason/fiat-crypto-worktrees/wp-f1/fiat-crypto	a5ee22098
kami	/data/jason/fiat-crypto-worktrees/wp-c/kami	2777a72
quartz	/data/jason/fiat-crypto-worktrees/wp-o/quartz	0b5b9e0
granite	/data/jason/fiat-crypto-worktrees/wp-d/granite	af1c5c4

Method: git grep -n -E 'Notation|Infix|Number Notation|Declare Scope|Bind Scope|Declare Custom Entry'
over *.v in each clone (submodule contents excluded), filtered to word/Zmod/bits, then the
definitions were read. Use-site counts are git grep -c line counts (lines containing the
token, summed over files) unless stated otherwise. Feasibility checks are in
/data/jason/fiat-crypto-worktrees/fu-a/scratch/t1_scopes.v … t4_bedrock.v, compiled with
rocq compile against the installed stdlib plus -Q for the built coqutil and bedrock2 clones.

---

1. Baseline: what stdlib provides

Stdlib/Zmod/ZmodDef.v:152-169:

notation	meaning	scope / kind
Zmod	Zmod.Zmod	global abbreviation
bits n	Zmod (2^n)	global abbreviation (only parsing implicitly: it is an abbreviation with a parameter, so it never prints; goals show Zmod (2 ^ n))
bits.of_Z n z	Zmod.of_Z (2^n) z	abbreviation in module bits
Zmod_scope, delimiter %Zmod, bound to type Zmod		Declare/Delimit/Bind Scope
0, 1	Zmod.zero, Zmod.one	Zmod_scope
+, -, - x, *, ^	Zmod.add, Zmod.sub, Zmod.opp, Zmod.mul, Zmod.pow (exponent is a Z)	Zmod_scope
to_Z	unsigned	only parsing alias; plus ~70 to_Z_* lemma aliases in ZmodBase.v/Bits.v

What stdlib does not provide: any notation for Zmod.unsigned/signed, for numeric literals of
type Zmod m (a bare 3 is a Z), for bitwise ops (and or xor not ndn), shifts (slu sru srs),
division (udiv umod squot srem mdiv), or comparisons (there is only eqb; no ltu/lts
at all: downstream code writes Z.ltb (Zmod.unsigned a) (Zmod.unsigned b)). No bits_scope
exists; bits n is just a spelling of a Zmod type, so Zmod_scope is the scope for it.

Because Zmod_scope is bound to the type, Zmod.add x 3 parses with no scope open once a
literal notation exists (t1 A). But the infix x + y on words needs Zmod_scope open or
%Zmod (t1 B, Fail Check ... x + y fails as expected with only Z_scope open).

2. Inventory per repository

2.1 coqutil (8b40a6c)

where	notation	meaning	scope	kind	uses
src/coqutil/Word/Bitwidth.v:24	Number Notation Zmod …	decimal literal k : Zmod m ↦ Zmod.of_Z m k; printer only fires for k >= 2 (so Zmod.zero/Zmod.one keep stdlib's 0/1, negatives print as Zmod.of_Z m (-k))	Zmod_scope	parse+print	used everywhere a literal appears in a Zmod arg position; e.g. bedrock2 Zmod.add rpc 4
Datatypes/OperatorOverloading.v:118,131,144	a * b, a + b, a - b for Zmod.mul/add/sub	printing side of the typeclass-based oo_scope overloading	oo_scope	only printing (parsing goes through Multiplication/Addition/Subtraction classes)	tests inside the file only; no importer opens oo_scope in the tree
Datatypes/ToConversion.v:31,72,91 (+ to nat, to byte, to Z)	x to word	Zmod.of_Z _ x via Conversion class	conversion_parse_scope / conversion_print_scope	parse via typeclass, separate print-only	self-test only; no importer opens the scopes
Map/Memory.v:13	xs $@ a	map.of_list_word_at a xs	global, level 10	parse+print	bedrock2 18 files / 100 lines; fiat-crypto 19 files / 145 lines (but see conflict C7)
Map/Memory.v:104, SeparationMemory.v:11,48	$+	map.putmany	Local		local
many files	Local Notation word := (bits width)		local		12 files in coqutil, 27 in riscv-coq, most of bedrock2

coqutil has no infix notation for word arithmetic, unsigned, or comparisons. Everything
downstream re-invents them.

2.2 riscv-coq (a98896f)

where	notation	meaning	scope	uses
src/riscv/Utility/Utility.v:107-119	<|>, <&>, +, -, *, /=, ==, <, >=	MachineWidth class fields or and add sub mul (negb reg_eqb) reg_eqb signed_less_than … — note < is signed	alu_scope	opened in 13 spec files (Spec/Execute*.v, CSR*.v, Machine.v)
Utility/Encode.v:156-158	a <|> b	Z.lor	z_bitwise_scope, opened globally in that file	78 lines in 7 files (mostly Encode)
Utility/Utility.v:94	fromImm	@ZToReg _ _	only parsing	130 lines use ZToReg
Examples/WMMFree.v:665-687, SMTVerif.v:246	bvadd A B, (_ bv2nat 32) A, …	SMT-LIB printing of Zmod.*	unscoped, mostly only printing	example files only
Examples/Fib.v:35-40	(WO~0~0~0~0~0)%word	Kami-style bit-list words		dead: Fib.v is not in _CoqProject and nothing in riscv-coq defines WO/%word

The alu_scope notations are the Haskell-derived spec DSL over the MachineWidth class
(Utility.v:28), whose single instance is MachineWidth (bits width)
(Utility/MkMachineWidth.v:8). They are not word notations in the sense of this survey and I
propose leaving them alone.

2.3 bedrock2 (447b97df)

bedrock2/src/bedrock2/WordNotations.v (whole file, 26 lines):

notation	meaning	level	kind
^+, ^-, ^*	Zmod.add sub mul	50/50/40 left	word_scope
^<<, ^>>	Zmod.slu, Zmod.sru (Z shift amount, unmasked)	37 left	word_scope
/[ x ]	parse: bits.of_Z (_ :> WordWidth) x; print: Zmod.of_Z _ x		separate parse/print pair
\[ x ]	parse: @Zmod.unsigned (2 ^ (_ :> WordWidth)) x; print: Zmod.unsigned x		separate parse/print pair

WordWidth is a Z-valued class whose hole is filled by unification or, failing that, by the
Bitwidth instance in scope (WordNotations.v:14-19). word_scope is declared here but has
no delimiting key (%word is not available from this file). Use counts across
bedrock2+compiler+LiveVerif+processor:

token	lines	files
\[	581	39
/[	378	35
^-	114	21
^+	102	28
^*	42	15
^>>	36	4
^<<	4	4
explicit Zmod.add/sub/mul (no notation)	473	68
Local Open Scope word_scope	19	19
direct Require … WordNotations	15	13 (plus LiveVerifLib.v:22 re-exports it; 57 files reach it)

Duplicates and variants inside bedrock2 itself (all re-Declare Scope word_scope):

where	notation	meaning	notes
bedrock2Examples/bsearch.v:16-24	^+ ^- ^<< ^>> (Local), /_, \_	same as WordNotations at fixed width 64	predates WordNotations
bedrock2Examples/lightbulb_spec.v:16-23	! n, # n, + - * - x	bits.of_Z width n, Z.of_nat n, Zmod.add …	inside a Section, so section-local (t2 confirms notations die at End); Delimit Scope word_scope with word also section-local
compiler/src/compiler/FlatToRiscvFunctions.v:184-192	identical copy of the lightbulb block		18 uses of !/# in the file
bedrock2Examples/FlatConstMem.v:202-210	+, -, ! x, xs $@ a	Zmod.add, Zmod.sub, bits.of_Z 32 x, map.of_list_word_at a%word xs	Local
compiler/src/compilerExamples/SimpleInvariant.v:56-57	[/ a ], [\ a ]	bits.of_Z width a, Zmod.unsigned a	mirror image of /[ ] \[ ]; 6 uses
bedrock2Examples/{cswap,ct,memconst,memequal,memswap,memmove}.v, Array.v:145	xs $@ a	Array.array ptsto (bits.of_Z _ 1) a xs (a sep-logic predicate, not the coqutil map)	Local; see C7
bedrock2/TracePredicate.v:169-170	P ^*, P ^+	Kleene star / plus on trace predicates	section-local, level 50 postfix: would clash with word_scope ^+/^* if both were open
NotationsCustomEntry.v:14-45	+ - * & ^ | << >> .>> < .< ==	bedrock2 expression AST ops in custom entry bedrock_expr (^ = xor, < = ltu, .< = lts)	custom entry, no interaction with term-level scopes
Semantics.v:64-73	none	Semantics.slu/sru/srs (word-valued, masked shift amount), ltu, lts	no notation anywhere in bedrock2
LiveVerif/…/Tests/PrintSmt.v:214-229, SampleSideconds.v	(bvadd a b) etc.	SMT printing of Zmod.*	local test files

Printing today (t4): with word_scope open, Zmod.add x (bits.of_Z width 3) prints x ^+ 3
(coqutil's Number Notation wins), while bits.of_Z width 0 prints x ^+ /[0] and
bits.of_Z width (-1) prints x ^+ /[-1]; Zmod.sub x Zmod.one prints \[x ^- 1].
Without word_scope open, Zmod.unsigned (Zmod.add x (bits.of_Z w 7)) prints
Zmod.unsigned (x + 7) (stdlib Zmod_scope via Bind Scope). So a goal can show + or ^+
for the same term depending on which file you are in.

2.4 rupicola (4764adf)

src/Rupicola/Lib/WordNotations.v (whole file, 22 lines), scope named word (no _scope
suffix, no delimiting key) and Open Scope word. executed at import (line 22):

notation	meaning	level	lines / files
~w	Zmod.not	30	2 / 2
*w, /w, /sw	Zmod.mul, Zmod.udiv, Zmod.squot	40	5/3, 2/2, 1/1
+w, -w	Zmod.add, Zmod.sub	50	6/4, 2/2
>>w, >>>w, <<w	Semantics.sru, Semantics.srs, Semantics.slu (masked, word-valued amount)	60	14/4, 1/1, 11/4
<w, >w, <sw, >sw, ==w	word.b2w (Semantics.ltu …) etc. — word-valued 0/1, not bool	70/80	12/4, 15/4, 1/1, 1/1, 3/2
&w, ^w, |w	Zmod.and, Zmod.xor, Zmod.or	90/92/94 (unusual: bitwise binds looser than comparison)	9/3, 10/5, 12/5

Only 4 files require it (Examples/Arrays.v, L64X128.v, Net/IPChecksum/Impl.v,
Utf8/Utf8.v). Total ≈ 100 use lines. word.b2w (Lib/Core.v:552) is rupicola-local.
Rupicola also has many Notation of_Z z := (bits.of_Z width z)-style local abbreviations
(Lib/ExprCompiler.v:3-7,161-275, Examples/Arrays.v:168-170).

2.5 fiat-crypto (a5ee22098)

fiat-crypto never imports bedrock2's or rupicola's WordNotations (0 hits). Its word/Zmod
notations:

where	notation	meaning	scope	uses
src/Spec/ModularArithmetic.v:8	Global Coercion Zmod.unsigned : Zmod >-> Z		global	field-arithmetic files
src/Spec/ModularArithmetic.v:11	/	Zmod.mdiv (field division)	Zmod_scope	33 lines / 10 files use Zmod.mdiv or /
5 files	Local Open Scope Zmod_scope			ModularArithmeticTheorems.v:38,212,234, PrimeFieldTheorems.v:22,109, LadderStep.v:9, MontgomeryLadder.v:50, EdwardsMontgomery25519.v:3
22 files	%Zmod			62 lines
Bedrock/End2End/RupicolaCrypto/ChaCha20.v:256-272, Broadcast.v:243-246	Declare Scope word_scope; Local +, *; unscoped Local a + b, a ^ b (xor), a <<< b (rotate)	Zmod.add/mul/xor, rotate via Semantics.slu/sru	Local	those files
Bedrock/P256.v:38-39, P256/JacobianAffine.v:41-42, P256/PrecomputedMultiples.v:52, End2End/X25519/EdwardsXYZT.v:212	$ n, p .+ n	bits.of_Z _ n, Zmod.add p (bits.of_Z _ n) (pointer + byte offset)	Local	.+: 14 lines / 4 files
End2End/X25519/EdwardsXYZT.v:214-216	Local unscoped 0 1 + * - / x ^ 2	field ops on Zmod M	Local, unscoped (shadow Z_scope inside the file)	that file
~19 files (Bedrock/**)	xs $@ a	Array.array ptsto (bits.of_Z _ 1) a xs or map.of_list_word_at a xs depending on file	Local	145 lines
Arithmetic/BarrettReduction/RidiculousFish.v:80-90	word_scope (%word, bound to its own word type): + - * / << >>, 1, 32	its own word n record (not Zmod)		that file

Hazard confirmed (t1 G): with the global Zmod.unsigned coercion, fun (x y : bits w) => x + y
with Z_scope on top typechecks silently as Zmod.unsigned x + Zmod.unsigned y : Z.
Anyone writing field arithmetic in fiat-crypto without %Zmod/Open Scope Zmod_scope gets
integers, not field elements, with no error.

2.6 kami (2777a72)

Kami/Lib/Word.v (word n := bits (Z.of_nat n), Word.v:30):

where	notation	meaning	scope	uses
Word.v:32-37	word_scope, %word, bound to word, Open Scope word_scope globally at line 37			%word: 37 lines each in Ex/ProcThreeStage.v, Ex/IsaRv32.v
Word.v:44,98-99	WO, w~1, w~0	Zmod.zero : word 0, WS true/false w	word_scope	Ex/IsaRv32/Pgm*.v (256 lines each, 8 files)
Word.v:101-104	^~, ^+, ^*, ^-	Zmod.opp add mul sub	unscoped global (arguments forced %word)	44 lines Ex/FifoCorrect.v, 34 SimpleFifoCorrect.v, 18 each in Multiplier*/Divider*.v
Word.v:111-114	<, >, <=, >=	wlt = unsigned, Prop-valued	word_scope	processor/KamiRiscvStep.v:314,321
Word.v:116-117	$ n, # n	natToWord _ n, wordToNat n	unscoped global, levels 1 and 5	$n: 256 lines each in 8 Pgm*.v; processor/*.v
Kami/Notations.v:39-63,99	+ - * *s *su / /s ~& ~| ~+ << >> ~>> < > >= <= <s >s == != $ n $$ e …	Kami expression AST (BinBit, BinBitBool, Const)	kami_expr_scope	Kami DSL, not word values
Ex/Multiplier{32,64}.v:395-399	w~0, w~P, w~N	Booth digits	bword_scope	local

2.7 bedrock2/processor (uses Kami + riscv-coq + bedrock2)

processor/src/processor/KamiRiscvStep.v:784 has (kpc ^+ $4) (Kami, unscoped) next to
Zmod.add rpc 4 (coqutil Number Notation) on the same line; :314,321 use Kami's %word
</<= (Prop) and relate them to Zmod.unsigned … < …. Only 1 line of ^+/^-/^* in
processor. This is the only place Kami's global notations meet the bedrock2 ones today.

2.8 quartz (0b5b9e0)

No term-level notations on Zmod values. Bits sz (lang/Syntax.v:16) is a constructor of
Quartz's type syntax whose denotation is stdlib bits sz (Syntax.v:25); mword := (Bits 32)
etc. are type abbreviations. The custom entry quartz_expr (Syntax.v:350-392) has
sz'd val (literal, bits.of_Z _ val), + - * & | ^ << >> .>> == < <= > >= .< .<= .> .>= ++
on expression ASTs (^ = xor, .< = signed). lang/domain.v:8-9 adds coercions
embed_bool : bool >-> bits 1 and nonzero : Zmod m >-> bool.

Oddity spotted while reading (not a notation-standardisation issue, but worth telling the
owners): lang/Syntax.v:382 maps e1 * e2 to binop.And and :385 maps e1 - e2 to
binop.Add.

2.9 granite (af1c5c4)

core/Bits.v:

where	notation	meaning	scope	uses
:8	bits n	Zmod (2 ^ n)%Z — re-declaration of the stdlib abbreviation (harmless duplicate)	global
:13-30	Number Notation Zmod …	non-negative literal ↦ bits_literal m z (a Zmod.mk with a typeclass-discharged range proof, so Zmod.unsigned (lit) = z by reflexivity, :80); negative literal ↦ Zmod.of_Z; printer only prints bits_literal	Zmod_scope	bits_literal: 8 lines
:32-33	0, 1	re-bound to bits_literal _ 0/_ 1 instead of stdlib's Zmod.zero/Zmod.one	Zmod_scope (overrides stdlib, warning notation-overridden)
:79	zeroes	bits_literal _ 0 (+ zeroes_zero bridging lemma to Zmod.zero)	global	257 lines
:98-106	list_bits scope, %bits: 1, 0, bs~0, bs~1, Ob~…	list bool → bits_to_word		0 uses of Ob~ / %bits
app/ToyISA.v:249	x.n	bits.of_Z regidx_sz n	isa_scope	local
8 sites	Open Scope Zmod_scope, %Zmod 18 lines

Granite is the only tree whose literal notation is not the coqutil one, and the only one that
overrides stdlib's 0/1. If a file ever loaded both coqutil's and granite's Number Notation
the later one silently wins (Coq warns notation-overridden), and Zmod.zero vs
bits_literal _ 0 are different terms (zeroes_zero exists precisely to bridge them).

3. Conflicts and overlaps

Same syntax, different meaning (C = conflict):

id	syntax	meanings in the tree
C1	^	pow (stdlib Zmod_scope, Z_scope); xor (bedrock_expr entry, quartz_expr entry, fiat ChaCha20 local, rupicola ^w)
C2	<, <= on words	Kami word_scope: unsigned, Prop; riscv alu_scope: signed, bool; bedrock_expr: ltu on ASTs; quartz_expr: unsigned on ASTs (.< signed); rupicola <w: unsigned, word-valued
C3	$ n	Kami: natToWord (global, level 1); fiat P256: bits.of_Z _ n (local, level 9); bedrock_expr/quartz_expr: constr escape; Kami expr: Const (natToWord …)
C4	# n	Kami: wordToNat (global, level 5); bedrock2 lightbulb/FlatToRiscvFunctions: Z.of_nat (section-local, level 0); Kami expr: Var
C5	<<, >>	fiat RidiculousFish word_scope (own type); Kami expr; bedrock_expr; quartz_expr; nobody uses them on Zmod values (bedrock2 uses ^<<)
C6	+ - * on words	stdlib Zmod_scope; bedrock2 lightbulb/FlatToRiscv/FlatConstMem word_scope; fiat ChaCha20/Broadcast word_scope and EdwardsXYZT unscoped; riscv alu_scope (class fields); coqutil oo_scope (print only); Kami/bedrock2 spell them ^+ ^- ^*; rupicola +w -w *w
C7	xs $@ a	coqutil global: map.of_list_word_at a xs (a map); bedrock2/fiat local in ≥10 files: Array.array ptsto (bits.of_Z _ 1) a xs (a separation-logic predicate); bedrock2 Array.v:145 and FlatConstMem.v:209 also redeclare the map meaning locally
C8	^+, ^*	Zmod add/mul (bedrock2 word_scope, Kami global) vs Kleene plus/star postfix (TracePredicate.v:169-170, section-local)
C9	shifts	^<< = Zmod.slu with a Z amount (bedrock2) vs <<w = Semantics.slu with a masked word amount (rupicola): look alike, differ semantically
C10	literals	coqutil Number Notation (Zmod.of_Z, prints ≥ 2) vs granite Number Notation (bits_literal, overrides 0/1)

Same meaning, different syntax (S = spelling variance):

id	meaning	spellings
S1	bits.of_Z width n	3 (coqutil literal), /[3] (bedrock2), [/ 3 ] (SimpleInvariant), /_ 3 (bsearch), !3 (lightbulb, FlatToRiscvFunctions, FlatConstMem), $3 (fiat P256), 3 to word (coqutil ToConversion), $3 (Kami natToWord), bits_literal/3 (granite), of_Z 3/to_w 3 (rupicola local abbreviations)
S2	Zmod.unsigned x	\[x] (bedrock2), [\ x ] (SimpleInvariant), \_ x (bsearch), x to Z (coqutil ToConversion), #x (Kami, via nat), bare x via coercion (fiat-crypto)
S3	Zmod.add	+ (Zmod_scope), ^+ (bedrock2, Kami), +w (rupicola), .+ (fiat, with an of_Z on the right), + in four local word_scopes, bvadd (SMT printers)
S4	scope name for word ops	word_scope declared independently in bedrock2 WordNotations.v, bsearch.v, lightbulb_spec.v, FlatToRiscvFunctions.v, FlatConstMem.v, Kami Lib/Word.v, fiat RidiculousFish.v, Broadcast.v, ChaCha20.v; rupicola uses word (no suffix). Re-declaring a scope is allowed silently (t2), and all of them pour different notations into the one global word_scope; delimiter %word is defined by Kami, fiat and the section-local copies but not by bedrock2's WordNotations.v.

4. Feasibility checks (all compiled; files in /data/jason/fiat-crypto-worktrees/fu-a/scratch/)

file	question	result
t1_scopes.v A-B	can the stdlib scope serve with only Bind Scope?	Zmod.add x 3 and Zmod.mul x 1 parse with nothing open; x + y needs %Zmod/open scope
t1_scopes.v D-F	is Open Scope Zmod_scope over Z_scope safe in files that mix Z and words?	No. Definition m (width : Z) := 2 ^ width fails (parsed as Zmod.pow); let z := x + y in z on Z fails. Positions with an expected Z type (: Z, arguments of Z.lt, Zmod.of_Z, …) are fine via Bind Scope. This is why bedrock2, whose proofs are ~600 \[…] lines of mixed Z/word arithmetic, uses distinct symbols ^+.
t1_scopes.v G	fiat-crypto's global coercion	x + y : Z silently, see 2.5
t1_scopes.v H, t4_bedrock.v	printing of literals	see 2.3: 3 prints as 3, 0/-1 as /[0]//[-1] with word_scope open, as Zmod.of_Z (2^w) 0 otherwise
t2_sections.v	do the Section-local copies (lightbulb, FlatToRiscvFunctions) leak?	No: notations, Delimit Scope, all die at End. Re-Declare Scope is silent.
t3_infix.v	can & | << >> <? <s? be added to Zmod_scope?	&, <<, >>, <?, <s? work with no clash. | is unusable: once an Infix "|" exists, (a | b) for Z.divide no longer parses even with %Z, and y | x inside a match arm is a syntax error (parenthesised too). Re-binding ^ to xor is accepted with only a notation-overridden warning, i.e. a silent trap.
t4_bedrock.v	does /[x] need WordWidth? can word_scope and Zmod_scope coexist?	x ^+ /[3] resolves by unification with no Bitwidth; a bare /[3] needs the Bitwidth instance (Fail Definition confirms). Opening both scopes: no overlapping symbols, x ^+ y = x + y typechecks (and prints x ^+ y = x ^+ y).

5. Proposal

5.1 Principles

1. One source of truth per layer. stdlib owns Zmod_scope (0 1 + - * ^, bound to the
   type). coqutil owns everything word-flavoured that is shared (literals, \[ ], /[ ], the
   ^-prefixed operators) in one file, coqutil.Word.WordNotations (new; Bitwidth.v keeps
   the Number Notation because it is the file every port already imports). Downstream repos
   import that file and delete their copies.
2. Never add a symbol to Zmod_scope that reads differently in Z_scope (^, |,
   <), and never rely on Open Scope Zmod_scope in files that mix Z and words (t1 D/F).
   Files that are pure field arithmetic (fiat-crypto Spec/, Arithmetic/) keep opening it.
3. Word operators that must coexist with Z arithmetic get distinct spellings, and the
   existing bedrock2 spelling wins on numbers (^+ 102 lines vs +w 6; \[ 581 lines vs
   nothing comparable).
4. Scope hygiene: exactly one Declare Scope word_scope (in coqutil), with
   Delimit Scope word_scope with word, and no Open Scope at import (rupicola
   WordNotations.v:22 and Kami Word.v:37 do this today).

5.2 The shared set (coqutil, word_scope, delimiter %word)

notation	meaning	decision
3 : bits w	Zmod.of_Z (2^w) 3	already in Bitwidth.v; keep (clear)
/[ x ]	bits.of_Z width x (parse via WordWidth hole; print Zmod.of_Z _ x)	move from bedrock2 verbatim, including the WordWidth class (clear)
\[ x ]	Zmod.unsigned x	move from bedrock2 verbatim (clear)
^+ ^- ^*	Zmod.add sub mul	move from bedrock2 (clear; Kami already agrees on spelling and levels)
^<< ^>>	Zmod.slu, Zmod.sru with a Z amount	move from bedrock2 (clear; 40 lines)
^>>>	Zmod.srs	add for symmetry; taste, low cost
bitwise and or xor not	no infix; write Zmod.and x y	bedrock2 has 0 uses of any infix for these; |/^ are unusable/ambiguous (t3, C1); rupicola's ~31 lines convert to names or keep a rupicola-local scope
comparisons	no shared infix; write \[a] < \[b] (unsigned) / Zmod.signed a < Zmod.signed b	this is what bedrock2 already does everywhere; the only infix users are Kami (Prop) and rupicola (word-valued), which disagree with each other and with riscv's signed < (C2)
masked shifts Semantics.slu/sru/srs, ltu/lts	no shared notation	bedrock2-specific semantics; stays in bedrock2 by name

Taste question T1, literal printing. Options: (a) status quo: x ^+ 3 but x ^+ /[0],
/[-1]; (b) let the Number Notation also print Zmod.of_Z m 0/1 as 0/1 (then Zmod.zero
and of_Z m 0 print identically although they are different terms, which bites rewrite);
(c) drop the printing side of /[ ] and always print Zmod.of_Z. Recommendation: (a); it is
the only option where what you read tells you which term you have.

Taste question T2, $@. Options: (a) keep coqutil's xs $@ a = map.of_list_word_at and
rename the sep-logic one in bedrock2/fiat to xs $@@ a or a plain bytes xs a abbreviation;
(b) the reverse; (c) leave both local. Recommendation: (a) with a bytes-style abbreviation,
because the map meaning is the one that is global today and the predicate meaning is already
spelled bytes in lightbulb.v:92, LAN9250.v:877, ARPResponderProofs.v:15.

5.3 Repo-local decisions

• bedrock2: WordNotations.v becomes Require Export coqutil.Word.WordNotations; delete the
  copies in bsearch.v, lightbulb_spec.v, FlatToRiscvFunctions.v, FlatConstMem.v,
  SimpleInvariant.v (!n→/[n], #n→Z.of_nat n, [/a]→/[a], [\a]→\[a], ~40 lines);
  rename TracePredicate's ^+/^* (C8) if that file ever needs word_scope. bedrock_expr
  custom-entry operators are untouched (they are AST syntax, not word syntax).
• rupicola: replace +w -w *w by ^+ ^- ^* (13 lines), <<w >>w >>>w by
  Semantics.slu/sru/srs or a rupicola-local ^<<w-style spelling that does not look like
  bedrock2's unmasked shift (C9, 26 lines), bitwise/comparison …w by names (~60 lines); remove
  Open Scope word. and the word scope. Rupicola keeps word.b2w.
• fiat-crypto: keep Global Coercion and / := Zmod.mdiv : Zmod_scope (field files are a
  legitimately different dialect; document the t1 G hazard in Spec/ModularArithmetic.v).
  ChaCha20.v/Broadcast.v/EdwardsXYZT.v local + * ^: ^→Zmod.xor, +→^+ or
  %Zmod; $ n→literal n; p .+ n → p ^+ n (14 lines) or keep as a local pointer-offset
  idiom (taste; I'd keep it, it is readable and local). RidiculousFish.v has its own word type
  and is out of scope.
• riscv-coq: nothing to standardise (alu_scope is the spec DSL). Delete or repair the dead
  Examples/Fib.v (Kami-era WO~ syntax, not built).
• Kami: put ^~ ^+ ^* ^-, $ n, # n into word_scope (Lib/Word.v:101-117) so they stop
  being global; Kami's own files are unaffected because Word.v:37 opens the scope, and
  processor then needs Local Open Scope word_scope (1-3 files). Kami's Prop-valued < <= > >=
  stay Kami-local; do not export them to coqutil.
• granite: (a) adopt coqutil's Number Notation semantics (map to Zmod.of_Z, stop
  overriding 0/1) and prove unsigned_literal by bits.unsigned_of_Z_small instead of
  reflexivity, or (b) keep bits_literal but drop the 0/1 override and make zeroes a
  notation for Zmod.zero, or (c) leave as is since granite shares no .vo with the coqutil
  world. Recommendation: (b) now (257 zeroes lines untouched, the zeroes_zero bridge
  disappears), (a) if granite ever depends on coqutil. Delete the unused list_bits/Ob~
  scope (0 uses).
• quartz: nothing (no value-level notations). Report the -/* mapping oddity
  (lang/Syntax.v:382,385) to the owners.

5.4 Migration order

1. coqutil: add src/coqutil/Word/WordNotations.v (scope + delimiter + WordWidth + /[ ] \[ ] ^+ ^- ^* ^<< ^>> ^>>>), tests as Goal … reflexivity like Bitwidth.v:29-34. Optionally
   decide T2 ($@) here.
2. riscv-coq: bump coqutil only (no notation changes; optional Fib.v cleanup).
3. bedrock2: bump; WordNotations.v → re-export; delete the five local copies; processor opens
   word_scope locally once Kami is scoped (step 6 can land before or after; the ^+ spelling
   is identical so both orders build).
4. rupicola: bump; rewrite Lib/WordNotations.v as above (~100 lines touched in 4 files).
5. fiat-crypto: bump submodules; ChaCha20/Broadcast/P256 local notations (~30 lines).
6. Kami (independent): scope the globals; then bedrock2/processor adds Local Open Scope word_scope.
7. granite (independent): T-granite option (b); quartz: nothing.

Steps 1-5 follow the usual submodule chain and each is a small PR; none changes a definition,
only notation files and use sites, so they can be reviewed by reading the diff.

---

GitHub-ready summary (for #186)

I surveyed every word/Zmod notation in stdlib, coqutil, riscv-coq, bedrock2 (+compiler,
LiveVerif, processor), rupicola, fiat-crypto, Kami, quartz and granite, and tried the obvious
unifications against Rocq 9.2.

What is there: stdlib gives Zmod_scope with 0 1 + - * ^, bound to the type, and nothing
for unsigned, literals, bitwise ops, shifts or comparisons. coqutil adds decimal literals.
bedrock2 adds \[x], /[x], ^+ ^- ^* ^<< ^>> (about 1250 use lines) and re-declares
word_scope four more times with !n, #n, +, [/a]. rupicola has +w, <w, &w, ...
(about 100 lines) and opens its scope at import. Kami has global ^+, $n, #n. fiat-crypto
has local $n, .+, ^ for xor. granite has its own literal notation that overrides 0/1.
Same symbol, different meaning: ^ (pow vs xor), < (unsigned Prop, signed bool, word-valued),
$@ (map vs sep-logic bytes).

Proposal: one file coqutil.Word.WordNotations owning word_scope (%word), containing
bedrock2's /[ ], \[ ], ^+ ^- ^* ^<< ^>> unchanged. No infix for bitwise ops or
comparisons: | breaks Z.divide's (a | b) and match arms (tested), ^ is pow, and
\[a] < \[b] already reads fine. Keep stdlib Zmod_scope for pure field files only, since
opening it over Z_scope mis-parses 2 ^ width (tested). Then bedrock2 re-exports and deletes
its copies, rupicola and fiat-crypto drop their local spellings, Kami scopes its globals, granite
stops overriding 0/1. Full report with counts, file:line evidence and compiled checks in the
follow-up document.

---

Written by Claude Fable 5.1 via Claude Code (session https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm).

[JasonGross]

The ZmodSqrt development builds on fiat-crypto master against released stdlib 9.1: mit-plv/fiat-crypto#2446 (draft: one admit left, sqrtspop_correct, with the original two gaps; quadratic_reciprocity' and the Euler criteria are closed under the global context).

Ported andres-erbsen/stdlib@5bd6d0db ("WIP ZmodSqrt") onto fiat-crypto master (a5ee22098) as
Crypto.Util.Factoring, Crypto.Arithmetic.ZmodSqrtDef and Crypto.Arithmetic.ZmodSqrt,
building against released rocq-stdlib 9.1.0 without any fork-only stdlib changes.
quadratic_reciprocity' (the last lemma of ZmodSqrt.v), both Euler criteria, sqrtp_square
and the power-of-two lemma are closed under the global context.

Changes needed: Injective_map_NoDup_in now comes from Lists.Finite; five Z.coprime
lemmas the WIP used but no stdlib version has (coprime_prime_prime, coprime_comm,
coprime_mul_{l,r}_iff, coprime_sqr_l_iff) are defined locally; Zstar.prod is a
definition, so the product notation now denotes prod and unfolding sites use prod_cons;
to_Zmod was already a coercion.

One real bug in ZmodSqrtDef.v: sqrtp_given_nonsquare had its two binders swapped relative
to its caller, so sqrtsp returned None for most squares (the file's own Compute blocks
show it: only 0 and 9 had roots mod 11). Fixed by reordering the binders.

ZmodSqrt.v was written against an older ZmodSqrtDef (sqrtp', sqrtp2', sqrtpop',
sqrtpp' on Z); those lemmas are restated for the committed definitions
(sqrtp_given_nonsquare, sqrtp2odd', liftSqrtPop, sqrtspop). The only admitted lemma
is sqrtspop_correct, which keeps the original two gaps: odd valuation contradicts the
existence of a root, and a / p^v has a root mod p. Also noted: sqrtsp2odd is wrong for
k = 1, and the Compute blocks print at build time.

Suggest opening the fiat-crypto PR with the admit and upstreaming the Z.coprime lemmas and
Factoring.v to stdlib afterwards.

---

Written by Claude Fable 5.1 via Claude Code (session https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm).

[andres-erbsen]

Yes, port genuinely useful and nontrivial content in a follow-up PR or PRs.

[JasonGross]

Will do: the closed, nontrivial parts (the Z.coprime lemmas, Factoring with its admits closed where feasible, and the Zmod square-root / Euler-criterion / reciprocity chain as far as it is admit-free) go to rocq-prover/stdlib as separate PRs; I will link them here.

---

Written by Claude Fable 5.1 via Claude Code (session https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm).

[JasonGross]

First stdlib PR: rocq-prover/stdlib#306 (Factoring.v with the fundamental theorem of arithmetic and the factorization induction principles, plus the coprimality iff lemmas; everything closed, full stdlib build). Next: the Euler criterion / Wilson / quadratic reciprocity part, which is closed and independent of the square-root definitions; the square-root correctness waits for its admit and the k = 1 fix.

---

Written by Claude Fable 5.1 via Claude Code (session https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm).

[JasonGross]

Second stdlib PR: rocq-prover/stdlib#307 (Euler's criterion, the Wilson direction and quadratic reciprocity, stacked on #306). The square-root definitions and their correctness stay in fiat-crypto#2446 until the admit is closed.

---

Written by Claude Fable 5.1 via Claude Code (session https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm).

[andres-erbsen]

Please make these PRs against fiat-crypto instead of stdlib

[JasonGross]

Understood; closed rocq-prover/stdlib#306/#307. The same cleaned content (Factoring + coprime lemmas; Euler criterion + quadratic reciprocity, no admits, no scratch) will come as fiat-crypto PRs, and fiat-crypto#2446 will shrink to the square-root part that still has the admit.

---

Written by Claude Fable 5.1 via Claude Code (session https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm).

[JasonGross]

As fiat-crypto PRs: mit-plv/fiat-crypto#2450 (Factoring.v with the fundamental theorem of arithmetic, in_ppfactor, the induction principles, and the coprimality/list helpers), mit-plv/fiat-crypto#2451 (Euler's criterion and quadratic reciprocity, stacked on #2450), and #2446 reduced to the square-root part (draft, one admit), stacked on #2451.

---

Written by Claude Fable 5.1 via Claude Code (session https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm).