module postprocess

sig Heading {
  index: one Int
}

sig TocEntry {
  index: one Int,
  hash: one Hash
}

sig Hash {}

-- heading과 toc entry는 같은 인덱스로 1:1 매핑
fact indexAlignment {
  all h: Heading | one t: TocEntry | t.index = h.index
  all t: TocEntry | one h: Heading | h.index = t.index
}

-- 인덱스는 0부터 연속
fact contiguousIndices {
  all h: Heading | h.index >= 0
  all h: Heading | h.index < #Heading
}

-- 해시는 유일
fact uniqueHashes {
  all disj t1, t2: TocEntry | t1.hash != t2.hash
}

-- heading 수와 toc 수가 같으면 모든 heading에 정확히 하나의 해시가 대응
assert bijection {
  #Heading = #TocEntry implies
    all h: Heading | one t: TocEntry |
      t.index = h.index
}

-- 해시 충돌 없음
assert noHashCollision {
  all disj t1, t2: TocEntry | t1.hash != t2.hash
}

check bijection for 6 but 6 Int
check noHashCollision for 6