Explain annotation and configuration in README

Author: coord-e

README.md

@@ -66,6 +66,64 @@ safe
 
 Integration test examples are located under `tests/ui/` and can be executed using `cargo test`. You can review these examples to understand what the current Thrust implementation can handle.
 
+## Annotation
+
+Thrust can verify a wide range of programs without explicit annotations, but you can use `#[thrust::requires(expr)]` and `#[thrust::ensures(expr)]` to annotate the precondition and postcondition of a function, aiding in verification or specifying the specification. Here, `expr` is a logical expression that supports basic integer, boolean, and reference operations.
+
+```rust
+#[thrust::requires(n >= 0)]
+#[thrust::ensures((result * 2) == n * (n + 1))]
+fn sum(n: i32) -> i32 {
+    if n == 0 {
+        0
+    } else {
+        n + sum(n - 1)
+    }
+}
+```
+
+You can use the `^` unary operator to denote the value of a mutable reference after the function is called. Note that in the current implementation, you need to specify both `requires` and `ensures` when using either one.
+
+```rust
+#[thrust::requires(true)]
+#[thrust::ensures(^ma == *ma + a)]
+fn add(ma: &mut i32, a: i32) {
+    *ma += a;
+}
+```
+
+The conditions on `thrust::requires` and `thrust::ensures` are internally encoded as refinement types for the parameter and return types. You can also specify these refinement types directly using `#[thrust::param(param: type)]` and `#[thrust::ret(type)]`.
+
+```rust
+#[thrust::param(n: { x: int | x >= 0 })]
+#[thrust::ret({ x: int | (x * 2) == n * (n + 1) })]
+fn sum(n: i32) -> i32 {
+    if n == 0 {
+        0
+    } else {
+        n + sum(n - 1)
+    }
+}
+```
+
+The bodies of functions marked with `#[thrust::trusted]` are not analyzed by Thrust. Additionally, `#[thrust::callable]` is an alias for `#[thrust::requires(true)]` and `#[thrust::ensures(true)]`.
+
+```rust
+#[thrust::trusted]
+#[thrust::callable]
+fn rand() -> i32 { unimplemented!() }
+```
+
+## Configuration
+
+Several environment variables are used by Thrust to configure its behavior:
+
+- `THRUST_SOLVER`: A CHC solver command used to solve CHC constraints generated by Thrust. Default: `z3`
+- `THRUST_SOLVER_ARGS`: Whitespace-separated command-line flags passed to the solver. The default is `fp.spacer.global=true fp.validate=true` when the solver is `z3`.
+- `THRUST_SOLVER_TIMEOUT_SECS`: Timeout for waiting on results from the solver. Default: `30`
+- `THRUST_OUTPUT_DIR`: When configured, Thrust outputs intermediate smtlib2 files into this directory.
+- `THRUST_ENUM_EXPANSION_DEPTH_LIMIT`: When Thrust works with enums, it "expands" the structure of the enum value onto its environment. This configuration value sets the limit on the depth of recursion during this expansion to handle enums that are defined recursively. It is our future work to discover a sensible value for this automatically. Default: `2`
+
 ## Development
 
 The implementation of the Thrust is largely divided into the following modules.