module Ex2 where

data Nat : Set where
  zero : Nat
  suc : Nat -> Nat

{-# BUILTIN NATURAL Nat #-}

data List (A : Set) : Set where
  [] : List A
  _::_ : A -> List A -> List A

infixr 40 _::_

_++_ : {A : Set} -> List A -> List A -> List A
_++_ [] b = b
_++_ (a :: as) b = a :: (as ++ b)

appx : ∀ {A} → Nat → List A → List A
appx zero _ = []
appx (suc x) a = a ++ (appx x a)

length : { A : Set } -> List A -> Nat
length [] = zero
length (_ :: as) = suc (length as)

firstX : ∀ {A} → Nat → List A → List A
firstX x [] = []
firstX zero l = []
firstX (suc x) (v :: l)  = v :: (firstX x l)


data _==_ { A : Set} (x : A) : A -> Set where
  refl : x == x

--core module is locked, and must be referenced through functions
module Core where
  private
    --Flag is significant to outer core and specifies some command.
    --since it's private, only functions within Core can create it
    data Flag : Set where
      flag : Flag


  call : (l : List Nat) -> length l == 10 -> Flag
  call x _ = flag

--attacker may make any changes here:
module Scratch where
  l : List Nat
  l = appx 500 (1 :: 2 :: 3 :: [])

  callInstance = Core.call l {! refl {x = (length!}