Fixes a bug in model verifier's handling of `branch'

collects/redex/examples/racket-machine/reduction.rkt

@@ -1,7 +1,7 @@
 #lang scheme
 
 (require redex/reduction-semantics)
-(require "grammar.ss")
+(require "grammar.ss" "util.ss")
 
 (define-extended-language runtime bytecode
   (p (V S H T C) error)
@@ -34,10 +34,6 @@
      (self-app x e_0 e_1 ...))
   (m n ?))
 
-(define-metafunction bytecode
-  [(count-up number)
-   ,(build-list (term number) (λ (x) x))])
-
 (define procedure-rules
   (reduction-relation
    runtime
@@ -245,10 +241,6 @@
   (T any)
   (l any))
 
-(define-metafunction loader
-  concat : (any ...) ... -> (any ...)
-  [(concat any ...) ,(apply append (term (any ...)))])
-
 (define-metafunction loader
   [(load e ((x_0 (name e_0 (proc-const (τ ...) e_b))) ...))
    (uninit (((ε))) H (concat ((x_0 e_0*) ...) T) (e_*))

collects/redex/examples/racket-machine/util.rkt

@@ -0,0 +1,16 @@
+#lang racket
+
+(require "grammar.ss"
+         redex/reduction-semantics)
+
+(provide (all-defined-out))
+
+(define-language any)
+
+(define-metafunction any
+  [(count-up number)
+   ,(build-list (term number) (λ (x) x))])
+
+(define-metafunction any
+  concat : (any ...) ... -> (any ...)
+  [(concat any ...) ,(apply append (term (any ...)))])

collects/redex/examples/racket-machine/verification-test.rkt

@@ -374,6 +374,15 @@
  (negate bytecode-ok?)
  '(let-one 'x (branch (loc-noclr 0) (loc-noclr 0) (loc-clr 0))))
 
+(test-predicate
+ bytecode-ok?
+ '(proc-const (val val val)
+              (branch (loc 0)
+                      (branch (loc 1)
+                              (loc-clr 2)
+                              void)
+                      (application (loc 2)))))
+
 ; let-rec
 (test-predicate
  bytecode-ok?

collects/redex/examples/racket-machine/verification.rkt

@@ -1,7 +1,7 @@
 #lang scheme
 
 (require redex/reduction-semantics)
-(require "grammar.ss")
+(require "grammar.ss" "util.ss")
 
 (define (bytecode-ok? e)
   (not (eq? 'invalid (car (term (verify ,e () 0 #f () () ∅))))))
@@ -58,11 +58,10 @@
   
   ; branch
   [(verify (branch e_c e_t e_e) s n_l b γ η f)
-   ; FIXME: should redo γ_2?
+   ((redo-clears γ_2 (trim s_3 s)) (concat γ_2 γ_3) η_3)
-   ((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))]
+   (where (s_3 γ_3 η_3) (verify e_e (undo-noclears η_2 (undo-clears γ_2 (trim s_2 s))) 0 b γ_1 η_1 f))]
   
   ; let-one
   [(verify (let-one e_r e_b) (ṽ_1 ...) n_l b γ η f)
@@ -346,9 +345,4 @@
   [(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))