[Idris; Discussion] Easy escape hatches for subverting the totality checker (cheat)

[DonaldKellett]

Currently, it is very easy to subvert the totality checker in Idris by marking partial functions as total - see https://www.codewars.com/kumite/5c7fde0290438512c5ce7bac?sel=5c7fde0290438512c5ce7bac . This would place theorem-proving Kata in Idris in jeopardy since the only reason Idris kata are not expected to have random tests is because the type system is expected to automatically reject incorrect proofs (represented by ill-typed programs in Idris). With easy escape hatches like assert_total, believe_me and the like, fake proofs can be constructed in Idris as easily as in Haskell.

What should we do if we discover someone abusing these loopholes? Some potential suggestions:

1. It is the responsibility of the Kata author/translator in Idris to check the user solution for such escape hatches (how? maybe read solution file and check for terms like "assert" and "partial"?)
2. It should be treated like runner cheats in other languages with harsh penalties for offenders, e.g. perma-ban.

Feel free to chime in :smile: Special mentions: @ice1000 @MarisaKirisame (feel free to mention others if they are also interested in Idris on Codewars)

[ice1000]

Thumb up for

2. It should be treated like runner cheats in other languages.

[DonaldKellett]

Thumb up for

2. It should be treated like runner cheats in other languages with harsh penalties for offenders, e.g. perma-ban.

IMO this is probably the more sensible option since cheaters will probably find easy ways around simple regexes like /assert/ and /partial/ (if we know how to read/parse the solution file in Idris in the first place). We probably need to document this somewhere though.

[Voileexperiments]

2. It should be treated like runner cheats in other languages with harsh penalties for offenders, e.g. perma-ban.

Completely disagree, because this is too easy to happen. Type holes trigger this too (see https://github.com/Codewars/codewars-runner-cli/issues/711#issuecomment-470157252).

Also this should go to the runner repo. @kazk Please migrate this issue ;-)

[ice1000]

https://github.com/Codewars/codewars-runner-cli/issues/717

[ice1000]

I can pattern match on a hole and it still works

[ice1000]

It should be treated like runner cheats in other languages with harsh penalties for offenders, e.g. perma-ban.

