Redstone DSL

[rollrat]

model Redstone2L {
    // ============================================================
    // Redstone2L DSL: 2층(ground/top) 조합회로(PnR/합성)용 선언형 모델
    // - "place"  : 배치 변수(블록을 놓을지)
    // - "state"  : 상태 변수(시나리오별 전기적 상태: 파워/온오프)
    // - "shape"  : 모양/연결 같은 파생 구조(더스트 축, 연결 방향 등)
    // - "sources": “어디서 파워가 들어오는가”를 집합으로 누적하는 개념(OR-원인 집합)
    // - "rule"   : 제약 묶음(ILP로 내려갈 논리식/등가식/함의/합 제약 등)
    // ============================================================

    // -------------------------
    // 0) Index / Topology
    // -------------------------

    // 격자상의 한 칸을 (x,z)로 인덱싱한다. (y는 Layer로 분리)
    index Cell = (x,z) in Grid;

    // 2층 레이어: 바닥(GROUND)과 그 위 1칸(TOP)
    enum Layer { GROUND=0, TOP=1 }

    // 4방향
    enum Dir { N,E,S,W }

    // c에서 방향 d로 인접한 셀(격자 밖이면 null 가능)
    fn neigh(c:Cell, d:Dir) -> Cell?;

    // 벽토치가 붙을 "지지 블록" 위치를 계산
    // (예: 벽토치가 c의 면 d에 붙으면, 실제로는 d방향 반대쪽 블록을 지지로 삼는 식)
    fn supportForWallTorch(c:Cell, d:Dir) -> Cell?;

    // 리피터 방향 d를 기준으로, 입력(back) 셀 위치
    fn back(c:Cell, d:Dir) -> Cell?;

    // 리피터 방향 d를 기준으로, 출력(front) 셀 위치
    fn front(c:Cell, d:Dir) -> Cell?;

    // -------------------------
    // 1) 시나리오 / 핀
    // -------------------------

    // 시나리오(진리표 검증용): IN=0인 세계(s=0)와 IN=1인 세계(s=1)를 동시에 풀도록 복제
    scenario Sc in {0,1};

    // 외부에서 관찰/강제하는 관측 지점(입력/출력 핀)
    pin IN  : ObsPoint;
    pin OUT : ObsPoint;

    // -------------------------
    // 2) 배치 변수 (place)
    // -------------------------
    // "place X[...] : Type" 는
    // "그 위치에 해당 블록/부품을 둘지"를 나타내는 0/1 결정변수.

    place S[Cell] : Solid;          // 해당 Cell에 '고체 블록(솔리드 블록)'을 둘지
    place D[Layer, Cell] : Dust;    // 해당 Layer/Cell에 레드스톤 더스트를 둘지
    place T_stand[Cell] : Torch;    // 해당 Cell에 '스탠딩 토치(위에 올리는 토치)'를 둘지
    place T_wall[Cell, Dir] : Torch;// Cell에 방향 Dir로 벽토치를 둘지(어느 면에 붙는지)
    place R[Cell, Dir] : Repeater;  // Cell에 방향 Dir로 리피터를 둘지

    // -------------------------
    // 3) 상태 변수 (state) - 시나리오별
    // -------------------------
    // "state"는 배치가 고정된 뒤, 시나리오 s마다 전기 상태(파워)를 나타냄.
    // 보통 place가 1이어야만 state가 1이 될 수 있게 R_DOMAIN에서 묶는다.

    state BP[Sc, Cell] : BlockPower;         // 블록이 파워(간접파워 포함) 되었는지
    state DP[Sc, Layer, Cell] : DustOn;      // 더스트가 켜졌는지(신호를 띄는지)
    state TO_stand[Sc, Cell] : TorchOn;      // 스탠딩 토치가 ON인지
    state TO_wall[Sc, Cell, Dir] : TorchOn;  // 벽토치가 ON인지
    state RO[Sc, Cell, Dir] : RepOn;         // 리피터 출력이 ON인지(활성화) — “리피터가 켜짐”

    // -------------------------
    // 4) 모양/연결(Shape) 변수
    // -------------------------
    // 레드스톤 더스트는 “연결 후보”에 따라 모양(축/크로스)이 결정되고,
    // 모양이 Conn에 반영되어 어떤 방향으로 전력이 전달되는지 컷(cutoff)된다.

    shape Conn[Layer, Cell, Dir] : Conn; // 더스트가 해당 방향 Dir로 "연결되어 있음"을 의미
    shape AxisNS[Layer, Cell] : Axis;    // 더스트가 NS축 모양(남북 직선)
    shape AxisEW[Layer, Cell] : Axis;    // 더스트가 EW축 모양(동서 직선)
    shape Cross[Layer, Cell] : Axis;     // 더스트가 4방향 교차 모양(크로스) 허용 여부/선택

    // -------------------------
    // 5) Source-set(원인 집합) 변수
    // -------------------------
    // “이 셀이 파워를 받는 원인들이 뭐냐”를 원인 집합으로 누적하고,
    // 나중에 OR{SrcSet} 형태로 "하나라도 있으면 켜짐"을 만든다.
    // (백엔드에서는 결국 OR-선형화로 내려갈 것)

    sources BlockSrc[Sc, Cell] : SrcSet;       // 블록을 파워시키는 원인들의 집합
    sources DustSrc[Sc, Layer, Cell] : SrcSet; // 더스트를 켜는 원인들의 집합

    // -------------------------
    // 6) 파생 헬퍼(derived helper) 선언
    // -------------------------
    // 네가 def로 쓰던 파생식들이 DSL에선 변수로 선언되어야 ILP로 내릴 수 있음.

    shape Cand[Layer, Cell, Dir] : Bool;                   // 해당 방향으로 연결 후보가 있는지(더스트/주변 환경 기반)
    shape DustPowersBlock[Sc, Layer, Cell, Dir] : Bool;    // 더스트가 그 방향 이웃 블록을 파워하는지(Conn 컷 포함)
    state RepIn[Sc, Cell, Dir] : Bool;                     // 리피터 입력이 들어왔는지(백 방향에서 신호가 들어오는지)

    // ============================================================
    // A) placement 제약
    // ============================================================
    rule R_PLACEMENT_BASE {
        forall(c in Cell) {
            // TOP 레이어에 더스트를 놓으려면, 그 아래(해당 Cell)에 솔리드 블록이 필요
            // (마인크래프트에서 더스트는 블록 위에만 올려둘 수 있다는 규칙)
            require D[TOP, c] -> S[c];

            // 스탠딩 토치도 블록 위에만 올려둘 수 있으므로, 블록이 있어야 한다
            require T_stand[c] -> S[c];
        }

        forall((c,d) in Cell * Dir) {
            // 벽토치 배치 규칙:
            // - 벽토치 자체는 "빈 공간" 위치(c)에 존재해야 하고(!S[c])
            // - 지지 블록(supportForWallTorch(c,d))은 솔리드여야 한다
            require T_wall[c,d] -> (!S[c] and S[supportForWallTorch(c,d)]);
        }

        forall(c in Cell) {
            // 한 칸에는 벽토치를 최대 1개 방향만 달 수 있게 제한
            require sum(d in Dir) T_wall[c,d] <= 1;

            // 한 칸에는 리피터도 최대 1개 방향만 둘 수 있게 제한
            require sum(d in Dir) R[c,d] <= 1;
        }

        feature PACKING_ONEHOT {
            forall(c in Cell) {
                // 패킹(배타) 제약:
                // 동일 Cell(동일 좌표)에 "서로 겹쳐서" 놓이면 안 되는 것들을 한 번에 제한
                // - ground 더스트 / top 더스트 / 스탠딩 토치 / 벽토치(4방 중 1) / 리피터(4방 중 1)
                // - 합이 1을 넘지 않게 해서 한 칸에는 최대 하나만 두도록 강제
                require D[GROUND,c] + D[TOP,c] + T_stand[c]
                    + sum(d in Dir) T_wall[c,d]
                    + sum(d in Dir) R[c,d] <= 1;
            }
        }
    }

    // ============================================================
    // B) domain linking (state <= placement)
    // ============================================================
    rule R_DOMAIN {
        forall(s in Sc) {
            forall(c in Cell) {
                // 상태 변수는 배치가 있어야만 켜질 수 있다(도메인 링크)
                // 예: 블록파워 BP가 1이면 그 위치에 블록 S가 반드시 존재
                require BP[s,c] -> S[c];

                // 더스트 상태 DP가 1이면 해당 더스트가 배치돼 있어야 함
                require DP[s,GROUND,c] -> D[GROUND,c];
                require DP[s,TOP,c]    -> D[TOP,c];

                // 토치 ON 상태는 토치가 배치돼 있어야 함
                require TO_stand[s,c]  -> T_stand[c];
            }
            forall((c,d) in Cell * Dir) {
                // 벽토치 ON 상태는 벽토치 배치가 있어야 함
                require TO_wall[s,c,d] -> T_wall[c,d];

                // 리피터 ON 상태는 리피터 배치가 있어야 함
                require RO[s,c,d]      -> R[c,d];
            }
        }
    }

    // ============================================================
    // C) torch inverter (토치 인버터 동작)
    // ============================================================
    rule R_TORCH_INVERTER {
        forall(s in Sc) {
            forall(c in Cell) {
                // 스탠딩 토치의 기본 동작:
                // - 토치가 설치되어 있고(T_stand=1)
                // - 붙어있는 블록이 파워되지 않았으면(!BP)
                // => 토치는 ON
                // 즉, 토치는 “부착 블록의 BP”를 반전한다(인버터)
                def TO_stand[s,c] <-> (T_stand[c] and !BP[s,c]);
            }
            forall((c,d) in Cell * Dir) {
                let sup = supportForWallTorch(c,d);

                // 벽토치도 마찬가지로, 지지 블록(sup)의 BP를 반전한다
                def TO_wall[s,c,d] <-> (T_wall[c,d] and !BP[s,sup]);
            }
        }
    }

    rule R_TORCH_ANTICHEAT_EXCLUDE_ATTACHED_BLOCK {
        // 토치 규칙의 중요한 예외:
        // "토치는 자신이 붙어있는 블록(attached/support)을 파워하지 않는다"
        // 즉, 토치 출력이 BlockSrc에 들어가더라도 attached 블록으로는 들어가면 안 됨.
        // 여기서는 sources 집합에서 특정 원인을 "exclude"로 빼는 형태로 표현.

        forall(s in Sc) {
            forall(c in Cell) {
                // 스탠딩 토치 출력이 BlockSrc[s,c]에 (자동으로) 들어가는 상황이 있더라도,
                // "자기 부착 블록(c)"에 대해서는 제외한다는 의미
                exclude BlockSrc[s,c] += TorchOut(stand,c);
            }
            forall((c,d) in Cell * Dir) {
                let sup = supportForWallTorch(c,d);

                // 벽토치도 지지 블록(sup)에는 파워 원인으로 추가되지 못하게 exclude
                exclude BlockSrc[s,sup] += TorchOut(wall,c,d);
            }
        }
    }

    // ============================================================
    // D) repeater (리피터 스켈레톤)
    // ============================================================
    rule R_REPEATER {
        forall(s in Sc) {
            forall((c,d) in Cell * Dir) {
                let b = back(c,d);   // 입력 방향(뒤)
                let f = front(c,d);  // 출력 방향(앞)

                // 리피터 입력 조건(대충의 OR):
                // - back쪽 셀의 더스트가 켜져 있거나
                // - back쪽 셀의 블록이 파워되어 있거나
                // - back쪽 셀에 토치 등이 파워를 주고 있거나(추상 헬퍼)
                // 실제 마크 리피터 입력 규칙을 더 정확히 모델링하려면 이 부분을 확장해야 함.
                def RepIn[s,c,d] <-> OR{
                    DP[s,GROUND,b],
                    DP[s,TOP,b],
                    BP[s,b],
                    TorchPowersCell(s,b)
                };

                // 리피터 ON: 리피터가 설치되어 있고, 입력이 들어오면 출력 ON
                def RO[s,c,d] <-> (R[c,d] and RepIn[s,c,d]);

                // 리피터 출력은 앞쪽 셀의 더스트/블록을 파워 소스로 추가한다
                // (DustSrc/BlockSrc에 원인으로 누적)
                add DustSrc[s,GROUND,f] += RepOut(c,d);
                add DustSrc[s,TOP,f]    += RepOut(c,d);
                add BlockSrc[s,f]       += RepOut(c,d);
            }
        }
    }

    // ============================================================
    // E) dust shape/conn (더스트 모양/연결)
    // ============================================================
    rule R_DUST_CONN_AXIS_CUT {
        forall((l,c,d) in Layer * Cell * Dir) {
            // Cand: 더스트가 있고(D=1), 그 방향으로 "연결 후보"가 존재하면 후보 true
            // ExistsConnectionCandidate는 주변에 더스트/리피터/토치/블록 등
            // 연결될 만한 것이 있는지를 보는 built-in(현재 백엔드 매핑 필요)
            def Cand[l,c,d] <-> (D[l,c] and ExistsConnectionCandidate(l,c,d));
        }

        feature DUST_AUTO_AXIS {
            forall((l,c) in Layer * Cell) {
                // 축 선택:
                // - NS 후보가 하나라도 있으면 AxisNS 가능
                // - EW 후보가 하나라도 있으면 AxisEW 가능
                // 여기서는 "자동으로" 축을 고르게 만들되,
                // 둘 다 동시에 선택은 금지(<=1)로 해서 직선 모양을 강제한다.
                def AxisNS[l,c] <-> OR{ Cand[l,c,N], Cand[l,c,S] };
                def AxisEW[l,c] <-> OR{ Cand[l,c,E], Cand[l,c,W] };
                require AxisNS[l,c] + AxisEW[l,c] <= 1;

                // Conn은 선택된 축에 따라 2방향만 true가 된다.
                // (AxisNS면 N/S만 연결, AxisEW면 E/W만 연결)
                def Conn[l,c,N] <-> AxisNS[l,c];
                def Conn[l,c,S] <-> AxisNS[l,c];
                def Conn[l,c,E] <-> AxisEW[l,c];
                def Conn[l,c,W] <-> AxisEW[l,c];
            }
        }

        feature DUST_ALLOW_CROSS {
            forall((l,c) in Layer * Cell) {
                // 교차(크로스) 모양을 허용하는 확장점:
                // AllowCrossChoice가 true면 Cross를 선택 가능하게 하고
                // Conn을 4방향으로 열어주는 식으로 확장할 수 있다.
                // (현재는 Cross 선언만 있고 Conn 반영은 아직 스켈레톤)
                def Cross[l,c] <-> AllowCrossChoice(l,c);
            }
        }
    }

    // ============================================================
    // F) dust on (더스트 상태)
    // ============================================================
    rule R_DUST_ON {
        forall(s in Sc) {
            forall((l,c) in Layer * Cell) {
                // 더스트가 ON이라는 것은:
                // - 더스트가 설치되어 있고(D=1)
                // - DustSrc(원인 집합) 중 하나라도 존재하면(OR{...})
                // => 켜진다
                def DP[s,l,c] <-> (D[l,c] and OR{ DustSrc[s,l,c] });
            }
        }
    }

    // ============================================================
    // G) dust -> block (더스트가 블록을 파워, Conn cutoff 반영)
    // ============================================================
    rule R_DUST_POWERS_BLOCK {
        forall(s in Sc) {
            forall((l,c,d) in Layer * Cell * Dir) {
                let b = neigh(c,d); // c에서 d방향 이웃 블록 셀

                // 더스트가 블록을 파워하는 조건:
                // - 더스트가 켜져 있고(DP)
                // - 해당 방향으로 연결이 열려 있고(Conn)
                // - 이웃 칸에 솔리드 블록이 실제로 존재해야(S[b])
                // => 그 블록은 파워 원인으로 "더스트"를 하나 가진다
                def DustPowersBlock[s,l,c,d] <-> (DP[s,l,c] and Conn[l,c,d] and S[b]);

                // 그 결과를 BlockSrc에 원인으로 추가(“이 블록은 저 더스트 때문에 파워됨”)
                add BlockSrc[s,b] += DustPowersBlock(s,l,c,d);
            }
        }
    }

    // ============================================================
    // H) block power (블록 파워)
    // ============================================================
    rule R_BLOCK_POWER {
        feature MINIMAL_NOT_STRONG {
            forall(s in Sc) {
                forall(c in Cell) {
                    // (단순화/근사) 블록 파워를 "TOP 더스트가 켜져 있느냐"로만 정의
                    // 즉, BP는 더스트 전파 규칙(토치/리피터/간접파워 등)을
                    // 강하게 모델링하지 않고 최소한으로 쓰겠다는 설정.
                    // 실제로는: BP[s,c] <-> OR{ BlockSrc[s,c] } 같은 형태가 더 일반적.
                    def BP[s,c] <-> DP[s,TOP,c];
                }
            }
        }
        // else: 블록은 OR(BlockSrc)로 정의하는 정식 버전을 넣을 수 있음
    }

    // ============================================================
    // J) truth table (NOT 게이트 진리표 강제)
    // ============================================================
    rule R_TRUTH_TABLE_NOT {
        // Observe(PIN, s=k)는 "시나리오 k에서 그 핀의 관측값"을 의미.
        // 여기서는 시나리오 0에서는 IN=0, 시나리오 1에서는 IN=1로 강제하고,
        // OUT은 그 반대로 나오도록 강제해서 NOT 게이트를 합성하게 만든다.

        force Observe(IN,  s=0) == 0;
        force Observe(IN,  s=1) == 1;
        force Observe(OUT, s=0) == 1;
        force Observe(OUT, s=1) == 0;
    }

    // ============================================================
    // K) objective (목적함수)
    // ============================================================
    objective minimize {
        // 가중치 기반 비용 최소화:
        // - 더스트 개수 * wD
        // - 토치 개수 * wT
        // - 솔리드 블록 개수 * wS
        // - 리피터 개수 * wR
        // 이렇게 하면 “가능하면 적은 부품으로” NOT을 만들도록 유도된다.

        wD * sum((l,c) in Layer * Cell) D[l,c]
      + wT * (sum(c in Cell) T_stand[c] + sum((c,d) in Cell * Dir) T_wall[c,d])
      + wS * sum(c in Cell) S[c]
      + wR * sum((c,d) in Cell * Dir) R[c,d]
    }
}

