proper descriptions of the rvm model bugs

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/14.diff

@@ -1,7 +1,7 @@
 3c3
 < (define the-error "no-error")
 ---
-> (define the-error "bug 14")
+> (define the-error "certain updates to initialized slots could break optimizer assumptions")
 142c142,143
 <    (where uninit (stack-ref n s_2))]
 ---

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/15.diff

@@ -1,7 +1,7 @@
 3c3
 < (define the-error "no-error")
 ---
-> (define the-error "bug 15")
+> (define the-error "neglected to restict case-lam to accept only 'val' arguments")
 125c125,126
 <   [(verify (case-lam (name l (lam (val ...) (n ...) e)) ...) s n_l b γ η f)
 ---

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/2.diff

@@ -1,3 +1,7 @@
+3c3
+< (define the-error "no-error")
+---
+> (define the-error "stack offset / pointer confusion")
 338c338,339
 <    (side-condition (< (term n_0) (term n_h)))]
 ---

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/3.diff

@@ -1,7 +1,7 @@
 3c3
 < (define the-error "no-error")
 ---
-> (define the-error "bug 3")
+> (define the-error "application slots not initialized properly")
 100c100
 <    (where s_1 (abs-push n not s))
 ---

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/4.diff

@@ -1,7 +1,7 @@
 3c3
 < (define the-error "no-error")
 ---
-> (define the-error "bug 4")
+> (define the-error "mishandling branches when then branch needs more stack than else branch")
 155c155,156
 <    (side-condition (< (term n_p) (term n_l)))]
 ---

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/6.diff

@@ -1,3 +1,7 @@
+3c3
+< (define the-error "no-error")
+---
+> (define the-error "forgot to implement the case-lam branch in verifier")
 127c127,128
 <    (side-condition (term (AND (lam-verified? l s ?) ...)))]
 ---

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-14.rkt

@@ -1,6 +1,6 @@
 #lang racket
 
-(define the-error "bug 14")
+(define the-error "certain updates to initialized slots could break optimizer assumptions")
 
 (require redex/reduction-semantics)
 (require "../../racket-machine/grammar.rkt" 

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-15.rkt

@@ -1,6 +1,6 @@
 #lang racket
 
-(define the-error "bug 15")
+(define the-error "neglected to restict case-lam to accept only 'val' arguments")
 
 (require redex/reduction-semantics)
 (require "../../racket-machine/grammar.rkt" 

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-2.rkt

@@ -1,6 +1,6 @@
 #lang racket
 
-(define the-error "no-error")
+(define the-error "stack offset / pointer confusion")
 
 (require redex/reduction-semantics)
 (require "../../racket-machine/grammar.rkt" 

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-3.rkt

@@ -1,6 +1,6 @@
 #lang racket
 
-(define the-error "bug 3")
+(define the-error "application slots not initialized properly")
 
 (require redex/reduction-semantics)
 (require "../../racket-machine/grammar.rkt" 

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-4.rkt

@@ -1,6 +1,6 @@
 #lang racket
 
-(define the-error "bug 4")
+(define the-error "mishandling branches when then branch needs more stack than else branch")
 
 (require redex/reduction-semantics)
 (require "../../racket-machine/grammar.rkt" 

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-6.rkt

@@ -1,6 +1,6 @@
 #lang racket
 
-(define the-error "no-error")
+(define the-error "forgot to implement the case-lam branch in verifier")
 
 (require redex/reduction-semantics)
 (require "../../racket-machine/grammar.rkt"