Skip to content

Commit c60275a

Browse files
Testclaude
andcommitted
docs: Phase 0 Sealing - add Getting Started guide and usage examples
Add comprehensive user documentation for valence-shell: - GETTING_STARTED.md: Installation, quick start, features, troubleshooting - EXAMPLES.md: Real-world usage patterns with 10 detailed examples Completes Component 4 of Phase 0 Sealing plan. Co-Authored-By: Claude Sonnet 4.5 <noreply@anthropic.com>
1 parent 7c2f266 commit c60275a

2 files changed

Lines changed: 902 additions & 0 deletions

File tree

impl/rust-cli/docs/EXAMPLES.md

Lines changed: 381 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,381 @@
1+
# Valence Shell - Usage Examples
2+
3+
Real-world usage patterns for valence-shell operations.
4+
5+
---
6+
7+
## Example 1: Project Scaffolding with Rollback
8+
9+
Create a project structure, verify it works, or rollback if it doesn't:
10+
11+
```bash
12+
vsh> begin new-project
13+
[txn:12345678] begin new-project
14+
15+
vsh> mkdir myapp
16+
[op:23456789] mkdir myapp
17+
18+
vsh> mkdir myapp/src
19+
[op:34567890] mkdir myapp/src
20+
21+
vsh> mkdir myapp/tests
22+
[op:45678901] mkdir myapp/tests
23+
24+
vsh> touch myapp/README.md
25+
[op:56789012] touch myapp/README.md
26+
27+
vsh> touch myapp/src/main.rs
28+
[op:67890123] touch myapp/src/main.rs
29+
30+
vsh> ls myapp > myapp/structure.txt
31+
[op:78901234] ls myapp
32+
33+
vsh> commit
34+
Transaction committed: 6 operations
35+
```
36+
37+
If you made a mistake:
38+
39+
```bash
40+
vsh> rollback new-project
41+
Transaction rolled back: 6 operations
42+
# All changes undone - clean slate
43+
```
44+
45+
---
46+
47+
## Example 2: Log File Rotation with Undo
48+
49+
Rotate logs safely with the ability to revert:
50+
51+
```bash
52+
vsh> ls logs
53+
📄 app.log
54+
📄 app.log.1
55+
📄 app.log.2
56+
57+
vsh> begin log-rotate
58+
[txn:abcdef01] begin log-rotate
59+
60+
vsh> rm logs/app.log.2
61+
[op:bcdef012] rm logs/app.log.2
62+
63+
vsh> mv logs/app.log.1 logs/app.log.2
64+
# (mv not implemented yet - use external command)
65+
66+
vsh> mv logs/app.log logs/app.log.1
67+
# (external mv not reversible)
68+
69+
vsh> touch logs/app.log
70+
[op:cdef0123] touch logs/app.log
71+
72+
vsh> commit
73+
```
74+
75+
Better approach (when you realize external mv isn't reversible):
76+
77+
```bash
78+
vsh> rollback log-rotate
79+
# Undoes only the vsh operations (rm, touch)
80+
81+
# Use transaction for atomic rotation
82+
# (Feature request: Built-in mv command)
83+
```
84+
85+
---
86+
87+
## Example 3: Batch File Operations
88+
89+
Create multiple files with redirection:
90+
91+
```bash
92+
vsh> begin batch-create
93+
[txn:def01234] begin batch-create
94+
95+
vsh> echo "File 1" > file1.txt
96+
[op:ef012345] echo
97+
98+
vsh> echo "File 2" > file2.txt
99+
[op:f0123456] echo
100+
101+
vsh> echo "File 3" > file3.txt
102+
[op:01234567] echo
103+
104+
vsh> ls > inventory.txt
105+
[op:12345678] ls
106+
107+
vsh> commit
108+
Transaction committed: 4 operations
109+
```
110+
111+
Undo creates and writes:
112+
113+
```bash
114+
vsh> undo 4
115+
[op:23456789] undo [op:12345678] DeleteFile inventory.txt
116+
[op:34567890] undo [op:01234567] DeleteFile file3.txt
117+
[op:45678901] undo [op:f0123456] DeleteFile file2.txt
118+
[op:56789012] undo [op:ef012345] DeleteFile file1.txt
119+
```
120+
121+
---
122+
123+
## Example 4: Redirection Pipelines
124+
125+
### Capture Command Output
126+
127+
```bash
128+
vsh> ls -la > full-listing.txt
129+
[op:67890123] ls
130+
# Long listing saved to file
131+
132+
vsh> cat full-listing.txt
133+
drwxr-xr-x project/
134+
-rw-r--r-- README.md
135+
```
136+
137+
### Append to Logs
138+
139+
```bash
140+
vsh> echo "[INFO] Starting process" >> app.log
141+
[op:78901234] echo
142+
143+
vsh> date >> app.log
144+
[op:89012345] date
145+
146+
vsh> echo "[INFO] Process complete" >> app.log
147+
[op:90123456] echo
148+
149+
vsh> cat app.log
150+
[INFO] Starting process
151+
Tue Jan 28 14:30:00 UTC 2026
152+
[INFO] Process complete
153+
```
154+
155+
### Error Logging
156+
157+
```bash
158+
vsh> find /restricted 2> errors.log
159+
# Permission errors captured in errors.log
160+
161+
vsh> cat errors.log
162+
find: /restricted: Permission denied
163+
```
164+
165+
---
166+
167+
## Example 5: Verification Workflow
168+
169+
Verify operations with proof references:
170+
171+
```bash
172+
vsh> mkdir build --verbose
173+
[op:01234567] mkdir build
174+
Proof: mkdir_rmdir_reversible (FilesystemModel.lean:158)
175+
Undo: rmdir build
176+
177+
vsh> history --proofs
178+
═══ Operation History ═══
179+
180+
[01234567] 14:30:00 mkdir build
181+
Theorem: mkdir_rmdir_reversible (FilesystemModel.lean:158)
182+
```
183+
184+
---
185+
186+
## Example 6: Safe Cleanup
187+
188+
Clean up temporary files with undo safety:
189+
190+
```bash
191+
vsh> begin cleanup
192+
[txn:12345678] begin cleanup
193+
194+
vsh> rm temp1.txt
195+
[op:23456789] rm temp1.txt
196+
197+
vsh> rm temp2.txt
198+
[op:34567890] rm temp2.txt
199+
200+
vsh> rmdir temp-dir
201+
[op:45678901] rmdir temp-dir
202+
203+
vsh> commit
204+
Transaction committed: 3 operations
205+
```
206+
207+
If you accidentally deleted something important:
208+
209+
```bash
210+
vsh> undo 3
211+
# All files restored from undo data
212+
```
213+
214+
---
215+
216+
## Example 7: Operation Independence
217+
218+
Operations on different paths don't interfere:
219+
220+
```bash
221+
vsh> mkdir alpha
222+
[op:56789012] mkdir alpha
223+
224+
vsh> mkdir beta
225+
[op:67890123] mkdir beta
226+
227+
vsh> undo
228+
[op:78901234] undo [op:67890123] rmdir beta
229+
230+
vsh> ls
231+
📁 alpha/
232+
# beta removed, alpha unaffected
233+
```
234+
235+
---
236+
237+
## Example 8: Transaction Rollback
238+
239+
Rollback when operations fail mid-transaction:
240+
241+
```bash
242+
vsh> begin risky
243+
[txn:89012345] begin risky
244+
245+
vsh> mkdir test
246+
[op:90123456] mkdir test
247+
248+
vsh> touch test/file.txt
249+
[op:01234567] touch test/file.txt
250+
251+
# Oops - need to abort
252+
vsh> rollback risky
253+
Transaction rolled back: 2 operations
254+
255+
vsh> ls test
256+
Error: Path does not exist
257+
# Everything cleaned up
258+
```
259+
260+
---
261+
262+
## Example 9: Redirected Undo
263+
264+
File modifications are tracked:
265+
266+
```bash
267+
vsh> echo "version 1" > data.txt
268+
[op:12345678] echo
269+
270+
vsh> cat data.txt
271+
version 1
272+
273+
vsh> echo "version 2" > data.txt
274+
[op:23456789] echo
275+
276+
vsh> cat data.txt
277+
version 2
278+
279+
vsh> undo
280+
[op:34567890] undo [op:23456789] WriteFile data.txt
281+
# File truncation reversed - original content restored
282+
283+
vsh> cat data.txt
284+
version 1
285+
```
286+
287+
---
288+
289+
## Example 10: Interrupting Long Commands
290+
291+
Ctrl+C stops external commands:
292+
293+
```bash
294+
vsh> sleep 300
295+
# Press Ctrl+C after a few seconds
296+
^C
297+
[Interrupted - exit code 130]
298+
299+
vsh> # Shell still responsive
300+
```
301+
302+
---
303+
304+
## Common Patterns
305+
306+
### Pattern: Experimental Changes
307+
308+
```bash
309+
begin experiment
310+
# Make changes
311+
# Test them
312+
commit # If good
313+
# OR
314+
rollback experiment # If bad
315+
```
316+
317+
### Pattern: Staged Operations
318+
319+
```bash
320+
mkdir stage1
321+
touch stage1/file.txt
322+
# Verify stage1 works
323+
mkdir stage2
324+
# Verify stage2 works
325+
# All operations are individually undoable
326+
```
327+
328+
### Pattern: Redirection with Undo Safety
329+
330+
```bash
331+
ls > backup-listing.txt
332+
# Oops - wrong file
333+
undo
334+
# File deleted automatically
335+
ls > correct-listing.txt
336+
```
337+
338+
---
339+
340+
## Advanced Usage
341+
342+
### Operation Graph Navigation
343+
344+
```bash
345+
vsh> graph
346+
# Shows current state in DAG
347+
348+
vsh> history
349+
# Shows linear history
350+
351+
vsh> undo
352+
# Move backward in DAG
353+
354+
vsh> redo
355+
# Move forward in DAG
356+
```
357+
358+
### Proof Verification
359+
360+
Every operation corresponds to a Lean 4 theorem:
361+
362+
| Operation | Theorem | File |
363+
|-----------|---------|------|
364+
| mkdir | mkdir_rmdir_reversible | FilesystemModel.lean:158 |
365+
| rmdir | rmdir_mkdir_reversible | FilesystemModel.lean:184 |
366+
| touch | createFile_deleteFile_reversible | FileOperations.lean:42 |
367+
| rm | deleteFile_createFile_reversible | FileOperations.lean:52 |
368+
| > | truncate_restore_reversible | FileContentOperations.lean:109 |
369+
| >> | append_truncate_reversible | FileContentOperations.lean:297 |
370+
371+
---
372+
373+
## Next Steps
374+
375+
- Read [PHASE6_M2_COMPLETE.md](PHASE6_M2_COMPLETE.md) for technical details
376+
- Explore `proofs/lean4/` for formal verification
377+
- Try building your own verified operations
378+
379+
---
380+
381+
**Remember**: vsh is a research prototype. Use it to explore formally verified computing, not for production systems (yet).

0 commit comments

Comments
 (0)