[rollrat]

// ============================================================
// FULL DSL (가정 문법)
// - 하위 의미론(마인크래프트-ish 레드스톤 제약) +
// - 상위 계층(netlist/pnr/component synthesize)
// - 목표: NOT/OR를 “템플릿 고정 없이” bbox 안에서 내부 합성(solve)하고,
//        상위에서는 인스턴스 배치 + wire routing만 푸는 2단계 스타일
// ============================================================


// ============================================================
// 1) 하위 의미론: Minecraft-ish 3D Redstone Core
//    (정확한 MC 100%가 아니라, “PnR에 유용한 핵심 제약” 위주)
//    포함:
//    - 3D Cell (x,y,z)
//    - Dust/Repeater/Torch는 "공간"에 놓이고, 아래칸이 Solid여야 함
//    - Dust는 15블록 한계: BaseSrc로부터 dust-edge 15번 이내로만 Reach 가능
//    - Repeater는 입력(back) 감지 후 출력(front)에 BaseSrc를 생성(거리 리셋)
//    - Torch는 attached(아래 Solid)의 BP를 반전, 그리고 attached 블록은 파워하지 않음(exclude)
// ============================================================
model Redstone3D_MCCore {
  // ----- grid -----
  index Cell = (x,y,z) in Grid;

  enum Dir6 { N,E,S,W,U,D }
  enum HDir { N,E,S,W }

  fn neigh6(c:Cell, d:Dir6) -> Cell?;
  fn neighH(c:Cell, d:HDir) -> Cell?;

  fn below(c:Cell) -> Cell?;      // (x,y-1,z)
  fn above(c:Cell) -> Cell?;      // (x,y+1,z)

  fn back(c:Cell, d:HDir)  -> Cell?; // repeater input cell
  fn front(c:Cell, d:HDir) -> Cell?; // repeater output cell

  // ----- scenarios -----
  scenario Sc in {0,1};

  // ----- 15-limit step index -----
  index Step = t in 0..15;

  // ----- pins / observe (가정: 백엔드가 제공) -----
  pin P_IN  : ObsPoint;
  pin P_OUT : ObsPoint;
  fn Observe(p:ObsPoint, s:Sc) -> Bool; // 관측/강제 인터페이스

  // ----- placement (공간 점유) -----
  // Solid는 "블록 공간"을 점유, Dust/Torch/Repeater는 "공간(air)"을 점유한다고 가정
  place S[Cell] : Solid;
  place D[Cell] : Dust;
  place T[Cell] : Torch;
  place R[Cell, HDir] : Repeater;

  // ----- packing -----
  rule R_PACKING {
    forall(c in Cell) {
      require sum(d in HDir) R[c,d] <= 1;
      // 같은 공간에 solid와 부품이 겹치지 않게
      require S[c] + D[c] + T[c] + sum(d in HDir) R[c,d] <= 1;
    }
  }

  // ----- support rules (아래에 블록이 있어야 놓을 수 있음) -----
  rule R_SUPPORT {
    forall(c in Cell) {
      let b = below(c);
      require D[c] -> S[b];
      require T[c] -> S[b];
      forall(d in HDir) { require R[c,d] -> S[b]; }
    }
  }

  // ----- states -----
  state DP[Sc, Cell] : Bool;         // dust on
  state BP[Sc, Cell] : Bool;         // block powered (only meaningful if S[c]=1)
  state TO[Sc, Cell] : Bool;         // torch on
  state RO[Sc, Cell, HDir] : Bool;   // repeater output on
  state RepIn[Sc, Cell, HDir] : Bool;

  // 15-limit reachability
  state Reach[Sc, Step, Cell] : Bool;

  // ----- sources (원인 집합) -----
  // BaseSrc: “강한 소스” (input pin, torch output, repeater output 등)
  sources BaseSrc[Sc, Cell]  : SrcSet;
  // BlockSrc: 블록 파워 원인
  sources BlockSrc[Sc, Cell] : SrcSet;

  // ----- domain link (state <= placement) -----
  rule R_DOMAIN {
    forall(s in Sc) {
      forall(c in Cell) {
        require DP[s,c] -> D[c];
        require TO[s,c] -> T[c];
        require BP[s,c] -> S[c];
      }
      forall((c,d) in Cell * HDir) { require RO[s,c,d] -> R[c,d]; }
    }
  }

  // ============================================================
  // Torch semantics (standing torch only, attached=below solid)
  // - TO = T && !BP(attached)
  // - torch outputs BaseSrc/BlockSrc to neighbors, BUT NOT to attached block
  // ============================================================
  rule R_TORCH_INVERTER {
    forall(s in Sc) {
      forall(c in Cell) {
        let a = below(c); // attached block
        def TO[s,c] <-> (T[c] and !BP[s,a]);
      }
    }
  }

  // Torch output propagation (simplified adjacency)
  shape TorchToCell[Sc, Cell, Dir6] : Bool;
  rule R_TORCH_OUTPUT {
    forall(s in Sc) {
      forall((c,d) in Cell * Dir6) {
        let n = neigh6(c,d);
        let a = below(c);

        // 토치가 켜져 있고, 이웃이 존재할 때 그 이웃에 소스를 제공
        def TorchToCell[s,c,d] <-> (TO[s,c] and (n != null));

        // attached block(아래 블록)에는 파워 주지 않음
        // (exclude 스타일 대신 직접 컷)
        require (d == D) -> (TorchToCell[s,c,d] == 0);

        // 토치 출력은 이웃 셀을 “강한 소스”로 만듦(더스트 15-limit의 시작점)
        add BaseSrc[s,n]  += TorchToCell(s,c,d);

        // 토치 출력은 이웃 솔리드 블록도 파워 원인으로 줌
        add BlockSrc[s,n] += TorchToCell(s,c,d);
      }
    }
  }

  // ============================================================
  // Repeater semantics (수평 4방향)
  // - RepIn = (뒤 셀의 DP) or (뒤 셀의 BP)
  // - RO = R && RepIn
  // - RO가 켜지면 front 셀에 BaseSrc 생성 (거리 리셋)
  // ============================================================
  rule R_REPEATER {
    forall(s in Sc) {
      forall((c,hd) in Cell * HDir) {
        let b = back(c,hd);
        let f = front(c,hd);

        def RepIn[s,c,hd] <-> OR{ DP[s,b], BP[s,b] };
        def RO[s,c,hd] <-> (R[c,hd] and RepIn[s,c,hd]);

        // repeater output is strong source at front cell
        add BaseSrc[s,f]  += RO(s,c,hd);
        add BlockSrc[s,f] += RO(s,c,hd);
      }
    }
  }

  // ============================================================
  // Dust connectivity (간소화 버전)
  // - dust edge는 수평 4방향으로만 전파(Conn은 D && D(neighbor))
  // - (실제 MC의 axis/cross 컷은 생략)
  // ============================================================
  shape Conn[Cell, HDir] : Bool;
  rule R_DUST_CONN {
    forall((c,d) in Cell * HDir) {
      let n = neighH(c,d);
      def Conn[c,d] <-> (D[c] and D[n]);
    }
  }

  // ============================================================
  // Dust 15-block limit via reachability
  // - Reach[s,0,c] <-> OR{BaseSrc[s,c]}
  // - Reach[s,t,c] -> D[c] && (exists neighbor dust with Reach[s,t-1,*] && Conn)
  // - DP[s,c] <-> D[c] && OR_{t=0..15} Reach[s,t,c]
  // ============================================================
  shape PredAny[Sc, Step, Cell] : Bool;

  rule R_DUST_15_LIMIT {
    forall(s in Sc) {
      forall(c in Cell) {
        def Reach[s,0,c] <-> OR{ BaseSrc[s,c] };
      }

      forall(t in Step) where (t > 0) {
        forall(c in Cell) {
          def PredAny[s,t,c] <-> OR{
            (Reach[s,t-1, neighH(c,N)] and Conn[neighH(c,N), S]),
            (Reach[s,t-1, neighH(c,S)] and Conn[neighH(c,S), N]),
            (Reach[s,t-1, neighH(c,E)] and Conn[neighH(c,E), W]),
            (Reach[s,t-1, neighH(c,W)] and Conn[neighH(c,W), E])
          };
          require Reach[s,t,c] -> (D[c] and PredAny[s,t,c]);
        }
      }

      forall(c in Cell) {
        def DP[s,c] <-> (D[c] and OR{
          Reach[s,0,c], Reach[s,1,c], Reach[s,2,c], Reach[s,3,c],
          Reach[s,4,c], Reach[s,5,c], Reach[s,6,c], Reach[s,7,c],
          Reach[s,8,c], Reach[s,9,c], Reach[s,10,c], Reach[s,11,c],
          Reach[s,12,c], Reach[s,13,c], Reach[s,14,c], Reach[s,15,c]
        });
      }
    }
  }

  // ============================================================
  // Dust -> Block power (간소화)
  // - dust가 켜져 있으면 인접(수평) 솔리드 블록을 파워 가능
  // ============================================================
  shape DustToBlock[Sc, Cell, HDir] : Bool;
  rule R_DUST_POWERS_BLOCK {
    forall(s in Sc) {
      forall((c,d) in Cell * HDir) {
        let n = neighH(c,d);
        def DustToBlock[s,c,d] <-> (DP[s,c] and S[n]);
        add BlockSrc[s,n] += DustToBlock(s,c,d);
      }
    }
  }

  // ============================================================
  // Block power definition
  // ============================================================
  rule R_BLOCK_POWER {
    forall(s in Sc) {
      forall(c in Cell) {
        def BP[s,c] <-> OR{ BlockSrc[s,c] };
      }
    }
  }

  // ============================================================
  // Objective knobs (PnR/게이트 합성에서 사용)
  // ============================================================
  param wS = 1.0;
  param wD = 1.0;
  param wT = 5.0;
  param wR = 2.0;

  objective minimize {
      wS * sum(c in Cell) S[c]
    + wD * sum(c in Cell) D[c]
    + wT * sum(c in Cell) T[c]
    + wR * sum((c,d) in Cell * HDir) R[c,d]
  }
}


