#lang scheme

(require redex/reduction-semantics)
(require "grammar.ss")

(define (bytecode-ok? e)
  (not (eq? 'invalid (car (term (verify ,e () 0 #f () () ∅))))))

(define-extended-language verification 
  bytecode
  (s (ṽ ...) invalid)
  (ṽ uninit imm box imm-nc box-nc not)
  (γ ((n ṽ) ...))
  (η (n ...))
  (f (n n (ṽ ...)) ∅)
  (m n ?))

(define-metafunction verification
  verify : e s n b γ η f -> (s γ η)
  
  ; localrefs
  [(verify (loc n) (ṽ_0 ... ṽ_n ṽ_n+1 ...) n_l #f γ η f)
   ((ṽ_0 ... ṽ_n ṽ_n+1 ...) γ η)
   (side-condition (= (length (term (ṽ_0 ...))) (term n)))
   (side-condition (memq (term ṽ_n) '(imm imm-nc)))]
  [(verify (loc n) (ṽ_0 ... ṽ_n ṽ_n+1 ...) n_l #t γ η f)
   ((ṽ_0 ... ṽ_n ṽ_n+1 ...) γ η)
   (side-condition (= (length (term (ṽ_0 ...))) (term n)))
   (side-condition (memq (term ṽ_n) '(imm imm-nc box box-nc)))]
  [(verify (loc-box n) (ṽ_0 ... ṽ_n ṽ_n+1 ...) n_l b γ η f)
   ((ṽ_0 ... ṽ_n ṽ_n+1 ...) γ η)
   (side-condition (= (length (term (ṽ_0 ...))) (term n)))
   (side-condition (memq (term ṽ_n) '(box box-nc)))]
  
  [(verify (loc-noclr n) (ṽ_0 ... ṽ_n ṽ_n+1 ...) n_l #f γ η f) 
   ((ṽ_0 ... (nc ṽ_n) ṽ_n+1 ...) γ (log-noclear n n_l η))
   (side-condition (= (length (term (ṽ_0 ...))) (term n)))
   (side-condition (memq (term ṽ_n) '(imm imm-nc)))]
  [(verify (loc-noclr n) (ṽ_0 ... ṽ_n ṽ_n+1 ...) n_l #t γ η f) 
   ((ṽ_0 ... (nc ṽ_n) ṽ_n+1 ...) γ (log-noclear n n_l η))
   (side-condition (= (length (term (ṽ_0 ...))) (term n)))
   (side-condition (memq (term ṽ_n) '(imm imm-nc box box-nc)))]
  [(verify (loc-box-noclr n) (ṽ_0 ... ṽ_n ṽ_n+1 ...) n_l b γ η f) 
   ((ṽ_0 ... box-nc ṽ_n+1 ...) γ (log-noclear n n_l η))
   (side-condition (= (length (term (ṽ_0 ...))) (term n)))
   (side-condition (memq (term ṽ_n) '(box box-nc)))]
  
  [(verify (loc-clr n) (ṽ_0 ... imm ṽ_n+1 ...) n_l #f γ η f)
   ((ṽ_0 ... not ṽ_n+1 ...) (log-clear n imm n_l γ) η)
   (side-condition (= (length (term (ṽ_0 ...))) (term n)))]
  [(verify (loc-clr n) (ṽ_0 ... ṽ_n ṽ_n+1 ...) n_l #t γ η f)
   ((ṽ_0 ... not ṽ_n+1 ...) (log-clear n ṽ_n n_l γ) η)
   (side-condition (= (length (term (ṽ_0 ...))) (term n)))
   (side-condition (memq (term ṽ_n) '(imm box)))]
  [(verify (loc-box-clr n) (ṽ_0 ... box ṽ_n+1 ...) n_l b γ η f) 
   ((ṽ_0 ... not ṽ_n+1 ...) (log-clear n box n_l γ) η)
   (side-condition (= (length (term (ṽ_0 ...))) (term n)))]
  
  ; branch
  [(verify (branch e_c e_t e_e) s n_l b γ η f)
   ; FIXME: should redo γ_2?
   ((redo-clears γ_3 (trim s_3 s)) γ_1 η_3)
   (where (s_1 γ_1 η_1) (verify e_c s n_l #f γ η ∅))
   (where (s_2 γ_2 η_2) (verify e_t (trim s_1 s) 0 b () () f))
   (where (s_3 γ_3 η_3) (verify e_e (undo-noclears η_2 (undo-clears γ_2 (trim s_2 s))) 0 b γ_2 η_1 f))]
  
  ; let-one
  [(verify (let-one e_r e_b) (ṽ_1 ...) n_l b γ η f)
   (verify e_b (imm ṽ_1* ...) ,(add1 (term n_l)) b γ η (shift 1 f))
   (where (s_1 γ_1 η_1) (verify e_r (uninit ṽ_1 ...) ,(add1 (term n_l)) #f γ η ∅))
   (side-condition (term (valid? s_1)))
   ;; MRF: the Racket implementation checks that s_1 starts with uninit
   (where (ṽ_1* ...) (trim s_1 (ṽ_1 ...)))]
  
  ; seq
  [(verify (seq e_0 ... e_n) s n_l b γ η f)
   (verify e_n s_1 n_l b γ_1 η_1 f)
   (where (s_1 γ_1 η_1) (verify* (e_0 ...) s n_l #t γ η))]
  
  ; application
  [(verify (application (name e_0 (loc-noclr n)) e_1 ...) s n_l b_i γ η (n_f n_s (ṽ ...)))
   (verify-self-app (application e_0 e_1 ...) s n_l γ η (n_f n_s (ṽ ...)))
   (side-condition (= (term n) (+ (term n_f) (length (term (e_1 ...))))))]
  [(verify (application (lam (τ_0 ...) (n_0 ...) e) e_0 ...) (name s (ṽ_0 ...)) n_l b γ η f)
   (verify*-ref (e_0 ...) (τ_0 ...) s_1 n_l* γ η)
   (where n ,(length (term (e_0 ...))))
   (where n_l* ,(+ (term n) (term n_l)))
   (where s_1 (abs-push n not s))
   (side-condition (term (verify-lam (lam (τ_0 ...) (n_0 ...) e) s_1 ?)))]
  [(verify (application (proc-const (τ_0 ...) e) e_0 ...) s n_l b γ η f)
   (verify (application (lam (τ_0 ...) () e) e_0 ...) s n_l b γ η f)]
  [(verify (application e_0 e_1 ...) (name s (ṽ_0 ...)) n_l b γ η f)
   (verify* (e_0 e_1 ...) (abs-push n not s) n_l* #f γ η)
   (where n ,(length (term (e_1 ...))))
   (where n_l* ,(+ (term n) (term n_l)))]
  
  ; let-void
  [(verify (let-void n e) (name s (ṽ_0 ...)) n_l b_i γ η f)
   (verify e (abs-push n uninit s) ,(+ (term n) (term n_l)) b_i γ η (shift n f))]
  [(verify (let-void-box n e) (name s (ṽ_0 ...)) n_l b_i γ η f)
   (verify e (abs-push n box s) ,(+ (term n) (term n_l)) b_i γ η (shift n f))]
  
  ; procedures in arbitrary context
  [(verify (lam ((name τ val) ...) (n_0 ...) e) s n_l b γ η f)
   (s γ η)
   (side-condition (term (verify-lam (lam (τ ...) (n_0 ...) e) s ?)))]
  [(verify (proc-const ((name τ val) ...) e) s n_l b γ η f)
   (verify (lam (τ ...) () e) s n_l b γ η f)]
  
  ; case-lam
  [(verify (case-lam (name l (lam (val ...) (n ...) e)) ...) s n_l b γ η f)
   (s γ η)
   (side-condition (term (AND (verify-lam l s ?) ...)))]
  
  ; literals
  [(verify number s n_l b γ η f) (s γ η)]
  [(verify b s n_l b_i γ η f) (s γ η)]
  [(verify (quote variable) s n_l b γ η f) (s γ η)]
  [(verify void s n_l b γ η f) (s γ η)]
  
  ; install-value
  [(verify (install-value n e_r e_b) s n_l b γ η f)
   (verify e_b (set imm n s_2) n_l b γ η f)
   (side-condition (< (term n) (term n_l)))
   (where (s_1 γ_1 η_1) (verify e_r s n_l #f γ η ∅))
   (where s_2 (trim s_1 s))
   (side-condition (term (valid? s_2)))
   (where uninit (stack-ref n s_2))]
  [(verify (install-value-box n e_r e_b) (name s (ṽ_0 ...)) n_l b γ η f)
   (verify e_b s_2 n_l b γ_1 η_1 f)
   (side-condition (< (term n) (length (term s))))
   (where (s_1 γ_1 η_1) (verify e_r s n_l #f γ η ∅))
   (where s_2 (trim s_1 s))
   (side-condition (term (valid? s_2)))
   (side-condition (memq (term (stack-ref n s_2)) '(box box-nc)))]
  
  ; boxenv
  [(verify (boxenv n_p e) (ṽ_0 ... imm ṽ_n+1 ...) n_l b γ η f)
   (verify e (ṽ_0 ... box ṽ_n+1 ...) n_l b γ η f)
   (side-condition (= (length (term (ṽ_0 ...))) (term n_p)))
   (side-condition (< (term n_p) (term n_l)))]
  
  ; let-rec
  [(verify (let-rec ((name l (lam ((name v val) ...) (n_0 ...) e_0)) ...) e) (ṽ_0 ... ṽ_n ...) n_l b γ η f)
   (verify e s_1 n_l b γ η f)
   (where n ,(length (term (l ...))))
   (side-condition (= (length (term (ṽ_0 ...))) (term n)))
   (side-condition (term (AND (same? ṽ_0 uninit) ...)))
   (side-condition (<= (term n) (term n_l)))
   (where s_1 (abs-push n imm (ṽ_n ...)))
   (where (n_i ...) (count-up ,(length (term (l ...)))))
   (side-condition (term (AND (verify-lam l s_1 n_i) ...)))]
  
  ; indirect
  [(verify (indirect x) s n_l b γ η f) (s γ η)]
  
  ; else
  [(verify e s n_l b γ η f) (invalid γ η)])

(define-metafunction verification
  verify* : (e ...) s n_l b γ η -> (s γ η)
  [(verify* () s n_l b γ η) (s γ η)]
  [(verify* (e_0 e_1 ...) s n_l b γ η)
   (verify* (e_1 ...) (trim s_1 s) n_l b γ_1 η_1)
   (where (s_1 γ_1 η_1) (verify e_0 s n_l b γ η ∅))])

(define-metafunction verification
  verify*-ref : (e ...) (τ ...) s n_l γ η -> (s γ η)
  [(verify*-ref () () s n_l γ η) (s γ η)]
  [(verify*-ref (e_0 e_1 ...) (val τ_1 ...) s n_l γ η)
   (verify*-ref (e_1 ...) (τ_1 ...) (trim s_1 s) n_l γ_1 η_1)
   (where (s_1 γ_1 η_1) (verify e_0 s n_l #f γ η ∅))]
  [(verify*-ref (e_0 e_1 ...) () s n_l γ η)
   (verify* (e_0 e_1 ...) s n_l #f γ η)]
  [(verify*-ref () (τ_0 τ_1 ...) s n_l γ η) (s γ η)]
  [(verify*-ref ((loc n) e_1 ...) (ref τ_1 ...) s n_l γ η)
   (verify*-ref (e_1 ...) (τ_1 ...) s_1 n_l γ_1 η_1)
   ; Require the reference to load a box.
   (where (s_1 γ_1 η_1) (verify (loc-box n) s n_l #f γ η ∅))]
  [(verify*-ref ((loc-noclr n) e_1 ...) (ref τ_1 ...) s n_l γ η)
   (verify*-ref (e_1 ...) (τ_1 ...) s_1 n_l γ_1 η_1)
   ; Require the reference to load a box.
   (where (s_1 γ_1 η_1) (verify (loc-box-noclr n) s n_l #f γ η ∅))]
  [(verify*-ref ((loc-clr n) e_1 ...) (ref τ_1 ...) s n_l γ η)
   (verify*-ref (e_1 ...) (τ_1 ...) s_1 n_l γ_1 η_1)
   ; Require the reference to load a box.
   (where (s_1 γ_1 η_1) (verify (loc-box-clr n) s n_l #f γ η ∅))]
  [(verify*-ref (e ...) (τ ...) s n_l γ η) (invalid γ η)])

(define-metafunction verification
  [(verify-lam (lam (τ_0 ...) (n_0 ...) e) (name s (ṽ_0 ...)) m)
   (valid? s_1)
   (where n_d ,(length (term s)))
   (where n_d* ,(+ (length (term (τ_0 ...))) (length (term (n_0 ...)))))
   (side-condition (term (AND (less-than? n_0 n_d) ...)))
   (side-condition (term (AND (not-member? (stack-ref n_0 s) (uninit not)) ...)))
   (where (ṽ ...) ((drop-noclear (stack-ref n_0 s)) ...))
   (where f (extract-self m (n_0 ...) (τ_0 ...) (ṽ ...)))
   (where (s_1 γ_1 η_1) (verify e (ṽ ... (arg τ_0) ...) n_d* #f () () f))]
  [(verify-lam any s m) #f])

(define-metafunction verification
  [(extract-self ? (n_0 ...) (τ_0 ...) (ṽ_0 ...)) ∅]
  [(extract-self n_i (n_0 ... n_i n_i+1 ...) (τ_0 ...) (ṽ_0 ...))
   (,(length (term (n_0 ...))) ,(length (term (τ_0 ...))) (ṽ_0 ...))
   ; When a closure captures itself multiple times, only the last 
   ; occurrence is considered a self-reference.
   (side-condition (term (not-member? n_i (n_i+1 ...))))]
  [(extract-self n (n_0 ...) (τ_0 ...) (ṽ_0 ...)) ∅])

(define-metafunction verification
  drop-noclear : ṽ -> ṽ
  [(drop-noclear imm-nc) imm]
  [(drop-noclear box-nc) box]
  [(drop-noclear ṽ) ṽ])

(define-metafunction verification
  [(verify-self-app (application e_0 e_1 ...) (name s (ṽ_0 ...)) n_l γ η (n_f n_s (ṽ_j ...)))
   (s_1 γ_1 η_1)
   (where n ,(length (term (e_1 ...))))
   (where n_l* ,(+ (term n) (term n_l)))
   (where (s_1 γ_1 η_1) (verify* (e_0 e_1 ...) (abs-push n not s) n_l* #f γ η))
   (side-condition (term (valid? s_1)))
   (where (n_j ...) (count-up ,(length (term (ṽ_j ...)))))
   (side-condition (term (closure-intact? ((stack-ref (plus n_j n_s) s_1) ...) (ṽ_j ...))))]
  [(verify-self-app e s n_l γ η f) (invalid γ η)])

(define-metafunction verification
  closure-intact? : (ṽ ...) (ṽ ...) -> b 
  [(closure-intact? () ()) #t]
  [(closure-intact? (imm-nc ṽ_1 ...) (imm ṽ_2 ...))
   (closure-intact? (ṽ_1 ...) (ṽ_2 ...))]
  [(closure-intact? (box-nc ṽ_1 ...) (box ṽ_2 ...))
   (closure-intact? (ṽ_1 ...) (ṽ_2 ...))]
  [(closure-intact? (ṽ ṽ_1 ...) (ṽ ṽ_2 ...))
   (closure-intact? (ṽ_1 ...) (ṽ_2 ...))]
  [(closure-intact? (ṽ_1 ...) (ṽ_2 ...)) #f])

(define-metafunction verification
  shift : n f -> f
  [(shift n ∅) ∅]
  [(shift n (n_f n_s (ṽ ...))) 
   (,(+ (term n) (term n_f)) ,(+ (term n) (term n_s)) (ṽ ...))])

(define-metafunction verification
  arg : τ -> ṽ
  [(arg val) imm]
  [(arg ref) box])

(define-metafunction verification
  abs-push : n ṽ (ṽ ...) -> s
  [(abs-push 0 ṽ (ṽ_0 ...)) (ṽ_0 ...)]
  [(abs-push n ṽ (ṽ_0 ...))
   (abs-push ,(sub1 (term n)) ṽ (ṽ ṽ_0 ...))])

(define-metafunction verification
  stack-ref : n (ṽ ...) -> ṽ
  [(stack-ref n (ṽ_0 ... ṽ_n ṽ_n+1 ...))
   ṽ_n
   (side-condition (= (length (term (ṽ_0 ...))) (term n)))])

(define-metafunction verification
  set : ṽ n (ṽ ...) -> (ṽ ...)
  [(set ṽ n (ṽ_0 ... ṽ_n ṽ_n+1 ...))
   (ṽ_0 ... ṽ ṽ_n+1 ...)
   (side-condition (= (length (term (ṽ_0 ...))) (term n)))])

(define-metafunction verification
  nc : ṽ -> ṽ
  [(nc imm) imm-nc]
  [(nc imm-nc) imm-nc]
  [(nc box) box-nc]
  [(nc box-nc) box-nc])

(define-metafunction verification
  log-noclear : n n η -> η
  [(log-noclear n_p n_l (n_0 ...))
   (,(- (term n_p) (term n_l)) n_0 ...)
   (side-condition (>= (term n_p) (term n_l)))]
  [(log-noclear n_p n_l η) η])

(define-metafunction verification
  undo-noclears : η s -> s
  [(undo-noclears η invalid) invalid]
  [(undo-noclears () s) s]
  [(undo-noclears (n_0 n_1 ...) (ṽ_0 ... imm-nc ṽ_i ...))
   (undo-noclears (n_1 ...) (ṽ_0 ... imm ṽ_i ...))
   (side-condition (= (length (term (ṽ_0 ...))) (term n_0)))]
  [(undo-noclears (n_0 n_1 ...) (ṽ_0 ... box-nc ṽ_i ...))
   (undo-noclears (n_1 ...) (ṽ_0 ... box ṽ_i ...))
   (side-condition (= (length (term (ṽ_0 ...))) (term n_0)))]
  [(undo-noclears (n_0 n_1 ...) s)
   (undo-noclears (n_1 ...) s)])

(define-metafunction verification
  log-clear : n ṽ n γ -> γ
  [(log-clear n_p ṽ n_l ((n_0 ṽ_0) ...))
   ((,(- (term n_p) (term n_l)) ṽ) (n_0 ṽ_0) ...)
   (side-condition (>= (term n_p) (term n_l)))]
  [(log-clear n_p ṽ n_l γ) γ])

(define-metafunction verification
  undo-clears : γ s -> s
  [(undo-clears γ invalid) invalid]
  [(undo-clears () s) s]
  [(undo-clears ((n_0 ṽ_0) (n_1 ṽ_1) ...) s)
   (undo-clears ((n_1 ṽ_1) ...) (set ṽ_0 n_0 s))])

(define-metafunction verification
  redo-clears : γ s -> s
  [(redo-clears γ invalid) invalid]
  [(redo-clears () s) s]
  [(redo-clears ((n_0 ṽ_0) (n_1 ṽ_1) ...) s) 
   (redo-clears ((n_1 ṽ_1) ...) (set uninit n_0 s))])

(define-metafunction verification
  trim : s s -> s
  [(trim invalid s) invalid]
  [(trim (ṽ_f ...) (ṽ_t ...))
   ,(take-right (term (ṽ_f ...)) 
                (length (term (ṽ_t ...))))])

(define-metafunction verification
  [(valid? invalid) #f]
  [(valid? (ṽ ...)) #t])


;; Typsetting tricks:

(define-metafunction verification
  [(AND) #t]
  [(AND #t any_1 ...) (AND any_1 ...)]
  [(AND any_0 any_1 ...) #f])

(define-metafunction verification
  [(same? any_1 any_1) #t]
  [(same? any_1 any_2) #f])

(define-metafunction verification
  [(less-than? n_1 n_2) ,(< (term n_1) (term n_2))])

(define-metafunction verification
  [(plus n_1 n_2) ,(+ (term n_1) (term n_2))])

(define-metafunction verification
  [(not-member? any_1 (any_2 ...))
   ,(not (member (term any_1) (term (any_2 ...))))])

;; Shouldn't have copied from "reduction.ss":
(define-metafunction bytecode
  [(count-up number)
   ,(build-list (term number) (λ (x) x))])

(provide (all-defined-out))