4 ms·
If you don't mind, could you drop some code? I'd be interested to see the result :)
by alexisread 7mo ago
If you don't mind, could you drop some code? I'd be interested to see the result :)
- fcatalan 7mo agosure, for example it generated this small demo of the type and contract safeguards. As you can see, it's mostly "Forth but with things": # bank.ax — The Safe Bank (Milestone 2) # # Demonstrates property-based verification of financial operations. # Each function has PRE/POST contracts. VERIFY auto-generates random # inputs, filters by PRE, runs the function, and checks POST holds. # DEPOSIT: add amount to balance # Stack: [amount, balance] (amount on top) # PRE: amount > 0 AND balance >= 0 # POST: result >= 0 DEF deposit : int int -> int PRE { OVER 0 GTE SWAP 0 GT AND } ADD POST DUP 0 GTE END # WITHDRAW: subtract amount from balance # Stack: [amount, balance] (amount on top) # PRE: amount > 0 AND balance >= amount # POST: result >= 0 DEF withdraw : int int -> int PRE { OVER OVER GTE SWAP 0 GT AND } SUB POST DUP 0 GTE END # Verify both functions — 500 random tests each VERIFY deposit 500 VERIFY withdraw 500 # Prove both functions — mathematically, for ALL inputs PROVE deposit PROVE withdraw # Demo: manual operations 1000 200 deposit SAY 1000 300 withdraw SAY Running it outputs: VERIFY deposit: OK — 500 tests passed (1056 skipped by PRE) VERIFY withdraw: OK — 500 tests passed (1606 skipped by PRE) PROVE deposit: PROVEN — POST holds for all inputs satisfying PRE PROVE withdraw: PROVEN — POST holds for all inputs satisfying PRE 1200 700
- fuzztester 7mo agoHow does it do the proving?
- fcatalan 7mo agoSpawns and calls z3 under the hood, I did let it cheat there because otherwise it's rabbit holes below rabbit holes all the way down :)
- fuzztester 7mo agothanks.