// ============================================================
// 2) 상위 계층: component / netlist / pnr (가정 문법)
//    - component는 "bbox 내에서 Redstone3D_MCCore를 이용해 내부를 합성"
//    - pnr는 "인스턴스 배치 + net routing"을 Redstone3D_MCCore 위에서 푼다
// ============================================================

library GateLib {

  component NotGate {
    port IN  : Port1;
    port OUT : Port1;
    param bbox_w : Int; param bbox_h : Int; param bbox_d : Int;

    // 내부는 Redstone3D_MCCore 의미론으로 합성
    synthesize using Redstone3D_MCCore within BBox(bbox_w, bbox_h, bbox_d) {
      // 포트를 내부 Observe 포인트에 연결(가정)
      bind Observe(P_IN,  s) == ObservePort(IN,  s);
      bind Observe(P_OUT, s) == ObservePort(OUT, s);

      // NOT 진리표
      force Observe(P_IN,  s=0) == 0;
      force Observe(P_IN,  s=1) == 1;
      force Observe(P_OUT, s=0) == 1;
      force Observe(P_OUT, s=1) == 0;

      // (선택) 부품 제한/가중치 조정 가능
      allow { Solid, Dust, Torch, Repeater };
      objective minimize { PartsCost };
    }
  }

  component OrGate {
    port A   : Port1;
    port B   : Port1;
    port OUT : Port1;
    param bbox_w : Int; param bbox_h : Int; param bbox_d : Int;

    synthesize using Redstone3D_MCCore within BBox(bbox_w, bbox_h, bbox_d) {
      scenario Sc in {0,1,2,3}; // 00,01,10,11
      bind Observe(A_PIN,   s) == ObservePort(A,   s);
      bind Observe(B_PIN,   s) == ObservePort(B,   s);
      bind Observe(OUT_PIN, s) == ObservePort(OUT, s);

      force Observe(A_PIN, s=0)==0; force Observe(B_PIN, s=0)==0; force Observe(OUT_PIN, s=0)==0;
      force Observe(A_PIN, s=1)==0; force Observe(B_PIN, s=1)==1; force Observe(OUT_PIN, s=1)==1;
      force Observe(A_PIN, s=2)==1; force Observe(B_PIN, s=2)==0; force Observe(OUT_PIN, s=2)==1;
      force Observe(A_PIN, s=3)==1; force Observe(B_PIN, s=3)==1; force Observe(OUT_PIN, s=3)==1;

      allow { Solid, Dust, Torch, Repeater };
      objective minimize { PartsCost };
    }
  }
}


