Module init 

SMT lowering for the Init safety property.

This first version proves only a local one-element write pattern:

ptr.write(value)
require Init(ptr, T, 1)

Forward visit records ptr.write as a KnownInit fact. The common SMT backend then checks whether the Init target has the same address as a known initialized pointer. Range initialization across loops still needs a loop summary and is intentionally left as Unknown.

Functions

array_elem_size 🔒

array_len_term 🔒

check 🔒

Check Init by lowering it to a common initialized-memory obligation.

check_for_checkpoint 🔒

Check Init at a return checkpoint for struct invariant verification.

compute_elem_size 🔒