Reads and writes · rule
data.stored_value_unproven
Update by id builds a value from a stored field that could break its type's rules.
Area 6, Reads and writes; not declinable; the next step is usually the human's.
Nothing checks a value the database works out before it is stored, so the declared ranges must prove it:
type Stock = Int { min: 0 max: 1000}entity Product { id: Uuid stock: Stock}action restock(product_id: Product.id) fails ProductNotFound -> Product { return attempt Product.update(product_id) { set: { stock: Stock(Product.stock + 1) } }}
error: `Product.update` by `id` could store a value that breaks `max: 1000` --> main.jadpo:14:20 |14 | stock: Stock(Product.stock + 1) | ^^^^^^^^^^^^^^^^^^^^^^^^ worked out by the database reason: The database works out a value from `Product`'s stored fields when it writes, so nothing checks it before it is stored: the declared ranges must prove it follows its type's rules. next: Load the record and build the value with `attempt` before `Product.update`, or loosen the type's rules (human) rule: data.stored_value_unproven help: https://jadpo.dev/docs/errors/data.stored_value_unprovencheck failed: 1 error, 1 file
Markdown for agents: /docs/errors/data.stored_value_unproven.md.Built from Jadpo main at a707efb.