// ============================================================
// 3) 논리 넷리스트: XOR를 NOT/OR만으로 합성(예시)
//    XOR = (A|B) & ~(A&B)
//    AND(X,Y) = NOT( OR(NOT X, NOT Y) )
// ============================================================
design XorNetlist using GateLib {
  net A, B, OUT;
  net nA, nB, t_or, t_nor, t_and, nX, nY, nnY, t_nor2;

  inst g_nA  : NotGate(bbox_w=7, bbox_h=5, bbox_d=7);
  inst g_nB  : NotGate(bbox_w=7, bbox_h=5, bbox_d=7);
  inst g_or1 : OrGate (bbox_w=9, bbox_h=5, bbox_d=9);

  inst g_or2 : OrGate (bbox_w=9, bbox_h=5, bbox_d=9);
  inst g_and : NotGate(bbox_w=7, bbox_h=5, bbox_d=7);

  inst g_nY  : NotGate(bbox_w=7, bbox_h=5, bbox_d=7);
  inst g_nX  : NotGate(bbox_w=7, bbox_h=5, bbox_d=7);
  inst g_nnY : NotGate(bbox_w=7, bbox_h=5, bbox_d=7);

  inst g_or3 : OrGate (bbox_w=9, bbox_h=5, bbox_d=9);
  inst g_out : NotGate(bbox_w=7, bbox_h=5, bbox_d=7);

  // wiring
  connect A -> g_nA.IN;
  connect B -> g_nB.IN;
  connect g_nA.OUT -> nA;
  connect g_nB.OUT -> nB;

  connect A -> g_or1.A;
  connect B -> g_or1.B;
  connect g_or1.OUT -> t_or;

  // t_and = AND(A,B) = NOT( OR(nA,nB) )
  connect nA -> g_or2.A;
  connect nB -> g_or2.B;
  connect g_or2.OUT -> t_nor;
  connect t_nor -> g_and.IN;
  connect g_and.OUT -> t_and;

  // nY = NOT(t_and)
  connect t_and -> g_nY.IN;
  connect g_nY.OUT -> nY;

  // nX = NOT(t_or)
  connect t_or -> g_nX.IN;
  connect g_nX.OUT -> nX;

  // nnY = NOT(nY)
  connect nY -> g_nnY.IN;
  connect g_nnY.OUT -> nnY;

  // OUT = AND(t_or, nY) = NOT( OR(nX, nnY) )
  connect nX  -> g_or3.A;
  connect nnY -> g_or3.B;
  connect g_or3.OUT -> t_nor2;
  connect t_nor2 -> g_out.IN;
  connect g_out.OUT -> OUT;
}


