ifc.rkt (1661B)
1 #lang turnstile 2 (extends "rosette.rkt" #:except) ; extends typed rosette 3 (require (prefix-in ro: rosette)) ; untyped 4 (require (prefix-in ro: rosette/lib/synthax)) 5 (require sdsl/ifc/instruction) ; program 6 (require sdsl/ifc/basic) ; Halt, Noop, Push, etc 7 (require (except-in sdsl/ifc/machine write read)) ; init, halted? 8 (require sdsl/ifc/indistinguishable) ; mem≈ 9 (require sdsl/ifc/verify) ; verify-EENI 10 11 (define-base-types Prog Instr Machine Witness) 12 13 (provide Prog Instr Machine Witness 14 (typed-out [Halt : Instr] 15 [Noop : Instr] 16 [Push : Instr] 17 [Pop : Instr] 18 [Load* : Instr] 19 [Store*AB : Instr] 20 [Store*B : Instr] 21 [Add* : Instr] 22 [Load : Instr] 23 [Store : Instr] 24 [Add : Instr] 25 26 [init : (→ Prog Machine)] 27 [halted? : (→ Machine Bool)] 28 [mem≈ : (→ Machine Machine Bool)] 29 30 [program : (→ Int (List Instr) Prog)] 31 32 [verify-EENI* : (→ (→ Prog Machine) 33 (→ Machine Bool) 34 (→ Machine Machine Bool) 35 Prog Bool 36 Witness)] 37 [EENI-witness? : (→ Witness Bool)])) 38 39 #;(define-typed-syntax program 40 [(_ n procs) ≫ 41 [⊢ [n ≫ n- ⇐ : Int]] 42 [⊢ [procs ≫ procs- ⇐ : (List Instr)]] 43 -------- 44 [⊢ [_ ≫ (ifc:program n- procs-) ⇒ : Prog]]]) 45