From 2ba4e97fa125227b74145679f1a33bab82e606b9 Mon Sep 17 00:00:00 2001
From: Burke Fetscher <bfetscher@racket-lang.org>
Date: Tue, 7 Oct 2014 17:42:57 -0500
Subject: [PATCH] redex: add typed generators to the benchmark

- change delim-cont to generate a store as well
- add version of rvm that works with #:satisfying
- add version of list-machine that works with #:satisfying
- new rewrites for the above
- infrastructure to wire all of this together
---
 .../models/delim-cont/delim-cont.rkt          |  50 +-
 .../models/delim-cont/generators.rkt          |  30 +-
 .../models/delim-cont/typed-info.rkt          |  14 +
 .../models/list-machine/generators.rkt        |  50 +-
 .../models/list-machine/list-machine-1.rkt    |  26 +-
 .../models/list-machine/list-machine-2.rkt    |   3 +-
 .../models/list-machine/list-machine-3.rkt    |   3 +-
 .../models/list-machine/ls-typed-gen.rkt      | 429 ++++++++++
 .../models/list-machine/typed-info.rkt        |  14 +
 .../benchmark/models/poly-stlc/generators.rkt |  12 +-
 .../benchmark/models/poly-stlc/typed-info.rkt |  14 +
 .../benchmark/models/rbtrees/generators.rkt   |  10 +
 .../benchmark/models/rbtrees/typed-info.rkt   |  14 +
 .../redex/benchmark/models/rvm/generators.rkt |  15 +
 .../benchmark/models/rvm/jdg-grammar.rkt      |  43 +
 .../redex/benchmark/models/rvm/rvm-14.rkt     |  34 +
 .../redex/benchmark/models/rvm/rvm-15.rkt     |  14 +
 .../redex/benchmark/models/rvm/rvm-2.rkt      |  13 +
 .../redex/benchmark/models/rvm/rvm-3.rkt      |  10 +-
 .../redex/benchmark/models/rvm/rvm-4.rkt      |  14 +
 .../redex/benchmark/models/rvm/rvm-5.rkt      |  15 +-
 .../redex/benchmark/models/rvm/rvm-6.rkt      |  10 +
 .../redex/benchmark/models/rvm/typed-info.rkt |  14 +
 .../redex/benchmark/models/rvm/util.rkt       |   8 +-
 .../redex/benchmark/models/rvm/verif-jdg.rkt  | 754 ++++++++++++++++++
 .../models/stlc+lists/generators.rkt          |  12 +-
 .../models/stlc+lists/typed-info.rkt          |  14 +
 .../models/stlc-subst/generators.rkt          |  12 +-
 .../models/stlc-subst/typed-info.rkt          |  14 +
 .../redex/benchmark/models/type-all-info.rkt  |  25 +
 .../redex/benchmark/models/util/info-util.rkt |   6 +-
 .../redex-doc/redex/scribblings/ref.scrbl     |   2 +-
 32 files changed, 1634 insertions(+), 64 deletions(-)
 create mode 100644 pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/delim-cont/typed-info.rkt
 create mode 100644 pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/list-machine/ls-typed-gen.rkt
 create mode 100644 pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/list-machine/typed-info.rkt
 create mode 100644 pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/poly-stlc/typed-info.rkt
 create mode 100644 pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/rbtrees/typed-info.rkt
 create mode 100644 pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/rvm/jdg-grammar.rkt
 create mode 100644 pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/rvm/typed-info.rkt
 create mode 100644 pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/rvm/verif-jdg.rkt
 create mode 100644 pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/stlc+lists/typed-info.rkt
 create mode 100644 pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/stlc-subst/typed-info.rkt
 create mode 100644 pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/type-all-info.rkt

diff --git a/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/delim-cont/delim-cont.rkt b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/delim-cont/delim-cont.rkt
index 696f721a1c..e2f46ed101 100644
--- a/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/delim-cont/delim-cont.rkt
+++ b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/delim-cont/delim-cont.rkt
@@ -38,7 +38,8 @@
      (Mark t) (List t))
   (B Num Bool Unit)
 
-  (x variable-not-otherwise-mentioned)
+  ;(x variable-not-otherwise-mentioned)
+  (x (variable-prefix var:))
 
   (b n s bool unit)
   (n number)