// ============================================================
// 4) PnR: 인스턴스 배치 + net 라우팅(더스트/리피터)로 구현
//    - 라우팅은 Redstone3D_MCCore의 dust 15-limit + repeater reset을 자동으로 따름
// ============================================================
pnr XorPnR uses Redstone3D_MCCore {

  region Board = Box(x=0..59, y=0..9, z=0..59);

  // 외부 핀 좌표(3D)
  pin A_pin   at ( 2,2, 8);
  pin B_pin   at ( 2,2,12);
  pin OUT_pin at (56,2,10);

  bind_net A   to A_pin;
  bind_net B   to B_pin;
  bind_net OUT to OUT_pin;

  place_instances {
    place XorNetlist.g_nA  in Board allow_rotations {0,90,180,270};
    place XorNetlist.g_nB  in Board allow_rotations {0,90,180,270};
    place XorNetlist.g_or1 in Board allow_rotations {0,90,180,270};
    place XorNetlist.g_or2 in Board allow_rotations {0,90,180,270};
    place XorNetlist.g_and in Board allow_rotations {0,90,180,270};
    place XorNetlist.g_nY  in Board allow_rotations {0,90,180,270};
    place XorNetlist.g_nX  in Board allow_rotations {0,90,180,270};
    place XorNetlist.g_nnY in Board allow_rotations {0,90,180,270};
    place XorNetlist.g_or3 in Board allow_rotations {0,90,180,270};
    place XorNetlist.g_out in Board allow_rotations {0,90,180,270};

    require no_overlap(all_instances);
  }

  // net routing: 더스트/리피터만 사용(토치는 gate 내부 합성에만 쓰게 하고 싶으면 여기서 금지)
  route_nets {
    route net A    using {Dust, Repeater} connect {A_pin, XorNetlist.g_nA.IN, XorNetlist.g_or1.A};
    route net B    using {Dust, Repeater} connect {B_pin, XorNetlist.g_nB.IN, XorNetlist.g_or1.B};

    route net nA   using {Dust, Repeater} connect {XorNetlist.g_nA.OUT, XorNetlist.g_or2.A};
    route net nB   using {Dust, Repeater} connect {XorNetlist.g_nB.OUT, XorNetlist.g_or2.B};

    route net t_or using {Dust, Repeater} connect {XorNetlist.g_or1.OUT, XorNetlist.g_nX.IN};

    route net t_nor using {Dust, Repeater} connect {XorNetlist.g_or2.OUT, XorNetlist.g_and.IN};
    route net t_and using {Dust, Repeater} connect {XorNetlist.g_and.OUT, XorNetlist.g_nY.IN};

    route net nY   using {Dust, Repeater} connect {XorNetlist.g_nY.OUT, XorNetlist.g_nnY.IN};
    route net nnY  using {Dust, Repeater} connect {XorNetlist.g_nnY.OUT, XorNetlist.g_or3.B};
    route net nX   using {Dust, Repeater} connect {XorNetlist.g_nX.OUT, XorNetlist.g_or3.A};

    route net t_nor2 using {Dust, Repeater} connect {XorNetlist.g_or3.OUT, XorNetlist.g_out.IN};

    route net OUT  using {Dust, Repeater} connect {XorNetlist.g_out.OUT, OUT_pin};
  }

  // 전체 비용: gate 내부 비용 + 배선 비용
  objective minimize {
      sum(inst in all_instances) inst.InternalPartsCost
    + wire_cost(sum(all_routed_cells))
    + repeater_cost(sum(all_repeaters))
    + area_cost(bounding_box(all_used_cells))
  }
}

