$ cat writeup.md…
$ cat writeup.md…
kitctf
Task: a holpy (HOL theorem prover) proof checker accepts a user-supplied proof and prints the flag if you can prove the const false with no hypotheses. Solution: chain an SMT-translation soundness bug (real_divide done in Python float, 2^54+2 / 2 collides to 2^53) to get a HOL-false-but-Z3-valid lemma, then exploit a dead axiom guard (list == int) to define false as that lemma, and discharge it with primitive kernel rules.
$ cat /etc/rate-limit
Rate limit reached (20 reads/hour per IP). Showing preview only — full content returns at the next hour roll-over.
The customer is always right. RIGHT? Experienced staff will tell you that customers are always worst case users. Just last week one customer proclaimed that pineapple does not belong on sushi pizza. Yeah I know, how could he? But the customer is always right. My friend fears for his sanity. So please help me work out the logic details for such an argument.
English summary: we are given checker.py, a proof checker built on a holpy fork (the HOL theorem prover in Python). It reads a hex-encoded JSON "proof" from the user, checks it, and if the checked theorem is the constant false with no hypotheses and no assumptions, it calls win() and prints the flag.
The flavor text is the spec: "the customer is always right" = the checker trusts the claimed theorem; "worst case users" = adversarial input; "work out the logic details for such an argument" = construct a (bogus) logical proof of falsehood. This is a soundness/explosion challenge: prove ⊢ false.
checker.py:
hex → bytes → UTF-8 JSON {"imports": [...], "content": [item, ...]}.basic.load_theory(imp) (failures only warned).items.parse_item, then:
thm item: monitor.check_proof(item, rewrite=False). If status is OK/ProofOK, run report = theory.thy.checked_extend(item.get_extension()).checked_extend.report:
if len(report.get_axioms()) > 1: exit(1)elif report.get_axioms() == 1 and item.ty != "thm": exit(1) ← dead code (see Bug 2)theorem_proves_false_unconditioned(thm), which is true iff the conclusion is the const false (prints as false/?false) with no assumptions and no hypotheses. If true → win().So: produce a thm item whose proof checks and whose theorem is ⊢ false (empty hyps/assums).
...
$ grep --similar