Require Import Bool String List Arith.
Require Import Omega.
Require Import Kami.All.

Require Import FunctionalExtensionality.

Set Implicit Arguments.

Module module'Testing.
    Variable instancePrefix: string.
    Variable NumInsts : nat.
    Variable InstrSz : nat.
    Variable PgmSz : nat.
    Variable pgm: ConstT (Array NumInsts (Bit InstrSz)).
    Definition pc : string := instancePrefix--"pc".
    Definition procSpecModule: Mod :=
         (MODULE {
        Register pc : Bit PgmSz <-  (* intwidth *) (natToWord PgmSz 0)
    with Method instancePrefix--"getInst" () : Bit InstrSz :=
    (
        Read pc_v : Bit PgmSz <- pc ;
        LET inst : Bit InstrSz (* non-call varbinding *) <- ( (* isConstT *) #pgm @[ #pc_v ] ) ;
        Ret #inst
         )}).
End module'Testing.