[rollrat]

// ============================================================
// RedstoneSeq3D_Core (PnR + 순차회로용 코어)
// - Cell = (x,y,z) 3D 격자
// - 부품: Solid, Dust, Torch(standing), Repeater
// - 시간: Tick t=0..H
// - 더스트 15블록 한계: 각 tick 내에서 Reach[k=0..15]로 “강한 소스(BaseSrc)”로부터
//   dust-edge를 최대 15번만 따라가며 DP[t]를 결정
// - Torch / Repeater는 1 tick 지연(TO[t]는 BP[t-1]에 의해 결정, RO[t]는 입력[t-1])
// ============================================================
model RedstoneSeq3D_Core {

  // -------------------------
  // 0) Space / Topology
  // -------------------------
  index Cell = (x,y,z) in Grid;

  enum Dir6 { N,E,S,W,U,D }
  enum HDir { N,E,S,W }

  fn neigh6(c:Cell, d:Dir6) -> Cell?; // 없으면 null (경계)
  fn neighH(c:Cell, d:HDir) -> Cell?;
  fn below(c:Cell) -> Cell?;          // (x,y-1,z) or null

  fn back(c:Cell, d:HDir)  -> Cell?;
  fn front(c:Cell, d:HDir) -> Cell?;

  // -------------------------
  // 1) Time + Scenarios
  // -------------------------
  param H : Int = 12;          // tick horizon
  index Tick = t in 0..H;

  // dust limit “15”
  index Step = k in 0..15;

  // 여러 입력 트레이스를 동시에 만족시키는 방식으로 검증/합성
  // (여기서는 인스턴스에서 enum으로 구체화한다고 가정)
  scenario Sc;

  // -------------------------
  // 2) Placement (world blocks)
  // -------------------------
  // 주의: 이 모델은 "부품은 공기 칸에 있고, 아래에 솔리드가 받쳐준다"는 표현을 쓴다.
  // - S[c]는 "그 칸 자체가 솔리드 블록"
  // - D/T/R는 "공기 칸에 놓이는 부품"으로 보고, 아래 칸이 솔리드여야 함.
  place S[Cell] : Solid;
  place D[Cell] : Dust;
  place T[Cell] : Torch;                 // standing torch
  place R[Cell, HDir] : Repeater;

  // -------------------------
  // 3) State (per scenario, per tick)
  // -------------------------
  state BP[Sc, Tick, Cell] : Bool;        // 블록 파워(솔리드 칸에 의미 있음)
  state DP[Sc, Tick, Cell] : Bool;        // 더스트 ON(부품 칸)
  state TO[Sc, Tick, Cell] : Bool;        // 토치 ON(부품 칸)
  state RepIn[Sc, Tick, Cell, HDir] : Bool;
  state RO[Sc, Tick, Cell, HDir] : Bool;  // 리피터 출력(부품 칸)

  // dust 15-limit reachability (tick 내부에서만 사용)
  state Reach[Sc, Tick, Step, Cell] : Bool;

  // -------------------------
  // 4) Source sets (원인 집합)
  // -------------------------
  sources BaseSrc[Sc, Tick, Cell]  : SrcSet;  // 강한 소스(입력/토치출력/리피터출력) -> dust reach 시작점
  sources BlockSrc[Sc, Tick, Cell] : SrcSet;  // 블록 파워 원인(토치/더스트 등)

  // -------------------------
  // 5) Hard constraints: packing + support
  // -------------------------
  rule R_PACKING_SUPPORT {
    forall(c in Cell) {
      // 같은 칸에는 하나만(대충)
      require S[c] + D[c] + T[c] + sum(d in HDir) R[c,d] <= 1;

      // 리피터 방향 1개 이하
      require sum(d in HDir) R[c,d] <= 1;

      // D/T/R는 아래에 솔리드 필요
      let b = below(c);
      require D[c] -> S[b];
      require T[c] -> S[b];
      forall(d in HDir) { require R[c,d] -> S[b]; }
    }
  }

  // -------------------------
  // 6) Domain linking (state <= placement)
  // -------------------------
  rule R_DOMAIN {
    forall(s in Sc) {
      forall(t in Tick) {
        forall(c in Cell) {
          require DP[s,t,c] -> D[c];
          require TO[s,t,c] -> T[c];
          require BP[s,t,c] -> S[c];
        }
        forall((c,d) in Cell * HDir) {
          require RO[s,t,c,d] -> R[c,d];
        }
      }
    }
  }

  // ============================================================
  // A) Torch semantics (1 tick delay)
  // - standing torch at c is attached to below(c)
  // - 토치 ON은 (T[c] && !BP[t-1, attached]) 로 둬서 1 tick 지연 모델링
  // ============================================================
  rule R_TORCH_DELAY_INVERT {
    forall(s in Sc) {
      // t=0에서는 이전 tick이 없으니 토치 출력은 0으로 초기화(보수적)
      forall(c in Cell) { force TO[s,0,c] == 0; }

      forall(t in Tick) where (t > 0) {
        forall(c in Cell) {
          let a = below(c); // attached block
          def TO[s,t,c] <-> (T[c] and !BP[s,t-1,a]);
        }
      }
    }
  }

  // Torch output -> BaseSrc + BlockSrc to neighbors (attached block 제외)
  shape TorchToCell[Sc, Tick, Cell, Dir6] : Bool;
  rule R_TORCH_OUTPUT {
    forall(s in Sc) {
      forall(t in Tick) {
        forall((c,dir) in Cell * Dir6) {
          let n = neigh6(c,dir);

          // 토치가 켜져 있으면 주변으로 전력 공급(근사)
          def TorchToCell[s,t,c,dir] <-> (TO[s,t,c] and (n != null));

          // attached block(below)로는 파워 주지 않음
          // standing torch attached는 DOWN 방향이므로 컷
          require (dir == D) -> (TorchToCell[s,t,c,dir] == 0);

          add BaseSrc[s,t,n]  += TorchToCell(s,t,c,dir);
          add BlockSrc[s,t,n] += TorchToCell(s,t,c,dir);
        }
      }
    }
  }

  // ============================================================
  // B) Repeater semantics (1 tick delay)
  // - RepIn[t] = DP[t-1,back] OR BP[t-1,back]
  // - RO[t]    = R && RepIn[t]
  // - RO[t]가 켜지면 front 셀에 BaseSrc(강한 소스) 생성 (거리 리셋)
  // ============================================================
  rule R_REPEATER_DELAY {
    forall(s in Sc) {
      // t=0 출력 0
      forall((c,d) in Cell * HDir) { force RO[s,0,c,d] == 0; }

      forall(t in Tick) where (t > 0) {
        forall((c,d) in Cell * HDir) {
          let b = back(c,d);
          let f = front(c,d);

          def RepIn[s,t,c,d] <-> OR{ DP[s,t-1,b], BP[s,t-1,b] };
          def RO[s,t,c,d] <-> (R[c,d] and RepIn[s,t,c,d]);

          add BaseSrc[s,t,f]  += RO(s,t,c,d);
          add BlockSrc[s,t,f] += RO(s,t,c,d);
        }
      }
    }
  }

  // ============================================================
  // C) Dust connectivity (간단 4-neighbor)
  // - 실제 MC의 axis/cross 컷은 생략(필요하면 확장)
  // ============================================================
  shape Conn[Cell, HDir] : Bool;
  rule R_DUST_CONN {
    forall((c,d) in Cell * HDir) {
      let n = neighH(c,d);
      def Conn[c,d] <-> (D[c] and D[n] and (n != null));
    }
  }

  // ============================================================
  // D) Dust 15-limit (tick 내부 reachability)
  // - Reach[t,0,c]  = OR{BaseSrc[t,c]}
  // - Reach[t,k,c] -> D[c] && exists neighbor dust with Reach[t,k-1,*] && Conn
  // - DP[t,c]       = D[c] && OR_{k=0..15} Reach[t,k,c]
  // ============================================================
  shape PredAny[Sc, Tick, Step, Cell] : Bool;

  rule R_DUST_15_LIMIT {
    forall(s in Sc) {
      forall(t in Tick) {
        forall(c in Cell) {
          def Reach[s,t,0,c] <-> OR{ BaseSrc[s,t,c] };
        }

        forall(k in Step) where (k > 0) {
          forall(c in Cell) {
            // 역방향 참조: (이웃이 c로 연결되어 있으면) 이웃에서 c로 들어올 수 있음
            def PredAny[s,t,k,c] <-> OR{
              (Reach[s,t,k-1, neighH(c,N)] and Conn[neighH(c,N), S]),
              (Reach[s,t,k-1, neighH(c,S)] and Conn[neighH(c,S), N]),
              (Reach[s,t,k-1, neighH(c,E)] and Conn[neighH(c,E), W]),
              (Reach[s,t,k-1, neighH(c,W)] and Conn[neighH(c,W), E])
            };

            require Reach[s,t,k,c] -> (D[c] and PredAny[s,t,k,c]);
          }
        }

        forall(c in Cell) {
          def DP[s,t,c] <-> (D[c] and OR{
            Reach[s,t,0,c], Reach[s,t,1,c], Reach[s,t,2,c], Reach[s,t,3,c],
            Reach[s,t,4,c], Reach[s,t,5,c], Reach[s,t,6,c], Reach[s,t,7,c],
            Reach[s,t,8,c], Reach[s,t,9,c], Reach[s,t,10,c], Reach[s,t,11,c],
            Reach[s,t,12,c], Reach[s,t,13,c], Reach[s,t,14,c], Reach[s,t,15,c]
          });
        }
      }
    }
  }

  // ============================================================
  // E) Dust -> Block power (근사)
  //  1) 더스트는 “자기 아래 블록”을 파워할 수 있음
  //  2) 더스트는 수평 인접 블록도 파워할 수 있다고 근사
  // ============================================================
  shape DustPowersBelow[Sc, Tick, Cell] : Bool;
  shape DustPowersSide[Sc, Tick, Cell, HDir] : Bool;

  rule R_DUST_POWERS_BLOCK {
    forall(s in Sc) {
      forall(t in Tick) {
        forall(c in Cell) {
          let b = below(c);
          def DustPowersBelow[s,t,c] <-> (DP[s,t,c] and S[b]);
          add BlockSrc[s,t,b] += DustPowersBelow(s,t,c);
        }

        forall((c,d) in Cell * HDir) {
          let n = neighH(c,d);
          def DustPowersSide[s,t,c,d] <-> (DP[s,t,c] and S[n]);
          add BlockSrc[s,t,n] += DustPowersSide(s,t,c,d);
        }
      }
    }
  }

  // ============================================================
  // F) Block power definition
  // ============================================================
  rule R_BLOCK_POWER {
    forall(s in Sc) {
      forall(t in Tick) {
        forall(c in Cell) {
          def BP[s,t,c] <-> OR{ BlockSrc[s,t,c] };
        }
      }
    }
  }

  // -------------------------
  // Objective (부품 최소화)
  // -------------------------
  param wS = 1.0;
  param wD = 1.0;
  param wT = 5.0;
  param wR = 2.0;

  objective minimize {
      wS * sum(c in Cell) S[c]
    + wD * sum(c in Cell) D[c]
    + wT * sum(c in Cell) T[c]
    + wR * sum((c,d) in Cell * HDir) R[c,d]
  }
}


