Add files using upload-large-folder tool

.gitattributes

@@ -33,3 +33,32 @@ saved_model/**/* filter=lfs diff=lfs merge=lfs -text
 *.zip filter=lfs diff=lfs merge=lfs -text
 *.zst filter=lfs diff=lfs merge=lfs -text
 *tfevents* filter=lfs diff=lfs merge=lfs -text
+align.bundle filter=lfs diff=lfs merge=lfs -text
+code/notes/0102[[:space:]]-[[:space:]]Policy[[:space:]]Gradient[[:space:]]and[[:space:]]Baselines.pdf filter=lfs diff=lfs merge=lfs -text
+code/notes/0103[[:space:]]-[[:space:]]Importance[[:space:]]Sampling[[:space:]]and[[:space:]]Off-Policy[[:space:]]Updates.pdf filter=lfs diff=lfs merge=lfs -text
+code/notes/0101[[:space:]]-[[:space:]]Autoregressive[[:space:]]Likelihood[[:space:]]and[[:space:]]SFT.pdf filter=lfs diff=lfs merge=lfs -text
+code/notes/0104[[:space:]]-[[:space:]]Trust[[:space:]]Regions[[:space:]]and[[:space:]]the[[:space:]]PPO[[:space:]]Clip.pdf filter=lfs diff=lfs merge=lfs -text
+code/notes/0106[[:space:]]-[[:space:]]DAPO.pdf filter=lfs diff=lfs merge=lfs -text
+code/notes/0105[[:space:]]-[[:space:]]GRPO[[:space:]]and[[:space:]]Dr[[:space:]]GRPO.pdf filter=lfs diff=lfs merge=lfs -text
+code/notes/0109[[:space:]]-[[:space:]]KL[[:space:]]Estimators.pdf filter=lfs diff=lfs merge=lfs -text
+code/notes/0107[[:space:]]-[[:space:]]CISPO.pdf filter=lfs diff=lfs merge=lfs -text
+code/notes/0108[[:space:]]-[[:space:]]Training-Inference[[:space:]]Mismatch.pdf filter=lfs diff=lfs merge=lfs -text
+code/notes/0202[[:space:]]-[[:space:]]Rejection[[:space:]]Sampling[[:space:]]and[[:space:]]Expert[[:space:]]Iteration[[:space:]]as[[:space:]]Policy[[:space:]]Improvement.pdf filter=lfs diff=lfs merge=lfs -text
+code/notes/0201[[:space:]]-[[:space:]]Verifier[[:space:]]in[[:space:]]the[[:space:]]Loop[[:space:]]as[[:space:]]a[[:space:]]Binary-Reward[[:space:]]MDP.pdf filter=lfs diff=lfs merge=lfs -text
+code/notes/0110[[:space:]]-[[:space:]]Reward[[:space:]]Shaping[[:space:]]for[[:space:]]Verifier[[:space:]]Rewards.pdf filter=lfs diff=lfs merge=lfs -text
+code/notes/0203[[:space:]]-[[:space:]]pass@k[[:space:]]Estimator,[[:space:]]Variance[[:space:]]and[[:space:]]the[[:space:]]pass@1[[:space:]]Trade-off.pdf filter=lfs diff=lfs merge=lfs -text
+code/notes/0204[[:space:]]-[[:space:]]Self-Correction[[:space:]]as[[:space:]]a[[:space:]]Multi-Turn[[:space:]]MDP.pdf filter=lfs diff=lfs merge=lfs -text
+code/notes/0205[[:space:]]-[[:space:]]Model[[:space:]]Averaging[[:space:]]and[[:space:]]Weight[[:space:]]Interpolation.pdf filter=lfs diff=lfs merge=lfs -text
+code/notes/0207[[:space:]]-[[:space:]]Test-Time[[:space:]]Scaling[[:space:]]Cost[[:space:]]Model.pdf filter=lfs diff=lfs merge=lfs -text
+code/notes/0206[[:space:]]-[[:space:]]Curriculum[[:space:]]by[[:space:]]Pass-Rate[[:space:]]Band.pdf filter=lfs diff=lfs merge=lfs -text
+code/notes/0208[[:space:]]-[[:space:]]Statistics[[:space:]]of[[:space:]]Evaluation.pdf filter=lfs diff=lfs merge=lfs -text
+code/notes/0209[[:space:]]-[[:space:]]Variance[[:space:]]Components[[:space:]]and[[:space:]]Equivalence[[:space:]]Tests.pdf filter=lfs diff=lfs merge=lfs -text
+code/notes/0210[[:space:]]-[[:space:]]Data[[:space:]]Selection[[:space:]]and[[:space:]]Contamination.pdf filter=lfs diff=lfs merge=lfs -text
+code/notes/0301[[:space:]]-[[:space:]]Curry-Howard.pdf filter=lfs diff=lfs merge=lfs -text
+code/notes/0302[[:space:]]-[[:space:]]Dependent[[:space:]]Types.pdf filter=lfs diff=lfs merge=lfs -text
+code/notes/0303[[:space:]]-[[:space:]]Hoare[[:space:]]Logic[[:space:]]and[[:space:]]Refinement.pdf filter=lfs diff=lfs merge=lfs -text
+code/notes/0304[[:space:]]-[[:space:]]Failed[[:space:]]Proof[[:space:]]to[[:space:]]Bug.pdf filter=lfs diff=lfs merge=lfs -text
+code/notes/0305[[:space:]]-[[:space:]]Spec[[:space:]]Generation[[:space:]]Risk.pdf filter=lfs diff=lfs merge=lfs -text
+code/notes/0306[[:space:]]-[[:space:]]Verified[[:space:]]Code[[:space:]]Benchmarks.pdf filter=lfs diff=lfs merge=lfs -text
+code/notes/0307[[:space:]]-[[:space:]]Aeneas[[:space:]]Semantics.pdf filter=lfs diff=lfs merge=lfs -text
+code/align/assets/tokenizer/goedel-prover-v2-8b/tokenizer.json filter=lfs diff=lfs merge=lfs -text

