Draft
Conversation
Extract five helper lemmas for better modularity: - countOutgoing_le_length: countOutgoing bounded by vector length - countIncoming_le_length: countIncoming bounded by vector length - totalOutgoing_le_totalCapacity: totalOutgoing bounded by totalCapacity - totalIncoming_le_totalCapacity: totalIncoming bounded by totalCapacity - totalFlow_bound: combined bound for field-to-integer lifting This makes balanced_adds_implies_netFlow more readable by removing deeply nested have statements. The extracted lemmas are reusable and have clear, documented purposes. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <noreply@anthropic.com>
- Extract field_sub_eq_neg_one_implies_swap_eq_one: In a field, a - b = -1 implies b - a = 1 - Extract finRange_map_getElem_eq_toList_map: Mapping over finRange with indexed access equals mapping over toList - Extract countTransitionInPath_first_pos: The first transition in a path has count > 0 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <noreply@anthropic.com>
🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <noreply@anthropic.com>
🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <noreply@anthropic.com>
- Use rfl instead of congr 1 in Loops.lean - Remove guard_hyp debugging from Subcircuit.lean - Use apply instead of exact, simplify proofs in Subcircuit.lean - Rename decodeInstructionSpec/Main/Elaborated/Circuit to decodeInstruction.Spec/main/elaborated/circuit 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <noreply@anthropic.com>
- Fill sorry in IsZero.lean localAdds_eq using collectAdds_foldlRange' - Fill sorry in AbsorbBlock.lean localAdds_eq using new helper lemma - Add collectAdds_mapFinRange' lemma in Loops.lean for .2 syntax matching 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <noreply@anthropic.com>
- Add weakenSpec to StructuralLemmas.lean analogous to FormalCircuit.weakenSpec - Add weakenSpec_assumptions simp lemma - Create circuitWithExecutionExistenceSpec using weakenSpec in TraceExecution.lean 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <noreply@anthropic.com>
Replace FormalAssertionChangingMultiset.weakenSpec (which had a sorry in completeness) with GeneralFormalCircuitChangingMultiset.weakenSpec which doesn't need a sorry because GeneralFormalCircuit.Completeness doesn't depend on Spec. Add FormalAssertionChangingMultiset.toGeneralCircuit conversion to bridge between the two types. The conversion has a sorry in completeness because FormalAssertion.CompletenessChangingMultiset requires Spec to hold, but GeneralFormalCircuit.Completeness doesn't - this is an inherent type mismatch. Update circuitWithExecutionExistenceSpec to use the new pattern. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <noreply@anthropic.com>
Remove FormalAssertionChangingMultiset.toGeneralCircuit and instead construct circuitWithExecutionExistenceSpec directly as a GeneralFormalCircuitChangingMultiset. When converting between formal circuit types is needed, it's better to use the appropriate FormalSomething type directly rather than having conversions with sorries. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <noreply@anthropic.com>
- Change ExecutionBundle.circuit from FormalAssertionChangingMultiset to GeneralFormalCircuitChangingMultiset so weakenSpec can be applied - Simplify circuitWithExecutionExistenceSpec to use weakenSpec directly - Remove unnecessary comment from StructuralLemmas.lean 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <noreply@anthropic.com>
The circuit_soundness theorem is now fully proved using: - circuit_proof_start to set up the proof context - Extract and rewrite eval equalities from h_input - Apply bundle specs with their corresponding assumptions - InteractionDelta.add_eq_append to convert ++ to + - add_assoc to handle associativity differences Completeness proof remains sorry as it depends on bundle completeness proofs which are also currently sorry. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <noreply@anthropic.com>
🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <noreply@anthropic.com>
- FemtoCairo.lean: Use decodeInstruction.circuit instead of decodeInstructionCircuit and unfold decodeInstruction.Spec in simp - ExecutionBundle.lean: Remove redundant rfl and add State.eval_* lemmas to normalize Expression.eval to (eval ...).field form 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <noreply@anthropic.com>
…s; also, start reformulating sound channels
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.
this PR is an attempt to
Channelsas an abstraction similar toTables, that model all cross-table interactionsstarted on top of #309 but heavily refactoring its contributions
The working example for Channels is 8-bit Fibonacci which we implement using 3 different channels that represent 3 prominent ways channels are used: