namespace main(8);
    col fixed first_step = [1] + [0]*;
    col witness pc;
    col fixed latch = [0, 1]*;
    col witness x;
    col witness y;
    col witness instr_foo;
    main::instr_foo $ [ 1 ] in main::latch $ [ main::x ];
    col witness instr_bar;
    main::instr_bar $ [ 2 ] in main::latch $ [ main::y ];
    col witness instr_baz;
    main::instr_baz $ [ 3 ] in main::latch $ [ main::y ];
    col witness instr_loop;
    main::pc' = ((1 - main::first_step') * ((main::instr_loop * main::pc) + ((1 - main::instr_loop) * (main::pc + 1))));
    col fixed p_line = [0, 1, 2, 3] + [3]*;
    col fixed p_instr_baz = [0, 0, 1, 0] + [0]*;
    col fixed p_instr_bar = [0, 1, 0, 0] + [0]*;
    col fixed p_instr_foo = [1, 0, 0, 0] + [0]*;
    col fixed p_instr_loop = [0, 0, 0, 1] + [1]*;
    [ main::pc, main::instr_foo, main::instr_bar, main::instr_baz, main::instr_loop ] in [ main::p_line, main::p_instr_foo, main::p_instr_bar, main::p_instr_baz, main::p_instr_loop ];
