Unix forever!

DSR enhanced security and "formal verification" course

One single line that made functional programming languages popular:

tr -cs A-Za-z '\n' | tr A-Z a-z | sort | uniq -c | sort -rn | sed 10q (more in the text)

Introduction into formal proof systems

We're living i a multidimensional world with many constraints and conditions that make our life more comple

We have invented plenty of methods to find (or exclude) solutions.

Learn: "Positive people find solutions. Negative people find reasons"

To fully understand this course i highly recommend to read Wittgenstein's Tractatus Logico Philosophicus, Frege's Begriffsschrift and Principia Mathematica by Whitehead and Russell

https://en.wikipedia.org/wiki/Ludwig_Wittgenstein
https://en.wikipedia.org/wiki/Tractatus_Logico-Philosophicus
https://en.wikipedia.org/wiki/Begriffsschrift
https://en.wikipedia.org/wiki/Principia_Mathematica

  1. What's the semantic triple or "RDF triple"
  2. Why formal verification of algorithms is essential
  3. Geoff Sutcliffe: "Who killed Aunt Agatha"
  4. From simple gates to higher order functions (From NAND to TETRIS)
  5. Truth tables, Domain Driven Design, Panes, Impedance Missmatch
  6. Essential: What matrices have to do with graphs?
    1. GraphBLAS discovers hidden relationships within big data
      1. Giving matrix elements a weight - heavily used in AI!!!
      2. The commercial end of Redis-Graph
    2. Practical use of GraphBLAS or OpenBLAS
      1. What building A² reveals
      2. Calculating A³ reveals clusters in community structures or social networks
      3. The inner structures of souce code
      4. The Girvan Newman algorithm
    3. Enabling massive deep neural networks with the GraphBLAS
    4. The Hindley - Milner type inference
  7. Essential: What are co- and contravriant types?
  8. The inventor of category theory: Aristotele's 10 categories
  9. Essential: Law of excluded middle - "Tertium non datur!"
  10. The "Tertium non datur!" (and other findings) in Agda:
  11. The famous Y-combinator
  12. The need for reducing dependencies in Source Code
    1. Going functional programming languages
  13. Best solver: Picat - written in pure C!
  14. The 4 color proof
  15. The Coq/OCaml verification process
  16. The process of seL4 verification with Haskell and Isabelle
  17. Wat! - The JavaScript / Microsoft TypeScript nightmare
  18. SAT "satisfiable" Solver in pure Python
  19. The cDMN "constaints tables - compare with "State Machines"
  20. The Extensionality Axiom - Zermelo-Fraenkel
  21. Math logic fallacy: Proof that: 2=1
  22. Proof that 29 is prime?
  23. The Zermelo-Fraenkel "extensionality axiom"
  24. What's a "formal spec" that i have to "verify"
  25. The 'environment' - Strange observations with Rust
  26. The general problem with math formulas
  27. Find invariants - things that are true for all times (and under all conditions)
    1. Proof of the Gauß summation formula with induction
    2. Sequences as invariants in programming
      1. Multiple XOR encryption
    3. Can we find the invariants in the Nim game?
  28. Dependent Types and Sound Types
    1. Why Excel miserably fails
    2. The need for a mathematical foundation
    3. Sound types in Dart
    4. Java has no sound types
    5. But the Java - like ABS language has
    6. Fabrice bellard's QuickJS has sound types!
    7. Smalltalk has sound types
    8. The WAT! unsoundness of a browser JS engine
  29. The formal verification process of the seL4 kernel
  30. The formal verification process of CompCert C compiler
  31. Word frequency count
    1. Lessons learned from the Word Frequency Count example
  32. Learning OCaml functional language
  33. The hoare triple - hoare calcucus
    1. Eiffel language - Design by Contract™
  34. Fully Homorphic Encryption
  35. Howto build your own "formally verifyable" functional language

What's the semantic triple or "RDF triple"

It describes the world in categories of "What is the case?" in Wittgenstein's sense:

1 The world is all that is the case.
1.1 The world is the totality of facts, not of things.
1.11 The world is determined by the facts, and by their being all the facts.
1.12 For the totality of facts determines what is the case, and also whatever is not the case.
1.13 The facts in logical space are the world.

https://en.wikipedia.org/wiki/Semantic_triple

Biggest databases on earth are RDF style:

https://www.w3.org/wiki/LargeTripleStores

https://www.ncbi.nlm.nih.gov/pmc/articles/PMC3965039/

That's how we mostly encode "data" that we type-in into our computers.

Why formal verification of algorithms is essential

Algorithms are all about <how> data is processed. In 2002 somebody noticed, that the "Timsort" algorithm, used for years in Java and Python - in very rare cases - forgot to sort one number. Nobody noticed, since typically all tests passed and nobody even thought that there could be a bug in it. Until one day ...

https://ercim-news.ercim.eu/en102/r-i/fixing-the-sorting-algorithm-for-android-java-and-python

The typical test scenario - at that time - only was to verify, if the result was correctly sorted in ascending, descending order. Nobody even thought about counting the numbers. One was missing! :-O

They used TLA+ by Leslie Lamport to verify the algorithm. You also can use e.g. Agda:

https://old.learntla.com/introduction/ (time related)
https://github.com/agda/agda (non time related)

Note, that mathematical proofs only work with /time unrelated/ algorithms. For proving e.g. Paxos or Raft algorithm, you need Temporal Logic as in TLA+.

I also highly recommend Leslie Lamport about the importance to program everything with human verifiable state machines:

https://github.com/gbmhunter/FunctionPointerStateMachineExample/

