Created
September 19, 2023 00:11
-
-
Save camoy/a4003ab7b837024d077a709b387bce44 to your computer and use it in GitHub Desktop.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#lang effect/racket | |
;; | |
;; require | |
;; | |
(unsafe-require "aux.rkt") | |
;; | |
;; 0 (introduction) | |
;; | |
;; * How did I get into effects? (flip) | |
;; * Studying contracts for protocols across API surface. | |
;; e.g. Unix I/O | |
;; But also across time | |
;; e.g. monotonicity | |
;; * Need effects, in particular state. | |
;; * Related work for that paper found tons of other examples (flip) | |
;; e.g. affine contracts (used in "gradual" typing) (flip) | |
;; * Found a bunch of other stuff (flip) | |
;; * Problems with this existing work from practical and theoretical perspective | |
;; * Practical: High-level API and low-level API to Racket's contract system | |
;; all of these require dropping down to the low level | |
;; * Theoretical: Important property should satisfy: erasure. Must prove for | |
;; each system on its own. (flip) | |
;; * Solution: A high-level contract form that (1) can express all these systems | |
;; and (2) for which we can prove erasure. | |
;; * Yes. Need effect handlers. | |
;; | |
;; 1 (contracts) | |
;; | |
#| | |
(define prime-maker/c | |
(-> (values prime? prime?))) | |
(define key-maker/c | |
(-> (values public-key? private-key?))) | |
(define/contract rsa | |
(-> prime-maker/c key-maker/c) | |
unsafe-rsa) | |
;; OK | |
;; ((rsa (λ () (values 11 19)))) | |
;; BAD | |
;; ((rsa (λ () (values 3 4)))) | |
|# | |
;; | |
;; 2 (main-effect handlers) | |
;; | |
(effect random ()) | |
(define (random-service seed) | |
(random-handler (seed->random-state seed))) | |
(define (random-handler state) | |
(handler | |
[(random) | |
(define state* (random-state-next state)) | |
(define number (random-state->number state)) | |
(with ((random-handler state*)) | |
(continue* number))])) | |
(define (with-prng thk) | |
(with ((random-service 42)) | |
(thk))) | |
#| | |
(with-prng | |
(λ () | |
(list (random) (random) (random)))) | |
|# | |
;; | |
;; 3 (main-effect contracts) | |
;; | |
#| | |
(define prime-maker/c | |
(and/c (-> (values prime? prime?)) | |
(->e random? (between/c 0 1)))) | |
(define key-maker/c | |
(-> (values public-key? private-key?))) | |
(define/contract rsa | |
(-> prime-maker/c key-maker/c) | |
unsafe-rsa) | |
(define (random-prime) | |
(define LOW 10000) | |
(define HIGH 50000) | |
(let go () | |
(define n (exact-ceiling (+ (* (random) (- HIGH LOW)) LOW))) | |
(if (prime? n) n (go)))) | |
;; OK | |
;; (with-prng | |
;; (λ () | |
;; ((rsa (λ () | |
;; (define p (random-prime)) | |
;; (define q (random-prime)) | |
;; (values p q)))))) | |
;; BAD | |
;; (with-prng | |
;; (λ () | |
;; ((rsa (λ () | |
;; (define p (random-prime)) | |
;; (define q (random-prime)) | |
;; (displayln p) | |
;; (values p q)))))) | |
|# | |
;; | |
;; 4 (contract-effect handlers) | |
;; | |
#| | |
(effect contract-box (default)) | |
(effect contract-box-get (box)) | |
(effect contract-box-set! (box val)) | |
(define (contract-box-service store) | |
(contract-handler | |
[(contract-box default) | |
(define-values (new-box new-store) | |
(store-allocate store default)) | |
(values new-box (contract-box-service new-store))] | |
[(contract-box-get b) | |
(values (store-ref store b) (contract-box-service store))] | |
[(contract-box-set! b v) | |
(values (void) (contract-box-service (store-set store b v)))])) | |
;; | |
(with ((contract-box-service empty-store)) | |
(define prime-maker/c | |
(self/c | |
(λ _ | |
(define previous (contract-box #false)) | |
(define (fresh? n) | |
(begin0 | |
(not (equal? n (contract-box-get previous))) | |
(contract-box-set! previous n))) | |
(and/c (-> (values prime? prime?)) | |
(->e random? (and/c fresh? (between/c 0 1))))))) | |
(define key-maker/c | |
(-> (values public-key? private-key?))) | |
(define/contract rsa | |
(-> prime-maker/c key-maker/c) | |
unsafe-rsa) | |
(define (random-prime) | |
(define LOW 10000) | |
(define HIGH 50000) | |
(let go () | |
(define n (exact-ceiling (+ (* (random) (- HIGH LOW)) LOW))) | |
(if (prime? n) n (go)))) | |
(define faulty-random-service | |
(handler | |
[(random) (continue 0.5)])) | |
(define (with-faulty-prng thk) | |
(with (faulty-random-service) | |
(thk))) | |
;; OK | |
;; (with-prng | |
;; (λ () | |
;; ((rsa (λ () | |
;; (define p (random-prime)) | |
;; (define q (random-prime)) | |
;; (values p q)))))) | |
;; BAD | |
;; (with-faulty-prng | |
;; (λ () | |
;; ((rsa (λ () | |
;; (define p (random-prime)) | |
;; (define q (random-prime)) | |
;; (values p q)))))) | |
) | |
|# | |
;; | |
;; 5 (contract-handler contract) | |
;; | |
#| | |
(effect secure? ()) | |
(define (secure?-service b) | |
(contract-handler | |
[(secure?) | |
(values b (secure?-service b))])) | |
(define secure-random-service | |
(handler | |
[(random) | |
(continue | |
(exact->inexact | |
(/ (integer-bytes->integer (crypto-random-bytes 8) #f) | |
(integer-bytes->integer (make-bytes 8 255) #f))))])) | |
(define/contract (with-secure-prng thk) | |
(-> (contract-handler/c (secure?-service #t)) any) | |
(with (secure-random-service) | |
(thk))) | |
(define/contract (with-prng thk) | |
(-> (contract-handler/c (secure?-service #f)) any) | |
(with ((random-service 42)) | |
(thk))) | |
;; | |
(define (secure-context/c _) | |
(secure?)) | |
(define prime-maker/c | |
(and/c (-> (values prime? prime?)) | |
(->e (and/c random? secure-context/c) | |
(between/c 0 1)))) | |
(define key-maker/c | |
(-> (values public-key? private-key?))) | |
(define/contract rsa | |
(-> prime-maker/c key-maker/c) | |
unsafe-rsa) | |
(define (random-prime) | |
(define LOW 10000) | |
(define HIGH 50000) | |
(let go () | |
(define n (exact-ceiling (+ (* (random) (- HIGH LOW)) LOW))) | |
(if (prime? n) n (go)))) | |
;; OK | |
;; (with-secure-prng | |
;; (λ () | |
;; ((rsa (λ () | |
;; (define p (random-prime)) | |
;; (define q (random-prime)) | |
;; (values p q)))))) | |
;; BAD | |
;; (with-prng | |
;; (λ () | |
;; ((rsa (λ () | |
;; (define p (random-prime)) | |
;; (define q (random-prime)) | |
;; (values p q)))))) | |
|# |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment