# Rules

Make one major heading per discussion topic

# Invariants

* pre and posconditions for functions in scope
* type invariants also to avoid duplication on signatures
* loop conditions are future work since they don't have much to do with signatures. They are useful though.

# Ghost functions

These will be a thing, to refer to in proofs which add invariants.
Useful to name properties.
Orthogonal to contracts work.

# Naming invariants

Some people think it's tangential. CSC might like this to relate tool output to contracts. Some people indicate that they agree that if proofs get large enough this could become relevant. However, not everyone (notably ralf) is convinced this is relevant.

# Abstract Machine + Logic

- Abstract Machine:
- Ghost Intrinsics (noop at runtime)
- It could eventually include I/O spec
- Sampling / Ownership:

# Spec

Layers:
- Safety
- correctness

2 Possible lowering:
- Pre / post-condition
- Only post-conditions:
- panic
- implication (pre => post)

# Links

- https://github.com/Artisan-Lab/tag-std/blob/main/primitive-sp.md
- [Idea: naming requirements allows tool-assisted safety reviews](https://hackmd.io/@predrag/ByVBjIWlyx) — a syntactic sugar for naming clauses in contract components would allow similar tool assists and lints
- [Felix presentation on Rust Contracts (Tenets](https://pnkfx.org/presentations/contracts2-rw2024.pdf)