1
2
3
4
5
6
7
8
static stateTransMatrixRow_t stateTransMatrix[] = {
    // CURR STATE  // EVENT              // NEXT STATE
    { ST_IDLE,     EV_BUTTON_PUSHED,     ST_LED_ON  },
    { ST_LED_ON,   EV_TIME_OUT,          ST_LED_OFF },
    { ST_LED_ON,   EV_BUTTON_PUSHED,     ST_IDLE    },
    { ST_LED_OFF,  EV_TIME_OUT,          ST_LED_ON  },
    { ST_LED_OFF,  EV_BUTTON_PUSHED,     ST_IDLE    }
};

State machines in TLA+ https://www.learntla.com/topics/state-machines.html
Short version (7 pages): https://www.microsoft.com/en-us/research/publication/computer-science-state-machines/?from=https://research.microsoft.com/en-us/um/people/lamport/pubs/deroever-festschrift.pdf
Long version (27 pages): https://www.microsoft.com/en-us/research/publication/computation-state-machines/
https://www.hyrumslaw.com/

Make yourself clear, that every Assembler Instruction - we have seen earlier - in itself is a state machine or better - a "State Transformer": It has <entry states> that go through some <transformation> and that have <output states>. Above that again - this time in in software - logical <entry states> and (a series of) commands that trigger some <state transformation> in the underlying hardware. Together they build a huge <state transformation system>.

Q: What's Java or Python bytecode then? A: Abstract transformers! They're working processor ISA (Instruction Set Architecture) independent.

Quick jump to Temporal logic: https://rentry.co/DSRsecuritycoursepart9

Geoff Sutcliffe: "Who killed Aunt Agatha"

It's about claims (predicates) and restrictions (constraints) and finding (or excluding) solutions.

It's a very old standard problem every solver had to solve in the past:

Someone who lives in Dreadbury Mansion killed Aunt Agatha.
Agatha, the butler, and Charles live in Dreadbury Mansion,
and are the only people who live therein. A killer always
hates his victim, and is never richer than his victim.
Charles hates no one that Aunt Agatha hates. Agatha hates
everyone except the butler. The butler hates everyone not
richer than Aunt Agatha. The butler hates everyone Aunt
Agatha hates. No one hates everyone. Agatha is not the
butler. Therefore : Agatha killed herself.

https://tptp.org/cgi-bin/SeeTPTP?Category=Problems&Domain=PUZ&File=PUZ001+1.p

Mathematically this problem is related to linear inequalities:
https://byjus.com/maths/linear-inequalities-in-two-variables/

These are typically solved with Simplex Tableaus: https://en.wikipedia.org/wiki/Simplex_algorithm

*In fact invented by: https://en.wikipedia.org/wiki/Leonid_Witaljewitsch_Kantorowitsch

(Stupid cowboys continuously rewrite whole Wikipedia for political reasons, http://www.ned.org with their ~88 billion dollar black budget)

Where's the difference? Linear inequalities work on floats, the Agatha problem has to be solved with booleans in the same manner as "truth tables", used in electric circuits:

https://en.wikipedia.org/wiki/NAND_logic

They all can be operated in a matrix, e.g. with GraphBLAS or OpenBLAS:

https://www.openblas.net/ - supported by the German Souvereign Tech Fund!

Q: What is SUDOKU then? A: It's a disjoint states game. Distributing a set { ... } of states horizontally, vertically, diagonal.

From simple gates to higher order functions (From NAND to TETRIS)

Interestingly, NAND not only is build from simple logic gates (NOT AND), but you again can express AND, OR, NOT, XOR by NAND circuits:

Q = A OR B = ( A NAND A ) NAND ( B NAND B )

Typically, you proof this formula with truth tables. Here you go through the complete state space which is generated by combinatorics. For example: "How many possibilities are there to randomly spread 4 bits over a field of 8 bits (one byte)?

The simple formula is: f(n, r) = n!/(r!(n-r!))

https://www.calculatorsoup.com/calculators/discretemathematics/combinations.php

Answer is 70. Always keep in mind, that to proof something true or to disproof something, you always have to go over the complete state space!!!

Note: Try other values with 3 and 5 = 28, 2 and 6 = 56, 1 and 7 = 8 and you'll notice that it is a Gauss curve: https://en.wikipedia.org/wiki/Gaussian_function

https://en.wikipedia.org/wiki/NAND_logic

In general: Here you can see, that I can express very simple things with more complex bricks. Obviously i can climb the complexity ladder (compare with famous Wittgenstein Tractatus Logico Philosophicus, TLP) without losing the ability to do or to calculate even simplest things with very complex machines. That's what you can observe using Mico$oft Windoof. It has become far too complex!

Also see famous "From NAND to TETRIS" course by Shimon Shocken. He teaches you to make your own Tetris computer from NAND gates (=transistors) alone. No software, all in pure hardware. Back to the roots!

Do that fucking course!!! https://www.nand2tetris.org/

Truth tables, Domain Driven Design, Panes, Impedance Missmatch

Simple truth tables like in this example here: https://en.wikipedia.org/wiki/NAND_logic can be combined to very large truth tables, as e.g. needed to verify computer chips. Interestingly you can split those up and insert logical intermediate layers, where complex states are evaluated and representated by something like "[a complex fact] is the case" to reflect upon. These are called "logical panes". Like summaries at school or Blinkist. The essence of whole books squeezed into 10 sentences.

  • Checkbox 2 (size of a hand, longish, curved, yellow?)
  • Checkbox 2 (the car is red) RDF triple!

What does that mean "The car is red"? What are the conditions that i can make such a claim?

This process of splitting up complex relationships (e.g. a huge matrix) into human understandable parts, connected by some "glue logic" (the panes) is called "Domain Driven Development".

The more incompatible the models are, the more "glue logic" is needed. That's called "impedance missmatch". See the [forever:] [[move 10 steps] -> [turn 15 degrees] ] example: https://snap.berkeley.edu/ . Can you bring it back to sine and cosine?

At impedance missmatch, the cost of projects explode.

Essential: What matrices have to do with graphs?

Highly recommended to watch these videos first:

The Applications of Matrices | What I wish my teachers told me way earlier
https://youtube.com/watch?v=rowWM-MijXU&t=15m48s

Introduction to GraphBLAS with Python
https://youtube.com/watch?v=JUbXW_f03W0

GraphBLAS discovers hidden relationships within big data

GraphBLAS operations all are operations on mathematical semirings that fulfill special properties. Also compare with: 'abelian group', 'rings', 'semifields', 'idempotency'

Adjacency Matrix

To the official homepage: https://graphblas.org/

Giving matrix elements a weight - heavily used in AI!!!

Python-Graphblas

https://python-graphblas.readthedocs.io/en/stable/getting_started/primer.html

The commercial end of Redis-Graph

https://redis.io/blog/redisgraph-eol/

This thesis from a student in St. Petersburg was the reason: https://dspace.spbu.ru/bitstream/11701/39638/2/Master_sThesisV_2.pdf

US CISA intervened, stopped that project: https://www.cisa.gov/about/leadership

Practical use of GraphBLAS or OpenBLAS

What building A² reveals

In the above videos you could see, that multiplying a matrix by itself, building A² from a simple adjacency matrix, that this reveals something about its inner structure, revealing hidden logical connections, that cannot be seen otherwise. In the case of A² you see who is connected with whom over one indirection.

Watch! https://en.wikipedia.org/wiki/Adjacency_matrix

Calculating A³ reveals clusters in community structures or social networks

By computing A³ you see who is connecred with whom over 2 indirections. With this it slowly begins, that you can see e.g. community structures in your enterprise, only by looking at e.g. the internal mail metadata (logs of who communicates with whom) clearly showing who is relevant or can be layed-off). Extract the mail logs, give every employee a number (1-500) and then build the adjacency matrix.

