Add experimental Dafny backend

[Philipp15b]

Summary

This adds an experimental Dafny backend for Caesar.

• adds caesar dafny and caesar to-dafny
• translates a restricted Boolean proc-based fragment of HeyVL to Dafny
• emits one .dfy file per input .heyvl file, with reachable and all output scopes
• adds backend-focused tests, curated comparison examples, and user documentation
• adds Dafny syntax highlighting for the docs site

Supported fragment

The current backend is intentionally narrow.

• proc, not coproc
• Boolean specifications via ?(b)
• classical statements, procedure calls, and while loops with @invariant(?(...))
• domains, axioms, definitional and bodyless functions, and built-in sequences

Limitations

This is an initial backend intended for iteration.

• quantitative features and most proof-rule-specific encodings are out of scope
• some translated programs still need manual adjustment before they pass dafny verify
• the main remaining Dafny-side issue is recursive helper functions over symbolic domains

Validation

• cargo test --quiet 'dafny::tests::'
• cargo test --test integration -- comparison
• npm run build in website/