// ============================================================
// RS Latch Synthesis Instance (NOR형 행동을 “트레이스”로 강제)
// - S, R 입력 트레이스를 여러 개 주고, Q/QB 출력이 latch 동작을 하도록 요구
// - solver가 S/D/T/R 배치를 찾아서 조건을 만족해야 함
// ============================================================
model RSLatch_Solve extends RedstoneSeq3D_Core {

  // -------------------------
  // 0) Traces (입력 시나리오들)
  // -------------------------
  enum Trace { SET, RESET, HOLD0 }
  scenario Sc = Trace;

  // -------------------------
  // 1) 핀 좌표(3D) — 고정(외부에서 바꿀 수 있음)
  // -------------------------
  const CS   : Cell = (2,2,2);   // S 입력 더스트 위치
  const CR   : Cell = (2,2,6);   // R 입력 더스트 위치
  const CQ   : Cell = (12,2,2);  // Q 출력 관측 더스트 위치
  const CQB  : Cell = (12,2,6);  // QB 출력 관측 더스트 위치

  // -------------------------
  // 2) 입력 트레이스(시간에 따른 S/R)
  // -------------------------
  state Ssig[Trace, Tick] : Bool;
  state Rsig[Trace, Tick] : Bool;

  rule R_INPUT_TRACES {
    // 금지 입력: S=R=1
    forall(s in Trace) {
      forall(t in Tick) {
        require Ssig[s,t] + Rsig[s,t] <= 1;
      }
    }

    // ---- Trace: SET ----
    // 0~1 tick: R=1로 초기화(리셋) -> Q=0 유도
    // 2~3 tick: S=1 펄스 -> Q=1 유도
    // 이후 hold
    force Rsig[SET,0]==1; force Rsig[SET,1]==1;
    force Ssig[SET,0]==0; force Ssig[SET,1]==0;

    force Ssig[SET,2]==1; force Ssig[SET,3]==1;
    force Rsig[SET,2]==0; force Rsig[SET,3]==0;

    forall(t in Tick) where (t >= 4) {
      force Ssig[SET,t]==0;
      force Rsig[SET,t]==0;
    }

    // ---- Trace: RESET ----
    // 0~1 tick: S=1로 초기화(셋) -> Q=1 유도
    // 2~3 tick: R=1 펄스 -> Q=0 유도
    // 이후 hold
    force Ssig[RESET,0]==1; force Ssig[RESET,1]==1;
    force Rsig[RESET,0]==0; force Rsig[RESET,1]==0;

    force Rsig[RESET,2]==1; force Rsig[RESET,3]==1;
    force Ssig[RESET,2]==0; force Ssig[RESET,3]==0;

    forall(t in Tick) where (t >= 4) {
      force Ssig[RESET,t]==0;
      force Rsig[RESET,t]==0;
    }

    // ---- Trace: HOLD0 ----
    // 0~1 tick: R=1로 초기화해서 Q=0 만든 뒤
    // 이후 hold(0,0)에서 유지되는지 확인
    force Rsig[HOLD0,0]==1; force Rsig[HOLD0,1]==1;
    force Ssig[HOLD0,0]==0; force Ssig[HOLD0,1]==0;

    forall(t in Tick) where (t >= 2) {
      force Ssig[HOLD0,t]==0;
      force Rsig[HOLD0,t]==0;
    }
  }

  // -------------------------
  // 3) 입력을 BaseSrc로 주입 + 출력 관측 정의
  // -------------------------
  rule R_PIN_BINDINGS {
    // 핀 칸에는 더스트를 깔아둔다(관측/주입이 쉬움)
    force D[CS]  == 1;
    force D[CR]  == 1;
    force D[CQ]  == 1;
    force D[CQB] == 1;

    // 받침 블록도 필요(코어의 support 규칙 때문에)
    force S[below(CS)]  == 1;
    force S[below(CR)]  == 1;
    force S[below(CQ)]  == 1;
    force S[below(CQB)] == 1;

    forall(s in Trace) {
      forall(t in Tick) {
        // 입력=1이면 해당 셀을 강한 소스로 만든다
        add BaseSrc[s,t,CS] += Ssig(s,t);
        add BaseSrc[s,t,CR] += Rsig(s,t);

        // OUT 관측은 더스트 ON으로 본다
        force Observe(P_OUT, s) == 0; // (사용 안 하면 무시해도 됨)
      }
    }
  }

  // -------------------------
  // 4) RS Latch 동작 요구(시간 기반)
  // -------------------------
  // 이 코어는 토치/리피터가 1 tick 지연이라 “반응 지연”이 생김.
  // 따라서 안정적으로 기대하는 tick부터 Q/QB를 강제한다.
  param STABLE_FROM : Int = 6;

  rule R_EXPECTED_BEHAVIOR {
    forall(t in Tick) where (t >= STABLE_FROM) {
      // SET trace: 최종 Q=1, QB=0 유지
      force DP[SET,t,CQ]  == 1;
      force DP[SET,t,CQB] == 0;

      // RESET trace: 최종 Q=0, QB=1 유지
      force DP[RESET,t,CQ]  == 0;
      force DP[RESET,t,CQB] == 1;

      // HOLD0 trace: 최종 Q=0, QB=1 유지
      force DP[HOLD0,t,CQ]  == 0;
      force DP[HOLD0,t,CQB] == 1;
    }

    // 보수 관계(항상 Q xor QB)
    forall(s in Trace) {
      forall(t in Tick) {
        require DP[s,t,CQ] + DP[s,t,CQB] == 1;
      }
    }
  }

  // -------------------------
  // 5) 회로 크기/영역 제한(필수는 아니지만 성능에 중요)
  // -------------------------
  // 예: bounding box 밖은 아예 못 쓰게 강제(외부에서 파라미터화 가능)
  param X0=0; param X1=16;
  param Y0=0; param Y1=4;
  param Z0=0; param Z1=8;

  rule R_BOUNDING_BOX {
    forall(c in Cell) {
      let inBox = (x(c) >= X0 and x(c) <= X1 and
                   y(c) >= Y0 and y(c) <= Y1 and
                   z(c) >= Z0 and z(c) <= Z1);

      // 박스 밖은 아무것도 놓지 말기
      require (!inBox) -> (S[c]==0 and D[c]==0 and T[c]==0 and sum(d in HDir) R[c,d]==0);
    }
  }

  // -------------------------
  // 6) 선택: “부품 제한” (예: 리피터 없이도 되나 확인)
  // -------------------------
  feature NO_REPEATER {
    // 필요하면 켜서 디버깅
    // forall((c,d) in Cell*HDir) { force R[c,d]==0; }
  }

  // objective는 코어에서 상속(minimize parts)
}