Or use meta data logs provided by on Twitter/X, Telegram which btw. become highly relevant for our secret services finding "terrorist clusters" in social networks (or just a harmless community of people interested in Ornithology (birds).

The inner structures of souce code

You can discover the inner structures of source code over time, e.g. with Gource:

https://youtube.com/watch?v=9mput42uZsQ

There you sometimes see blobs getting bigger and bigger, building "god classes", which then have to be smashed by refactoring to keep your code maintainable. "God classes" are a clear indicator for "technical debt". That's why e.g. Microsoft had to completely rewrite .NET 3x now. Oracle hasn't even started yet with its Java libraries.

Reason: That would break downwards compatibility. But programming with Java becomes more and more a pain. Most programming patterns are simply outdated, do not fit in the new age of distributed computing with many cores. See e.g. the Disruptor pattern.

Highly recommended: New age of HPC algorithms: https://en.algorithmica.org/hpc/

GTK3 GUI library - written in pure C - also had a problem with one god class (the GObject) attracting more and more functionality: https://youtube.com/watch?v=aZf2g__6DkY

The Girvan Newman algorithm

Instead of building A², A³ of the Adjacency Matrix you also can use the Girvan Newman algorithm to discover community structures in metadata of communication or within software:

https://flosshub.org/sites/flosshub.org/files/gonzalezBarahona44-48.pdf

https://www.researchgate.net/figure/SIDG-of-Most-Popular-Instance-of-Bugzilla-in-Debian-4-optional-depend-not-shown_fig7_4297130

Enabling massive deep neural networks with the GraphBLAS

This here is the burner: https://arxiv.org/abs/1708.02937

https://dspace.spbu.ru/bitstream/11701/39638/2/Master_sThesisV_2.pdf

The Hindley - Milner type inference

Cython neccessarily needs type hints, while CPython typically can figure out on its own, what of what type the variables are. Interestingly Cython can internally autocomplete missing type hints. This typically is done with Hindley-Milner algorithm, especially in functional languages. But it also can be done with GraphBLAS.

Essential: What are co- and contravriant types?

Co-Contravariant

Co- and contravariant types differ in preservation (keeping unchanged) of certain properties. E.g. in a gravitational, spheric world, everything should be on curved coordinates, but for simplicity we keep it Euclidean: Span is: {0,0,1}, {0,1,0}, {1,0,0} as our unit vectors, which always are rectangular to each other. Means: I may vary x or y or z coordinates independently from each other.

Applied to compilers i always have problems with transforming from decimal to binary "coordinates". 0.3 in decimal poses a serios problem in binary format:

The binary representation of 0.3 is 0.0100110011001100110011001100110011... where the sequence 0011 repeats infinitely. This means that in binary, 0.3 is a non-terminating, repeating decimal. Note: Precision is not equal to accuracy!!!

Same for the algorithm themselves. In Binary format they vastly differ from what we know from math at school, see: https://graphics.stanford.edu/~seander/bithacks.html

So when Xavier Leroy reports about the "formal verification" of the CompCert C compiler, you might think of this model when you read of "covariant" and "contravariant"

https://xavierleroy.org/publi/compcert-CACM.pdf

The inventor of category theory: Aristotele's 10 categories

When e.g. Bartosz Milewski is phantasising about his catagories, he's in fact citing Aristotele from his Organon, chapter IV: https://en.wikisource.org/w/index.php?title=Organon_(Owen)/Categories#Chapter_4

Milewski

https://github.com/hmemcpy/milewski-ctfp-pdf
https://en.wikipedia.org/wiki/Categories_(Aristotle)

He's the true originator of all that "category stuff" in functional programming:

Aristotele at his time (~350 b.c.) considered 10 categories to be sufficient:

  • (1) substance
  • (2) quantity
  • (3) quality
  • (4) relatives
  • (5) somewhere
  • (6) sometime
  • (7) being in a position
  • (8) having
  • (9) acting (protagonist)
  • (10) being acted upon (antagonist). (Organon, chapter IV)

Q: Living today in a modern civilization: What "qualities" had to be added?

Essential: Law of excluded middle - "Tertium non datur!"

Aristotele: "It is impossible, then, that "being a man" should mean precisely "not being a man", if "man" not only signifies something about one subject but also has one significance. … And it will not be possible to be and not to be the same thing, except in virtue of an ambiguity, just as if one whom we call "man", and others were to call "not-man"; but the point in question is not this, whether the same thing can at the same time be and not be a man in name, but whether it can be in fact. (Metaphysics 4.4)

https://en.wikipedia.org/wiki/Law_of_excluded_middle

In normal human logic the opposite of e.g. "blue" is not "red". It can be brown, green, yellow or whatsever be. Their opposite never will be "blue" again either.

But in mathematics we need this "narrowing down" to make reasoning about the world in logical, close models (groups, rings) with algebraic notation at all possible.

Mathematicians so are all a little bit, let's say "small-minded". But therefore they can be - very precise in their description of the world in physics, chemistry, biology, genetic, philosophy (see Wittenstein's TLP) ... Also see Gotthard Günther - https://www.vordenker.de/ggphilosophy/ggphilo.htm and Wolfgang Stegmüller - https://www.sgipt.org/wisms/analogik/ist-ws.htm