align.bundle

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:df359f82968d15e36d48b4b604240543f253978d711d41f48401b1da00388b1e
+size 18368694

code/align/assets/tokenizer/goedel-prover-v2-8b/tokenizer.json

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:aeb13307a71acd8fe81861d94ad54ab689df773318809eed3cbe794b4492dae4
+size 11422654

code/assets/tokenizer/mistral-7b-v0.3/tokenizer.model

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:37f00374dea48658ee8f5d0f21895b9bc55cb0103939607c8185bfd1c6ca1f89
+size 587404

code/bugfind/bench/kernels/mldsa_norm/post/src/lib.rs

@@ -0,0 +1,3 @@
+pub fn response_bound(gamma1_exponent: u32, beta: i32) -> i32 {
+    (1i32 << gamma1_exponent) - beta
+}

code/bugfind/bench/kernels/mldsa_norm/pre/Cargo.toml

@@ -0,0 +1,9 @@
+[package]
+name = "k_mldsa_norm_pre"
+version = "0.1.0"
+edition = "2021"
+
+[lib]
+path = "src/lib.rs"
+
+[workspace]

code/bugfind/bench/kernels/mldsa_norm/pre/src/lib.rs

@@ -0,0 +1,3 @@
+pub fn response_bound(gamma1_exponent: u32, beta: i32) -> i32 {
+    (2i32 << gamma1_exponent) - beta
+}

code/bugfind/bench/kernels/nanoid_mask/post/Cargo.lock

@@ -0,0 +1,7 @@
+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+version = 4
+
+[[package]]
+name = "k_nanoid_mask_post"
+version = "0.1.0"

code/bugfind/bench/kernels/nanoid_mask/post/Cargo.toml

@@ -0,0 +1,9 @@
+[package]
+name = "k_nanoid_mask_post"
+version = "0.1.0"
+edition = "2021"
+
+[lib]
+path = "src/lib.rs"
+
+[workspace]

code/bugfind/bench/kernels/nanoid_mask/post/src/lib.rs

@@ -0,0 +1,7 @@
+pub fn alphabet_mask(len: usize) -> usize {
+    let mut p = 1usize;
+    while p < len {
+        p = p * 2;
+    }
+    p - 1
+}

code/bugfind/bench/kernels/nanoid_mask/pre/Cargo.lock

@@ -0,0 +1,7 @@
+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+version = 4
+
+[[package]]
+name = "k_nanoid_mask_pre"
+version = "0.1.0"

code/bugfind/bench/kernels/nanoid_mask/pre/Cargo.toml

@@ -0,0 +1,9 @@
+[package]
+name = "k_nanoid_mask_pre"
+version = "0.1.0"
+edition = "2021"
+
+[lib]
+path = "src/lib.rs"
+
+[workspace]

code/bugfind/bench/kernels/nanoid_mask/pre/src/lib.rs

@@ -0,0 +1,3 @@
+pub fn alphabet_mask(len: usize) -> usize {
+    len - 1
+}

code/bugfind/bench/kernels/nostr_iv/post/Cargo.lock

@@ -0,0 +1,7 @@
+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+version = 4
+
+[[package]]
+name = "k_nostr_iv_post"
+version = "0.1.0"

code/bugfind/bench/kernels/nostr_iv/post/Cargo.toml

@@ -0,0 +1,9 @@
+[package]
+name = "k_nostr_iv_post"
+version = "0.1.0"
+edition = "2021"
+
+[lib]
+path = "src/lib.rs"
+
+[workspace]

code/bugfind/bench/kernels/nostr_iv/post/src/lib.rs