@@ -188,8 +189,11 @@
    (--> (monitor (-> ctc_a ctc_r) (name v (λ (x : t) e)) k l j)
         (λ (x_1 : t)
            ((λ (x_2 : t) (monitor ctc_r (v x_2) k l j))
-            (monitor ctc_a x_1 l k j))))
-
+            (monitor ctc_a x_1 l k j)))
+        ;;added this (10/7/14):
+        (where/hidden (x_1 x_2) 
+                      ,(variables-not-in (term (ctc_a ctc_r v))
+                                         '(var: var:))))
    ;; prompt-tag/c
    (--> (monitor (prompt-tag/c ctc_1 ctc_2 t_1 t_2) v_p k l j)
         (PG ctc_1 ctc_2 v_p k l j))
@@ -822,15 +826,17 @@
 
 
 
+
 (define (random-exp depth)
   (match
       (generate-term
        abort+Γ-lang
        #:satisfying
-       (tc · · e t)
+       (tc · Σ e t)
        depth)
     [#f #f]
-    [`(tc · · ,e ,t) e]))
+    [`(tc · ,Σ ,e ,t) 
+     (list Σ e)]))
 
 (define (eval-random-exps n [depth 4])
   (for ([_ n])
@@ -877,19 +883,19 @@
   (or (redex-match abort-lang (in-hole E (seq (update mk e_1) e_2)) exp)
       (redex-match abort-lang (in-hole E (check e v l_1 l_2)) exp)))
 
-(define (soundness-holds? e)
-  (define t (judgment-holds (tc · · ,e t) t))
+(define (soundness-holds? e [inp-Σ '·])
+  (define t (judgment-holds (tc · ,inp-Σ ,e t) t))
   (define exceeded-max-steps #f)
   (define steps 0)
   (or (not t)
       (match (apply-reduction-relation* 
-              abort-red `(<> ,e ·)
+              abort-red `(<> ,e ,inp-Σ)
               #:stop-when
               (λ (_)
                 (set! steps (add1 steps))
-                ;; treat 20 steps as non-terminating
+                ;; treat 40 steps as non-terminating
                 ;; larger examples tend to be useless...
-                (and (steps . > . 20)
+                (and (steps . > . 40)
                      (set! exceeded-max-steps #t))))
         ['() #t] ;; looping reduction graph
         [`((<> ,e* ,st*))
@@ -901,16 +907,22 @@
                       (equal? (judgment-holds (tc · ,st* ,e* t) t)
                               t))))]
         [_
-         (error 'soundness "multiple reductions found for ~s" e)])))
+         (if exceeded-max-steps
+             #t
+             (error 'soundness "multiple reductions found for ~s" e))])))
 
-(define (check-random-exps n [depth 4])
-  (for ([_ n])
+(define (check-random-exps n [depth 4] #:verbose [verbose? #f])
+  (for/and ([_ n])
     (define e (random-exp depth))
-    (when e
-      (pretty-write e)
-      (unless (soundness-holds? e)
-        (error 'check "soundness failed for: ~s" e)))))
+    (or (not e)
+        (match-let* ([(list s e) e]
+                     [ok? (soundness-holds? e s)])
+          (when verbose?
+            (pretty-write e))
+          (unless ok?
+            (error 'check "soundness failed for: ~s\n~s" s e))
+          ok?))))
 
-(define (type-check e)
-  (judgment-holds (tc · · ,e t)))
+(define (type-check e Σ)
+  (judgment-holds (tc · ,Σ ,e t)))
 
diff --git a/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/delim-cont/generators.rkt b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/delim-cont/generators.rkt
index 0ca7b2b640..08dde678a2 100644
--- a/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/delim-cont/generators.rkt
+++ b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/delim-cont/generators.rkt
@@ -3,7 +3,8 @@
 (require (except-in redex/benchmark/models/delim-cont/delim-cont let)
          (only-in redex/private/generate-term pick-an-index)
          redex/reduction-semantics
-         racket/bool)
+         racket/bool
+         racket/match)
 
 (provide (all-defined-out))
 
@@ -12,14 +13,14 @@
   (define (get-generator) generate)
   (define type 'grammar)
   (define (generate)
-    (generate-term abort-lang e 4)))
+    (generate-term abort+Γ-lang (<> e Σ) 4)))
 
 (module+ enum-mod
   (provide generate get-generator type)
   (define (get-generator) generate)
   (define type 'enum)
   (define (generate [p-value 0.125])
-    (generate-term abort-lang e #:i-th (pick-an-index p-value))))
+    (generate-term abort+Γ-lang (<> e Σ) #:i-th (pick-an-index p-value))))
 
 (module+ ordered-mod
   (provide generate get-generator type)
@@ -30,12 +31,27 @@
               (set! index (add1 index))))))
   (define type 'ordered)
   (define (generate [index 0])
-    (generate-term abort-lang e #:i-th index)))
+    (generate-term abort+Γ-lang (<> e Σ)  #:i-th index)))
+
+(module+ typed-mod
+  (provide generate get-generator type)
+  (define (get-generator) generate)
+  (define type 'search)
+  (define (generate)
+    (match (generate-term
+            abort+Γ-lang
+            #:satisfying
+            (tc · Σ e t)
+            4)
+      [`(tc ,_ ,Σ ,e ,_) `(<> ,e ,Σ)]
+      [#f #f])))
 
 (module+ check-mod
   (provide check)
   (define (check term)
-  (or (not term)
-      (implies (type-check term)
-               (soundness-holds? term)))))
+    (or (not term)
+        (match term
+          [`(<> ,e ,Σ)
+           (implies (type-check e Σ)
+                    (soundness-holds? e Σ))]))))
 
diff --git a/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/delim-cont/typed-info.rkt b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/delim-cont/typed-info.rkt
new file mode 100644
index 0000000000..3be674c381
--- /dev/null
+++ b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/delim-cont/typed-info.rkt
@@ -0,0 +1,14 @@
+#lang racket/base
+
+(require racket/runtime-path
+         "../util/info-util.rkt")
+
+(provide (all-defined-out))
+
+(define name "delim-cont")
+(define fname (make-path-root 'delim-cont))
+
+(define-runtime-path here ".")
+
+(define (all-mods)
+  (all-mods/type 'typed here name fname))
\ No newline at end of file
diff --git a/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/list-machine/generators.rkt b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/list-machine/generators.rkt
index e58ff531ee..067c2cbd25 100644
--- a/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/list-machine/generators.rkt
+++ b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/list-machine/generators.rkt
@@ -2,6 +2,7 @@
 
 (require redex/examples/list-machine/list-machine
          redex/examples/list-machine/list-machine-typing
+         (prefix-in typed: redex/benchmark/models/list-machine/ls-typed-gen)
          (only-in redex/private/generate-term pick-an-index)
          redex/reduction-semantics
          racket/bool
@@ -15,14 +16,14 @@
   (define (get-generator) generate)
   (define type 'grammar)
   (define (generate)
-    (generate-term list-machine-typing (l0 : ι p) 7)))
+    (generate-term list-machine-typing ((l0 : ι p) Π) 7)))
 
 (module+ enum-mod
   (provide generate get-generator type)
   (define (get-generator) generate)
   (define type 'enum)
   (define (generate [p-value 0.5])
-    (generate-term list-machine-typing (l0 : ι p) #:i-th (pick-an-index p-value))))
+    (generate-term list-machine-typing ((l0 : ι p) Π) #:i-th (pick-an-index p-value))))
 
 (module+ ordered-mod
   (provide generate get-generator type)
@@ -33,10 +34,23 @@
               (set! index (add1 index))))))
   (define type 'ordered)
   (define (generate [index 0])
-    (generate-term list-machine-typing (l0 : ι p) #:i-th index)))
+    (generate-term list-machine-typing ((l0 : ι p) Π) #:i-th index)))
+
+(module+ typed-mod
+  (provide generate get-generator type)
+  (define (get-generator) generate)
+  (define type 'search)
+  (define (generate)
+    (match (generate-term typed:list-machine-typing
+                          #:satisfying
+                          (typed:check-program (l0 : ι p) Π)
+                          7)
+      [`(typed:check-program ,p ,Π)
+       `(,p ,Π)]
+      [#f #f])))
 
 (module+ check-mod
-  (provide check)
+  (provide check type-check check-progress)
   
   (define (check-progress p)
     (define r_0 (term (empty v0 ↦ nil)))
@@ -64,23 +78,13 @@
                     (match (car closure)
                       [`(,p ,r ,ι)
                        (equal? ι 'halt)])))))))
-  
-  ;; TODO : change this to generate the program and type as a pair, (as the typed 
-  ;; generator does), so we are testing the different strategies fairly?
-  (define (type-check p)
-    ;; need to provide a program typing, so generate 10 randomly and
-    ;; see if any succeed...
-    ;; (succeeds more often than one might assume)
-    (let loop ([i 0])
-      (cond
-        [(i . > . 10) #f]
-        [else
-         (define guess-Π (generate-term list-machine-typing (l0 : (v0 : nil empty) Π) 7))
-         (or (and (judgment-holds (check-program ,p ,guess-Π))
-                  guess-Π)
-             (loop (add1 i)))])))
-  
-  (define (check p)
-    (or (not p)
-        (implies (type-check p) (check-progress p)))))
+
+  (define (type-check p Π)
+    (judgment-holds (check-program ,p ,Π)))
+  
+  (define (check pΠ)
+    (or (not pΠ)
+        (match pΠ
+          [`(,p ,Π)
+           (implies (type-check p Π) (check-progress p))]))))
 
diff --git a/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/list-machine/list-machine-1.rkt b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/list-machine/list-machine-1.rkt
index f33631e21a..2758d26ec4 100644
--- a/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/list-machine/list-machine-1.rkt
+++ b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/list-machine/list-machine-1.rkt
@@ -22,6 +22,19 @@
   #:variables (rest)
   #:exactly-once)
 
+(define-rewrite bug1-typed
+  ((:lookup-Γ Γ v_0 τ_0) 
+   (:lookup-Γ Γ v_1 τ_1)
+   . rest)
+  ==> 
+  ((:lookup-Γ Γ v_0 τ_0) 
+   (:lookup-Γ Γ v_0 τ_1)
+   . rest)
+  #:context (define-judgment-form)
+  #:variables (rest)
+  #:exactly-once)
+
+
 (define-rewrite return-stopped-rw
   (let ([closure (apply-reduction-relation* 
                          red
@@ -62,9 +75,18 @@
 
 (include/rewrite (lib "redex/examples/list-machine/list-machine-typing.rkt") list-machine-typing bug1)
 
-(include/rewrite "generators.rkt" generators bug-mod-rw return-stopped-rw)
+(include/rewrite (lib "redex/benchmark/models/list-machine/ls-typed-gen.rkt") ls-typed-gen bug1-typed)
+
+(define-rewrite bug-mod3
+  redex/benchmark/list-machine/ls-typed-gen
+  ==>
+  (submod ".." ls-typed-gen)
+  #:context (require))
+
+(include/rewrite "generators.rkt" generators bug-mod-rw return-stopped-rw bug-mod3)
 
 (define small-counter-example
-  (term (l0 : (begin (cons v0 Z v0) halt) end)))
+  (term ((l0 : (begin (cons v0 Z v0) halt) end)
+         (l0 : (v0 : nil empty) empty))))
 
 (test small-counter-example)
diff --git a/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/list-machine/list-machine-2.rkt b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/list-machine/list-machine-2.rkt
index 0ff19f9e1d..8f7dbd8535 100644
--- a/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/list-machine/list-machine-2.rkt
+++ b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/list-machine/list-machine-2.rkt
@@ -67,6 +67,7 @@
 (include/rewrite "generators.rkt" generators bug-mod-rw stop-earlier-rw)
 
 (define small-counter-example
-  (term (l0 : (begin (cons v0 v0 v0) halt) end)))
+  (term ((l0 : (begin (cons v0 v0 v0) halt) end)
+          (l0 : (v0 : nil empty) empty))))
 
 (test small-counter-example)
diff --git a/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/list-machine/list-machine-3.rkt b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/list-machine/list-machine-3.rkt
index c4feb524db..c85f17594b 100644
--- a/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/list-machine/list-machine-3.rkt
+++ b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/list-machine/list-machine-3.rkt
@@ -29,6 +29,7 @@
 (include/rewrite "generators.rkt" generators bug-mod-rw)
 
 (define small-counter-example
-  (term (l0 : (begin (cons v0 v0 v0) (begin (fetch-field v0 1 v0) halt)) end)))
+  (term ((l0 : (begin (cons v0 v0 v0) (begin (fetch-field v0 1 v0) halt)) end)
+         (l0 : (v0 : nil empty) empty))))
 
 (test small-counter-example)
diff --git a/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/list-machine/ls-typed-gen.rkt b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/list-machine/ls-typed-gen.rkt
new file mode 100644
index 0000000000..5adfd5d7e6
--- /dev/null
+++ b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/list-machine/ls-typed-gen.rkt
@@ -0,0 +1,429 @@
+#lang racket
+
+(define the-error "no error")
+
+(require redex/reduction-semantics
+         racket/list
+         racket/match)
+
+(provide (all-defined-out))
+
+(define-language list-machine
+  (a nil
+     (cons a a))
+  (v variable-not-otherwise-mentioned)
+  (r empty
+     (r v ↦ a))
+  (l variable-not-otherwise-mentioned)
+  (ι (jump l)
+     (branch-if-nil v l)
+     (fetch-field v 0 v)
+     (fetch-field v 1 v)
+     (cons v v v)
+     halt
+     (begin ι ι))
+  (p (l : ι p)
+     end))
+
+(define-judgment-form list-machine
+  #:contract (var-lookup r v a)
+  #:mode (var-lookup I I O)
+  [-----
+   (var-lookup (r v ↦ a) v a)]
+  [(where #t (different v_1 v_2))
+   (var-lookup r v_2 a_2)
+   -----
+   (var-lookup (r v_1 ↦ a_1) v_2 a_2)])
+
+(define-judgment-form list-machine
+  #:contract (var-set r v a r)
+  #:mode (var-set I I I O)
+  [-----
+   (var-set (r v ↦ a) v a_2 (r v ↦ a_2))]
+  [(where #t (different v v_2))
+   (var-set r v_2 a_2 r_2)
+   -----
+   (var-set (r v ↦ a) v_2 a_2 (r_2 v ↦ a))]
+  [-----
+   (var-set empty v a (empty v ↦ a))])
+
+(define-judgment-form list-machine
+  #:contract (program-lookup p l ι)
+  #:mode (program-lookup I I O)
+  [-----
+   (program-lookup (l : ι p) l ι)]
+  [(where #t (different l l_2))
+   (program-lookup p l_2 ι_2)
+   -----
+   (program-lookup (l : ι p) l_2 ι_2)])
+
+(define red 
+  (reduction-relation 
+   list-machine
+   #:domain (p r ι)
+   (--> (p r (begin (begin ι_1 ι_2) ι_3))
+        (p r (begin ι_1 (begin ι_2 ι_3)))
+        "step-seq")
+   (--> (p r (begin (fetch-field v 0 v_2) ι))
+        (p r_2 ι)
+        "step-fetch-field-0"
+        (judgment-holds (var-lookup r v (cons a_0 a_1)))
+        (judgment-holds (var-set r v_2 a_0 r_2)))
+   (--> (p r (begin (fetch-field v 1 v_2) ι))
+        (p r_2 ι)
+        "step-fetch-field-1"
+        (judgment-holds (var-lookup r v (cons a_0 a_1)))
+        (judgment-holds (var-set r v_2 a_1 r_2)))
+   (--> (p r (begin (cons v_0 v_1 v_2) ι))
+        (p r_2 ι)
+        "step-cons"
+        (judgment-holds (var-lookup r v_0 a_0))
+        (judgment-holds (var-lookup r v_1 a_1))
+        (judgment-holds (var-set r v_2 (cons a_0 a_1) r_2)))
+   (--> (p r (begin (branch-if-nil v l) ι))
+        (p r ι)
+        "step-branch-not-taken"
+        (judgment-holds (var-lookup r v (cons a_0 a_1))))
+   (--> (p r (begin (branch-if-nil v l) ι))
+        (p r ι_2)
+        "step-branch-taken"
+        (judgment-holds (var-lookup r v nil))
+        (judgment-holds (program-lookup p l ι_2)))
+   (--> (p r (jump l))
+        (p r ι_2)
+        "step-jump"
+        (judgment-holds (program-lookup p l ι_2)))))
+
+(define (run-prog p)
+  (define r_0 (term (empty v0 ↦ nil)))
+  (define ι_0 (car (judgment-holds (program-lookup ,p l0 ι) ι)))
+  (apply-reduction-relation* red `(,p ,r_0 ,ι_0)))
+
+
+(define (check-progress p)
+  (define r_0 (term (empty v0 ↦ nil)))
+  (define ι_0 (car (judgment-holds (program-lookup ,p l0 ι) ι)))
+  (or (equal? ι_0 'halt)
+      (and
+       (= 1
+          (length (apply-reduction-relation 
+                   red
+                   `(,p ,r_0 ,ι_0))))
+       (let ([closure (apply-reduction-relation* 
+                       red
+                       `(,p ,r_0 ,ι_0)
+                       #:stop-when
+                       (let ([count 0])
+                         (λ (_)
+                           (begin0
+                             (count . > . 1000)
+                             (set! count (add1 count))))))])
+         ;; if reduction terminates in less than 1000 steps, check it ends with halt
+         ;; (if the #:stop-when condition is true, we get back an empty list, 
+         ;; and the same thing for a reduction cycle)
+         (or (empty? closure)
+             (and (= 1 (length closure))
+                  (match (car closure)
+                    [`(,p ,r ,ι)
+                     (equal? ι 'halt)])))))))
+
+(define (check p)
+  (or (not p)
+      (check-progress p)))
+  
+(define-metafunction list-machine
+  different : any any -> any
+  [(different any_1 any_1)
+   #f]
+  [(different any_1 any_2)
+   #t])
+
+(define-extended-language list-machine-typing list-machine
+  (τ nil (list τ) (listcons τ))
+  (Γ empty (v : τ Γ))
+  (Π empty (l : Γ Π)))
+
+(define-judgment-form list-machine-typing
+  #:contract (check-program p Π)
+  #:mode (check-program I I)
+  [(:lookup-Π Π l0 (v0 : nil empty))
+   (labels-distinct (l0 : ι p))
+   ;; note : changed from l-⊂
+   (d= Π (l0 : ι p))
+   (labels-distinct-Π Π)
+   (check-blocks Π (l0 : ι p))
+   -----
+   (check-program (l0 : ι p) Π)])
+
+(define-judgment-form list-machine-typing
+  #:contract (Γ-⊂ Γ Γ)
+  #:mode (Γ-⊂ I I)
+  [-----
+   (Γ-⊂ Γ empty)]
+  [(:lookup-Γ Γ_1 v τ_1) 
+   (⊂ τ_1 τ_2)
+   (Γ-⊂ Γ_1 Γ_2)
+   ----
+   (Γ-⊂ Γ_1 (v : τ_2 Γ_2))])
+
+(define-judgment-form list-machine-typing
+  #:contract (check-blocks Π p)
+  #:mode (check-blocks I I)
+  [(:lookup-Π Π l Γ)
+   (check-block Π Γ ι)
+   (check-blocks Π p)
+   -----
+   (check-blocks Π (l : ι p)) ]
+  [-----
+   (check-blocks Π end)])
+
+(define-judgment-form list-machine-typing
+  #:contract (check-block Π Γ ι)
+  #:mode (check-block I I I)
+  [-----
+   (check-block Π Γ halt)]
+  [(check-instr Π Γ ι_1 Γ_2) 
+   (check-block Π Γ_2 ι_2)
+   -----
+   (check-block Π Γ (begin ι_1 ι_2))]
+  [(:lookup-Π Π l Γ_2)
+   (Γ-⊂ Γ Γ_2)
+   -----
+   (check-block Π Γ (jump l))])
+
+(define-judgment-form list-machine-typing
+  #:contract (check-instr Π Γ ι Γ)
+  #:mode (check-instr I I I O)
+  [(check-instr Π Γ ι_1 Γ_1)
+   (check-instr Π Γ_1 ι_2 Γ_2)
+   -----
+   (check-instr Π Γ (begin ι_1 ι_2) Γ_2)]
+  [(:lookup-Γ Γ v (list τ))
+   (:lookup-Π Π l Γ_1)
+   (:set Γ v nil Γ_3)
+   (Γ-⊂ Γ_3 Γ_1)
+   (:set Γ_3 v (listcons τ) Γ_2)
+   -----
+   (check-instr Π Γ (branch-if-nil v l) Γ_2)]
+  [(:lookup-Γ Γ v (listcons τ))
+   (:lookup-Π Π l Γ_1)
+   (:set Γ v nil Γ_2)
+   (Γ-⊂ Γ_2 Γ_1)
+   -----
+   (check-instr Π Γ (branch-if-nil v l) Γ)]
+  [(:lookup-Γ Γ v nil)
+   (:lookup-Π Π l Γ_1)
+   (Γ-⊂ Γ Γ_1)
+   -----
+   (check-instr Π Γ (branch-if-nil v l) Γ)]
+  [(:lookup-Γ Γ v (listcons τ)) (:set Γ v_2 τ Γ_2)
+   -----
+   (check-instr Π Γ (fetch-field v 0 v_2) Γ_2)]
+  [(:lookup-Γ Γ v (listcons τ)) (:set Γ v_2 (list τ) Γ_2)
+   -----
+   (check-instr Π Γ (fetch-field v 1 v_2) Γ_2)]
+  [(:lookup-Γ Γ v_0 τ_0) (:lookup-Γ Γ v_1 τ_1)
+   (⊔ (list τ_0) τ_1 (list τ)) (:set Γ v (listcons τ) Γ_2)
+   -----
+   (check-instr Π Γ (cons v_0 v_1 v) Γ_2)])
+
+(define-judgment-form list-machine-typing
+  #:contract (⊂ τ τ)
+  #:mode (⊂ O I)
+  [-----
+   (⊂ τ τ)]
+  [-----
+   (⊂ nil (list τ))]
+  [(⊂ τ τ_2)
+   -----
+   (⊂ (list τ) (list τ_2))]
+  [(⊂ τ τ_2)
+   -----
+   (⊂ (listcons τ) (list τ_2))]
+  [(⊂ τ τ_2)
+   -----
+   (⊂ (listcons τ) (listcons τ_2))])
+
+(define-judgment-form list-machine-typing
+  #:contract (⊔ τ τ τ)
+  #:mode (⊔ I I O)
+  [-----
+   (⊔ τ τ τ)]
+  [-----
+   (⊔ (list τ) nil (list τ))]
+  [-----
+   (⊔ nil (list τ) (list τ))]
+  [(⊔ (list τ_1) (list τ_2) τ_3)
+   -----
+   (⊔ (list τ_1) (listcons τ_2) τ_3)]
+  [(⊔ (list τ_1) (list τ_2) τ_3)
+   -----
+   (⊔ (listcons τ_1) (list τ_2) τ_3)]
+  [(⊔ τ_1 τ_2 τ_3)
+   -----
+   (⊔ (list τ_1) (list τ_2) (list τ_3))]
+  [-----
+   (⊔ (listcons τ) nil (list τ))]
+  [-----
+   (⊔ nil (listcons τ) (list τ))]
+  [(⊔ τ_1 τ_2 τ_3)
+   -----
+   (⊔ (listcons τ_1) (listcons τ_2) (listcons τ_3))])
+
+(define-judgment-form list-machine-typing
+  #:contract (:lookup any v any)
+  #:mode (:lookup I I O)
+  [-----
+   (:lookup (v : any_τ any_Γ) v any_τ)]
+  [(where #t (different v_1 v_2))
+   (:lookup any_Γ v_2 any_τ2)
+   -----
+   (:lookup (v_1 : any_τ1 any_Γ) v_2 any_τ2)])
+
+(define-judgment-form list-machine-typing
+  #:contract (:lookup-Γ Γ v τ)
+  #:mode (:lookup-Γ I I O)
+  [-----
+   (:lookup-Γ (v : τ Γ) v τ)]
+  [(where #t (different v_1 v_2))
+   (:lookup-Γ Γ v_2 τ_2)
+   -----
+   (:lookup-Γ (v_1 : τ_1 Γ) v_2 τ_2)])
+
+(define-judgment-form list-machine-typing
+  #:contract (:lookup-Π Π l Γ)
+  #:mode (:lookup-Π I I O)
+  [-----
+   (:lookup-Π (l : Γ Π) l Γ)]
+  [(where #t (different l_1 l_2))
+   (:lookup-Π Π l_2 Γ_2)
+   -----
+   (:lookup-Π (l_1 : Γ_1 Π) l_2 Γ_2)])
+
+(define-judgment-form list-machine-typing
+  #:contract (:set Γ v τ Γ)
+  #:mode (:set I I I O)
+  [-----
+   (:set (v : any_τ any_Γ) v any_τ2 (v : any_τ2 any_Γ))]
+  [(where #t (different v v_2))
+   (:set any_Γ v_2 any_τ2 any_Γ2)
+   -----
+   (:set (v : any_τ any_Γ) v_2 any_τ2 (v : any_τ any_Γ2))]
+  [-----
+   (:set empty v any_τ (v : any_τ empty))])
+
+(define-metafunction list-machine-typing
+  [(dom (l_1 : any_1 any_2))
+   (l_1 (dom any_2))]
+  [(dom empty) empty])
+
+(define-metafunction list-machine-typing
+  [(dom-P (l_1 : ι_1 p))
+   (l_1 (dom p))]
+  [(dom-P end) empty])
+
+(define-metafunction list-machine-typing
+  [(dom-Π (l_1 : Γ_1 Π))
+   (l_1 (dom Π))]
+  [(dom-Π empty) empty])
+
+#;
+(define-metafunction list-machine-typing
+  l-⊂ : (l ...) (l ...) -> any
+  [(l-⊂ (l_1 ...) (l_2 ...))
+   ,(let ([ht (make-hash)])
+      (for ([l (in-list (term (l_2 ...)))])
+        (hash-set! ht l #t))
+      (for/and ([l (in-list (term (l_1 ...)))])
+        (hash-ref ht l #f)))])
+
+(define-relation list-machine-typing
+  [(l-⊂ (l_1 empty) l_2)
+   (where #t (lmem l_1 l_2))]
+  [(l-⊂ (l_1 l_2) l_3)
+   (l-⊂ l_2 l_3)
+   (where #t (lmem l_1 l_3))]
+  [(l-⊂ empty any)])
+
+(define-relation list-machine-typing
+  [(d= (l_1 : Γ_1 Π) (l_1 : ι p))
+   (d= Π p)]
+  [(d= empty end)])
+
+(define-relation list-machine-typing
+  [(d-⊂ (l_1 : Γ_1 Π) p)
+   (has-label p l_1)
+   (d-⊂ Π p)]
+  [(d-⊂ (l_1 : Γ_1 Π) (l_2 : ι p))
+   (d-⊂ (l_1 : Γ_1 Π) p)]
+  [(d-⊂ empty p)])
+
+(define-relation list-machine-typing
+  [(has-label (l_1 : ι p) l_1)]
+  [(has-label (l_1 : ι p) l_2)
+   (has-label p l_2)])
+
+(define-relation list-machine-typing
+  [(labels-distinct (l_1 : ι p))
+   (label-not-in l_1 p)
+   (labels-distinct p)]
+  [(labels-distinct end)])
+
+(define-relation list-machine-typing
+  [(label-not-in l_1 (l_2 : ι p))
+   (different l_1 l_2)
+   (label-not-in l_1 p)]
+  [(label-not-in l_1 end)])
+
+(define-metafunction list-machine-typing
+  [(lmem l_1 (l_1 l_2))
+   #t]
+  [(lmem l_1 (l_2 l_3))
+   (lmem l_1 l_3)]
+  [(lmem l_1 empty)
+   #f])
+
+(define-relation list-machine-typing
+  [(labels-distinct-Π (l_1 : Γ Π))
+   (label-not-in-Π l_1 Π)
+   (labels-distinct-Π Π)]
+  [(labels-distinct-Π empty)])
+
+(define-relation list-machine-typing
+  [(label-not-in-Π l_1 (l_2 : Γ Π))
+   (different l_1 l_2)
+   (label-not-in-Π l_1 Π)]
+  [(label-not-in-Π l_1 empty)])
+
+(define (generate-M-term)
+  (generate-term list-machine-typing (l0 : ι p) 7))
+
+(define (type-check p)
+  ;; need to provide a program typing, so generate 10 randomly and
+  ;; see if any succeed...
+  (let loop ([i 0])
+    (cond
+      [(i . > . 10) #f]
+      [else
+       (define guess-Π (generate-term list-machine-typing (l0 : (v0 : nil empty) Π) 7))
+       (or (judgment-holds (check-program ,p ,guess-Π))
+           (loop (add1 i)))])))
+
+(define (typed-generator)
+  (let ([g (redex-generator list-machine-typing 
+                            (check-program p Π)
+                            7)])
+    (λ () 
+      (match (g)
+        [`(check-program ,p ,Π)
+         p]
+        [#f #f]))))
+
+(define (generate-typed-term)
+  (match (generate-term list-machine-typing
+                        #:satisfying
+                        (check-program p Π)
+                        7)
+    [`(check-program ,p ,Π)
+     p]
+    [#f #f]))
\ No newline at end of file
diff --git a/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/list-machine/typed-info.rkt b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/list-machine/typed-info.rkt
new file mode 100644
index 0000000000..7dd4ca4e5a
--- /dev/null
+++ b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/list-machine/typed-info.rkt
@@ -0,0 +1,14 @@
+#lang racket/base
+
+(require racket/runtime-path
+         "../util/info-util.rkt")
+
+(provide (all-defined-out))
+
+(define name "list-machine")
+(define fname (make-path-root 'list-machine))
+
+(define-runtime-path here ".")
+
+(define (all-mods)
+  (all-mods/type 'typed here name fname))
\ No newline at end of file
diff --git a/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/poly-stlc/generators.rkt b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/poly-stlc/generators.rkt
index e2798b3a40..9f83fabe8a 100644
--- a/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/poly-stlc/generators.rkt
+++ b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/poly-stlc/generators.rkt
@@ -3,7 +3,8 @@
 (require redex/examples/poly-stlc
          (only-in redex/private/generate-term pick-an-index)
          redex/reduction-semantics
-         racket/bool)
+         racket/bool
+         racket/match)
 
 (provide (all-defined-out))
 
@@ -32,6 +33,15 @@
   (define (generate [index 0])
     (generate-term poly-stlc M #:i-th index)))
 
+(module+ typed-mod
+  (provide generate get-generator type)
+  (define type 'search)
+  (define (get-generator) generate)
+  (define (generate)
+    ((match-lambda [`(typeof • ,M ,τ) M]
+                   [#f #f])
+     (generate-term poly-stlc #:satisfying (typeof • M τ) 3))))
+
 (module+ check-mod
   (provide check)
   (define (check term)
diff --git a/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/poly-stlc/typed-info.rkt b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/poly-stlc/typed-info.rkt
new file mode 100644
index 0000000000..3eb557b44d
--- /dev/null
+++ b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/poly-stlc/typed-info.rkt
@@ -0,0 +1,14 @@
+#lang racket/base
+
+(require racket/runtime-path
+         "../util/info-util.rkt")
+
+(provide (all-defined-out))
+
+(define name "poly-stlc")
+(define fname (make-path-root 'poly-stlc))
+
+(define-runtime-path here ".")
+
+(define (all-mods)
+  (all-mods/type 'typed here name fname))
\ No newline at end of file
diff --git a/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/rbtrees/generators.rkt b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/rbtrees/generators.rkt
index ebcd0df775..8995e4275b 100644
--- a/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/rbtrees/generators.rkt
+++ b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/rbtrees/generators.rkt
@@ -33,6 +33,16 @@
   (define (generate [index 0])
     (generate-term rbtrees t #:i-th index)))
 
+(module+ typed-mod
+  (provide generate get-generator type)
+  (define type 'search)
+  (define (get-generator) generate)
+  (define (generate)
+    ((match-lambda 
+       [`(rb-tree ,t) t]
+       [#f #f])
+     (generate-term rbtrees #:satisfying (rb-tree t) 3))))
+
 (module+ check-mod
   (provide check)
   (define (check t)
diff --git a/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/rbtrees/typed-info.rkt b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/rbtrees/typed-info.rkt
new file mode 100644
index 0000000000..1c82a18f00
--- /dev/null
+++ b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/rbtrees/typed-info.rkt
@@ -0,0 +1,14 @@
+#lang racket/base
+
+(require racket/runtime-path
+         "../util/info-util.rkt")
+
+(provide (all-defined-out))
+
+(define name "rbtrees")
+(define fname (make-path-root 'rbtrees))
+
+(define-runtime-path here ".")
+
+(define (all-mods)
+  (all-mods/type 'typed here name fname))
\ No newline at end of file
diff --git a/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/rvm/generators.rkt b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/rvm/generators.rkt
index 60194d2260..e65070925e 100644
--- a/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/rvm/generators.rkt
+++ b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/rvm/generators.rkt
@@ -7,6 +7,7 @@
          redex/examples/racket-machine/grammar
          redex/examples/racket-machine/verification
          redex/examples/racket-machine/randomized-tests
+         (prefix-in jdg: redex/benchmark/models/rvm/verif-jdg)
          (only-in redex/private/generate-term pick-an-index))
 
 (provide (all-defined-out))
@@ -36,6 +37,20 @@
   (define (generate [index 0])
     (fix (generate-term bytecode e #:i-th index))))
 
+(module+ typed-mod
+  (provide generate get-generator type)
+  (define (get-generator) generate)
+  (define type 'search)
+  (define (generate)
+    (match (generate-term
+            jdg:vl
+            #:satisfying
+            (jdg:V e • O #f • • ∅ s_1 γ_1 η_1)
+            4)
+      [#f #f]
+      [`(jdg:V ,e • O #f • • ∅ ,s_1 ,γ_1 ,η_1)
+       (fix (term (jdg:trans-e ,e)))])))
+
 (module+ check-mod
   (provide check)
   (define (check e)
diff --git a/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/rvm/jdg-grammar.rkt b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/rvm/jdg-grammar.rkt
new file mode 100644
index 0000000000..53bd3b2298
--- /dev/null
+++ b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/rvm/jdg-grammar.rkt
@@ -0,0 +1,43 @@
+#lang racket
+
+(require redex/reduction-semantics)
+
+(define-language bytecode
+  (e (loc n)
+     (loc-noclr n)
+     (loc-clr n)
+     (loc-box n)
+     (loc-box-noclr n)
+     (loc-box-clr n)
+     
+     (let-one e e)
+     (let-void n e)
+     (let-void-box n e)
+     
+     (boxenv n e)
+     (install-value n e e)
+     (install-value-box n e e)
+     
+     (application e e ...)
+     (seq e e e ...)
+     (branch e e e)
+     (let-rec (l ...) e)
+     (indirect x)
+     (proc-const (τ ...) e)
+     (case-lam l ...)
+     l
+     v)
+  
+  (l (lam (τ ...) (n ...) e))
+  
+  (v number
+     void
+     'variable
+     b)
+  
+  (τ val ref)
+  (n natural)
+  (b #t #f)
+  ((x y) variable))
+
+(provide bytecode)
diff --git a/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/rvm/rvm-14.rkt b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/rvm/rvm-14.rkt
index 02b197a40f..5d79277450 100644
--- a/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/rvm/rvm-14.rkt
+++ b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/rvm/rvm-14.rkt
@@ -39,6 +39,38 @@
   #:variables (rest rest1 rest2 ellipsis)
   #:exactly-once)
 
+(define-rewrite bug14a-jdg
+  ((where uninit (sref n s_2))
+   . rest)
+  ==> 
+  rest
+  #:context (define-judgment-form)
+  #:variables (rest)
+  #:exactly-once)
+
+(define-rewrite bug14b-jdg
+  ((uninits s_a)
+   . rest)
+  ==> 
+  rest
+  #:context (define-judgment-form)
+  #:variables (rest)
+  #:exactly-once)
+
+(define-rewrite bug14c-jdg
+  ([(closure-intact (imm-nc sl_1) (imm sl_2))
+    (closure-intact sl_1 sl_2)]
+   . rest)
+  ==> 
+  ([(closure-intact (imm-nc sl_1) (imm sl_2))
+    (closure-intact sl_1 sl_2)]
+   [(closure-intact (box sl_1) (imm sl_2))
+    (closure-intact sl_1 sl_2)]
+   . rest)
+  #:context (define-relation)
+  #:variables (rest)
+  #:exactly-once)
+
 (define-rewrite/compose bug14 bug14a bug14b bug14c)
 
 (include/rewrite (lib "redex/examples/racket-machine/grammar.rkt") grammar)
@@ -47,6 +79,8 @@
 
 (include/rewrite (lib "redex/examples/racket-machine/randomized-tests.rkt") randomized-tests rt-rw)
 
+(include/rewrite (lib "redex/benchmark/models/rvm/verif-jdg.rkt") verif-jdg bug14a-jdg bug14b-jdg bug14c-jdg)
+
 (include/rewrite "generators.rkt" generators bug-mod-rw)
 
 (define small-counter-example
diff --git a/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/rvm/rvm-15.rkt b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/rvm/rvm-15.rkt
index 187d2c6674..6951a6bf86 100644
--- a/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/rvm/rvm-15.rkt
+++ b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/rvm/rvm-15.rkt
@@ -24,12 +24,26 @@
   #:context (match)
   #:exactly-once)
 
+(define-rewrite bug15-jdg
+  [(lam-verified?* ((lam τl nl e) el) sl m)
+   (vals τl)
+   (lam-verified? (lam τl nl e) sl m)
+   (lam-verified?* el sl m)]
+  ==>
+  [(lam-verified?* ((lam τl nl e) el) sl m)
+   (lam-verified? (lam τl nl e) sl m)
+   (lam-verified?* el sl m)]
+  #:context (define-judgment-form)
+  #:exactly-once)
+
 (include/rewrite (lib "redex/examples/racket-machine/grammar.rkt") grammar)
 
 (include/rewrite (lib "redex/examples/racket-machine/verification.rkt") verification bug15v)
 
 (include/rewrite (lib "redex/examples/racket-machine/randomized-tests.rkt") randomized-tests rt-rw bug15rt)
 
+(include/rewrite (lib "redex/benchmark/models/rvm/verif-jdg.rkt") verif-jdg bug15-jdg)
+
 (include/rewrite "generators.rkt" generators bug-mod-rw)
 
 (define small-counter-example
diff --git a/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/rvm/rvm-2.rkt b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/rvm/rvm-2.rkt
index b9cc452c3f..30a0b65505 100644
--- a/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/rvm/rvm-2.rkt
+++ b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/rvm/rvm-2.rkt
@@ -20,10 +20,23 @@
   #:variables (ellipsis1 ellipsis2)
   #:exactly-once)
 
+(define-rewrite bug2-jdg
+  [(redo-clrs ((n ν) γ) s (supdt (n- (n- (slen s) n) (S O)) not s_2))
+   (n< n (slen s))
+   (n≠ (n- (slen s) n) O)
+   (redo-clrs γ s s_2)]
+  ==>
+  [(redo-clrs ((n ν) γ) s (supdt (n- (n- (slen s) n) (S O)) not s_2))
+   (redo-clrs γ s s_2)]
+  #:context (define-judgment-form)
+  #:exactly-once)
+
 (include/rewrite (lib "redex/examples/racket-machine/grammar.rkt") grammar)
 
 (include/rewrite (lib "redex/examples/racket-machine/verification.rkt") verification bug2)
 
+(include/rewrite (lib "redex/benchmark/models/rvm/verif-jdg.rkt") verif-jdg bug2-jdg)
+
 (include/rewrite (lib "redex/examples/racket-machine/randomized-tests.rkt") randomized-tests rt-rw)
 
 (include/rewrite "generators.rkt" generators bug-mod-rw)
diff --git a/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/rvm/rvm-3.rkt b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/rvm/rvm-3.rkt
index 901f929029..ced95be9d7 100644
--- a/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/rvm/rvm-3.rkt
+++ b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/rvm/rvm-3.rkt
@@ -11,8 +11,12 @@
 (define-rewrite bug3
   (abs-push n not s)
   ==> 
-  (abs-push n uninit s)
-  #:context (define-metafunction))
+  (abs-push n uninit s))
+
+(define-rewrite bug3-jdg
+  (abs-push n not sl)
+  ==> 
+  (abs-push n uninit sl))
 
 (include/rewrite (lib "redex/examples/racket-machine/grammar.rkt") grammar)
 
@@ -20,6 +24,8 @@
 
 (include/rewrite (lib "redex/examples/racket-machine/randomized-tests.rkt") randomized-tests rt-rw)
 
+(include/rewrite (lib "redex/benchmark/models/rvm/verif-jdg.rkt") verif-jdg bug3 bug3-jdg)
+
 (include/rewrite "generators.rkt" generators bug-mod-rw)
 
 (define small-counter-example
diff --git a/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/rvm/rvm-4.rkt b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/rvm/rvm-4.rkt
index 1781fed437..a6db20f403 100644
--- a/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/rvm/rvm-4.rkt
+++ b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/rvm/rvm-4.rkt
@@ -16,12 +16,26 @@
   #:variables (rest)
   #:exactly-once)
 
+(define-rewrite bug4-jdg
+  [(V (boxenv n_p e) s n_l b γ η f s_2 γ_2 η_2)
+    (where imm (sref n_p s))
+    (V e (supdt n_p box s) n_l b γ η f s_2 γ_2 η_2)
+    (n< n_p n_l)]
+  ==> 
+  [(V (boxenv n_p e) s n_l b γ η f s_2 γ_2 η_2)
+    (where imm (sref n_p s))
+    (V e (supdt n_p box s) n_l b γ η f s_2 γ_2 η_2)]
+  #:context (define-judgment-form)
+  #:exactly-once)
+
 (include/rewrite (lib "redex/examples/racket-machine/grammar.rkt") grammar)
 
 (include/rewrite (lib "redex/examples/racket-machine/verification.rkt") verification bug3)
 
 (include/rewrite (lib "redex/examples/racket-machine/randomized-tests.rkt") randomized-tests rt-rw)
 
+(include/rewrite (lib "redex/benchmark/models/rvm/verif-jdg.rkt") verif-jdg bug4-jdg)
+
 (include/rewrite "generators.rkt" generators bug-mod-rw)
 
 (define small-counter-example
diff --git a/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/rvm/rvm-5.rkt b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/rvm/rvm-5.rkt
index 5dad2bc4f6..94a0f0c7aa 100644
--- a/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/rvm/rvm-5.rkt
+++ b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/rvm/rvm-5.rkt
@@ -7,7 +7,7 @@
 
 (define the-error "mishandling branches when then branch needs more stack than else branch; bug in the let-rec case not checking a stack bound")
 
-(define-rewrite bug3
+(define-rewrite bug5
   ((side-condition (<= (term n) (term n_l)))
    . rest)
   ==> 
@@ -16,12 +16,23 @@
   #:variables (rest)
   #:exactly-once)
 
+(define-rewrite bug5-jdg
+  ((n<= n n_l)
+   . rest)
+  ==> 
+  rest
+  #:context (define-judgment-form)
+  #:variables (rest)
+  #:exactly-once)
+
 (include/rewrite (lib "redex/examples/racket-machine/grammar.rkt") grammar)
 
-(include/rewrite (lib "redex/examples/racket-machine/verification.rkt") verification bug3)
+(include/rewrite (lib "redex/examples/racket-machine/verification.rkt") verification bug5)
 
 (include/rewrite (lib "redex/examples/racket-machine/randomized-tests.rkt") randomized-tests rt-rw)
 
+(include/rewrite (lib "redex/benchmark/models/rvm/verif-jdg.rkt") verif-jdg bug5-jdg)
+
 (include/rewrite "generators.rkt" generators bug-mod-rw)
 
 (define small-counter-example
diff --git a/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/rvm/rvm-6.rkt b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/rvm/rvm-6.rkt
index 90524aac6f..0d80ae0b6d 100644
--- a/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/rvm/rvm-6.rkt
+++ b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/rvm/rvm-6.rkt
@@ -16,12 +16,22 @@
   #:variables (rest ellipsis)
   #:exactly-once)
 
+(define-rewrite bug6-jdg
+  [(V (case-lam el) s n_l b γ η f s γ η)
+   (lam-verified?* el s ?)]
+  ==>
+  [(V (case-lam el) s n_l b γ η f s γ η)]
+  #:context (define-judgment-form)
+  #:exactly-once)
+
 (include/rewrite (lib "redex/examples/racket-machine/grammar.rkt") grammar)
 
 (include/rewrite (lib "redex/examples/racket-machine/verification.rkt") verification bug6)
 
 (include/rewrite (lib "redex/examples/racket-machine/randomized-tests.rkt") randomized-tests rt-rw)
 
+(include/rewrite (lib "redex/benchmark/models/rvm/verif-jdg.rkt") verif-jdg bug6-jdg)
+
 (include/rewrite "generators.rkt" generators bug-mod-rw)
 
 (define small-counter-example
diff --git a/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/rvm/typed-info.rkt b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/rvm/typed-info.rkt
new file mode 100644
index 0000000000..c40b5eb7f8
--- /dev/null
+++ b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/rvm/typed-info.rkt
@@ -0,0 +1,14 @@
+#lang racket/base
+
+(require racket/runtime-path
+         "../util/info-util.rkt")
+
+(provide (all-defined-out))
+
+(define name "rvm")
+(define fname (make-path-root 'rvm))
+
+(define-runtime-path here ".")
+
+(define (all-mods)
+  (all-mods/type 'typed here name fname))
\ No newline at end of file
diff --git a/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/rvm/util.rkt b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/rvm/util.rkt
index 92e0097956..640551b953 100644
--- a/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/rvm/util.rkt
+++ b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/rvm/util.rkt
@@ -24,6 +24,12 @@
   (submod ".." randomized-tests)
   #:context (require))
 
+(define-rewrite bug-mod-4
+  redex/benchmark/models/rvm/verif-jdg
+  ==> 
+  (submod ".." verif-jdg)
+  #:context (require))
+
 ;; adjust large numbers to keep the reduction from blowing up
 (define-rewrite rt-rw
   [`(,(and (or 'let-void 'let-void-box) i) ,n ,e)
@@ -34,7 +40,7 @@
   #:exactly-once
   #:context (match))
 
-(define-rewrite/compose bug-mod-rw bug-mod-1 bug-mod-2 bug-mod-3)
+(define-rewrite/compose bug-mod-rw bug-mod-1 bug-mod-2 bug-mod-3 bug-mod-4)
 
 (define-syntax-rule (test cexp)
   (module+ test
diff --git a/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/rvm/verif-jdg.rkt b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/rvm/verif-jdg.rkt
new file mode 100644
index 0000000000..bdb6ea2afe
--- /dev/null
+++ b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/rvm/verif-jdg.rkt
@@ -0,0 +1,754 @@
+#lang racket
+
+(require redex/reduction-semantics)
+(require "jdg-grammar.rkt")
+
+(require redex/private/gen-trace
+         (only-in redex/private/generate-term
+                  enable-gen-trace!))
+
+(provide (all-defined-out))
+
+
+(define (bytecode-ok? e)
+  (not (eq? 'invalid (car (term (verify ,e () 0 #f () () ∅))))))
+
+(define (bytecode-ok/V? e)
+  (judgment-holds
+   (V ,e • O #f • • ∅ s_1 γ_1 η_1)))
+
+(define-extended-language verification 
+  bytecode
+  (s (ṽ ...) invalid)
+  (ṽ uninit imm box imm-nc box-nc not)
+  (γ ((n ṽ) ...))
+  (η (n ...))
+  (f (n n (ṽ ...)) ∅)
+  (m n ?))
+
+(define-language bl
+  (e (loc n)
+     (loc-noclr n)
+     (loc-clr n)
+     (loc-box n)
+     (loc-box-noclr n)
+     (loc-box-clr n)
+     
+     (let-one e e)
+     (let-void n e)
+     (let-void-box n e)
+     
+     (boxenv n e)
+     (install-value n e e)
+     (install-value-box n e e)
+     
+     (application e el)
+     ;; change to (seq el) ?
+     (seq e e)
+     (branch e e e)
+     (let-rec ll e)
+     (indirect x)
+     (proc-const τl e)
+     (case-lam ll)
+     l
+     v)
+  
+  (el (e el) •)
+  
+  (l (lam τl nl e))
+  
+  (ll (l ll) •)
+  
+  (τl (τ τl) •)
+  
+  (nl (n nl) •)
+  
+  (v n
+     void
+     'variable
+     b)
+  
+  (τ val ref)
+  (n O (S n))
+  (b boolean)
+  ((x y) variable))
+
+(define-metafunction bl
+  [(trans-e (application e el))
+   (application (trans-e e) (trans-e e_2) ...)
+   (where (e_2 ...) (cns->lst el))]
+  [(trans-e (proc-const τl e))
+   (proc-const (cns->lst τl) (trans-e e))]
+  [(trans-e (case-lam el))
+   (case-lam any ...)
+   (where (e ...) (cns->lst el))
+   (where (any ...) ((trans-e e) ...))]
+  [(trans-e (any n e))
+   (any (trans-n n) (trans-e e))
+   (side-condition (memq (term any) '(let-void let-void-box)))]
+  [(trans-e (seq e_1 e_2))
+   (seq any_3 ... any_4 ...)
+   (where (any_3 ...) (un-seq e_1))
+   (where (any_4 ...) (un-seq e_2))]
+  [(trans-e (branch e_1 e_2 e_3))
+   (branch (trans-e e_1) (trans-e e_2) (trans-e e_3))]
+  [(trans-e (let-one e_1 e_2))
+   (let-one (trans-e e_1) (trans-e e_2))]
+  [(trans-e (boxenv n e))
+   (boxenv (trans-n n) (trans-e e))]
+  [(trans-e (any n e_1 e_2))
+   (any (trans-n n) (trans-e e_1) (trans-e e_2))
+   (side-condition (memq (term any) '(install-value install-value-box)))]
+  [(trans-e (proc-const τl e))
+   (proc-const (cns->lst τl) (trans-e e))]
+  [(trans-e (let-rec ll e))
+   (let-rec ((trans-l any_l) ...) (trans-e e))
+   (where (any_l ...) (cns->lst ll))]
+  [(trans-e (any n))
+   (any (trans-n n))
+   (side-condition (memq (term any) '(loc loc-noclr loc-clr loc-box loc-box-clr loc-box-noclr)))]
+  [(trans-e l_1)
+   (trans-l l_1)]
+  [(trans-e n)
+   (trans-n n)]
+  [(trans-e any)
+   any])
+
+(define-metafunction bl
+  [(trans-l (lam τl nl e))
+   (lam (cns->lst τl) (number_2 ...) (trans-e e))
+   (where (n_1 ...) (cns->lst nl))
+   (where (number_2 ...) ((trans-n n_1) ...))])
+
+(define-metafunction bl
+  [(un-seq e_1)
+   (any_2 ...)
+   (where (seq any_2 ...) (trans-e e_1))]
+  [(un-seq e)
+   ((trans-e e))])
+
+(define-metafunction bl
+  [(trans-n O)
+   0]
+  [(trans-n (S n))
+   ,(add1 (term (trans-n n)))])
+
+(define-extended-language vl
+  bl
+  (sl (ν sl) •)
+  (s sl invalid)
+  (ν uninit imm box imm-nc box-nc not)
+  (γ ((n ν) γ) •)
+  (η (n η) •)
+  (f (n n sl) ∅)
+  (m n ?))
+
+
+(define (check-V-res v-res)
+  ;(displayln (list 'check-V-res v-res))
+  (match v-res
+    [`(V ,e ,s1 ,n ,b ,γ1 ,η1 ,f ,s2 ,γ2 ,η2)
+     (unless
+         (equal?
+          (term
+           (verify
+            (trans-e ,e)
+            (trans-s ,s1)
+            (trans-n ,n)
+            ,b
+            (trans-γ ,γ1)
+            (trans-η ,η1)
+            (trans-f ,f)))
+          (term
+           ((trans-s ,s2)
+            (trans-γ ,γ2)
+            (trans-η ,η2))))
+       (error 'check-V-res "failed on ~s " e))]))
+
+(define (check-Vs n #:generator [g #f])
+  (define gen (redex-generator vl
+                               (V e • O #f • • ∅ s_1 γ_1 η_1)
+                               6))
+  (for ([_ (in-range n)])
+    (define maybe-V 
+      (if g 
+          (gen)
+          (generate-term
+           vl
+           #:satisfying
+           ;(V e s n b γ η f s_1 γ_1 η_1)
+           (V e • O #f • • ∅ s_1 γ_1 η_1)
+           5)))
+    (match maybe-V
+      [#f
+       (display ".")]
+      [`(V ,e ,s ,n ,b ,γ ,η ,f ,s_1 ,γ_1 ,η_1)
+       (displayln (term (trans-e ,e)))
+       (check-V-res maybe-V)])))
+
+(define-metafunction vl
+  [(trans-γ ((n ν) γ))
+   (((trans-n n) ν) any ...)
+   (where (any ...) (trans-γ γ))]
+  [(trans-γ •)
+   ()])
+
+(define-metafunction vl
+  [(trans-η (n η))
+   ((trans-n n) any ...)
+   (where (any ...) (trans-η η))]
+  [(trans-η •)
+   ()])
+         
+(define-metafunction vl
+  [(trans-f ∅)
+   ∅]
+  [(trans-f (n_1 n_2 sl))
+   ((trans-n n_1) (trans-n n_2) (cns->lst sl))])
+
+(define-metafunction vl
+  [(trans-s invalid)
+   invalid]
+  [(trans-s sl)
+   (cns->lst sl)])
+         
+(define-metafunction vl
+  [(cns->lst (any_1 any_2))
+   (any_1 any_3 ...)
+   (where (any_3 ...) (cns->lst any_2))]
+  [(cns->lst •)
+   ()])
+
+
+;; verification judgment -----------------------------------------------
+
+
+(define-judgment-form vl
+  #:mode (V I I I I I I I O O O)
+  #:contract (V e s n b γ η f s γ η)
+  
+  ;localrefs
+  [(V (loc n) s n_l #f γ η f s γ η)
+   (lmem (sref n s) (imm (imm-nc •)))]
+  [(V (loc n) s n_l #t γ η f s γ η)
+   (lmem (sref n s) (imm (imm-nc (box (box-nc •)))))]
+  [(V (loc-box n) s n_l b γ η f s γ η)
+   (lmem (sref n s) (box (box-nc •)))]
+  
+  [(V (loc-noclr n) s n_l #f γ η f (supdt n (nc ν_n) s) γ η_l)
+   (where ν_n (sref n s))
+   (log-noclr n n_l ν_n η η_l)
+   (lmem ν_n (imm (imm-nc •)))]
+  [(V (loc-noclr n) s n_l #t γ η f (supdt n (nc ν_n) s) γ η_l)
+   (where ν_n (sref n s))
+   (log-noclr n n_l ν_n η η_l)
+   (lmem ν_n (imm (imm-nc (box (box-nc •)))))]
+  [(V (loc-box-noclr n) s n_l b γ η f (supdt n box-nc s) γ η_l)
+   (where ν_n (sref n s))
+   (log-noclr n n_l ν_n η η_l)
+   (lmem ν_n (box (box-nc •)))]
+  
+  
+  [(V (loc-clr n) s n_l #f γ η f (supdt n not s) γ_l η)
+   (where imm (sref n s))
+   (log-clr n s n_l γ γ_l)]
+  [(V (loc-clr n) s n_l #t γ η f (supdt n not s) γ_l η)
+   (lmem (sref n s) (imm (box •)))
+   (log-clr n s n_l γ γ_l)]
+  [(V (loc-box-clr n) s n_l b γ η f (supdt n not s) γ_l η)
+   (where box (sref n s))
+   (log-clr n s n_l γ γ_l)]
+
+  ;branch
+  [(V (branch e_c e_t e_e) s n_l b γ η f s_n (concat γ_2 γ_3) η_3)
+   (V e_c s n_l #f γ η ∅ s_1 γ_1 η_1)
+   (V e_t (trim s_1 s) O b • • f s_2 γ_2 η_2)
+   (undo-clrs γ_2 (trim s_2 s) s_21)
+   (undo-noclrs η_2 s_21 s_22)
+   (V e_e s_22 O b γ_1 η_1 f s_3 γ_3 η_3)
+   (redo-clrs γ_2 (trim s_3 s) s_n)]
+  
+  ;let-one
+  [(V (let-one e_r e_b) sl n_l b γ η f s_2 γ_2 η_2)
+   (where sl_0 (uninit sl))
+   (V e_r sl_0 (n+ n_l (S O)) #f γ η ∅ sl_1 γ_1 η_1)
+   (where (uninit sl_1*) (trim sl_1 sl_0))
+   (V e_b (imm sl_1*) (n+ n_l (S O)) b γ_1 η_1 (shift (S O) f) s_2 γ_2 η_2)]
+  
+  ;seq
+  [(V (seq e_0 e_1) s n_l b γ η f s_2 γ_2 η_2)
+   (V e_0 s n_l #t γ η ∅ s_1 γ_1 η_1)
+   (V e_1 (trim s_1 s) n_l b γ_1 η_1 f s_2 γ_2 η_2)]
+  
+  ;application
+  [(V (application (loc-noclr n) el) s n_l b_i γ η (n_f n_s sl_f) s_2 γ_2 η_2)
+   (n= n (n+ n_f (len el)))
+   (V-self-app (application (loc-noclr n) el) s n_l γ η (n_f n_s sl_f) s_2 γ_2 η_2)]
+  [(V (application (lam τl nl e) el) s n_l b γ η f s_2 γ_2 η_2)
+   (where n (len el))
+   (where n_l* (n+ n n_l))
+   (where s_1 (abs-push n not s))
+   (V*-ref el τl s_1 n_l* γ η s_2 γ_2 η_2)
+   (lam-verified? (lam τl nl e) s_1 ?)]
+  [(V (application (proc-const τl e) el) s n_l b γ η f s_2 γ_2 η_2)
+   (V (application (lam τl • e) el) s n_l b γ η f s_2 γ_2 η_2)]
+  [(V (application e_0 el) s n_l b γ η f s_2 γ_2 η_2)
+   ;; the only place where cases might overlap, so exclude that explicitly
+   (not-self-app (application e_0 el) s f)
+   (where n (len el))
+   (where n_l* (n+ n n_l))
+   (V* (e_0 el) (abs-push n not s) n_l* #f γ η s_2 γ_2 η_2)]
+  
+  ; literals
+  [(V n s n_l b γ η f s γ η)]
+  [(V b s n_l b_i γ η f s γ η)]
+  [(V (quote variable) s n_l b γ η f s γ η)]
+  [(V void s n_l b γ η f s γ η)]
+  
+  ; install-value
+  [(V (install-value n e_r e_b) s n_l b γ η f s_3 γ_3 η_3)
+   (n< n n_l)
+   (V e_r s n_l #f γ η ∅ s_1 γ_1 η_1)
+   (where s_2 (trim s_1 s))
+   (where uninit (sref n s_2))
+   (V e_b (supdt n imm s_2) n_l b γ η f s_3 γ_3 η_3)]
+  [(V (install-value-box n e_r e_b) s n_l b γ η f s_3 γ_3 η_3)
+   (n< n (len s))
+   (V e_r s n_l #f γ η ∅ s_1 γ_1 η_1)
+   (where s_2 (trim s_1 s))
+   (lmem (sref n s_2) (box (box-nc •)))
+   (V e_b s_2 n_l b γ_1 η_1 f s_3 γ_3 η_3)]
+  
+  ; boxenv
+  [(V (boxenv n_p e) s n_l b γ η f s_2 γ_2 η_2)
+   (where imm (sref n_p s))
+   (V e (supdt n_p box s) n_l b γ η f s_2 γ_2 η_2)
+   (n< n_p n_l)]
+  
+  ; indirect
+  [(V (indirect x) s n_l b γ η f s γ η)]
+  
+  ; let-void
+  [(V (let-void n e) s n_l b_i γ η f s_1 γ_1 η_1)
+   (V e (abs-push n uninit s) (n+ n n_l) b_i γ η (shift n f) s_1 γ_1 η_1)]
+  [(V (let-void-box n e) s n_l b_i γ η f s_1 γ_1 η_1)
+   (V e (abs-push n box s) (n+ n n_l) b_i γ η (shift n f) s_1 γ_1 η_1)]
+  
+   ; procedures in arbitrary context
+  [(V (lam τl nl e) s n_l b γ η f s γ η)
+   (vals (val τl))
+   (lam-verified? (lam τl nl e) s ?)]
+  [(V (proc-const τl e) s n_l b γ η f s_1 γ_1 η_1)
+   (vals τl)
+   (V (lam τl • e) s n_l b γ η f s_1 γ_1 η_1)]
+  
+  ; case-lam
+  [(V (case-lam el) s n_l b γ η f s γ η)
+   (lam-verified?* el s ?)]
+  
+   ; let-rec
+  [(V (let-rec ll e) s n_l b γ η f s_2 γ_2 η_2)
+   (where n (len ll))
+   (n<=  n n_l)
+   (lsplit n s s_a s_b)
+   (uninits s_a)
+   (where s_1 (abs-push n imm s_b))
+   (verify-ll O s_1 ll)
+   (V e s_1 n_l b γ η f s_2 γ_2 η_2)])
+
+(define-judgment-form vl
+  #:mode (verify-ll I I I)
+  [(verify-ll n s •)]
+  [(verify-ll n s ((lam τl (n_l nl) e) ll))
+   (vals τl)
+   (lam-verified? (lam τl (n_l nl) e) s n)
+   (verify-ll (S n) s ll)])
+
+(define-judgment-form vl
+  #:mode (V* I I I I I I O O O)
+  #:contract (V* el s n b γ η s γ η)
+  [(V* • s n_l b γ η s γ η)]
+  [(V* (e_0 el) s n_l b γ η s_2 γ_2 η_2)
+   (V e_0 s n_l b γ η ∅ s_1 γ_1 η_1)
+   (V* el (trim s_1 s) n_l b γ_1 η_1 s_2 γ_2 η_2)])
+
+(define-judgment-form vl
+  #:mode (V-self-app I I I I I I O O O)
+  #:contract (V-self-app e s n γ η f s γ η)
+  [(V-self-app (application e_0 el) sl n_l γ η (n_f n_s sl_f) sl_1 γ_1 η_1)
+   (where n (len el))
+   (where n_l* (n+ n n_l))
+   (V* (e_0 el) (abs-push n not sl) n_l* #f γ η sl_1 γ_1 η_1)
+   (closure-intact (ssblst n_s (slen sl_f) sl_1) sl_f)])
+
+(define-judgment-form vl
+  #:mode (V*-ref I I I I I I O O O)
+  [(V*-ref • • s n_l γ η s γ η)]
+  [(V*-ref (e_0 el) (val τl) s n_l γ η s_2 γ_2 η_2)
+   (V e_0 s n_l #f γ η ∅ s_1 γ_1 η_1)
+   (V*-ref el τl (trim s_1 s) n_l γ_1 η_1 s_2 γ_2 η_2)]
+  [(V*-ref (e_0 el) • s n_l γ η s_2 γ_2 η_2)
+   (V* (e_0 el) s n_l #f γ η s_2 γ_2 η_2)]
+  [(V*-ref • (τ_0 τl) s n_l γ η s γ η)]
+  [(V*-ref ((loc n) el) (ref τl) s n_l γ η s_2 γ_2 η_2)
+   ; Require the reference to load a box.
+   (V (loc-box n) s n_l #f γ η ∅ s_1 γ_1 η_1)
+   (V*-ref el τl s_1 n_l γ_1 η_1 s_2 γ_2 η_2)]
+  [(V*-ref ((loc-noclr n) el) (ref τl) s n_l γ η s_2 γ_2 η_2)
+   ; Require the reference to load a box.
+   (V (loc-box-noclr n) s n_l #f γ η ∅ s_1 γ_1 η_1)
+   (V*-ref el τl s_1 n_l γ_1 η_1 s_2 γ_2 η_2)]
+  [(V*-ref ((loc-clr n) el) (ref τl) s n_l γ η s_2 γ_2 η_2)
+   ; Require the reference to load a box.
+   (V (loc-box-clr n) s n_l #f γ η ∅ s_1 γ_1 η_1)
+   (V*-ref el τl s_1 n_l γ_1 η_1 s_2 γ_2 η_2)])
+ 
+(define-relation vl 
+  [(closure-intact • •)]
+  [(closure-intact (imm-nc sl_1) (imm sl_2))
+   (closure-intact sl_1 sl_2)]
+  [(closure-intact (box-nc sl_1) (box sl_2))
+   (closure-intact sl_1 sl_2)]
+  [(closure-intact (ν sl_1) (ν sl_2))
+   (closure-intact sl_1 sl_2)])
+
+(define-relation vl
+  [(vals (val τl))
+   (vals τl)]
+  [(vals •)])
+
+(define-relation vl
+  [(uninits (uninit sl))
+   (uninits sl)]
+  [(uninits •)])
+
+(define-judgment-form vl
+  #:mode (lam-verified? I I I)
+  [(lam-verified? (lam τl nl e) sl m)
+   ;(where n_d (len sl))
+   ;(lmax nl n_m)
+   ;(n< n_m n_d)
+   (where n_d* (n+ (len nl) (len τl)))
+   (where sl_0 (collate-refs nl sl))
+   (not-lmem uninit sl_0)
+   (not-lmem not sl_0)
+   (where s_d (drop-noclrs sl_0))
+   (extract-self m nl τl s_d f)
+   (V e (concat s_d (arg τl)) n_d* #f • • f sl_1 γ_1 η_1)])
+
+(define-judgment-form vl
+  #:mode (lam-verified?* I I I)
+  [(lam-verified?* • sl m)]
+  [(lam-verified?* ((lam τl nl e) el) sl m)
+   (vals τl)
+   (lam-verified? (lam τl nl e) sl m)
+   (lam-verified?* el sl m)])
+
+;; suffers from ?/n confusion
+;; fixable by transforming to a metafunction
+;; but need to add judgment-holds support 
+
+(define-judgment-form vl
+  #:mode (extract-self I I I I O)
+  [(extract-self ? nl τl sl ∅)]
+  [(extract-self n nl τl sl ∅)
+   (not-lmem n nl)]
+  [(extract-self n_i (n_i nl) τl sl (O (len τl) sl))
+   (not-lmem n_i nl)]
+  [(extract-self n_i (n_0 nl) τl sl ((S n_n) n_τ sl))
+   (extract-self n_i nl τl sl (n_n n_τ sl))
+   (nlmem n_i nl)])
+
+(define-metafunction vl
+  [(loc-noclr? (loc-noclr e))
+   #t]
+  [(loc-noclr? e)
+   #f])
+
+(define-relation vl
+  [(not-self-app (application e el) s ∅)]
+  [(not-self-app (application e el) s f)
+   (where #f (loc-noclr? e))]
+  [(not-self-app (application (loc-noclr n) el) s (n_f n_s s_f))
+   (n≠ n (n+ n_f (len el)))])
+
+(define-relation vl
+  [(n≠ O (S n))]
+  [(n≠ (S n) O)]
+  [(n≠ (S n_1) (S n_2))
+   (n≠ n_1 n_2)])
+
+#;
+(define-metafunction vl
+  [(es ? nl τl sl)
+   ∅]
+  [(extract-self n nl τl sl)
+   ∅
+   (judgment-holds (not-lmem n nl))]
+  [(extract-self n_i (n_i nl) (τ_0 τl) sl (O O sl))
+   (not-lmem n_i nl)]
+  [(extract-self n_i (n_0 nl) (τ_0 τl) sl ((S n_n) (S n_τ) sl))
+   (extract-self n_i nl τl sl (n_n n_τ sl))
+   (nlmem n_i nl)])
+
+(define-metafunction vl
+  [(ssblst O O sl)
+   •]
+  [(ssblst O (S n) (ν sl))
+   (ν (ssblst O n sl))]
+  [(ssblst (S n_1) n_2 (ν sl))
+   (ssblst n_1 n_2 sl)])
+  
+(define-relation vl
+  [(lmem ν (ν sl))]
+  [(lmem ν (ν_1 sl))
+   (lmem ν sl)])
+
+(define-relation vl
+  [(nlmem n (n nl))]
+  [(nlmem n (n_1 nl))
+   (nlmem n nl)])
+
+(define-relation vl
+  [(not-lmem any_1 (any_2 any_3))
+   (not-lmem any_1 any_3)
+   (where (any_!_4 any_!_4) (any_1 any_2))]
+  [(not-lmem any_1 •)])
+
+(define-judgment-form vl
+  #:mode (lmax I O)
+  [(lmax • O)]
+  [(lmax (n nl) n)
+   (lmax nl n_m)
+   (n< n_m n)]
+  [(lmax (n nl) n_m)
+   (lmax nl n_m)
+   (n< n n_m)])
+
+(define-metafunction vl
+  [(sref O (ν sl))
+   ν]
+  [(sref (S n) (ν_1 sl))
+   (sref n sl)]
+  [(sref n •)
+   #f])
+
+(define-metafunction vl
+  #;[(supdt O ν_1 •)
+   (ν_1 •)]
+  [(supdt O ν_1 (ν_2 sl))
+   (ν_1 sl)]
+  [(supdt (S n) ν_1 (ν_2 sl))
+   (ν_2 (supdt n ν_1 sl))])
+
+(define-metafunction vl
+  [(n- n_1 O)
+   n_1]
+  [(n- (S n_1) (S n_2))
+   (n- n_1 n_2)]
+  #;
+  [(n- O (S n))
+   #f])
+
+(define-metafunction vl
+  [(n+ O n)
+   n]
+  [(n+ (S n_1) n_2)
+   (n+ n_1 (S n_2))])
+
+(define-metafunction vl
+  [(slen •)
+   O]
+  [(slen (ν sl))
+   (S (slen sl))])
+
+(define-metafunction vl
+  [(len •)
+   O]
+  [(len (any_1 any_2))
+   (S (len any_2))])
+
+(define-relation vl
+  [(n< O (S n))]
+  [(n< (S n_1) (S n_2))
+   (n< n_1 n_2)])
+
+(define-relation vl
+  [(n<= O n)]
+  [(n<= (S n_1) (S n_2))
+   (n<= n_1 n_2)])
+  
+(define-relation vl
+  [(n= O O)]
+  [(n= (S n_1) (S n_2))
+   (n= n_1 n_2)])
+
+(define-judgment-form vl
+  #:mode (lsplit I I O O)
+  [(lsplit O any_1 • any_1)]
+  [(lsplit (S n) (any_1 any_2) (any_1 any_3) any_4)
+   (lsplit n any_2 any_3 any_4)])
+   
+
+(define-metafunction vl
+  shift : n f -> f
+  [(shift n ∅) ∅]
+  [(shift n (n_f n_s sl)) 
+   ((n+ n n_f) (n+ n n_s) sl)])
+
+(define-metafunction vl
+  abs-push : n ν sl -> sl
+  [(abs-push O ν sl) sl]
+  [(abs-push (S n) ν sl)
+   (abs-push n ν (ν sl))])
+
+;; note: could turn this back into a metafunction
+;; if the restriction on relations in term positions
+;; is removed....
+;; or support judgment-holds, maybe that is better
+;; naturally a metafunction in any case...
+(define-judgment-form vl
+  #:contract (log-noclr n n ν η η)
+  #:mode (log-noclr I I I I O)
+  [(log-noclr n_p n_l ν_p η ((n- n_p n_l) η))
+   (n<= n_l n_p)
+   (lmem ν_p (imm (box •)))]
+  [(log-noclr n_p n_l ν_p η η)
+   (lmem ν_p (imm-nc (box-nc (uninit (not •)))))]
+  [(log-noclr n_p n_l ν_p η η)
+   (n< n_p n_l)])
+
+
+(define-metafunction vl
+  nc : ν -> ν
+  [(nc imm) imm-nc]
+  [(nc imm-nc) imm-nc]
+  [(nc box) box-nc]
+  [(nc box-nc) box-nc])
+
+(define-judgment-form vl
+  #:contract (log-clr n s n γ γ)
+  #:mode (log-clr I I I I O)
+  [(log-clr n_p s n_l γ (((n- (n- (slen s) n_p) (S O)) ν_np) γ))
+   (where ν_np (sref n_p s))
+   (n<= n_l n_p)]
+  [(log-clr n_p s n_l γ γ)
+   (n< n_p n_l)])
+
+;; need more specific nt types in
+;; relations like this or there can be problems
+;; satisfying constraings (i.e. trying to satisfy an sl with anys)
+(define-metafunction vl
+  [(concat • any_1)
+   any_1]
+  [(concat (any_1 any_2) any_3)
+   (any_1 (concat any_2 any_3))])
+
+
+(define-judgment-form vl
+  #:mode (undo-clrs I I O)
+  [(undo-clrs γ invalid invalid)]
+  [(undo-clrs • s s)]
+  [(undo-clrs ((n ν) γ) s (supdt (n- (n- (slen s) n) (S O)) ν s_2))
+   (n< n (slen s))
+   (n≠ (n- (slen s) n) O)
+   (undo-clrs γ s s_2)]
+  [(undo-clrs ((n ν) γ) s s)
+   (n<= (slen s) n)])
+
+(define-judgment-form vl
+  #:mode (undo-noclrs I I O)
+  [(undo-noclrs η invalid invalid)]
+  [(undo-noclrs • s s)]
+  [(undo-noclrs (n η) s (supdt n imm s_2))
+   (where imm-nc (sref n s))
+   (undo-noclrs η s s_2)]
+  [(undo-noclrs (n η) s (supdt n box s_2))
+   (where box-nc (sref n s))
+   (undo-noclrs η s s_2)]
+  [(undo-noclrs (n η) s s_2)
+   (undo-noclrs η s s_2)
+   ;; Bug 1
+   ;; (lmem (sref n s) (uninit (imm (imm-nc (boc-nc (box (not •)))))))
+   (lmem (sref n s) (uninit (imm (box (not •)))))])
+
+(define-judgment-form vl
+  #:mode (redo-clrs I I O)
+  [(redo-clrs γ invalid invalid)]
+  [(redo-clrs • s s)]
+  [(redo-clrs ((n ν) γ) s (supdt (n- (n- (slen s) n) (S O)) not s_2))
+   (n< n (slen s))
+   (n≠ (n- (slen s) n) O)
+   (redo-clrs γ s s_2)]
+  [(redo-clrs ((n ν) γ) s s)
+   (n<= (slen s) n)])
+
+(define-metafunction vl
+  [(collate-refs • sl)
+   •]
+  [(collate-refs (n nl) sl)
+   ((sref n sl) (collate-refs nl sl))])
+
+(define-metafunction vl
+  [(drop-noclrs (imm-nc sl))
+   (imm (drop-noclrs sl))]
+  [(drop-noclrs (box-nc sl))
+   (box sl)]
+  [(drop-noclrs (ν sl))
+   (ν (drop-noclrs sl))]
+  [(drop-noclrs •)
+   •])
+
+;; had to make both of these
+;; j-forms for the below reasons...
+#;
+(define-metafunction vl
+  undo-clrs : γ s -> s
+  [(undo-clrs γ invalid) invalid]
+  [(undo-clrs • s) s]
+  [(undo-clrs ((n ν) γ) s)
+   (undo-clrs γ (supdt (n- (n- (slen s) n) (S O)) ν s))]
+  ;; --> (slen s) < n
+  ;; but generation doesn't support this fall-through!!
+  [(undo-clrs ((n ν) γ) s)
+   (undo-clrs γ s)])
+#;
+(define-metafunction vl
+  redo-clrs : γ s -> s
+  [(redo-clrs γ invalid) invalid]
+  [(redo-clrs • s) s]
+  [(redo-clrs ((n ν) γ) s) 
+   (redo-clrs γ (supdt (n- (n- (slen s) n) (S O)) not s))]
+  ;; --> (slen s) < n
+  ;; but generation doesn't support this fall-through!!
+  [(redo-clrs ((n ν) γ) s)
+   (redo-clrs γ s)])
+
+(define-metafunction vl
+  trim : s s -> s
+  [(trim invalid s) invalid]
+  [(trim s_1 s_2)
+   (sdrp (n- (slen s_1) (slen s_2)) s_1)])
+
+(define-metafunction vl
+  [(sdrp O sl)
+   sl]
+  [(sdrp (S n) (ν sl))
+   (sdrp n sl)]
+  [(sdrp n •)
+   •])
+
+(define-metafunction vl
+  [(valid? invalid) #f]
+  [(valid? sl) #t])
+
+(define-metafunction vl
+  [(arg •)
+   •]
+  [(arg (val τl))
+   (imm (arg τl))]
+  [(arg (ref τl))
+   (box (arg τl))])
+
+
+(provide (all-defined-out))
\ No newline at end of file
diff --git a/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/stlc+lists/generators.rkt b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/stlc+lists/generators.rkt
index 7f628aa306..5acf428c39 100644
--- a/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/stlc+lists/generators.rkt
+++ b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/stlc+lists/generators.rkt
@@ -3,7 +3,8 @@
 (require (lib "redex/examples/stlc+lists.rkt")
          (only-in redex/private/generate-term pick-an-index)
          redex/reduction-semantics
-         racket/bool)
+         racket/bool
+         racket/match)
 
 (provide (all-defined-out))
 
@@ -32,6 +33,15 @@
   (define (generate [index 0])
     (generate-term stlc M #:i-th index)))
 
+(module+ typed-mod
+  (provide generate get-generator type)
+  (define type 'search)
+  (define (get-generator) generate)
+  (define (generate)
+    ((match-lambda [`(typeof • ,M ,τ) M]
+                   [#f #f])
+     (generate-term stlc #:satisfying (typeof • M τ) 5))))
+
 (module+ check-mod
   (provide check)
   (define (check term)
diff --git a/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/stlc+lists/typed-info.rkt b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/stlc+lists/typed-info.rkt
new file mode 100644
index 0000000000..947d05bdaf
--- /dev/null
+++ b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/stlc+lists/typed-info.rkt
@@ -0,0 +1,14 @@
+#lang racket/base
+
+(require racket/runtime-path
+         "../util/info-util.rkt")
+
+(provide (all-defined-out))
+
+(define name "stlc")
+(define fname (make-path-root 'stlc+lists))
+
+(define-runtime-path here ".")
+
+(define (all-mods)
+  (all-mods/type 'typed here name fname))
\ No newline at end of file
diff --git a/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/stlc-subst/generators.rkt b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/stlc-subst/generators.rkt
index 2b67d71258..a7940ebe14 100644
--- a/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/stlc-subst/generators.rkt
+++ b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/stlc-subst/generators.rkt
@@ -3,7 +3,8 @@
 (require redex/examples/stlc+lists+subst
          (only-in redex/private/generate-term pick-an-index)
          redex/reduction-semantics
-         racket/bool)
+         racket/bool
+         racket/match)
 
 (provide (all-defined-out))
 
@@ -32,6 +33,15 @@
   (define (generate [index 0])
     (generate-term stlc M #:i-th index)))
 
+(module+ typed-mod
+  (provide generate get-generator type)
+  (define type 'search)
+  (define (get-generator) generate)
+  (define (generate)
+    ((match-lambda [`(typeof • ,M ,τ) M]
+                   [#f #f])
+     (generate-term stlc #:satisfying (typeof • M τ) 5))))
+
 (module+ check-mod
   (provide check)
   (define (check term)
diff --git a/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/stlc-subst/typed-info.rkt b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/stlc-subst/typed-info.rkt
new file mode 100644
index 0000000000..bfa70a40f0
--- /dev/null
+++ b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/stlc-subst/typed-info.rkt
@@ -0,0 +1,14 @@
+#lang racket/base
+
+(require racket/runtime-path
+         "../util/info-util.rkt")
+
+(provide (all-defined-out))
+
+(define name "stlc-sub")
+(define fname (make-path-root 'stlc-subst))
+
+(define-runtime-path here ".")
+
+(define (all-mods)
+  (all-mods/type 'typed here name fname))
\ No newline at end of file
diff --git a/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/type-all-info.rkt b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/type-all-info.rkt
new file mode 100644
index 0000000000..e6aa0e20a5
--- /dev/null
+++ b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/type-all-info.rkt
@@ -0,0 +1,25 @@
+#lang racket/base
+
+(require racket/runtime-path
+         racket/list
+         racket/path)
+
+(provide all-mods)
+
+(define-runtime-path here ".")
+
+(define (all-info-files)
+  (for/list ([f (in-directory here)]
+             #:when (and (file-exists? f)
+                         (regexp-match #rx"^.*typed-info\\.rkt$"
+                                       (path->string f)))
+             #:unless (regexp-match #rx".*all-info.*"
+                                    (path->string f)))
+    (path->string 
+     (find-relative-path (simplify-path (current-directory))
+                         (simplify-path f)))))
+
+(define (all-mods)
+  (append-map (λ (f)
+                ((dynamic-require f 'all-mods)))
+              (all-info-files)))
diff --git a/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/util/info-util.rkt b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/util/info-util.rkt
index 71d1bcc24b..d72a85cca5 100644
--- a/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/util/info-util.rkt
+++ b/pkgs/redex-pkgs/redex-benchmark/redex/benchmark/models/util/info-util.rkt
@@ -5,7 +5,8 @@
          racket/runtime-path)
 
 (provide make-all-mods
-         make-path-root)
+         make-path-root
+         all-mods/type)
 
 (define-runtime-path here ".")
 
@@ -14,7 +15,8 @@
 (define type->genmod
   (hash 'grammar 'adhoc-mod
         'enum 'enum-mod
-        'ordered 'ordered-mod))
+        'ordered 'ordered-mod
+        'typed 'typed-mod))
 
 (define (get-name/modpaths filename type path-root)
   (define model-name (first (regexp-split #rx"\\." (last (regexp-split #rx"/" filename)))))
diff --git a/pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl b/pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl
index fdb4029f5a..62a89b670e 100644
--- a/pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl
+++ b/pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl
@@ -2204,7 +2204,7 @@ with @racket[#:satisfying].}
 
 Toggles whether or not redex will dynamically adjust the
 chance that more recursive clauses of judgment forms or metafunctions 
-are chosen earlierwhen attempting to generate terms 
+are chosen earlier when attempting to generate terms 
 with forms that use @racket[#:satisfying]. It is @racket[#t] by
 default, which causes redex to favor more recursive clauses at
 lower depths and less recursive clauses at depths closer to the