[DRAFT] KDF groups impl#34
Draft
pratapsingh1729 wants to merge 128 commits into
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>
…en processing the KDF scope
…olved appropriately
…issue due to no length refinement on KDF names
… form, makes the kdf_inj_lemma work properly
…t typecheck at the correct type yet
…e refinements rather than elsewhere in the context. Seems to partially work
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
2 participants
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.