Make yourself clear, that - as a programmer - you're parametrizing the world to computable states. You're the interface between the physical world with its (Wittgenstein) "facts" - according you your interpretation - and some stupid transistors, doing some logical things for you with it: Nonsense in - nonsense out!

The "Tertium non datur!" (and other findings) in Agda:

The ""Tertium non datur":* https://github.com/agda/agda-stdlib/blob/master/src/Axiom/DoubleNegationElimination.agda

The "Extensionality Axiom": https://github.com/agda/agda-stdlib/blob/master/src/Axiom/Extensionality/Heterogeneous.agda

Peano / Zermelo Fraenkel Axioms: https://boarders.github.io/posts/peano.html

When it comes that you have to (purely mathematical) proof an algorithm you can use Agda. For temporal related proofs you have to use TLA+.

The famous Y-combinator

It is a so-called higher-order function, that replicates itself when put into the λ calculus: λƒ.(𝜆𝑥.ƒ(𝑥.𝑥))(𝜆𝑥.ƒ(𝑥.𝑥)) or in simple form: y f = f (y f)

This discovery made the λ useful for programming loops (while true do ... done) and finally to proof the equivalence with the Turing machine:

https://en.wikipedia.org/wiki/Church-Turing_thesis

The need for reducing dependencies in Source Code

Two examples:

Code Dependencies

https://blog.ndepend.com/identify-net-code-structure-patterns-with-no-effort/

and:

Ghidra analyzing .dll

Source: https://clearbluejar.github.io/posts/callgraphs-with-ghidra-pyhidra-and-jpype/

Going functional programming languages

One single line that made functional programming languages popular:

tr -cs A-Za-z '\n' | tr A-Z a-z | sort | uniq -c | sort -rn | sed 10q (more in the text)

Functional programming languages significantly reduce cross dependencies of modules and so not only lower long term maintenance cost, but also make "formal verification" possible. As the example impressingly shows, you can replace 1000nds of lines of code by a simple one-liner in bash.

https://onceupon.github.io/Bash-Oneliner

Best solver: Picat - written in pure C!

The biggest advantage of his solver is, that is seamlessly integrates into $ bash shell programs to make even $ bash scripts "intelligent".

Best tutorial so far: http://retina.inf.ufsc.br/picat_guide/

Beginner's intro: https://www.linuxjournal.com/content/introduction-tabled-logic-programming-picat

Picat is very B-Prolog like: https://en.wikipedia.org/wiki/B-Prolog

http://picat-lang.org/download/picat_compared_to_prolog_haskell_python.html

Homepage and docs: http://picat-lang.org/ and http://hakank.org/picat/

1000 examples: https://github.com/hakank/hakank/tree/master/picat

Picat tutorial: https://www.hillelwayne.com/post/picat/

From: http://picat-lang.org/p99/constraints.html

8 Queens problem:

1
2
3
4
5
6
7
8
9
import cp.
queens(N,Qs) =>
    Qs = new_array(N),
    Qs :: 1..N,
    foreach (I in 1..N-1, J in I+1..N)
        Qs[I] #!= Qs[J],
        abs(Qs[I]-Qs[J]) #!= J-I
    end,
    solve([ff],Qs).

IMHO: Don't look any further. It's the best solver of all times!

Always have in mind, that a solver has to go through all possible states. So it permutates through all possibilities. In the inner for loop you see the constraints, the "rule of the game". This is also called "the model".

The 4 color proof

4 color proof

A mixture between mathematical, formal and computational proof:
https://youtube.com/watch?v=yBXGdJw1xBI

The Coq/OCaml verification process

https://www.google.com/search?q=ocaml+verification+with+coq+isabelle

Introduction into the COQ/Isabelle proof assistent: https://www.lri.fr/~paulin/LASER/course-notes.pdf
Online proof assistent: https://coq.vercel.app/

Equivalence of imperative (state based) and functional (transformer based) languages:

https://en.wikipedia.org/wiki/Church-Turing_thesis

The long process of proving correctness of the CompCert C compiler:

https://xavierleroy.org/publi/compcert-CACM.pdf

The process of seL4 verification with Haskell and Isabelle

https://www21.in.tum.de/teaching/proof21/SS18/files/14-final.pdf
http://web1.cs.columbia.edu/~junfeng/09fa-e6998/papers/sel4.pdf
https://sel4.systems/Foundation/Board/
https://sel4.systems/About/

Rust on top of seL4? https://sel4.systems/Foundation/Board/Minutes/230928-minutes-unconfirmed.pdf

People do not know what they're doing! US money involved?

Wat! - The JavaScript / Microsoft TypeScript nightmare

https://youtube.com/watch?v=et8xNAc2ic8

The original talk by Gary Bernhardt:

https://www.destroyallsoftware.com/talks/wat

Compare with https://bellard.org/quickjs/ unique features!

SAT "satisfiable" Solver in pure Python

Mathematical proofs are broken down into sub-proofs. 
A proof is complete if all sub-proofs are satisfied.

SAT solvers use backtracking algorithms with heuristics (e.g. DLIS, VSIDS) 
well known from *Prolog programming language*.

SAT solver pseudocode:

function SAT-solver(formula f) {
  if (f is satisfiable)
     return "The formula is satisfiable"
  else if f contains an unsatisfiable clause
     return "The formula is unsatisfiable"
  else
     choose a variable x in f 
     SAT-solver(f with x = true)
     SAT-solver(f with x = false)
}

SAT solver written in Python: https://github.com/eprover/PyRes/blob/master/saturation.py

The cDMN "constaints tables - compare with "State Machines"

https://dmcommunity.org/wp-content/uploads/2014/10/who-killed-aunt-agatha-corticon.pdf

The cDMN tables notation: https://cdmn.readthedocs.io/en/latest/notation.html

The Extensionality Axiom - Zermelo-Fraenkel

https://en.wikipedia.org/wiki/Zermelo-Fraenkel_set_theory

To find f(n), add 5 to n and then multiply with 2.
To find g(n), multiply n by 2 and then add 10.

Interestingly, those two functions obviously are not identical but extensionally they deliver same values for n>0:

f(3)=16; f(8)=26;
g(3)=16; g(8)=26; Surprising, isn't it?

Obviously two different operations, but same outcome! Can you proof their equivalence?

Math logic fallacy: Proof that: 2=1

Gödel sais, that a logical system (math) cannot be proven within itself. And this is the result. There are inconsistencies.

Mathematical proofs all have their own "quirks and flaws". While differentiation of math formulas always is straightforward following simple rules, the opposite, the integration can be quite challenging. And quite often things are overseen, as in this example:

1
2
3
4
5
6
7
8
a = b      | *a
a² = ba    | - b²
a² - b² = ab - b²  | 3rd binominal formula rewrite
(a+b)(a-b) = b(a-b)  | divide by (a-b)
a+b = b  | because a = b we can replace
b+b = b
2b = b    | divide by b
2 = 1     | q.e.d.

This kind of logical error is typical for kids at school. They always forget, that "dividing by zero" will heavily be punished! But also the opposite "multiplication with 0" is also problematic, when you go through in "bottom up" reverse order.

Proof that 29 is prime?

https://en.wikipedia.org/wiki/Primality_test

"Certain number-theoretic methods exist for testing whether a number is prime, such as the Lucas test and Proth's test. These tests typically require factorization of n + 1, n − 1, or a similar quantity, which means that they are not useful for general-purpose primality testing, but they are often quite powerful when the tested number n is known to have a special form

The Lucas test relies on the fact that the multiplicative order of a number a modulo n is n − 1 for a prime n when a is a primitive root modulo n. If we can show a is primitive for n, we can show n is prime."

29 as natural number is between 28 and 30 and we know their prime factors

28 < 29 < 30 we can rewrite to:

4*7 < 29 < 5*6 (imagine 4*7 and 5*6 as rectangles)

There obviously is no other decomposition possible between 4 and 5 and 7 and 6 possible. Therefore 29 must be prime! q.e.d?

WTF is going on here?

Answer: https://en.wikipedia.org/wiki/Axiom_of_extensionality

The problem: There can be other decompositions. It have to make sure, that 4*7 and 5*6 are the only prime factors, which they aren't! 2*2*7 and 5*2*3 are possible.

Note: To 'proof' something i have to go through all possible states!

The Zermelo-Fraenkel "extensionality axiom"

In the formal language of the Zermelo–Fraenkel axioms, the axiom reads:

∀𝐴∀𝐵 (∀𝑋 (𝑋∈𝐴 ⟺ 𝑋∈𝐵) ⟹ 𝐴=𝐵)

or in words:

"Given any set A and any set B, if for every set X, X is a member of A if and only if X is a member of B, then A is equal to B."

"If it looks like a duck, swims like a duck, and quacks like a duck, then it probably is a duck." - The "duck" argument: https://en.wikipedia.org/wiki/Duck_test

Interestingly, Zermelo-Fraenkel axioms ("set theory") are the base of the SQL language. All other math above is based on the Peano-Axioms.

Zermelo Fraenkel SQL joins!

https://en.wikipedia.org/wiki/Zermelo–Fraenkel_set_theory
https://en.wikipedia.org/wiki/Peano_axioms

In mathematical proofs I thus have to go though all possibilities. Same for data flow in computer programs. I have to check every possible branch e.g. for dead ends.

What's a "formal spec" that i have to "verify"

