lunalunaa

# Google CTF 2023
# mytls challenge: https://capturetheflag.withgoogle.com/challenges/crypto-mytls

import binascii
from cryptography import x509
from cryptography.hazmat.primitives import serialization
from cryptography.hazmat.primitives import hashes
from cryptography.hazmat.primitives import hmac
from cryptography.hazmat.primitives.asymmetric import ec
from cryptography.hazmat.primitives.ciphers import Cipher, algorithms, modes

lunalunaa

-- universe polymorphism
module UnivPoly where

-- core language
type Ix = Int

data Term
  = Var Ix
  | Abs Term
  | App Term Term

lunalunaa

{-# LANGUAGE LambdaCase #-}
import Data.Maybe

data Ty
    = Base
    | TyArr Ty Ty
    deriving (Show, Eq)

data Term
    = TmVar Integer

lunalunaa

{-# LANGUAGE LambdaCase #-}

module MonoJSonParser where

import Data.Char
import Control.Monad
import Control.Applicative
import Data.Foldable
import Data.Maybe

lunalunaa

data Term
    = TmVar Integer
    | TmAbs String Term
    | TmApp Term Term
    deriving (Show, Eq)

termShift :: Integer -> Term -> Term
termShift d = walk 0
  where
    walk :: Integer -> Term -> Term

lunalunaa

data Term
    = TmVar Integer
    | TmAbs String Term
    | TmApp Term Term
    deriving (Show, Eq)

termShift :: Integer -> Term -> Term
termShift d = walk 0
  where
    walk :: Integer -> Term -> Term

lunalunaa

(******************************************************)
(** //// Validation of the "filter" Function ////     *)
(******************************************************)

Require Import List Bool Lt.

Section Filter.


(*////////////////////////////////////////////////////*)

lunalunaa

Keybase proof

I hereby claim:

• I am weitaoxin on github.
• I am triplethink (https://keybase.io/triplethink) on keybase.
• I have a public key ASDY5LYhbea8RwT4HrbmG6DCKsKb8XmE_JKGJC0A1X9lcQo

To claim this, I am signing this object: