/-
  Generated by lsc from majority.ts
  Do not edit — re-run `lsc gen` to regenerate.
-/
import «majority.spec»

set_option loom.semantics.termination "total"
set_option loom.semantics.choice "demonic"

method occOf (arr : Array Int) (x : Int) (n : Nat) return (res : Int)
  require 0 ≤ n
  require n ≤ arr.size
  do
    return Pure.occOf arr x n

method majority (arr : Array Int) return (res : Int)
  require ∀ k : Nat, k < arr.size → arr[k]! ≥ 0
  ensures res = -1 ∨ res ≥ 0 ∧ 2 * Pure.occOf arr res arr.size > arr.size
  ensures (∃ x : Nat, 2 * Pure.occOf arr x arr.size > arr.size) → res ≠ -1
  do
    let mut cand : Int := 0
    let mut cnt : Int := 0
    let mut i : Nat := 0
    while i < arr.size
      invariant 0 ≤ i
      invariant i ≤ arr.size
      invariant cnt ≥ 0
      invariant cand ≥ 0
      invariant 2 * Pure.occOf arr cand i ≤ i + cnt
      invariant ∀ y : Int, y ≠ cand → 2 * Pure.occOf arr y i ≤ i - cnt
      decreasing arr.size - i
    do
      if cnt = 0 then
        cand := arr[i]!
        cnt := 1
      else if arr[i]! = cand then
        cnt := cnt + 1
      else
        cnt := cnt - 1
      i := i + 1
    let mut occ : Int := 0
    let mut j : Nat := 0
    while j < arr.size
      invariant 0 ≤ j
      invariant j ≤ arr.size
      invariant occ = Pure.occOf arr cand j
      decreasing arr.size - j
    do
      if arr[j]! = cand then
        occ := occ + 1
      j := j + 1
    if 2 * occ > arr.size then
      return cand
    else
      return -1