Draft
Conversation
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
- Step 2 (AST.hs): Remove NT_KDF payload (bare kdfkey marker), remove KDFPos/KDFBody/KDFSelector types, add IKMAtom, SaltExpr, InfoExpr, KDFGroupWhere, KDFOutputSpec, KDFGroupRuleBody, KDFGroupRule, KDFGroupEntry, KDFGroupRuleRef, DeclKDFGroup; update CKDF to [KDFGroupRuleRef] [NameKind] Int. - Step 3 (Parse.hs): Remove old kdf/dualkdf/odh parsers; add kdfkey bare nametype; add kdf_group block parser with sub-parsers for entries (DH name, kdfkey name, nametype), rules (kdf/odh), salt, ikm (++ concatenated atoms), info, where clause, output spec; update CKDF call-site parser to new Group.Label<idxs> form. - Step 4 (Pretty.hs): Add OwlPretty instances for all new AST types; update NT_KDF and CKDF pretty-printers. Stub out downstream files (TypingBase, Typing, LabelChecking, SMTBase, PathResolution, Concretify) minimally so the build stays clean. Full type-checker rewrite deferred to steps 7-10. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Create tests/parse/kdf_group/ with 13 .owl files covering all required parse cases (basic entries, kdf/odh rules, where clauses, info wildcards, multi-output, single/multi-label call sites, ikm concat, func-wrapped ikm, and a stripped-down full WG_KDF block). All files pass --only-parse. Mark steps 5+6 as complete in the implementation plan. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
…pKDFGroupRule Replace _odh with _kdfGroups in ModBody. Add KDFGroupDef type with _kgdRules and _kgdOdhPairs fields. Add lookupKDFGroupRule to resolve a rule by path, label, and indices. Update ModuleFlattening to use the new field. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
…write Add DeclKDFGroup case to checkDecl: registers qualified names for entries (DH, kdfkey, nametype) and stores rules in _kdfGroups. Add tryHint and sub-checkers (checkWhereClause, checkSaltMatch, checkIKMMatch, checkInfoMatch) for matching kdf_group rule hints against salt/ikm/info arguments. Rewrite CKDF case to use tryHint for each hint, falling back to public Data<adv> if no hint matches. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
NT_KDF returns trivially true flow axiom (bare kdfkey marker). Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
SMT.hs/SMTBase.hs already have bare NT_KDF sort (no changes needed). Clean up remaining TODO step comments. Build compiles cleanly. Parse tests for basic kdf_group, odh_rule, kdf_rule, multi_output, info_wildcard, and ikm_concat all pass. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
- parseKDFGroupEntryNameType: use parseIdxParamBinds (supports <@n>) instead of parseIdxParamBinds1 - KGENameType: change binding from ([IdxVar],[DataVar]) to ([IdxVar],[IdxVar]) for consistency - parseKDFGroupRuleRef: use identifier instead of parsePath (avoids greedy path consumption) - parseIKMAtom: add notFollowedBy to IKMKdfKeyName branch to reject function calls (which go to IKMPublicExpr) - full_wg_group.owl: simplify to non-indexed localities and Data<adv> types - ikm_func_wrap.owl: use 0x instead of dh_combine in nested func args (dh_combine is reserved) Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Two fixes in the DeclKDFGroup case: - Register the group name into defPaths so that kdf<G.L<i>; ...> call-site references to G resolve correctly (previously "Unknown def: G"). - Resolve the locality in KGEDHName entries (e.g. @ alice) so the typechecker receives a resolved path rather than ?alice. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
- KGEKdfKey now carries a Locality (like KGEDHName), requiring `name psk : kdfkey @ alice` syntax; updated AST, parser, pretty-printer, path-resolution, and typechecker accordingly. - Remove dh_combine from reservedNames: it was added erroneously and broke expression-level uses like dh_combine(dhpk(get(X)), get(Y)). - Add kdfGroupPaths to ResolveEnv so that kdf_group-qualified name paths (e.g. G.C1) flatten to PDot PTop "G.C1" instead of navigating into a non-existent sub-module G. - Update test files to supply the required locality on kdfkey names. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Add a new alternative to parseNameExp that handles the kdf_group-based SecName format KDF<G.L<i>; kdfkey; 0>(a, b, c), matching the kdf<...> expression syntax. Rule refs are parsed and discarded (KDFName has no slot for them); the NameType is inferred from nks[j] via nameKindToNameType. The old KDF<nks; j; nt>(...) form is preserved as a fallback. Full integration with CKDF typing (connecting KDFName and gkdf semantics) remains a future step. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
KDFName gains a [KDFGroupRuleRef] field (empty for old syntax). Parser: new KDF<rule_refs; nks; j>(...) format stores refs in KDFName. PathResolution: resolve refs in KDFName the same way as in CKDF exprs. tryHint (KDFStrict): when the salt is actually a secret name, return TRefined(TName(KDFName ... [hint])) with an embedded (pNot (pFlow (nameLbl ne) advLbl)) refinement — mirroring what old matchODH did. This lets checkSubRefinement prove SecName's label constraint trivially from context without needing ODH axioms in SMT. When the salt is public, fall back to tData advLbl advLbl. subKDFName: when both sides carry non-empty refs, check ref alpha-equality instead of subNameType (refs already identify the output type). Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
KGEKdfKey now holds [Locality] instead of Locality, supporting syntax like: name psk<@n,m> : kdfkey @ initiator<n>, responder<m> Updated parser (sepBy1 comma), pretty-printer, path resolution, and typechecker (passes all localities to addNameDef). Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
# Conflicts: # docs/internals/claude-docs/kdf-group-implementation-plan.md
Drop AExpr AExpr AExpr (salt, ikm, info) from the KDFName NameExpX constructor. The output type of a kdf_group rule is fully determined by the rule reference; value identity is already captured by the AEKDF refinement at the kdf<>() call site, so the runtime args don't need to be repeated in type annotations. - AST: KDFName now holds [NameKind] Int NameType (Ignore Bool) [KDFGroupRuleRef] - Parse: KDF<G.L<i>; nks; j> (no trailing parens); old KDF<nks;j;nt>(a,b,c) removed; SecName(KDF<...>) with refs emits TName directly (no TRefined wrapper needed) - Pretty: KDF<refs; nks; j> without args - Typing: subtype case inlined (no subKDFName helper); tryHint builds arg-free KDFName - SMTBase: KDFName(start, segment) — 2-arg SMT term; prelude updated accordingly - SMT: kdfRefinement for KDFName is sTrue (no value-identity assertion without args) - TypingBase/PathResolution/Extraction: remove AExpr handling throughout Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Each rule in a kdf_group block is now checked for three structural soundness conditions via a new helper `validateKDFGroupRule`: 1. Secret material: the salt must contain a kdfkey from the group (an explicit `name _: kdfkey` entry, or a `KDF<L;...>` derived key where the selected output kind is kdfkey), OR the IKM must contain such a kdfkey, OR the IKM must contain a `dh_combine(A, B)` where at least one of A, B is a DH key declared in the group. Without this, the KDF output would not depend on any group-local secret. 2. Index parameter coverage: every session/PId index parameter bound by the rule (i.e., every variable in `is1 ++ is2` after unbinding `_kgrIdxs`) must appear as a free variable somewhere in the salt, IKM, or info. An unanchored index parameter provides no protection against cross-session confusion. 3. Bytestring parameter coverage: every data variable bound by the rule (every variable in `dvars`) must similarly appear free in the salt, IKM, or info. An unused parameter is dead and likely a mistake. The name checks in (1) pattern-match on the resolved path's bare name component (PDot _ n) rather than relying on parser-construction invariants about IKMKdfKeyName, so the check remains correct if the parser changes. Free-variable checks in (2) and (3) use `toListOf fv` on the triple `(salt, ikm, info)` with explicit type annotations `:: [IdxVar]` / `:: [DataVar]` to collect each variable kind. Three new failure tests exercise each constraint independently: - kdf-group-no-secret.owl (constraint 1) - kdf-group-unused-idx.owl (constraint 2) - kdf-group-unused-dvar.owl (constraint 3) Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
…rules In tryHint, assert that the name kinds list at a kdf<L;nks;j> call site has the same length as the rule's output spec and that each nks[i] matches getNameKind of the declared output type. In getNameInfo, look up the KDF group rule for every KDFName node (not just trusted ones), return the actual outNt from the rule instead of the NT_KDF placeholder stored by the parser, and for untrusted (parsed) KDF<L;nks;j> annotations additionally validate nks against the rule. Error messages use owlpretty (kdfkey || enckey) rather than show. Three new failure tests cover: wrong output count, wrong kind at a call site, and wrong kind in a SecName(KDF<...>) return-type annotation. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
The field was always NT_KDF at parse time (a bare placeholder) and was ignored by getNameInfo, which already derives the output type from the kdf_group rule via lookupKDFGroupRule. Removing it eliminates the soundness gap where user-written KDF<...> annotations carried a wrong NT_KDF type instead of the rule-declared output type. - stripDataVar now uses getNameType (→ getNameInfo → lookupKDFGroupRule) to check free variables in the rule's actual output NameType, which is strictly more correct than checking fv(NT_KDF) = ∅ - normalizeNameExp and PathResolution.resolveNameExp become no-ops for KDFName (the rule bodies are resolved/normalized via their own paths) Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
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.