commit c2731fdb4334a289e4e2216a76b75e13263fb73b
Author: Michael Zhang <mail@mzhang.io>
Date:   Fri Jun 11 00:07:55 2021 -0500

    initial

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..9c5f578
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1 @@
+_build
\ No newline at end of file
diff --git a/CoqSSH.opam b/CoqSSH.opam
new file mode 100644
index 0000000..5538a8b
--- /dev/null
+++ b/CoqSSH.opam
@@ -0,0 +1 @@
+name: "CoqSSH"
\ No newline at end of file
diff --git a/Extract.v b/Extract.v
new file mode 100644
index 0000000..e160ee8
--- /dev/null
+++ b/Extract.v
@@ -0,0 +1,6 @@
+From Coq Require Extraction.
+
+Require CSSH.
+
+Extraction "SSH" SSH.
+Extraction "CryptoPrims" CryptoPrims.
\ No newline at end of file
diff --git a/coq_ssh.ml b/coq_ssh.ml
new file mode 100644
index 0000000..03a02b9
--- /dev/null
+++ b/coq_ssh.ml
@@ -0,0 +1,37 @@
+open Unix
+open Printf
+open CoqSSH
+
+let () =
+  let addr_str = "10.7.0.4" in
+
+  let socket_fd = socket PF_INET SOCK_STREAM 0 in
+  let inet_addr = inet_addr_of_string addr_str in
+  let sock_addr = ADDR_INET (inet_addr, 22) in
+
+  connect socket_fd sock_addr;
+  printf "Connected to %s.\n" addr_str;
+
+  (* protocol negotiation *)
+
+  let hello = "2.0 Hellosu\r\n" |> Bytes.of_string in
+  let bytes_written = write socket_fd hello 0 (Bytes.length hello) in
+  printf "Sent greeting (%d bytes).\n" bytes_written;
+
+  let buf = Bytes.create 1024 in
+  let bytes_read = read socket_fd buf 0 1024 in
+  let actual = Bytes.sub buf 0 bytes_read |> Bytes.to_string in
+  printf "Read '%s' (%d bytes).\n" actual bytes_read;
+
+  let version = "SSH-2.0-CoqSSH0.1 Coggers\r\n" |> Bytes.of_string in
+  let bytes_written = write socket_fd version 0 (Bytes.length version) in
+  printf "Sent protocol version (%d bytes).\n" bytes_written;
+
+  (* key exchange *)
+
+  let n : SSH.nat = SSH.O in
+  match n with
+  | SSH.O -> print_endline "o"
+  | _ -> ();
+
+  close socket_fd;
diff --git a/crypto_prims.ml b/crypto_prims.ml
new file mode 100644
index 0000000..3d638ed
--- /dev/null
+++ b/crypto_prims.ml
@@ -0,0 +1,44 @@
+module IFC = struct
+  (*
+  "Principals" are people (or hosts, or organizations) that may have
+  different access to information. It's described here by a string;
+  each principal has a unique string.
+  *)
+  type principal = string
+
+  (*
+  Labels represent who is allowed to have access to a certain piece
+  of information. Labels form a lattice, with Public at the bottom and
+  Secret at the top.
+
+  Every time information flows through the program,
+  it must be checked to make sure that it's not revealing information
+  when it isn't allowed to.
+
+  For example, 
+  *)
+  type label =
+    (* a list of principals that have access to the information described
+    by this label *)
+    | LCanRead of principal list
+
+    (* join of 2 labels *)
+    | LJoin of label * label
+
+    (* bottom of the lattice *)
+    | LPublic
+
+  (* base type of bytes *)
+  type bytes =
+    (* a literal string *)
+    | BLit of string
+    (* 2 sets of byte-strings concatenated *)
+    | BConcat of bytes * bytes
+    (* cryptographically random set of bytes *)
+    | BRand of principal
+end
+
+module type CryptoPrims = sig
+  (* A function for generating a random nonce of n bytes *)
+  (* val rand :  *)
+end
\ No newline at end of file
diff --git a/dune b/dune
new file mode 100644
index 0000000..66d2511
--- /dev/null
+++ b/dune
@@ -0,0 +1,9 @@
+(executable
+ (name coq_ssh)
+ (public_name coq_ssh)
+ (libraries unix CoqSSH)
+ (package CoqSSH))
+
+(env
+  (dev
+    (flags (:standard -warn-error -A))))
diff --git a/dune-project b/dune-project
new file mode 100644
index 0000000..c8d78ef
--- /dev/null
+++ b/dune-project
@@ -0,0 +1,2 @@
+(lang dune 2.8)
+(using coq 0.3)
diff --git a/theories/CryptoPrims.v b/theories/CryptoPrims.v
new file mode 100644
index 0000000..e79832e
--- /dev/null
+++ b/theories/CryptoPrims.v
@@ -0,0 +1,30 @@
+From Coq Require Extraction.
+Require Import Strings.String.
+
+(*
+Abstract cryptographic primitives.
+
+For proof-checking, this will resolve to a set of axioms, but when
+extracting to ocaml, this should be replaced with the real implementation
+of the cryptographic primitives.
+*)
+Module Type AbsCryptoPrims.
+  Definition principal : Type := string.
+
+  Inductive label : Set :=
+    Public : label
+  .
+End AbsCryptoPrims.
+
+Module NullCryptoPrims : AbsCryptoPrims.
+  Definition principal : Type := string.
+
+  Inductive label : Set :=
+    Public : label
+  .
+End NullCryptoPrims.
+
+Extraction Language OCaml.
+Set Extraction Optimize.
+Set Extraction AccessOpaque.
+Extraction "CryptoPrims" NullCryptoPrims.
diff --git a/theories/SSH.v b/theories/SSH.v
new file mode 100644
index 0000000..b473174
--- /dev/null
+++ b/theories/SSH.v
@@ -0,0 +1,15 @@
+From Coq Require Extraction.
+Module SSH.
+
+Inductive natlist : Type :=
+  | nil
+  | cons (n : nat) (l : natlist).
+
+Fixpoint length (l:natlist) : nat :=
+  match l with
+  | nil => O
+  | cons h t => S (length t)
+  end.
+
+End SSH.
+Extraction "SSH" SSH.
diff --git a/theories/dune b/theories/dune
new file mode 100644
index 0000000..865ea5b
--- /dev/null
+++ b/theories/dune
@@ -0,0 +1,11 @@
+(library
+  (name CoqSSH)
+  (package CoqSSH))
+
+(coq.extraction
+ (prelude SSH)
+ (extracted_modules SSH))
+
+(coq.extraction
+ (prelude CryptoPrims)
+ (extracted_modules CryptoPrims))