Completely disagree, because this is too easy to happen. Type holes trigger this too (see Codewars/codewars-runner-cli#711 (comment)). Also this should go to the runner repo. @kazk Please migrate this issue ;-)

Then we can simply forbid this and ... just forbid this.

[Bubbler-4]

If we ban the use of partial/assert/holes/whatever altogether, won't it affect non-theorem-proving katas that require you to write partial functions by nature?

[ice1000]

If we ban the use of partial/assert/holes/whatever altogether, won't it affect non-theorem-proving katas that require you to write partial functions by nature?

No, partial functions are possible with the absense of %default total in tests. People don't need holes to write partial functions.

[Bubbler-4]

Another question. Suppose that we want to write A + B = B + A kata in Idris. If I write a line of test code

x : 3 + 5 = 5 + 3 -- just an example
x = plusCommutes 3 5 -- just an example

and a user tries to cheat with incomplete proof, which of the possible cheats can be caught with e.g. compile-time infinite loop or runtime crash?

[ice1000]

This won't be a compile time infinite proof due to totality. Runtime crash may not be caught due to erasure.

I suppose only type error can be caught.

[Bubbler-4]

Erm... looks like we have one more loophole, namely postulate (related SO question). Unlike typed holes, it is designed for assertions that aren't provable inside Idris, e.g. those about built-in types.

[ice1000]

Can we pattern match a postulated i.e. equality proof with Refl? Is it gonna work on earth?

[Bubbler-4]

No chance, even with properly proven ones.

plusComm : (a : Nat) -> (b : Nat) -> a + b = b + a
plusComm = plusCommutative

proofEval : {a : Nat} -> {b : Nat} -> (a + b = b + a) -> Nat
proofEval {a=a} {b=b} Refl = a + b

main : IO ()
main = do
  putStrLn "Compiled Successfully!"

  |
5 | proofEval {a=a} {b=b} Refl = a + b
  | ~~~~~~~~~
When checking left hand side of proofEval:
When checking an application of Main.proofEval:
        Type mismatch between
                plus b a = plus b a (Type of Refl)
        and
                a + b = b + a (Expected type)

        Specifically:
                Type mismatch between
                        plus b a
                and
                        plus a b

[ice1000]

Try this

proofEval : {a : Nat} -> {b : Nat} -> (a + b) -> (a + b = b + a) -> Nat
proofEval {a=a} {b=b} (b + a) Refl = a + b

[Bubbler-4]

No, Refl is not recognized as a constructor for a + b = b + a type.

Meanwhile, I found a way to catch postulate and holes using dependent tuples:

plusComm : (a : Nat) -> (b : Nat) -> a + b = b + a
plusComm = plusCommutative

proofEval : (a : Nat ** (b : Nat ** (a + b = b + a)))
proofEval = (1 ** (2 ** plusComm 1 2))

main : IO ()
main = do
  putStrLn "Compiled Successfully!"
  print $ fst $ snd proofEval -- `print $ fst proofEval` doesn't work for the purpose

Output:

Compiled Successfully!
2

Some possible fake proofs and the results:

-- typed hole
plusComm : (a : Nat) -> (b : Nat) -> a + b = b + a
plusComm = ?plusComm
-- result: runtime error (abort)
ABORT: Attempt to evaluate hole Main.plusComm1

-- postulate
postulate plusComm : (a : Nat) -> (b : Nat) -> a + b = b + a
-- result: compilation error
reachable postulates:
  Main.plusComm

But assert_total and believe_me are not caught. Can we remove those definitions (assert_total, believe_me, really_believe_me) from the Idris stdlib?

[ice1000]

This is really cool, admire

[ice1000]

Banned postulate in https://www.codewars.com/kata/5c82b661562a2074bbeac980/discuss

[ice1000]

We should special mention this in some wiki or kata example test cases

[ice1000]

Banned postulate in https://www.codewars.com/kata/5c7fdf0b00718714fd002bd2/ as well

[Bubbler-4]

But assert_total and believe_me are not caught. Can we remove those definitions (assert_total, believe_me, really_believe_me) from the Idris stdlib?

On second thought, we can't remove assert_total because the stdlib itself (e.g. some Nat functions) depends on it. Then we probably really need source code pattern matching on them?

What if we put a line of bash script (say, grep) into the runner so that it refuses to run if the source contains one of assert or believe_me? IMO it's more gentle and overall better option than e.g. a perma-ban, if anything should be done on the runner side.

[kazk]

@Bubbler-4 Yeah, we can check if the solution contains any of those and consider failed. I don't know if there's a way to workaround, but that should be enough to prevent accidental cheating. We'll have false positives like assert_total in a comment, but that should be acceptable trade-off.

So disallow the following?

• assert_total
• believe_me
• really_belive_me

I'll probably still allow it to run and just mark it as failed, similar to the hole #717.

[Bubbler-4]

Yes, the three are the identified ones. I think we can disallow using the keyword postulate too - while it's catchable, the exact mechanism of catching it is unknown, so it may not be applicable to all cases.

Edit: Additional possible loophole functions (not tested):

• assert_unreachable
• assert_smaller
  • These two weaken the totality checker in some way
• prim__believe_me
  • Looks like the primitive version of believe_me

Edit: Yet another possible loophole functions:

• idris_crash: tested and works
• unsafePerformIO: tested and works in combination with any of System.exit, System.exitWith, System.exitFailure, System.exitSuccess
• unsafePerformPrimIO: not tested

[MarisaKirisame]

update: it turnout idris has so much loophole it is impossible. https://www.reddit.com/r/Idris/comments/b008b5/how_do_i_stop_people_from_writing_partial_program/

[Bubbler-4]

@MarisaKirisame That's exactly why we're going for pattern-matching on source code at #725.

In the (likely incomplete) list of possible loopholes, I tried to identify all the functions in the stdlib that open the access to a -> b while keeping it total (or faking it). For x -> Void functions (aka impossibility proofs), it's impossible to construct a value of type x in the first place (without introducing a new axiom, which in turn requires a use of postulate or other loophole functions).

[kazk]

I'm closing this because #725 is deployed and I think that's the most we can do at the moment. But feel free to continue the discussion here if necessary.