It's a set of behaviours: Spec: Set { behaviour 1, behaviour 2 ... behaviour n }

Means: Things have to move to watch if they behave correct. A cat that does not move any longer - e.g. because it's dead - does no longer show "a behaviour" any longer!

So if the "behaviours" described in the specs and in the source code finally show up in the machine code, then your program and compiler - together - are "formally verified".

Note: The complete chain must be verified!!! (As described here: https://xavierleroy.org/publi/compcert-CACM.pdf)

The 'environment' - Strange observations with Rust

A Rust programmer pointed me to a strange observation: One of the environment variables in Bash shell had an incorrect Unicode type as "malformed character" in it.
Result was: Rust compiler as well as all with Rust compiled programs crashed.

Obviously there was the inner logic within Rust code and compiled Rust binaries depending on some strange characters which have nothing to do with either Rust Code nor with the generated Binary. Or - at least - they shouldn't!

Why is Rust behaving in such a unpredictable way? Microsoft is heavily sponsoring Rust development and Microsoft wanted to make sure, that Rust runs on Linux console as well as in Windows GUI environment, or - in a open Powershell window.

The Rust 'println' function description here sais:

Note: “User-friendly” printing is done using the Display trait, debug output (human-readable but targeted at developers) uses the Debug trait. You can find more information about the syntax you can use in println! in the documentation for the std::fmt module. Source: https://rust-cli.github.io/book/tutorial/output.html

What does that mean: Depending on its environment Rust binary shows different behaviours. In Windows, the Rust binary looks, of outout in Powershell or Windows GUI is wanted and behaves correspondingly. Unluckily in Windows all Unicode is 16 bit only, while in Linux Unicode varies between UTF-8 (ascii like) and 16bit and 32bit versions. Linux is fully compatible with global Unicode specs, while Windows isn't. And here suddenly Rust had an obvious problem. What leads us to the next problem:

The general problem with math formulas

In our above examples, the environment is not considered. In physical reality we have two baskets containing things, neccessarily at visually distinguishable places. So the bags cannot be the same as well as the items in the bags. In math, that fact is ignored. Not so in computing. Memory locations are distinguishable as well.

Another thing that is permanently ignored, is ***time***. The instruction pointer IP within a CPU core cannot be at the same time at different places.

See the "ABA" and the *"TOCTOU" problems:

ABA: https://en.wikipedia.org/wiki/ABA_problem

TOCTOU: https://en.wikipedia.org/wiki/Time-of-check_to_time-of-use

To address these problems, Intel introduced the atomic Compare-And-Swap (CAS) instruction: https://en.wikipedia.org/wiki/Compare-and-swap

Find invariants - things that are true for all times (and under all conditions)

Proof of the Gauß summation formula with induction

https://de.wikipedia.org/wiki/Gaußsche_Summenformel

Gauss sum formula

What's the sum of e.g. 1 ... 10? We divide in 2 parts and reverse one part:

. 1 2 3 4 5
10 9 8 7 6
=========
11 11 ... 11 = 10/2 * (10+1) obviously. Replacing '10' by x gives me the formula:

½x(x+1) - can i proof that? For x=10 it was correct. And when i replace x by x+1?

½(x+1)(x+2) then should be the same as ½x(x+1)+(x+1), right?

½(x²+3x+2) == ½x² + ½x + (x + 1)

Interestingly, this should also hold for an odd number of numbers like [1 ...11]. Why? Because it didn't matter when we added (x+1) to our example with 10. Why? In this case, you can add a "0" to make the number even again.

Seems, the right duck always quacks like the left duck! q.e.d.

Seems, with ½x(x+1) we have found an "invariant" which is working for all sums of natural, positive numbers. Same proof in Agda:

https://github.com/jsiek/B522-PL-Foundations/blob/master/lecture-notes-part1.lagda.md

Finding and proving "invariants" - that's what mathematics is all about!

Sequences as invariants in programming

The Random Number in your head:

Choose a 2-digit number, say 23, your "seed". Form a new 2-digit number:

The 10's digit plus 6 times the units digit - gives you the next number.

The example sequence is: 23 - 20 - 02 - 12 - 13 - 19 - 55 - 35 ...

The whole cycle is - until it repeats:

01 06 36 39 57 47 46 40 04 24 26 38 51 11 07 42 16
37 45 34 27 44 28 50 05 30 03 18 49 58 53 23 20 02
12 13 19 55 35 33 21 08 48 52 17 43 22 14 25 32 15
31 09 54 29 56 41 10 01

https://groups.google.com/g/sci.math/c/6BIYd0cafQo/m/Ucipn_5T_TMJ?hl=en

These cycles are a huge problem in Pseudo Random Number Generators and such in RSA and DKHE (https / ssh protocol)

Multiple XOR encryption

To prevent this you can use several different PRNG, shifting and XOR'ing them against each other. So when you use 4 x 4096 bits of random numbers, you shift them by some random offset, the first repeating sequence logically appears after 4096^4 bits. Enough to confuse your MITM.

1
2
3
4
5
6
10001110011011010101....
offset x    01101110111010111010101....
offset y             10000111110101101110101010....
offset z                              00111011101010110101010110101.....
===========================================
XOR result ->       1010111000101001010101101

So you virtually use a telescope like mechanism. It's pretty hard to solve this equation system. You need to invert a 4096^4 elements (2.8147498e+14) quadratic bool matrix. Here again, state space explodes.

Another example would be the "Mandelbrot set" (of pixels):

https://colineberhardt.github.io/wasm-mandelbrot/

Can we find the invariants in the Nim game?

Let's play the Nim game: Nim Game 16 matches

Two players take between 1-3 matches, the player who takes the last match, loses!

Finding the invariant (n%4)+1 saves you from building a tree at all! Why?

Nim search tree

https://cgm.cs.mcgill.ca/~avis/Kyoto/courses/ia/2013/notes/luc_devroye.htm

That's what AI in fact does: Finding the inner dependencies in high dimensional state information and reducing them to only some few relavant states very much like with a funnel.

State Space Funnel

Finally genomes are nothing else than "State Space Reducers". They're shaping the world, they work against the 2nd law of entropy:

https://en.wikipedia.org/wiki/Folding_funnel

Second law of thermodynamics: https://fs.blog/entropy/

Dependent Types and Sound Types

Why Excel miserably fails

Excel has no "sound types": Here you can see, what happens, when your types are not "sound":/https://exceloffthegrid.com/excel-calculate-wrong-results/

The need for a mathematical foundation

So an idea could be here, that "types" in programming should also have a mathematical foundation. And, indeed, there are "Dependent types" and there are "Sound types" which do have exactly hat kind of mathematical "duck argument" foundation!

https://en.wikipedia.org/wiki/Dependent_type

Sound types in Dart

https://dart.dev/language/type-system

"Dart has sound types, which means that it guarantees that the runtime type of a variable will match its static type. TypeScript has no such guarantee, and the added constraint means that any additions to Dart's type system must be very carefully designed and implemented to preserve soundness. In exchange though, you get much more confidence in the runtime behavior of your code, and there are many more opportunities for optimization and dead code elimination that helps Dart run faster and slimmer"

https://medium.com/dartlang/dart-and-the-performance-benefits-of-sound-types-6ceedd5b6cdc

Java has no sound types

https://hackernoon.com/java-is-unsound-28c84cb2b3f

But the Java - like ABS language has

From: https://abs-models.org/manual/

"ABS is a language for Abstract Behavioral Specification, which combines implementation-level specifications with verifiability, high-level design with executablity, and formal semantics with practical usability. ABS is a concurrent, object-oriented, modeling language that features functional data-types."

Fabrice bellard's QuickJS has sound types!

And Fabrice Bellard's https://bellard.org/quickjs/ has: BigNum and BigDecimal long arithmetic!!! These also build "sound types" because e.g. multiply of 2 64 bit integers cannot overflow!

12,000 lines of magic: https://github.com/bellard/quickjs/blob/master/quickjs.c

Smalltalk has sound types

Smalltalk is one of the oldest programming languages and also the safest one. Not only it automatically switches between BigDecimal, Fractional, BigNum arithmetic it's inner architecture is quite amazing. Everything is an object that is floating around in a vivarium of <<object space>>. Types are implicit. Buffer overflows, by design, do not exist. The only method of objects to communicate is to talk with each other. If one message of a sender is of wrong format, the receiver simply answers with "message not understood": https://wiki.c2.com/?DoesNotUnderstand

Smalltalk fraction type: http://tpcg.io/_JZSTQ1

The WAT! unsoundness of a browser JS engine

What can happen, when you implement compilers without verification, you have seen in the above "WAT! talk" by Gary Bernhardt:

https://www.destroyallsoftware.com/talks/wat

The formal verification process of the seL4 kernel

https://gernot-heiser.org/
https://sel4.systems/news/#seL4-13.0.0
https://youtube.com/watch?v=E1hWlg-Ms9I&t=13m0s

The formal verification process of CompCert C compiler

42000 lines of COQ proof code had to be written to ensure, that CompCert pricisely does, what it is supposed to do: Translating to machine code. Here the story:

https://xavierleroy.org/publi/compcert-CACM.pdf

On the other hand there is Fabrice Ballards OTCC C (subset) compiler that fits onto one A4 page, into 2048 bytes, to be precise. Both do exactly the same!

http://bellard.org/otcc/

Word frequency count

https://www.cs.tufts.edu/~nr/cs257/archive/don-knuth/pearls-2.pdf

Douglas McIlroy of Bell Labs criticized Knuth's solution as not even able to process a full text of the Bible, and replied with a one-liner, that is not as quick, but gets the job done:

tr -cs A-Za-z '\n' | tr A-Z a-z | sort | uniq -c | sort -rn | sed 10q

Revolutionary: It's the way of thinking in "transformers"!!!

https://dev.to/kcdchennai/example-for-text-processing-shell-commands-tr-uniq-sort-sed-and-awk-335f

Examples to get the "mindset": https://www.grymoire.com/Unix/Sed.html

Primary goal is to reduce cross dependencies between functional modules!

It makes your language predictable: https://youtube.com/watch?v=KPa8Yw_Navk&t=34m30s

https://fsharpforfunandprofit.com/posts/is-your-language-unreasonable/

With that, "formal proofs" become possible.

A followup article about "Literate Programming":

https://web.archive.org/web/20210725060244/https://www.cs.upc.edu/~eipec/pdf/p583-van_wyk.pdf

Haskell solution: https://franklinchen.com/blog/2011/12/08/revisiting-knuth-and-mcilroys-word-count-programs/

Benchmarks: https://codegolf.stackexchange.com/questions/188133/bentleys-coding-challenge-k-most-frequent-words

Lessons learned from the Word Frequency Count example

tr -cs A-Za-z '\n' | tr A-Z a-z | sort | uniq -c | sort -rn | sed 10q

  • Functional programs always can be split up into 'state independent' modules
  • There is no 'state propagation' since everything is implemented as 'transformer'
  • All operations follow mathematical laws. There always is the "negative element" for "undoing" or reversing a operation: https://en.wikipedia.org/wiki/Inverse_element E.g. SQL servers do not follow these mathematical principles
  • These modules always can be independently verified (see http://justine.lol/lambda example)
  • Functions are always pure - no side effects! (https://purescript.org/ und https://agraef.github.io/pure-lang/)
  • When a λ function once is verified, it is exactly doing what it was meant for - ans nothing else!
  • λ functions never have any secret functionality, no "encapsulation", no "private" or "protected", unseen or unreachable states or functionalities
  • Immutablitity is always granted. Never change facts in databases backwards in time!!! Compare Datomic with e.g. SQL servers. Compare to blockchain.
  • Functional integrity and correctness only can be granted within the program. Any kind of storage or output therefore always is a 'maybe monad'. (You can never know, if hard drive is working or graphics card it there. Same for all kinds of input over keyboard, mouse, ... see the evil Rust traits example

Learning OCaml functional language

The new 2024 OCaml learning book:

https://cs3110.github.io/textbook/ocaml_programming.pdf

The book: https://cs3110.github.io/textbook/cover.html

OCaml tutorials: https://youtube.com/playlist?list=PLre5AT9JnKShBOPeuiD9b-I4XROIJhkIU

Note: OCaml has no US dependencies like LLVM, GNU. It's french! Think european!

Also worth knowing: F# is an OCaml clone. ReasonML is a JavaScript clone written on OCaml compiler. It is like as OCaml has morphed its syntax. With ReasonML you now can reimplement OCaml again, if you like. ML stands for Meta Language. Meta = (greek) above, beside.

https://en..wikipedia.org/wiki/Reason_(programming_language)
https://en.wikipedia.org/wiki/Standard_ML

HINDLEY-MILNER TYPE INFERENCE: https://www.youtube.com/watch?v=_yDo9Q9EOHY

https://en.wikipedia.org/wiki/Hindley-Milner_type_system

The hoare triple - hoare calcucus

The central feature of Hoare logic is the Hoare triple. A triple describes how the execution of a piece of code changes the state of the computation. A Hoare triple is of the form: {𝑃}𝐶{P}

{P} is named the precondition and {Q} the postcondition: when the precondition is met, executing the command establishes the postcondition. Assertions are formulae in predicate logic.

Hoare logic provides axioms and inference rules for all the constructs of a simple imperative programming language. In addition to the rules for the simple language in Hoare's original paper, rules for other language constructs have been developed since then by Hoare and many other researchers. There are rules for concurrency, procedures, jumps, and pointers.

https://en.wikipedia.org/wiki/Hoare_logic

https://www.eiffel.org/doc/eiffel/ET-_Design_by_Contract_%28tm%29%2C_Assertions_and_Exceptions#Preconditions

Eiffel language - Design by Contract™

https://www.eiffel.org/doc/eiffel/ET-_Design_by_Contract_(tm)%2C_Assertions_and_Exceptions#Design_by_Contract

Fully Homorphic Encryption

The idea: End-to-End encryption and all calculations happen on encrypted data only!

Slideshow: https://www.zama.ai/introduction-to-homomorphic-encryption

Paper: https://thomas-plantard.github.io/pdf/Chen18.pdf

Lattice based cryptography: Points do have 10000's of coordinates. So finding a combination of the basis vectors that simultaneously makes all 10,000 generated coordinates turns out to be quite hard.

https://medium.com/cryptoblog/what-is-lattice-based-cryptography-why-should-you-care-dbf9957ab717

There are many lattices possible to use. Let's take e.g. a logarithmic lattice:

Rechenschieber

The core idea: Instead of multiplying 2 numbers you can add their precomputed logarithms. For dividing, subtract their logarithms.

Addition you can do, if you precompute 2^x or 10^x values: log(10^x) = x.

So log(10^x)+ log(10^y) = x + y; Same for subtraction.

Only can do +, -, * , / operations, no loops: https://github.com/google/fully-homomorphic-encryption/tree/main/transpiler

On a lattice, it's then just a affine jump - compute offset + (x,y)

On top you can use the "Vernam" XOR-cypher to make it quantum safe:

https://en.wikipedia.org/wiki/XOR_cipher
https://en.wikipedia.org/wiki/Gilbert_Vernam

Interestingly you don't need to precompute so many numbers. You can do a stepwise approach:

log(10,0 + 0,1) = ?

This formula helps: ln(a + b) = ln(a) + ln(1 + b/a) = ln(b) + ln(1 + a/b)

So to reduce the amount of precomputed values on an endless lattice, you can compute the logarithms step-wise to finally reach the needed accuracy. That's why FHE typically is dog-slow (several seconds per operation).

To further increase compute on Linux:

https://man7.org/linux/man-pages/man2/memfd_secret.2.html

Note: You need to activate this with a special boot parameter. It's no default.

Howto build your own "formally verifyable" functional language

Justine Tunney is a brilliant programmer to learn from. She implemented her own lambda operator in C and x86 assembler to put her own small Lisp on top. It has everything, modern functional programming languages have, like a fully featured garbage collector, tail recursion, even (Haskell's) lazyness.

Implemented in under 512 bytes: http://justine.lol/sectorlisp

Also see: http://justine.lol/lambda

Note: Only simple systems are (single human) understandable, verifiable and finally reliable and maintainable. Especially interpreters that fit on one A4 page!

The C version of her lambda interpreter you can easily extend with C libraries, of course! See: https://rentry.co/DSRsecuritycoursepart11

Have fun!

Back to last lesson - https://rentry.co/DSRsecuritycoursepart5 Next lesson: https://rentry.co/DSRsecuritycoursepart7

Edit
Pub: 27 Jun 2024 09:17 UTC
Edit: 24 Jul 2024 13:11 UTC
Views: 511