@@ -0,0 +1,12 @@
+pub fn load_iv(iv: &[u8]) -> Result<[u8; 16], u8> {
+    if iv.len() != 16 {
+        return Err(1);
+    }
+    let mut out = [0u8; 16];
+    let mut i = 0usize;
+    while i < 16 {
+        out[i] = iv[i];
+        i += 1;
+    }
+    Ok(out)
+}

code/bugfind/bench/kernels/nostr_iv/pre/Cargo.lock

@@ -0,0 +1,7 @@
+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+version = 4
+
+[[package]]
+name = "k_nostr_iv_pre"
+version = "0.1.0"

code/bugfind/bench/kernels/nostr_iv/pre/Cargo.toml

@@ -0,0 +1,9 @@
+[package]
+name = "k_nostr_iv_pre"
+version = "0.1.0"
+edition = "2021"
+
+[lib]
+path = "src/lib.rs"
+
+[workspace]

code/bugfind/bench/kernels/nostr_iv/pre/src/lib.rs

@@ -0,0 +1,9 @@
+pub fn load_iv(iv: &[u8]) -> Result<[u8; 16], u8> {
+    let mut out = [0u8; 16];
+    let mut i = 0usize;
+    while i < 16 {
+        out[i] = iv[i];
+        i += 1;
+    }
+    Ok(out)
+}

code/bugfind/bench/kernels/odoh_split/post/Cargo.lock

@@ -0,0 +1,7 @@
+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+version = 4
+
+[[package]]
+name = "k_odoh_split_post"
+version = "0.1.0"

code/bugfind/bench/kernels/odoh_split/post/Cargo.toml

@@ -0,0 +1,9 @@
+[package]
+name = "k_odoh_split_post"
+version = "0.1.0"
+edition = "2021"
+
+[lib]
+path = "src/lib.rs"
+
+[workspace]

code/bugfind/bench/kernels/odoh_split/post/src/lib.rs

@@ -0,0 +1,7 @@
+pub fn encrypted_payload_len(msg: &[u8], key_size: usize) -> Result<usize, u8> {
+    if key_size > msg.len() {
+        return Err(1);
+    }
+    let ct = &msg[key_size..];
+    Ok(ct.len())
+}

code/bugfind/bench/kernels/odoh_split/pre/Cargo.lock

@@ -0,0 +1,7 @@
+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+version = 4
+
+[[package]]
+name = "k_odoh_split_pre"
+version = "0.1.0"

code/bugfind/bench/kernels/odoh_split/pre/Cargo.toml

@@ -0,0 +1,9 @@
+[package]
+name = "k_odoh_split_pre"
+version = "0.1.0"
+edition = "2021"
+
+[lib]
+path = "src/lib.rs"
+
+[workspace]

code/bugfind/bench/kernels/odoh_split/pre/src/lib.rs

@@ -0,0 +1,4 @@
+pub fn encrypted_payload_len(msg: &[u8], key_size: usize) -> Result<usize, u8> {
+    let ct = &msg[key_size..];
+    Ok(ct.len())
+}

code/bugfind/bench/kernels/phone_ctx/post/Cargo.lock

@@ -0,0 +1,7 @@
+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+version = 4
+
+[[package]]
+name = "k_phone_ctx_post"
+version = "0.1.0"

code/bugfind/bench/kernels/phone_ctx/post/Cargo.toml

@@ -0,0 +1,9 @@
+[package]
+name = "k_phone_ctx_post"
+version = "0.1.0"
+edition = "2021"
+
+[lib]
+path = "src/lib.rs"
+
+[workspace]

code/bugfind/bench/kernels/phone_ctx/post/src/lib.rs

@@ -0,0 +1,3 @@
+pub fn context_prefix_skip(s: &[u8]) -> usize {
+    if !s.is_empty() && s[0] == b'+' { 1 } else { 0 }
+}

code/bugfind/bench/kernels/phone_ctx/pre/Cargo.lock

@@ -0,0 +1,7 @@
+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+version = 4
+
+[[package]]
+name = "k_phone_ctx_pre"
+version = "0.1.0"

code/bugfind/bench/kernels/phone_ctx/pre/Cargo.toml

@@ -0,0 +1,9 @@
+[package]
+name = "k_phone_ctx_pre"
+version = "0.1.0"
+edition = "2021"
+
+[lib]
+path = "src/lib.rs"
+
+[workspace]

code/bugfind/bench/kernels/phone_ctx/pre/src/lib.rs

@@ -0,0 +1,3 @@
+pub fn context_prefix_skip(s: &[u8]) -> usize {
+    if s[0] == b'+' { 1 } else { 0 }
+}

code/bugfind/bench/kernels/poly1305_key/post/Cargo.lock

@@ -0,0 +1,7 @@
+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+version = 4
+
+[[package]]
+name = "k_poly1305_key_post"
+version = "0.1.0"

