Cairo Compiler Learning Notes
Excerpts from How Cairo Works Introduction to Cairo Registers ap: allocation pointer fp: frame pointer pc: program counter Basic instructions [fp - 1] = [ap - 2] + [fp + 4] [ap - 1] = [fp + 10] * [ap]; ap++ [ap - 1] = [fp + 10] + 12345; ap++ #…
61 2022-06-02 去围观Rosette Learning Notes
Excerpts from The Rosette Guide. Rosette Essentials Symbolic Values (define-symbolic b boolean?) Specification (define (check-mid impl lo hi) ; Assuming that (assume (bvsle (int32 0) lo)) ; 0 ≤ lo and (assume (bvsle lo hi)) …
40 2022-06-02 去围观Notes of "The Logic of Computer Programming"
Link: The Logic of Computer Programming Four aspect: correctness termination transformation development Program A: Partial Correctness totally correct: if we execute Program A on any input satisfying the input assertion, the program will ha…
611 2021-11-13 去围观
