[racket-dev] Redex for abstract machines / analysis prototypes

Machine semantics for real machines (like the JVM or Racket's VM) or non-standard semantics for an abstract interpretation (like what I end up getting into) can get up to monstrous numbers of components for each state that usually don't matter. I and I'm sure many others would appreciate a reduction relation language that is a little more like UIUC's K.

Here is a concrete suggestion of what I imagine (some support for patterns on hashes):
1) Add a pattern (hash (literal pat) ...) to match hashes up to the specified keys (hashes with more keys are still accepted).
2) Add rewrite rules for changing the current state.
-- (next-state (r r) ...)
-- (get r r)
-- (set r r r)
-- (set* r (r r) ...)
Where 
(get r_0 r_1) is ,(hash-ref (term r_0) (term r_1) 'something-that-never-matches)
(set r_0 r_1 r_2) is ,(hash-set (term r_0) (term r_1) (term r_2))
(set* r_0 (r_k r_v) ...) is the obvious extension of set, but is annoying to write.
And assuming the LHS is named state,
 (next-state (r_k r_v) ...) is (set* state (r_k r_v) ...)

Not-the-best-example-since-it's-so-minimal:

(define-language CEK
 [e x (e e) lam]
 [lam (lambda (x) e)]
 [rho (hash)]
 [kont mt (ar e rho kont) (fn e rho kont))])

(define R
 (machine-step CEK
  [--> (hash (C x) (E rho))
       (next-state (C lam) (E rho*))
       (where (lam rho*) (get rho x))]

  [--> (hash (C (e_0 e_1)) (E rho) (K kont))
       (next-state (C e_0) (K (ar e_1 rho kont)))]

  [--> (hash (C lam) (E rho) (K (ar e rho_0 kont)))
       (next-state (C e) (E rho_0) (K (fn lam rho kont)))]

  [--> (hash (C v) (K (fn (lambda (x) e) rho kont)))
       (next-state (C e) (E (set rho x (v rho))) (K kont))]))

(define (inject e) (term (set* #hash() (C ,e) (E #hash()) (K mt))))

Is this reasonably simple to add to Redex? It would be a very welcome addition.
-Ian