Skip to content

Commit e9e181b

Browse files
will-break-itwill-break-it
authored
Workshop (#281)
* docs: workshop recap day 1
1 parent fba21d5 commit e9e181b

File tree

1 file changed

+130
-0
lines changed

1 file changed

+130
-0
lines changed

‎docs/workshop/1-day-recap.md‎

Lines changed: 130 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,130 @@
1+
# Edinburgh Workshop Day 1 Recap
2+
3+
## Ledger Design Solution Space Matrix
4+
5+
| | Labeled UTxOs (Explicit Shards) | Accounts (Implicit Shards) |
6+
|---------------------|--------------------------------|---------------------------|
7+
| **Fees** | • Explicit shard labeling<br>• Consumed on every tx<br>• Bootstrap: requires additional transaction<br>• Strong guarantees | • Staking credential defines shard<br>• No replay protection<br>• No bootstrap transaction needed<br>• Registration costs |
8+
| **Collateral** | • Only consumed on conflicts<br>• Return address needed<br>• Helps prevent conflicts | • Only consumed on conflicts<br>• No replay protection |
9+
| **All-Labeled Inputs (Extension)** | • Every input gets labeled<br>• Maximum conflict prevention<br>• Higher bootstrapping cost | N/A |
10+
11+
### Labeled UTxOs - Fees
12+
Explicit shard labeling of UTxOs with fees consumed on every transaction. Provides strong guarantees for conflict prevention. Requires one initial bootstrap transaction to transition from Praos to Leios, enabling immediate protocol participation.
13+
14+
### Labeled UTxOs - Collateral
15+
Collateral consumed only when conflicts occur, requiring a return address. Offers weaker guarantees than the fees approach while maintaining system integrity through explicit shard labeling.
16+
17+
### Labeled UTxOs - All-Labeled Inputs Extension
18+
The all-labeled inputs extension represents the most comprehensive approach, where every input gets labeled. This provides maximum conflict prevention but comes with higher bootstrapping costs. This approach offers the strongest guarantees but requires significant upfront work for migration.
19+
20+
### Accounts - Fees
21+
The Accounts approach uses staking credentials to implicitly define shards, eliminating the need for explicit bootstrap transactions. However, it lacks replay protection and has registration costs. This approach is more natural for existing Cardano users but requires careful consideration of replay attacks.
22+
23+
### Accounts - Collateral
24+
In the Accounts approach, collateral is only consumed on conflicts but lacks replay protection. This simpler mechanism avoids double spending but may be less robust against certain types of attacks. The integration with existing staking credentials makes it more user-friendly but potentially less secure.
25+
26+
### Accounts - All-Labeled Inputs Extension
27+
This extension is not applicable to the Accounts approach.
28+
29+
## Key Design Considerations & Insights
30+
31+
### User Bootstrapping Flow
32+
- Initial transaction requires a UTxO input for replay protection
33+
- Uses implicit sharding via staking credential
34+
- Can create labeled outputs in same transaction
35+
- Provides seamless user experience without separate bootstrap transaction
36+
37+
### Network Transition Considerations
38+
- Existing Praos UTxOs and reward accounts remain valid
39+
- Need to consider both:
40+
1. Network transition (Praos → Leios)
41+
2. Individual user onboarding into Leios
42+
- Gradual transition possible without hard cutover
43+
44+
### Critical Edge Cases
45+
46+
1. **New User Onboarding**
47+
- Exchange withdrawals are a critical flow
48+
- Pure account-based approach problematic:
49+
- Would require registering staking credential
50+
- Complex transaction needing receiving wallet signature
51+
- Impractical for exchange withdrawals
52+
53+
2. **Account Recovery**
54+
- Risk of users accidentally emptying fee accounts
55+
- No built-in recovery mechanism for empty reward accounts
56+
- Requires careful balance management consideration
57+
58+
3. **Fee Payment**
59+
- Must ensure reward accounts have sufficient funds
60+
- Need to consider initial distribution and maintenance
61+
- Balance between user experience and security
62+
63+
### System Properties
64+
65+
1. **Replay Protection**
66+
- UTxO input requirement prevents transaction replay
67+
- Critical for system security
68+
- Must be maintained regardless of sharding approach
69+
70+
2. **Conflict Resolution**
71+
- Explicit vs implicit sharding tradeoffs
72+
- Impact on throughput and user experience
73+
- Balance between complexity and guarantees
74+
75+
3. **Governance Compatibility**
76+
- Must work with existing governance mechanisms
77+
- Support for:
78+
- UTxO and reference inputs
79+
- Votes and proposals
80+
- Reward account withdrawals
81+
- Treasury assertions
82+
- Parameter changes
83+
- Hardfork events
84+
85+
### Conformance Testing Considerations
86+
87+
Two complementary approaches were discussed for ensuring implementation correctness:
88+
89+
1. **QuickCheck Dynamic Approach**
90+
- Executable formal specification in Agda
91+
- Specification converted to Haskell using standard Agda compiler
92+
- QuickCheck Dynamic test driver for generating test cases
93+
- Test adapters needed for both Haskell and Rust simulations
94+
- Challenges:
95+
- Complex generator development for meaningful test cases
96+
- Need for adapters to interface with simulations
97+
- Higher implementation effort but enables adversarial testing
98+
99+
2. **Trace Verification Approach**
100+
- Uses simulation log files as input
101+
- Verifies traces against relational specification
102+
- Lower implementation overhead
103+
- Requires standardized log format between implementations
104+
- Limitations:
105+
- Only tests behaviors that naturally occur in simulations
106+
- May miss edge cases or adversarial scenarios
107+
- Cannot directly test invalid behaviors
108+
109+
3. **Coverage Enhancement Strategy**
110+
- Track which parts of specification are exercised by traces
111+
- Use Haskell Program Coverage (HPC) on generated code
112+
- Identify untested branches and conditions
113+
- Benefits:
114+
- Clear visibility of test coverage gaps
115+
- Guide development of targeted test scenarios
116+
- Help prioritize adversarial test case development
117+
118+
4. **Implementation Requirements**
119+
- Standardized logging format across implementations
120+
- Support for negative events (e.g., "could not produce IB")
121+
- Clear separation between node and environment
122+
- Ability to track specification coverage
123+
- Support for both valid and invalid test cases
124+
125+
5. **Phased Testing Strategy**
126+
- Start with trace verification for basic correctness
127+
- Add coverage tracking to identify gaps
128+
- Develop targeted test cases for uncovered scenarios
129+
- Implement QuickCheck approach for adversarial testing?
130+
- Focus on high-priority edge cases identified in coverage analysis

0 commit comments

Comments
 (0)