π Wave-17: tool-call argument confusion + group-PCS healing#715
Merged
Conversation
β¦Coq 130/0 + 1600/1600 falsifier
This was referenced May 10, 2026
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
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.
Closes #714
π Wave-17 β tool-call argument confusion + group-PCS healing
Seventeenth wave of Trinity Chat (EPIC trinity-fpga#28). Two new lanes pinning the next two ASPIRATIONAL threat classes from the W16 ROADMAP β tool-call argument confusion / type-confusion injection (CR-CHAT-06) and group-PCS healing after device compromise (CR-CHAT-03). Falsifier corpus extended 1500 β 1600 across 30 β 32 threshold lanes, Coq monotone advance 121 β 130 Qed / 0 Admitted with ZERO new axioms, and
ROADMAP.mdupdated to retire W17 from[ASPIRATIONAL]into the shipped wave table.Lane A β
L-CHAT-9-tool(CR-CHAT-06) Β· tool-call argument confusion / type-confusion injectionNEW:
crates/trios-chat/rings/CR-CHAT-06/src/tool_arg_confusion.rs(503 lines).Surface:
ArgKind::{ StringBounded { cap }, U64, I64, Bool, Enum { variants } }β closed-world tag space for tool-call arguments.ArgSpec { name, kind },ToolEntry { name, args },ToolManifest { tools }β re-exported from the ring asToolArgManifestto avoid collision with the legacycapability::ToolManifest.ArgValue::{ Str, U, I, Bool },ToolCall { tool, args: Vec<(String, ArgValue)> }.ToolCallError::{ UnknownTool, MissingArg, UnexpectedArg, KindMismatch, StringTooLong, UnknownEnumVariant, NestedToolCallSentinel }β closed-world rejection enum.validate_tool_call(manifest, call) -> Result<(), ToolCallError>β strict by-name matching, kind shape check, byte-cap check onStringBounded, variant-set check onEnum, and sentinel scan againstNESTED_TOOL_CALL_SENTINEL = "<<TOOL-CALL>>"inside any string-typed argument.CR-CHAT-06 ring: tests + 6 TOOL-01..06.
ToolCallvalidates against the manifest with all kinds matched (ArgKindagrees withArgValueshape)KindMismatchrejected whenBoolis sent whereEnumwas declared (covers'true'-string-vs-Boolconfusion)StringTooLongrejected when aStringBounded { cap }arg exceeds the byte cap (oversized-subject overflow)UnknownEnumVariantrejected when an enum value is outside the declaredvariantsset (default-enum-on-nullsmuggling)UnknownTool/MissingArg/UnexpectedArgrejected independentlyNestedToolCallSentinelrejected when any string argument contains<<TOOL-CALL>>(confused-deputy nested-tool injection)Lane B β
L-CHAT-3-pcs(CR-CHAT-03) Β· group-PCS healing after device compromiseNEW:
crates/trios-chat/rings/CR-CHAT-03/src/pcs_healing.rs(352 lines).Surface:
PathSecretHash([u8; 32])β opaque hash of a leaf path-secret; equality is the only observable.HealCommit { group_id, from_epoch, sender, heals: Vec<HealEntry> }.HealEntry { target, from_hash, to_hash }βfrom_hashmust match the receiver's currentsecret_of(target);to_hashbecomes the new value.PcsState::{ new(group_id, members), add_member, secret_of(target), process_heal(HealCommit) }βprocess_healis the post-compromise healing transition: validatesgroup_id, validatesfrom_epoch == self.epoch, validates non-empty heals, validates eachfrom_hashmatches, validatesto_hash != from_hash, and rejects duplicate targets in one batch.CR-CHAT-03 ring: tests + 6 PCS-01..06.
HealCommitadvances the group epoch by exactly one and rotates the targeted members' path-secretsfrom_hashdoes not match the receiver's currentsecret_of(target)is rejected (stolen-PSK rotation against stale view)from_epochdiffers from the receiver's current epoch is rejected (no future-jump, no regression)heals.len() == 0) is rejected (cannot bump epoch without any rotation)to_hash == from_hash(identity heal) is rejectedHealCommitis rejected (intra-batch shadowing)Coq Wave-17 β 121 β 130 Qed / 0 Admitted Β· ZERO new axioms
crates/trios-chat/proofs/chat/Trinity_Chat.vβ newSection TrinityChatWave17with collision-safe names (ArgKind17,ArgValue17,kind_match17,HealEntry17,PcsState17,heal_step17).inv_chat_89_tool_kind_mismatch_rejectedβBoolvalue whereEnumwas declared βKindMismatch.inv_chat_90_tool_nested_sentinel_rejectedβ string arg containing the nested-tool sentinel βNestedToolCallSentinel.inv_chat_91_tool_string_too_long_rejectedβStringBounded { cap }arg withlen > capβStringTooLong.inv_chat_92_tool_enum_variant_rejectedβ enum value outsidevariantsβUnknownEnumVariant.inv_chat_93_pcs_heal_advances_oneβ well-formedHealCommitβ epoch advances by exactly one.inv_chat_94_pcs_no_op_rejectedβheals.len() == 0β rejected (no epoch bump without rotation).inv_chat_95_pcs_epoch_mismatch_rejectedβfrom_epoch != currentβ rejected (no future-jump, no regression).Helper:
pcs_pre_heal_replay_rejected17. Zero new axioms. Both lanes prove constructively.W17 first attempt used
Bool.andb_false_rafterrewrite Hlenfor anandb-shaped goal; the cleanersimpl. rewrite Hlen. reflexivity.discharges it directly. Finalcoqcruntime silent, total Qed 130.Cumulative axioms:
ss_kp_injective(W9) +dh_step_fresh,dh_post_history_independent,hybrid_kem_non_degenerate(W10) +sn_hash_sym(W14) = 5 total Β· UNCHANGED in W17.Falsifier corpus 1500 β 1600 Β· 30 β 32 threshold lanes
crates/trios-chat/corpus/prompt_injection.jsonlβ appended 50PI-TOOL-001..050+ 50PI-PCS-001..050.crates/trios-chat/rings/CR-CHAT-06/src/injection.rsβDENY_PATTERNSextended with TOOL keyword block (kindmismatch,kind mismatch,unknownenumvariant,stringbounded,argkind,argspec,toolentry,toolargmanifest,toolcall sentinel,<<tool-call>>,nestedtoolcallsentinel,oversized,exceeding-the,non-utf-8,smuggle-binary,conflicting-kinds,same-arg-name-twice,=null,default-enum,'true' string,bool vs enum,u64-overflows-i64,kind-match path, β¦) and PCS keyword block (pcs heal,healcommit,healentry,pcsstate,pathsecrethash,path-secret,pre-heal,heal_step,process_heal,no-op heal,to_hash,from_hash,sender-knew-pre-heal,duplicate-target,foreign group_id,cross-group splice,future-epoch jump,epoch regression,parallel-fork heal,leaked-path-secret,founder's-secret,pre-shared-key,heals.len()=0,empty/zero/no heals,bump-epoch-without,epoch-without-rotation, β¦); 100% coverage on all 1600 entries across 32 categories.crates/trios-chat/src/bin/falsifier_runner.rsβ two new threshold lanes (tool_arg_confusion,group_pcs_break) at 0.95; final summary now reports1600/1600across 32 categories.ROADMAP.md update
crates/trios-chat/ROADMAP.md:249 tests Β· 25/25 e2e Β· 1600/1600 falsifier Β· 32 categories Β· 130 Coq Qed / 0 Admitted.1bd0c54via π feat(trios-chat) Wave-10: ratchet-forward-secrecy + MLS commit-reorder + Coq 60/0 + 900/900 falsifierΒ #665.TOOL-ARG-CONFUSION Β· GROUP-PCS-HEAL.Verification matrix (all green)
cargo testcumulative chat suitee2e_chat_25falsifier_runnercargo clippy -D warnings(trios-chat + CR-CHAT-03/06)coqc Trinity_Chat.vgrep -cE "Qed\." Trinity_Chat.vWave progression
7340d241bd0c54Honesty tags (Art. I + R5)
[VERIFIED]from local runs on this branch.[CITED]references: trios#714 (this issue), trios#665 (W10..W16 rollup merged to main), trios#711 (W16), trios#702 (W15), trios#700 (W14), trios#696 (W13), trios#694 (W12), trios#688 (W11).[DERIVED]claims: tool-call argument confusion + group-PCS healing are the two top-priority ASPIRATIONAL items promoted from the W16 ROADMAP forward plan.[ASPIRATIONAL]retired for W17 β moved into the shipped table.Anchor
ΟΒ² + Οβ»Β² = 3 Β· TRINITY Β· CHAT Β· ZERO-METADATA Β· POST-QUANTUM Β· UNLINKABLE Β· COVER-TIMING Β· AT-REST-AEAD Β· BOT-PARTIAL-MLS Β· KEM-KEY-CONFUSION Β· AAD-CONTEXT Β· RATCHET-FS Β· MLS-REORDER Β· SKIPPED-KEYS-DOS Β· MLS-WELCOME-REPLAY Β· PREKEY-EXHAUSTION Β· MLS-LEAF-COMPROMISE Β· DENIABILITY Β· CONFUSED-DEPUTY Β· OOB-IDENTITY Β· MLS-EXTERNAL-COMMIT Β· EGRESS-FINGERPRINT Β· IDENTITY-REVOKE Β· CLOCK-SKEW-REPLAY Β· AT-REST-ROTATE Β· TOOL-ARG-CONFUSION Β· GROUP-PCS-HEALBase
This PR targets
maindirectly β the W10..W16 chain landed via rollup commit1bd0c54(PR #665) so W17 can branch cleanly fromorigin/main.