code/bugfind/bench/kernels/poly1305_key/post/Cargo.toml

@@ -0,0 +1,9 @@
+[package]
+name = "k_poly1305_key_post"
+version = "0.1.0"
+edition = "2021"
+
+[lib]
+path = "src/lib.rs"
+
+[workspace]

code/bugfind/bench/kernels/poly1305_key/post/src/lib.rs

@@ -0,0 +1,4 @@
+pub const KEY_LEN: usize = 32;
+pub fn key_len_ok(key: &[u8]) -> bool {
+    key.len() == KEY_LEN
+}

code/bugfind/bench/kernels/poly1305_key/pre/Cargo.lock

@@ -0,0 +1,7 @@
+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+version = 4
+
+[[package]]
+name = "k_poly1305_key_pre"
+version = "0.1.0"

code/bugfind/bench/kernels/poly1305_key/pre/Cargo.toml

@@ -0,0 +1,9 @@
+[package]
+name = "k_poly1305_key_pre"
+version = "0.1.0"
+edition = "2021"
+
+[lib]
+path = "src/lib.rs"
+
+[workspace]

code/bugfind/bench/kernels/poly1305_key/pre/src/lib.rs

@@ -0,0 +1,4 @@
+pub const KEY_LEN: usize = 16;
+pub fn key_len_ok(key: &[u8]) -> bool {
+    key.len() == KEY_LEN
+}

code/bugfind/bench/kernels/ring_ctr/post/Cargo.lock

@@ -0,0 +1,7 @@
+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+version = 4
+
+[[package]]
+name = "k_ring_ctr_post"
+version = "0.1.0"

code/bugfind/bench/kernels/ring_ctr/post/Cargo.toml

@@ -0,0 +1,9 @@
+[package]
+name = "k_ring_ctr_post"
+version = "0.1.0"
+edition = "2021"
+
+[lib]
+path = "src/lib.rs"
+
+[workspace]

code/bugfind/bench/kernels/ring_ctr/post/src/lib.rs

@@ -0,0 +1,3 @@
+pub fn increment_by(old_value: u32, increment_by: u32) -> u32 {
+    old_value.wrapping_add(increment_by)
+}

code/bugfind/bench/kernels/ring_ctr/pre/Cargo.lock

@@ -0,0 +1,7 @@
+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+version = 4
+
+[[package]]
+name = "k_ring_ctr_pre"
+version = "0.1.0"

code/bugfind/bench/kernels/ring_ctr/pre/Cargo.toml

@@ -0,0 +1,9 @@
+[package]
+name = "k_ring_ctr_pre"
+version = "0.1.0"
+edition = "2021"
+
+[lib]
+path = "src/lib.rs"
+
+[workspace]

code/bugfind/bench/kernels/ring_ctr/pre/src/lib.rs

@@ -0,0 +1,3 @@
+pub fn increment_by(old_value: u32, increment_by: u32) -> u32 {
+    old_value + increment_by
+}

code/bugfind/bench/kernels/stack_insert/post/Cargo.lock

@@ -0,0 +1,7 @@
+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+version = 4
+
+[[package]]
+name = "k_stack_insert_post"
+version = "0.1.0"

code/bugfind/bench/kernels/stack_insert/post/Cargo.toml

@@ -0,0 +1,9 @@
+[package]
+name = "k_stack_insert_post"
+version = "0.1.0"
+edition = "2021"
+
+[lib]
+path = "src/lib.rs"
+
+[workspace]

code/bugfind/bench/kernels/stack_insert/post/src/lib.rs

@@ -0,0 +1,6 @@
+pub fn insert_shift_len(len: usize, index: usize) -> Result<usize, u8> {
+    if index > len {
+        return Err(1);
+    }
+    Ok(len - index)
+}

code/bugfind/bench/kernels/stack_insert/pre/Cargo.lock

@@ -0,0 +1,7 @@
+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+version = 4
+
+[[package]]
+name = "k_stack_insert_pre"
+version = "0.1.0"

code/bugfind/bench/kernels/stack_insert/pre/Cargo.toml

@@ -0,0 +1,9 @@
+[package]
+name = "k_stack_insert_pre"
+version = "0.1.0"
+edition = "2021"
+
+[lib]
+path = "src/lib.rs"
+
+[workspace]

code/bugfind/bench/kernels/stack_insert/pre/src/lib.rs

@@ -0,0 +1,3 @@
+pub fn insert_shift_len(len: usize, index: usize) -> Result<usize, u8> {
+    Ok(len.wrapping_sub(index))
+}

code/bugfind/bench/kernels/tar_pax/post/Cargo.lock

@@ -0,0 +1,7 @@
+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+version = 4
+
+[[package]]
+name = "k_tar_pax_post"
+version = "0.1.0"