Normalize refactoring - #19
Merged
Merged
Conversation
[cryptis/lib/sms.v] introduces SMS: lists over a type [T] carrying a decidable total order [R] and an involution [i], viewed up to cancellation of inverse pairs. [SMS.count] is the signed multiplicity, [SMS.insert] / [SMS.cancel] remove inverse pairs, [SMS.to] is the canonical form (cancel, then sort) and [SMS.wf] says a list already is one. The main results are [wf_to], [count_to] and [to_eq]: two lists have the same canonical form iff they have the same signed counts. [cryptis/primitives/sms.v] gives HeapLang implementations of insert, cancel and to, parameterised by closures for the element operations (equality, the involution, and the order) and specified against the pure model, in the style of the [twp_hl_*] specs of [primitives/pre_term.v]. [to] reuses the shared [insertion_sort] of [lib/list.v]. This is the machinery that pre-term multiplication currently open-codes; the following commits reroute it through SMS. [PreTerm.invs_canceled] also becomes a genuine [bool] -- a [forallb] over the decidable non-membership test -- so it can sit in [PreTerm.wf] without a [bool_decide] wrapper. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01E8khwa8zca1fMdMbwHLikG
Make SMS the cancellation engine for pre-term multiplication and for the term-level factor lists, replacing the bespoke count/cancel reasoning in normalize.v and core/term/base.v. - normalize.v: the mul-algebra core (perm_mul, mul_cat, sortcancel_catr) goes through SMS.to / SMS.count via SMS.to_eq. The pre-term-level cancellation definitions [PreTerm.cancel_invs], [PreTerm.insert_factor] and [PreTerm.invs_canceled] are deleted: they were definitionally equal to SMS.cancel / SMS.insert at [inv_aux] and SMS.invs_canceled at [inv], so the rebase is a name swap that needs no proof changes. - sms.v: [SMS.wf] becomes self-certifying -- it carries the involution laws for the list's own elements, so a single [wf X] fact discharges the per-list hypotheses downstream. Adds the extractors, constructors and to-lemmas that go with it, plus [SMS.to_app_cancel_l], which lets [TExpN_injr] be reproved with an equational conclusion. - core/term/base.v, core/minted.v: the term layer now presents only [SMS.to term_order TInv] and [SMS.wf term_order TInv]; the bespoke cancel_invs / invs_canceled / four-conjunct wf_mul_list notions are gone. A conjugation bridge ([unfold_to] and friends) connects the T = term forms to the pre-term factor computations. Lemmas that are permutation-stable take a spelled-out "no inverse pairs" side condition instead, so SMS internals do not surface at all. - public.v, dh.v and the DH examples are adapted to the new spellings. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01E8khwa8zca1fMdMbwHLikG
Follow-up cleanup so that only the public SMS interface -- [SMS.to], [SMS.wf], [SMS.count] and their lemmas -- appears above cryptis/lib/sms.v. The internal [SMS.cancel] / [SMS.insert] / [SMS.invs_canceled] now show up only in the HeapLang specs that implement them. - sms.v: [SMS.to] and [SMS.wf] are [simpl never], so their merge_sort / cancel implementations never leak into goals. New [SMS.to_id_perm] (a list with no inverse pairs is only reordered by [to]) and [SMS.to_fmap] (transport of [to] along an injective, order-preserving, involution- conjugating map) generalise bridges that base.v was doing by hand. - normalize.v: the whole cancel/insert count cluster goes; what survives is re-derived through the count engine or the abstract to/wf lemmas. "No inverse pairs" is spelled out first-order, matching the term layer. Also drops [inv_aux_eq_op], the [wf_term] alias and the [wf_*E] unfolding lemmas. - core/term/base.v: [count_exp] / [count_exp_nat] and their ~16 lemmas are replaced by one structural bridge [exps_TExp] plus a small [SMS.count] family; the dead count/cat cluster left over from [TExpN_injr] is deleted; [term_rect]'s product and exponent cases take a single [SMS.wf] premise instead of separate sortedness and no-inverse-pair conditions. - lib/list_sort.v gains [fmap_rem] and [count_mem_fmap], which are general; [Forall_mem] is dropped in favour of stdpp's [list.Forall_forall]. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01E8khwa8zca1fMdMbwHLikG
[SMS.to R i X] now drops the elements [x] with [i x = x] (via a new [prune] filter) before cancelling and sorting. Such fixed points have signed count 0, so pruning changes no count -- but it lets the to-lemmas ([to_eq], [wf_to], [to_Permutation], [to_cat_to], [to_app_cancel_l]) require only that [i] be involutive on the list's elements, and no longer that it be fixed-point-free. At T = term that removes the atomicity side condition wherever it was there only to feed [TInv_Nid]: [perm_cancel_invs] becomes unconditional, and [TExpN_injr] and the normalize.v wrappers shed their fixed-point-free discharges. The executable [to] must prune too: [primitives/sms.v] gains [sms_prune] and [twp_sms_prune], and -- since [inv_aux] is unconditionally fixed-point-free -- [PreTerm.to_inv_aux] lets the pre-term primitive specs unfold [SMS.to] without exposing [prune]. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01E8khwa8zca1fMdMbwHLikG
Establish the algebra of the term operations as a small set of FUNDAMENTAL equations lifted from the wf-assuming pre-term identities, and derive every other equation once, at the term level, from those -- never by re-proving it on pre-terms. - core/term/base.v: a "Fundamental algebra" block introduces the binary product [TMul a b := TMulN [a; b]] and proves the six generating laws ([TMulC] / [TMulA] / [TMul1] / [TMulK], with [TExpNA] / [TExpN0] above), plus the reconstruction and inverse-over-factors fundamentals ([tfactorsK], [TInv_tfactors], [TMulN_TInv_cancel], [TMulN_app]). From these it derives [TMul_cancel], [TInvK] and [TInv_fixed], which used to be lifted from [PreTerm.invK] / [PreTerm.inv_fixed]. A signed-count API on term factors is developed alongside, so the group laws can be discharged by counting. - The pre-term laws move out of normalize.v into a new core/pre_term/laws.v, leaving normalize.v with the normal forms and the [wf] / [normalize] machinery only. laws.v is then trimmed against the term-level derivations: the equations that the term layer now proves for itself are dropped, and what is left is marked up for the next round of deletion. No fundamental equation's proof mentions a derived one. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01E8khwa8zca1fMdMbwHLikG
The 2600-line core/term/base.v becomes six files under core/term/,
aggregated as before by core/term.v:
base.v foundation: the term inductive, the unfold/fold <-> pre_term
conjugation, smart constructors, instances, destructor
definitions, the is_* predicates and the signed factor-count API
algebra.v multiplicative-group and DH-exponentiation laws, tsize, and the
term_rect / term_ind induction principles
repr.v val_of_term / repr, the HeapLang value embedding
nonces.v nonces_of_term
subterms.v subterms
spec.v Tag and the Module Spec surface API
Downstream imports cryptis.core.term and is unchanged; the only fix needed
was three stale module-qualified references in examples/opaque/shared.v.
Each split file re-declares the file-local [Implicit Types] and [Set Implicit
Arguments] block, which does not cross a [Require] boundary.
The multiplicative group laws are also rerouted through the term-level
factor-count lemmas rather than the pre-term algebra, which lets
[PreTerm.mul_invs] be deleted from core/pre_term/laws.v.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01E8khwa8zca1fMdMbwHLikG
[term_rect] / [term_ind] no longer go through the well-founded [tsize] recursion: the eliminator is proved by structural induction on the underlying well-formed pre-term. Its exponentiation case is also restated with the binary [TExp t1 t2] -- [t1] the non-exponential base, [t2] the whole exponent -- rather than the n-ary [TExpN], which is what the callers want; a proof that needs the individual exponents can still induct on [tsize] with [term_lt_ind]. The product case is weakened at the same time. It used to hand out [SMS.wf term_order TInv ts]; it now hands out the spelled-out, permutation-stable [forall t' in ts, TInv t' not-in ts]. Of wf's conjuncts only sortedness is really dropped, and a case that needs a canonical factor list can re-sort, since [TMulN] is permutation-invariant and every side condition is permutation-stable. That also removes [term_rect]'s last dependency on the multiplicative group laws. [subtermsP] and [False_public], the two [elim: t] sites, are reproved against the new cases, and [term_rect] moves to base.v now that it no longer needs the algebra. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01E8khwa8zca1fMdMbwHLikG
[tsize], its termination lemmas and the well-founded [term_lt_rect] / [term_lt_ind] move from core/term/algebra.v into a new core/term/tsize.v, which slots into the term chain right after algebra (base -> algebra -> tsize -> repr -> nonces -> subterms -> spec). The dependency is one-way, so nothing had to be reordered or duplicated: the moved block consumes algebra lemmas, but no algebra lemma mentions [tsize]. Along the way, drop the term lemmas left unused after the previous two commits, and tidy the statements across algebra.v, base.v, nonces.v, subterms.v, minted.v and public.v. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01E8khwa8zca1fMdMbwHLikG
Collapse the pre-term "laws" layer into the term layer. core/pre_term/laws.v is deleted outright: the equations it held are either fundamentals that normalize.v already proves, or derived equations that core/term/ now proves for itself by counting factors. core/term/algebra.v loses roughly half its size in the process, and core/term/base.v is restructured around the [count] API ([count], [count_inj], [count_TMulN], [count_TInv], ...) which the derivations run on. Net: -680 lines across the pre-term and term layers. NOTE: this commit does not build. It is the WIP state where the algebra has been cut down but its consumers have not caught up: core/term/nonces.v still calls the deleted [PreTerm.inv_factors], and primitives/sms.v and primitives/pre_term.v are mid-edit. The next three commits close the gap. (An experiment redefining [term] as a record subset type of well-formed pre-terms was made and abandoned inside this range; the datatype is unchanged.) Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01E8khwa8zca1fMdMbwHLikG
Both files are rewritten over stdpp: [seq]/[nth]/[size] and the [%O] order give way to stdpp lists, and primitives/sms.v stops pulling primitives/notations.v, whose [From mathcomp Require order] was its final transitive mathcomp import beyond [ssreflect]. primitives/sms.v also loses [Set Implicit Arguments] / [Unset Strict Implicit], which were silently turning the [R] and [i] parameters of the [twp_sms_*] specs implicit even though they are declared with explicit binders and cannot be inferred from the WP. The tree still does not build: core/term/nonces.v and primitives/pre_term.v are repaired in the next commit. primitives/sms.v, which this commit rewrites, compiles again. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01E8khwa8zca1fMdMbwHLikG
Bring everything under cryptis/ back to compiling against the rebuilt term algebra. - primitives/pre_term.v is reworked over the stdpp-side pre-term operations, with the mathcomp-to-stdpp translation it needs added to core/pre_term/with_stdpp.v. Its HeapLang functions are also renamed to mirror the pure ones they implement: [hl_inv_aux] / [hl_mul_aux] for [inv_aux] / [mul_aux], and [hl_inv] / [hl_mul_list] for [inv] / [mul]. - core/term/: nonces.v, subterms.v, tsize.v, repr.v and spec.v are repaired, with the subterm proofs restructured around [factors_TMulN] and the non-[Spec] lemmas in spec.v moved down to the files they belong in. algebra.v gains [TExpK] / [TExpKV] and [invs_canceled1] so that public.v need not inline them. - core/minted.v, core/public.v, lib/dh.v and primitives/comp.v are adapted; the removed [atomic] / [wf_mul_list] premises are replaced throughout by [invs_canceled], and [negb (is_exp t)] replaces [~ is_exp t] for house consistency. The affected examples get the matching one-line fixes. Everything under cryptis/ compiles again after this commit; three example files (iso_dh/proofs/base.v, nsl_dh/proofs/base.v, tls13/proofs/cshare.v) still fail, and are fixed in the next commit. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01E8khwa8zca1fMdMbwHLikG
Adapt the DH-based case studies to the new term API: the removed [atomic] / [wf_mul_list] / [atom_exps] / [no_inv_exps] premises become [invs_canceled], [exps_count_gt0] becomes [count_gt0] over [exps], and the deleted [base_TExpN] / [is_nonce_TExp] / [exps_expN] are inlined at their use sites. [opaque/shared.v] needs the most work: [subterm_exp] is reproved (its old [STMul] inversion branch relied on the [length ts <> 1] component that [invs_canceled] no longer carries), and [subterm_TExpN_exp'] takes [invs_canceled (ts ++ exps t')]. Whole tree builds again, with no admits anywhere. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01E8khwa8zca1fMdMbwHLikG
Remove comments that describe the history of the refactoring rather than the code -- notes about which predicate replaced which, and about which file a definition was split out of -- and comments naming identifiers that no longer exist ([atomic], [wf_mul_list], [hl_insert_exp], [hl_cancel_invs], [is_nonce_TExp]). CLAUDE.md is corrected against the tree: [TNonFree] takes [PreTerm.wf], not [PreTerm.wf_term]; the counting API is [count] and friends, not [count_factors_*]; and the opaque/ and tls13/ file inventories are brought up to date. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01E8khwa8zca1fMdMbwHLikG
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.