nkaretnikov

; test@test:~$ nasm -f elf64 -o call.o call.s
; test@test:~$ ld -o call call.o
; test@test:~$ ./call
; test@test:~$ echo $?
; 13
; test@test:~$
; test@test:~$ gdb -q call
; Reading symbols from call...(no debugging symbols found)...done.
; (gdb) b _start
; Breakpoint 1 at 0x400080

nkaretnikov

from idc      import *
from idaapi   import *
from idautils import *

counter = 0
lst = []
addr = 0x01073E62


# See idapython/src/examples/debughook.py

nkaretnikov

#include <stdio.h>                                                                                                                                                                  
#include <unistd.h>                                                                                                                                                                 
                                                                                                                                                                                    
int main()                                                                                                                                                                          
{                                                                                                                                                                                   
    int d = 0;                                                                                                         

nkaretnikov

class ConsLub (h :: *) (t :: [*]) (l :: [*]) | h t -> l where
  consLub :: h -> t -> l
  
{-
Data/HList/RecordAdv.hs:157:19:
    Expected a type, but ‘t’ has kind ‘[*]’
    In the type ‘h -> t -> l’
    In the class declaration for ‘ConsLub’
-}

nkaretnikov

nix-build -E "let nixpkgs = import <nixpkgs> {}; f = import ./default.nix; in nixpkgs.pkgs.haskellPackages.callPackage f {}"

nkaretnikov

module Sets where

-- Set.
-- A = {x : P(x)}
data PSet {A : Set} (P : A → Set) : Set where
  pset : ∀ {x : A} → P x → PSet P

-- Set membership.
_∈_ : {A : Set} → A → (A → Set) → Set
x ∈ p = p x

nkaretnikov

-- might be wrong
f p b g n = forM_ [0..n] $ \x -> putStrLn $ mconcat [ "x:", show x, ", res1:", show (b^x `mod` p), ", res2:", show (((b^x `mod` p) * g) `mod` p) ]
f' p b g n = sort $ concat $ flip fmap [0..n] $ \x -> [ (b^x `mod` p),(((b^x `mod` p) * g) `mod` p) ]
f'' p b g n =  flip fmap [0..n] $ \x -> (((b^x `mod` p) * g) `mod` p)
bin = \x -> showIntAtBase 2 $ intToDigit x ""

nkaretnikov

-- Set.
-- A = {x : P(x)}
data PSet (A : Set) {P : A → Set} : Set where
  pset : ∀ {x : A} → P x → PSet A

nkaretnikov

{-
Inductive and (P Q : Prop) : Prop :=
  conj : P -> Q -> (and P Q).
-}

data and {A : Set} {a : A} {P Q : A → Set} : P a → Q a → (A → Set) where
  conj : P a → Q a → and (P a) (Q a)
{-
Sets.agda:4,27-30
Set₁ != Set

nkaretnikov

*-assoc : ∀ a b c → (a * b) * c ≡ a * (b * c)
*-assoc zero     b c = refl
*-assoc (succ a) b c =
  *+-dist b (a * b) c ~ cong (λ x → b * c + x) (*-assoc a b c)