diff --git a/.dockerignore b/.dockerignore
new file mode 100644
index 0000000..89f5b3c
--- /dev/null
+++ b/.dockerignore
@@ -0,0 +1,3 @@
+target/
+.git/
+**/.DS_Store
diff --git a/.github/workflows/secure_release.yml b/.github/workflows/secure_release.yml
index 8294193..61be607 100644
--- a/.github/workflows/secure_release.yml
+++ b/.github/workflows/secure_release.yml
@@ -1,8 +1,6 @@
 name: Secure Release & Publish Pipeline
 
 on:
-  pull_request:
-    branches: [ master ]
   push:
     tags:
       - 'v*.*.*'
diff --git a/core/constant-time/Cargo.toml b/core/constant-time/Cargo.toml
index 56b1d46..16d2999 100644
--- a/core/constant-time/Cargo.toml
+++ b/core/constant-time/Cargo.toml
@@ -7,21 +7,18 @@ license.workspace = true
 
 [dependencies]
 
-[dev-dependencies]
-dudect-bencher = "0.6.0"
-rand = "0.10.0"
-
 [build-dependencies]
 cc = "1.0.106"
 
 [features]
 default = []
 audit_mode = []
+saw_verify = ["audit_mode"]
 valgrind_taint_audit = []
 
-[[bench]]
-name = "dudect_audit"
-harness = false
+[[bin]]
+name = "dudect-eval"
+path = "dudect/main.rs"
 
 [[test]]
 name = "taint_audit"
diff --git a/core/constant-time/benches/dudect_audit.rs b/core/constant-time/benches/dudect_audit.rs
deleted file mode 100644
index ffd40c8..0000000
--- a/core/constant-time/benches/dudect_audit.rs
+++ /dev/null
@@ -1,88 +0,0 @@
-//! TODO: 베어메탈에서 실행되야 할 벤치마킹입니다. 구글링해보니 퍼블릭 클라우드 인프라 서비스는
-//!       VM에 노이즈와 하이퍼바이저 개입으로 인해 t-test 값이 오염된다고 합니다.
-//!       운영체제 전원 관리 및 CPU 클럭 변동 기술을 BIOS/UEFI 수준에서 비활성화하거나,
-//!       OS에서 주파수를 고정해야 한다고 하네요... 잘은 모르겠습니다.
-//!
-//! DudeCT 벤치마크는 최적화 방지 및 런타임 벤치마킹 기능 활용을 위해 nightly 툴체인이 권장됩니다.
-//! 다음과 같이 빌드 후 바이너리를 실행하여 벤치마킹 할 수 있습니다.
-//! ```bash
-//! # 빌드
-//! $ cargo +nightly build --release -p entlib-native-constant-time --bench dudect_audit
-//!
-//! # 실행
-//! $ ./target/release/deps/dudect_audit-...
-//! ```
-
-use dudect_bencher::rand::Rng;
-use dudect_bencher::{BenchRng, Class, CtRunner, ctbench_main};
-use entlib_native_constant_time::choice::Choice;
-use entlib_native_constant_time::traits::{ConstantTimeEq, ConstantTimeSelect};
-
-/// [ConstantTimeEq::ct_eq] 검증
-/// 두 값이 완벽히 동일한 경우([Class::Right])와 서로 다른 경우([Class::Left])의
-/// 연산 소요 시간 분포를 교차 검증합니다.
-fn bench_ct_eq(runner: &mut CtRunner, rng: &mut BenchRng) {
-    let mut inputs = vec![(0u64, 0u64); 100_000];
-    let mut classes = vec![Class::Right; 100_000];
-
-    for (input, class) in inputs.iter_mut().zip(classes.iter_mut()) {
-        let a: u64 = rng.r#gen();
-        let b: u64 = rng.r#gen();
-
-        // 50% 확률로 동일한 값 쌍과 다른 값 쌍을 생성
-        if rng.r#gen::<bool>() {
-            *input = (a, a);
-            *class = Class::Right; // 일치 상태
-        } else {
-            *input = (a, b);
-            *class = Class::Left; // 불일치 상태
-        }
-    }
-
-    for (class, (a, b)) in classes.into_iter().zip(inputs.into_iter()) {
-        runner.run_one(class, || {
-            // black_box를 통해 컴파일러 DCE 최적화 억제
-            let _ =
-                core::hint::black_box(core::hint::black_box(a).ct_eq(core::hint::black_box(&b)));
-        });
-    }
-}
-
-/// [ConstantTimeSelect::ct_select] 검증
-/// 조건 마스크가 0xFF(True)인 경우([Class::Right])와 0x00(False)인 경우([Class::Left])
-/// 데이터 선택 과정에서 타이밍 차이가 발생하는지 검증합니다.
-fn bench_ct_select(runner: &mut CtRunner, rng: &mut BenchRng) {
-    let mut inputs = vec![(0u64, 0u64, 0u8); 100_000];
-    let mut classes = vec![Class::Right; 100_000];
-
-    for (input, class) in inputs.iter_mut().zip(classes.iter_mut()) {
-        let a: u64 = rng.r#gen();
-        let b: u64 = rng.r#gen();
-
-        if rng.r#gen::<bool>() {
-            *input = (a, b, 0xFF);
-            *class = Class::Right; // True 분기
-        } else {
-            *input = (a, b, 0x00);
-            *class = Class::Left; // False 분기
-        }
-    }
-
-    for (class, (a, b, mask)) in classes.into_iter().zip(inputs.into_iter()) {
-        // Choice 구조체의 내부 필드는 private이라서 벤치마크 환경에 한하여
-        // 메모리 transmute를 통해 강제로 마스크 값 주입
-        let choice = unsafe { core::mem::transmute::<u8, Choice>(mask) };
-
-        runner.run_one(class, || {
-            let _ = core::hint::black_box(u64::ct_select(
-                core::hint::black_box(&a),
-                core::hint::black_box(&b),
-                core::hint::black_box(choice),
-            ));
-        });
-    }
-}
-
-// todo: 더
-
-ctbench_main!(bench_ct_eq, bench_ct_select);
diff --git a/core/constant-time/dudect/main.rs b/core/constant-time/dudect/main.rs
new file mode 100644
index 0000000..83ea59e
--- /dev/null
+++ b/core/constant-time/dudect/main.rs
@@ -0,0 +1,326 @@
+#![allow(unsafe_code)]
+
+//! # DudeCT 통계적 타이밍 분석
+//! "dude, is my code constant time?" (Reparaz et al., CHES 2017)
+//! 대상: Ubuntu 24.04 x86_64 베어메탈
+
+use std::hint::black_box;
+
+use entlib_native_constant_time::traits::{
+    ConstantTimeEq, ConstantTimeIsNegative, ConstantTimeIsZero, ConstantTimeSelect,
+    ConstantTimeSwap,
+};
+
+const N: usize = 1_000_000;
+const CROP: f64 = 0.05;
+const T_WARN: f64 = 4.5;
+const T_FAIL: f64 = 10.0;
+const MAX_CYCLES: u64 = 10_000;
+
+// Xoshiro256** PRNG — 외부 의존성 없음
+struct Prng([u64; 4]);
+
+impl Prng {
+    fn from_seed(seed: u64) -> Self {
+        let mut x = seed;
+        let mut sm = || {
+            x = x.wrapping_add(0x9e3779b97f4a7c15);
+            x = (x ^ (x >> 30)).wrapping_mul(0xbf58476d1ce4e5b9);
+            x = (x ^ (x >> 27)).wrapping_mul(0x94d049bb133111eb);
+            x ^ (x >> 31)
+        };
+        Self([sm(), sm(), sm(), sm()])
+    }
+
+    #[inline]
+    fn u64(&mut self) -> u64 {
+        let r = self.0[1].wrapping_mul(5).rotate_left(7).wrapping_mul(9);
+        let t = self.0[1] << 17;
+        self.0[2] ^= self.0[0];
+        self.0[3] ^= self.0[1];
+        self.0[1] ^= self.0[2];
+        self.0[0] ^= self.0[3];
+        self.0[2] ^= t;
+        self.0[3] = self.0[3].rotate_left(45);
+        r
+    }
+}
+
+/// # Security Note
+/// LFENCE는 이전 명령어가 완전히 retire된 후 RDTSC가 실행되도록 보장하여
+/// 측정 외부 명령어가 측정 구간으로 재정렬되는 것을 방지합니다.
+#[inline(always)]
+fn tsc() -> u64 {
+    #[cfg(all(target_arch = "x86_64", target_feature = "sse2"))]
+    unsafe {
+        core::arch::x86_64::_mm_lfence();
+        core::arch::x86_64::_rdtsc()
+    }
+    #[cfg(not(all(target_arch = "x86_64", target_feature = "sse2")))]
+    {
+        use std::time::{SystemTime, UNIX_EPOCH};
+        SystemTime::now()
+            .duration_since(UNIX_EPOCH)
+            .map(|d| d.subsec_nanos() as u64)
+            .unwrap_or(0)
+    }
+}
+
+// Welch's t-검정 — Welford 온라인 알고리즘 (수치 안정성)
+#[derive(Default)]
+struct Ttest {
+    n:    [u64; 2],
+    mean: [f64; 2],
+    m2:   [f64; 2],
+}
+
+impl Ttest {
+    fn push(&mut self, class: usize, x: f64) {
+        self.n[class] += 1;
+        let d = x - self.mean[class];
+        self.mean[class] += d / self.n[class] as f64;
+        self.m2[class] += d * (x - self.mean[class]);
+    }
+
+    fn t(&self) -> f64 {
+        let (n0, n1) = (self.n[0] as f64, self.n[1] as f64);
+        if n0 < 2.0 || n1 < 2.0 {
+            return 0.0;
+        }
+        let se = ((self.m2[0] / (n0 - 1.0)) / n0 + (self.m2[1] / (n1 - 1.0)) / n1).sqrt();
+        if se == 0.0 { 0.0 } else { (self.mean[0] - self.mean[1]) / se }
+    }
+}
+
+fn parse_args() -> usize {
+    let args: Vec<String> = std::env::args().collect();
+    let mut warmup: usize = 10_000;
+    let mut i = 1;
+    while i < args.len() {
+        match args[i].as_str() {
+            "--warmup" | "-w" => {
+                i += 1;
+                match args.get(i).and_then(|s| s.parse().ok()) {
+                    Some(v) => warmup = v,
+                    None => {
+                        eprintln!("오류: --warmup 인자는 양의 정수여야 합니다.");
+                        eprintln!("사용법: dudect-eval [--warmup <N> | -w <N>]");
+                        std::process::exit(1);
+                    }
+                }
+            }
+            arg => {
+                eprintln!("오류: 알 수 없는 인자 '{arg}'");
+                eprintln!("사용법: dudect-eval [--warmup <N> | -w <N>]");
+                std::process::exit(1);
+            }
+        }
+        i += 1;
+    }
+    warmup
+}
+
+fn dudect<F>(label: &str, warmup: usize, rng: &mut Prng, mut f: F) -> bool
+where
+    F: FnMut(usize, &mut Prng) -> u64,
+{
+    for _ in 0..warmup {
+        let class = (rng.u64() & 1) as usize;
+        let _ = black_box(f(class, rng));
+    }
+
+    let mut c0: Vec<u64> = Vec::with_capacity(N / 2 + 1);
+    let mut c1: Vec<u64> = Vec::with_capacity(N / 2 + 1);
+
+    for _ in 0..N {
+        let class = (rng.u64() & 1) as usize;
+        let elapsed = f(class, rng);
+        if elapsed > 0 && elapsed < MAX_CYCLES {
+            if class == 0 { c0.push(elapsed); } else { c1.push(elapsed); }
+        }
+    }
+
+    // 상위 CROP% 이상값 제거 (OS 인터럽트 / 캐시 미스 필터링)
+    c0.sort_unstable();
+    c1.sort_unstable();
+    c0.truncate((c0.len() as f64 * (1.0 - CROP)) as usize);
+    c1.truncate((c1.len() as f64 * (1.0 - CROP)) as usize);
+
+    let mut tt = Ttest::default();
+    c0.iter().for_each(|&v| tt.push(0, v as f64));
+    c1.iter().for_each(|&v| tt.push(1, v as f64));
+
+    let t = tt.t();
+    let a = t.abs();
+    let s = if a < T_WARN { "PASS" } else if a < T_FAIL { "WARN" } else { "FAIL" };
+    println!("  {:<48} t={:+8.3}  [{s}]", label, t);
+    a < T_WARN
+}
+
+fn main() {
+    let seed = std::time::SystemTime::now()
+        .duration_since(std::time::UNIX_EPOCH)
+        .map(|d| d.as_nanos() as u64 ^ d.as_secs().wrapping_mul(0x517cc1b727220a95))
+        .unwrap_or(0xdeadbeef_cafef00d);
+
+    let warmup = parse_args();
+    let mut rng = Prng::from_seed(seed);
+    let mut ok = true;
+    let sep = "─".repeat(68);
+
+    println!("DudeCT 타이밍 분석 ─ entlib-native-constant-time");
+    println!(
+        "N={N}  warmup={warmup}  crop={crop_pct:.0}%  PASS=|t|<{T_WARN}  FAIL=|t|≥{T_FAIL}",
+        crop_pct = CROP * 100.0,
+    );
+    println!("{sep}");
+
+    // ─── u64 ──────────────────────────────────────────────────────────────────
+    // 양 클래스 모두 동일한 횟수의 PRNG 호출 수행 (비대칭 PRNG 호출은
+    // CPU 마이크로-아키텍처 상태 편차를 유발하여 위음성 DudeCT FAIL의 원인이 됨)
+    println!("\n[u64 :: ConstantTimeEq / ct_ne / ct_is_ge]");
+    ok &= dudect("ct_eq   equal vs. unequal", warmup, &mut rng, |cls, rng| {
+        let a = rng.u64();
+        let r = rng.u64(); // 양 클래스 동일하게 2회 호출
+        let b = if cls == 0 { a } else { r };
+        let t0 = tsc();
+        let _ = black_box(black_box(a).ct_eq(&black_box(b)));
+        tsc().saturating_sub(t0)
+    });
+    ok &= dudect("ct_ne   equal vs. unequal", warmup, &mut rng, |cls, rng| {
+        let a = rng.u64();
+        let r = rng.u64();
+        let b = if cls == 0 { a } else { r };
+        let t0 = tsc();
+        let _ = black_box(black_box(a).ct_ne(&black_box(b)));
+        tsc().saturating_sub(t0)
+    });
+    ok &= dudect("ct_is_ge  equal vs. random", warmup, &mut rng, |cls, rng| {
+        let a = rng.u64();
+        let r = rng.u64();
+        // cls=0: a >= a (항상 True), cls=1: a >= r (임의 결과)
+        let b = if cls == 0 { a } else { r };
+        let t0 = tsc();
+        let _ = black_box(black_box(a).ct_is_ge(&black_box(b)));
+        tsc().saturating_sub(t0)
+    });
+
+    // ─── u32 ──────────────────────────────────────────────────────────────────
+    println!("\n[u32 :: ConstantTimeEq]");
+    ok &= dudect("ct_eq   equal vs. unequal", warmup, &mut rng, |cls, rng| {
+        let a = rng.u64() as u32;
+        let r = rng.u64() as u32;
+        let b: u32 = if cls == 0 { a } else { r };
+        let t0 = tsc();
+        let _ = black_box(black_box(a).ct_eq(&black_box(b)));
+        tsc().saturating_sub(t0)
+    });
+
+    // ─── u8 ───────────────────────────────────────────────────────────────────
+    println!("\n[u8 :: ConstantTimeEq]");
+    ok &= dudect("ct_eq   equal vs. unequal", warmup, &mut rng, |cls, rng| {
+        let a = rng.u64() as u8;
+        let r = rng.u64() as u8;
+        let b: u8 = if cls == 0 { a } else { r };
+        let t0 = tsc();
+        let _ = black_box(black_box(a).ct_eq(&black_box(b)));
+        tsc().saturating_sub(t0)
+    });
+
+    // ─── ConstantTimeSelect ───────────────────────────────────────────────────
+    // Choice를 외부에서 직접 생성할 수 없으므로 ct_eq로 0xFF / 0x00을 유도
+    println!("\n[u64 :: ConstantTimeSelect]");
+    ok &= dudect("ct_select  choice=0xFF vs 0x00", warmup, &mut rng, |cls, rng| {
+        let a = rng.u64();
+        let b = rng.u64();
+        // cls=0 → 0u8==0u8 → Choice(0xFF), cls=1 → 1u8==0u8 → Choice(0x00)
+        let choice = black_box(cls as u8).ct_eq(&black_box(0u8));
+        let t0 = tsc();
+        let _ = black_box(<u64 as ConstantTimeSelect>::ct_select(
+            &black_box(a),
+            &black_box(b),
+            black_box(choice),
+        ));
+        tsc().saturating_sub(t0)
+    });
+
+    // ─── ConstantTimeSwap ─────────────────────────────────────────────────────
+    println!("\n[u64 :: ConstantTimeSwap]");
+    ok &= dudect("ct_swap  swap vs. noop", warmup, &mut rng, |cls, rng| {
+        let mut a = rng.u64();
+        let mut b = rng.u64();
+        let choice = black_box(cls as u8).ct_eq(&black_box(0u8));
+        let t0 = tsc();
+        <u64 as ConstantTimeSwap>::ct_swap(
+            black_box(&mut a),
+            black_box(&mut b),
+            black_box(choice),
+        );
+        let t1 = tsc();
+        let _ = black_box((a, b));
+        t1.saturating_sub(t0)
+    });
+
+    // ─── ConstantTimeIsZero ───────────────────────────────────────────────────
+    println!("\n[u64 :: ConstantTimeIsZero]");
+    ok &= dudect("ct_is_zero  0 vs. nonzero", warmup, &mut rng, |cls, rng| {
+        let r = rng.u64(); // 양 클래스 동일하게 1회 호출
+        let v: u64 = if cls == 0 { 0 } else { r | 1 };
+        let t0 = tsc();
+        let _ = black_box(black_box(v).ct_is_zero());
+        tsc().saturating_sub(t0)
+    });
+
+    // ─── ConstantTimeIsNegative (u64 MSB) ────────────────────────────────────
+    println!("\n[u64 :: ConstantTimeIsNegative]");
+    ok &= dudect("ct_is_negative  MSB=1 vs. MSB=0", warmup, &mut rng, |cls, rng| {
+        let r = rng.u64();
+        let v: u64 = if cls == 0 {
+            r | 0x8000_0000_0000_0000   // MSB 강제 설정
+        } else {
+            r & 0x7fff_ffff_ffff_ffff   // MSB 강제 소거
+        };
+        let t0 = tsc();
+        let _ = black_box(black_box(v).ct_is_negative());
+        tsc().saturating_sub(t0)
+    });
+
+    // ─── i64 ──────────────────────────────────────────────────────────────────
+    println!("\n[i64 :: ConstantTimeEq / ct_is_ge / ct_is_negative]");
+    ok &= dudect("ct_eq   equal vs. unequal", warmup, &mut rng, |cls, rng| {
+        let a = rng.u64() as i64;
+        let r = rng.u64() as i64;
+        let b: i64 = if cls == 0 { a } else { r };
+        let t0 = tsc();
+        let _ = black_box(black_box(a).ct_eq(&black_box(b)));
+        tsc().saturating_sub(t0)
+    });
+    ok &= dudect("ct_is_ge  equal vs. random", warmup, &mut rng, |cls, rng| {
+        let a = rng.u64() as i64;
+        let r = rng.u64() as i64;
+        let b: i64 = if cls == 0 { a } else { r };
+        let t0 = tsc();
+        let _ = black_box(black_box(a).ct_is_ge(&black_box(b)));
+        tsc().saturating_sub(t0)
+    });
+    ok &= dudect("ct_is_negative  MSB=1 vs. MSB=0", warmup, &mut rng, |cls, rng| {
+        let r = rng.u64();
+        // 부호 없는 비트로 MSB 제어 후 i64로 해석
+        let v: i64 = if cls == 0 {
+            (r | 0x8000_0000_0000_0000) as i64   // 항상 음수
+        } else {
+            (r & 0x7fff_ffff_ffff_ffff) as i64   // 항상 양수
+        };
+        let t0 = tsc();
+        let _ = black_box(black_box(v).ct_is_negative());
+        tsc().saturating_sub(t0)
+    });
+
+    println!("\n{sep}");
+    if ok {
+        println!("결과: PASS ─ 모든 연산이 상수-시간 기준을 충족합니다.");
+    } else {
+        eprintln!("결과: FAIL ─ 타이밍 의존성이 검출된 연산이 존재합니다.");
+        std::process::exit(1);
+    }
+}
diff --git a/core/constant-time/saw/Dockerfile b/core/constant-time/saw/Dockerfile
new file mode 100644
index 0000000..7765a8c
--- /dev/null
+++ b/core/constant-time/saw/Dockerfile
@@ -0,0 +1,26 @@
+FROM ubuntu:22.04
+
+ENV DEBIAN_FRONTEND=noninteractive
+ENV SAW_VERSION=1.5
+
+RUN apt-get update && apt-get install -y --no-install-recommends \
+    ca-certificates \
+    curl \
+    build-essential \
+    pkg-config \
+    libssl-dev \
+    z3 \
+    unzip \
+    && rm -rf /var/lib/apt/lists/*
+
+RUN curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs \
+    | sh -s -- -y --default-toolchain nightly --component llvm-tools-preview
+ENV PATH="/root/.cargo/bin:${PATH}"
+
+RUN mkdir -p /opt/saw && \
+    curl -fL "https://github.com/GaloisInc/saw-script/releases/download/v${SAW_VERSION}/saw-${SAW_VERSION}-ubuntu-22.04-X64-with-solvers.tar.gz" \
+    | tar xz --strip-components=1 -C /opt/saw
+ENV PATH="/opt/saw/bin:${PATH}"
+
+COPY . /workspace
+WORKDIR /workspace
diff --git a/core/constant-time/saw/compose.yaml b/core/constant-time/saw/compose.yaml
new file mode 100644
index 0000000..32e871f
--- /dev/null
+++ b/core/constant-time/saw/compose.yaml
@@ -0,0 +1,52 @@
+services:
+  saw-verify:
+    build:
+      context: ../../..
+      dockerfile: core/constant-time/saw/Dockerfile
+    working_dir: /workspace
+    command:
+      - bash
+      - -c
+      - |
+        set -euo pipefail
+        echo "=== entlib-native-constant-time SAW Formal Verification ==="
+        echo ""
+
+        SYSROOT=$$(rustc --print sysroot)
+        TARGET_TRIPLE=$$(rustc -vV | awk '/^host:/{print $2}')
+        LLVM_NM="$${SYSROOT}/lib/rustlib/$${TARGET_TRIPLE}/bin/llvm-nm"
+
+        echo "=== Version Diagnostics ==="
+        rustc -vV
+        saw --version 2>&1 | head -5 || true
+        "$${LLVM_NM}" --version 2>&1 | head -2
+        echo ""
+
+        echo "Building LLVM bitcode (saw_verify)..."
+        cargo rustc --release \
+          --features "saw_verify" \
+          -p entlib-native-constant-time \
+          -- --emit=llvm-bc -C lto=off -C codegen-units=1
+
+        BC=$$(find target/release/deps -name 'entlib_native_constant_time-*.bc' -type f \
+               -printf '%T@ %p\n' | sort -rn | head -1 | awk '{print $$2}')
+        if [ -z "$$BC" ]; then
+          echo "ERROR: bitcode not found"
+          exit 1
+        fi
+        echo "Bitcode: $$BC ($(wc -c < "$$BC") bytes)"
+
+        echo "Verifying audit_verify_* symbols..."
+        SYMS=$$("$${LLVM_NM}" "$$BC" 2>&1 | grep 'audit_verify' || true)
+        if [ -z "$$SYMS" ]; then
+          echo "ERROR: no audit_verify_* symbols in bitcode."
+          echo "All symbols:"
+          "$${LLVM_NM}" "$$BC" 2>&1 || true
+          exit 1
+        fi
+        echo "$$SYMS"
+        echo ""
+
+        cd core/constant-time/saw
+        cp "/workspace/$$BC" entlib_native_constant_time.bc
+        saw verify.saw
diff --git a/core/constant-time/saw/docker_verify.sh b/core/constant-time/saw/docker_verify.sh
new file mode 100755
index 0000000..9818d0c
--- /dev/null
+++ b/core/constant-time/saw/docker_verify.sh
@@ -0,0 +1,6 @@
+#!/usr/bin/env bash
+set -euo pipefail
+
+cd "$(dirname "$0")"
+
+docker compose -f compose.yaml run --rm --build saw-verify
diff --git a/core/constant-time/saw/entrypoint.sh b/core/constant-time/saw/entrypoint.sh
new file mode 100755
index 0000000..67bc286
--- /dev/null
+++ b/core/constant-time/saw/entrypoint.sh
@@ -0,0 +1,37 @@
+#!/usr/bin/env bash
+set -euo pipefail
+
+WORKSPACE_ROOT="/workspace"
+CRATE_DIR="${WORKSPACE_ROOT}/core/constant-time"
+SAW_DIR="${CRATE_DIR}/saw"
+
+echo "=== entlib-native-constant-time SAW Formal Verification ==="
+echo ""
+
+if [ ! -f "${WORKSPACE_ROOT}/Cargo.toml" ]; then
+    echo "ERROR: ${WORKSPACE_ROOT}/Cargo.toml not found."
+    exit 1
+fi
+
+# Phase 0: Build LLVM bitcode
+echo "Building LLVM bitcode (saw_verify + audit_mode)..."
+cd "${WORKSPACE_ROOT}"
+RUSTFLAGS="--emit=llvm-bc" cargo build --release \
+    --features "entlib-native-constant-time/saw_verify" \
+    --features "audit_mode" \
+    -p entlib-native-constant-time 2>&1
+
+BC_FILE=$(find target/release/deps -name 'entlib_native_constant_time-*.bc' -type f | head -1)
+
+if [ -z "${BC_FILE}" ]; then
+    echo "ERROR: LLVM bitcode not found in target/release/deps/"
+    exit 1
+fi
+
+echo "Bitcode: ${BC_FILE}"
+echo ""
+
+# Phase 1 + 2: SAW verification
+export ENTLIB_CT_BC="${WORKSPACE_ROOT}/${BC_FILE}"
+cd "${SAW_DIR}"
+saw verify.saw
diff --git a/core/constant-time/saw/specs/ConstantTime.cry b/core/constant-time/saw/specs/ConstantTime.cry
new file mode 100644
index 0000000..432e48e
--- /dev/null
+++ b/core/constant-time/saw/specs/ConstantTime.cry
@@ -0,0 +1,116 @@
+module ConstantTime where
+
+type Choice = [8]
+
+from_mask_normalized : [8] -> Choice
+from_mask_normalized m = -is_nonzero
+  where
+    msb_set = m || (-m)
+    is_nonzero = msb_set >> 7
+
+choice_not : Choice -> Choice
+choice_not c = ~c
+
+choice_unwrap : Choice -> [8]
+choice_unwrap c = c
+
+ct_eq_u64 : [64] -> [64] -> Choice
+ct_eq_u64 a b = from_mask_normalized mask
+  where
+    v = a ^ b
+    msb = (v || (-v)) >> 63
+    msb_u8 : [8]
+    msb_u8 = drop`{56} msb
+    mask = -(msb_u8 ^ 0x01)
+
+ct_ne_u64 : [64] -> [64] -> Choice
+ct_ne_u64 a b = choice_not (ct_eq_u64 a b)
+
+ct_is_ge_u64 : [64] -> [64] -> Choice
+ct_is_ge_u64 a b = from_mask_normalized mask
+  where
+    sub = a - b
+    borrow = (~a && b) || (~(a ^ b) && sub)
+    borrow_msb : [8]
+    borrow_msb = drop`{56} (borrow >> 63)
+    mask = -(borrow_msb ^ 0x01)
+
+ct_is_negative_u64 : [64] -> Choice
+ct_is_negative_u64 a = from_mask_normalized (-(masked))
+  where
+    msb_u8 : [8]
+    msb_u8 = drop`{56} (a >> 63)
+    masked = msb_u8 && 0x01
+
+ct_is_zero_u64 : [64] -> Choice
+ct_is_zero_u64 a = ct_eq_u64 a 0
+
+ct_select_u64 : [64] -> [64] -> Choice -> [64]
+ct_select_u64 a b c = (a && mask) || (b && ~mask)
+  where mask = sext_8_64 c
+
+ct_swap_u64 : [64] -> [64] -> Choice -> ([64], [64])
+ct_swap_u64 a b c = (a ^ t, b ^ t)
+  where
+    mask = sext_8_64 c
+    t = (a ^ b) && mask
+
+sext_8_64 : [8] -> [64]
+sext_8_64 x = ext || lo
+  where
+    lo : [64]
+    lo = (zero : [56]) # x
+    s : [64]
+    s = (zero : [56]) # (x >> 7)
+    ext = (-s) && 0xFFFFFFFFFFFFFF00
+
+// === Specification Correctness Properties ===
+
+property from_mask_is_boolean m =
+  from_mask_normalized m == 0x00 \/ from_mask_normalized m == 0xFF
+
+property ct_eq_correct (a : [64]) (b : [64]) =
+  (a == b) == (ct_eq_u64 a b == (0xFF : Choice))
+
+property ct_eq_reflexive (a : [64]) =
+  ct_eq_u64 a a == (0xFF : Choice)
+
+property ct_eq_symmetric (a : [64]) (b : [64]) =
+  ct_eq_u64 a b == ct_eq_u64 b a
+
+property ct_ne_correct (a : [64]) (b : [64]) =
+  (a != b) == (ct_ne_u64 a b == (0xFF : Choice))
+
+property ct_is_ge_correct (a : [64]) (b : [64]) =
+  (a >= b) == (ct_is_ge_u64 a b == (0xFF : Choice))
+
+property ct_is_ge_reflexive (a : [64]) =
+  ct_is_ge_u64 a a == (0xFF : Choice)
+
+property ct_is_ge_antisymmetric (a : [64]) (b : [64]) =
+  (ct_is_ge_u64 a b == (0xFF : Choice) /\ ct_is_ge_u64 b a == (0xFF : Choice)) ==> a == b
+
+property ct_is_ge_total (a : [64]) (b : [64]) =
+  ct_is_ge_u64 a b == (0xFF : Choice) \/ ct_is_ge_u64 b a == (0xFF : Choice)
+
+property ct_is_zero_correct (a : [64]) =
+  (a == 0) == (ct_is_zero_u64 a == (0xFF : Choice))
+
+property ct_is_negative_correct (a : [64]) =
+  (a >> 63 == 1) == (ct_is_negative_u64 a == (0xFF : Choice))
+
+property ct_select_true (a : [64]) (b : [64]) =
+  ct_select_u64 a b 0xFF == a
+
+property ct_select_false (a : [64]) (b : [64]) =
+  ct_select_u64 a b 0x00 == b
+
+property ct_swap_true (a : [64]) (b : [64]) =
+  ct_swap_u64 a b 0xFF == (b, a)
+
+property ct_swap_false (a : [64]) (b : [64]) =
+  ct_swap_u64 a b 0x00 == (a, b)
+
+property choice_not_involution c =
+  (c == (0x00 : Choice) \/ c == (0xFF : Choice)) ==>
+    choice_not (choice_not c) == c
diff --git a/core/constant-time/saw/verify.saw b/core/constant-time/saw/verify.saw
new file mode 100644
index 0000000..a45d507
--- /dev/null
+++ b/core/constant-time/saw/verify.saw
@@ -0,0 +1,223 @@
+// SAW Formal Verification Script
+// Target: entlib-native-constant-time
+//
+// Proves functional equivalence between the Rust LLVM bitcode and
+// the Cryptol reference specification via SMT solving (Z3).
+//
+// SAW's symbolic execution engine processes all paths simultaneously.
+// Successful verification implies the LLVM IR contains no secret-dependent
+// branches — providing mathematical evidence of constant-time behavior
+// at the IR level.
+
+enable_experimental;
+
+import "specs/ConstantTime.cry";
+
+// ========================================================
+// Phase 1: Prove Cryptol specification correctness
+// ========================================================
+
+print "Phase 1: Cryptol specification property proofs";
+print "------------------------------------------------";
+
+print "[1/14] from_mask_is_boolean";
+prove_print z3 {{ from_mask_is_boolean }};
+
+print "[2/14] ct_eq_correct";
+prove_print z3 {{ ct_eq_correct }};
+
+print "[3/14] ct_eq_reflexive";
+prove_print z3 {{ ct_eq_reflexive }};
+
+print "[4/14] ct_eq_symmetric";
+prove_print z3 {{ ct_eq_symmetric }};
+
+print "[5/14] ct_ne_correct";
+prove_print z3 {{ ct_ne_correct }};
+
+print "[6/14] ct_is_ge_correct";
+prove_print z3 {{ ct_is_ge_correct }};
+
+print "[7/14] ct_is_ge_reflexive";
+prove_print z3 {{ ct_is_ge_reflexive }};
+
+print "[8/14] ct_is_ge_antisymmetric";
+prove_print z3 {{ ct_is_ge_antisymmetric }};
+
+print "[9/14] ct_is_ge_total";
+prove_print z3 {{ ct_is_ge_total }};
+
+print "[10/14] ct_is_zero_correct";
+prove_print z3 {{ ct_is_zero_correct }};
+
+print "[11/14] ct_is_negative_correct";
+prove_print z3 {{ ct_is_negative_correct }};
+
+print "[12/14] ct_select_true / ct_select_false";
+prove_print z3 {{ ct_select_true }};
+prove_print z3 {{ ct_select_false }};
+
+print "[13/14] ct_swap_true / ct_swap_false";
+prove_print z3 {{ ct_swap_true }};
+prove_print z3 {{ ct_swap_false }};
+
+print "[14/14] choice_not_involution";
+prove_print z3 {{ choice_not_involution }};
+
+print "";
+print "Phase 1 complete: all specification properties proven.";
+print "";
+
+// ========================================================
+// Phase 2: LLVM bitcode ↔ Cryptol equivalence proofs
+// ========================================================
+
+print "Phase 2: LLVM bitcode verification";
+print "------------------------------------";
+
+m <- llvm_load_module "entlib_native_constant_time.bc";
+
+// --- from_mask_normalized ---
+print "[1/10] audit_verify_choice_from_mask_normalized";
+let from_mask_normalized_spec = do {
+    a <- llvm_fresh_var "a" (llvm_int 8);
+    llvm_execute_func [llvm_term a];
+    llvm_return (llvm_term {{ from_mask_normalized a }});
+};
+from_mask_ov <- llvm_verify m "audit_verify_choice_from_mask_normalized"
+    [] false from_mask_normalized_spec z3;
+
+// --- choice_not ---
+print "[2/10] audit_verify_choice_not";
+let choice_not_spec = do {
+    c <- llvm_fresh_var "c" (llvm_int 8);
+    llvm_precond {{ c == 0x00 \/ c == 0xFF }};
+    llvm_execute_func [llvm_term c];
+    llvm_return (llvm_term {{ choice_not c }});
+};
+choice_not_ov <- llvm_verify m "audit_verify_choice_not"
+    [] false choice_not_spec z3;
+
+// --- choice_unwrap_u8 ---
+// Requires saw_verify feature (bypasses core::hint::black_box inline asm)
+print "[3/10] audit_verify_choice_unwrap_u8";
+let choice_unwrap_spec = do {
+    c <- llvm_fresh_var "c" (llvm_int 8);
+    llvm_execute_func [llvm_term c];
+    llvm_return (llvm_term {{ choice_unwrap c }});
+};
+choice_unwrap_ov <- llvm_verify m "audit_verify_choice_unwrap_u8"
+    [] false choice_unwrap_spec z3;
+
+// --- ct_eq ---
+print "[4/10] audit_verify_u64_ct_eq";
+let ct_eq_spec = do {
+    a <- llvm_fresh_var "a" (llvm_int 64);
+    b <- llvm_fresh_var "b" (llvm_int 64);
+    a_ptr <- llvm_alloc (llvm_int 64);
+    b_ptr <- llvm_alloc (llvm_int 64);
+    llvm_points_to a_ptr (llvm_term a);
+    llvm_points_to b_ptr (llvm_term b);
+    llvm_execute_func [a_ptr, b_ptr];
+    llvm_return (llvm_term {{ ct_eq_u64 a b }});
+};
+ct_eq_ov <- llvm_verify m "audit_verify_u64_ct_eq"
+    [] false ct_eq_spec z3;
+
+// --- ct_ne ---
+print "[5/10] audit_verify_u64_ct_ne";
+let ct_ne_spec = do {
+    a <- llvm_fresh_var "a" (llvm_int 64);
+    b <- llvm_fresh_var "b" (llvm_int 64);
+    a_ptr <- llvm_alloc (llvm_int 64);
+    b_ptr <- llvm_alloc (llvm_int 64);
+    llvm_points_to a_ptr (llvm_term a);
+    llvm_points_to b_ptr (llvm_term b);
+    llvm_execute_func [a_ptr, b_ptr];
+    llvm_return (llvm_term {{ ct_ne_u64 a b }});
+};
+ct_ne_ov <- llvm_verify m "audit_verify_u64_ct_ne"
+    [] false ct_ne_spec z3;
+
+// --- ct_is_ge ---
+print "[6/10] audit_verify_u64_ct_is_ge";
+let ct_is_ge_spec = do {
+    a <- llvm_fresh_var "a" (llvm_int 64);
+    b <- llvm_fresh_var "b" (llvm_int 64);
+    a_ptr <- llvm_alloc (llvm_int 64);
+    b_ptr <- llvm_alloc (llvm_int 64);
+    llvm_points_to a_ptr (llvm_term a);
+    llvm_points_to b_ptr (llvm_term b);
+    llvm_execute_func [a_ptr, b_ptr];
+    llvm_return (llvm_term {{ ct_is_ge_u64 a b }});
+};
+ct_is_ge_ov <- llvm_verify m "audit_verify_u64_ct_is_ge"
+    [] false ct_is_ge_spec z3;
+
+// --- ct_is_negative ---
+print "[7/10] audit_verify_u64_ct_is_negative";
+let ct_is_negative_spec = do {
+    a <- llvm_fresh_var "a" (llvm_int 64);
+    a_ptr <- llvm_alloc (llvm_int 64);
+    llvm_points_to a_ptr (llvm_term a);
+    llvm_execute_func [a_ptr];
+    llvm_return (llvm_term {{ ct_is_negative_u64 a }});
+};
+ct_is_negative_ov <- llvm_verify m "audit_verify_u64_ct_is_negative"
+    [] false ct_is_negative_spec z3;
+
+// --- ct_is_zero ---
+print "[8/10] audit_verify_u64_ct_is_zero";
+let ct_is_zero_spec = do {
+    a <- llvm_fresh_var "a" (llvm_int 64);
+    a_ptr <- llvm_alloc (llvm_int 64);
+    llvm_points_to a_ptr (llvm_term a);
+    llvm_execute_func [a_ptr];
+    llvm_return (llvm_term {{ ct_is_zero_u64 a }});
+};
+ct_is_zero_ov <- llvm_verify m "audit_verify_u64_ct_is_zero"
+    [] false ct_is_zero_spec z3;
+
+// --- ct_select ---
+// Requires saw_verify feature (black_box bypass for unwrap_u8 in select path)
+print "[9/10] audit_verify_u64_ct_select";
+let ct_select_spec = do {
+    a <- llvm_fresh_var "a" (llvm_int 64);
+    b <- llvm_fresh_var "b" (llvm_int 64);
+    c <- llvm_fresh_var "c" (llvm_int 8);
+    a_ptr <- llvm_alloc (llvm_int 64);
+    b_ptr <- llvm_alloc (llvm_int 64);
+    llvm_points_to a_ptr (llvm_term a);
+    llvm_points_to b_ptr (llvm_term b);
+    llvm_precond {{ c == 0x00 \/ c == 0xFF }};
+    llvm_execute_func [a_ptr, b_ptr, llvm_term c];
+    llvm_return (llvm_term {{ ct_select_u64 a b c }});
+};
+ct_select_ov <- llvm_verify m "audit_verify_u64_ct_select"
+    [] false ct_select_spec z3;
+
+// --- ct_swap ---
+// Requires saw_verify feature (black_box bypass for unwrap_u8 in swap path)
+print "[10/10] audit_verify_u64_ct_swap";
+let ct_swap_spec = do {
+    a <- llvm_fresh_var "a" (llvm_int 64);
+    b <- llvm_fresh_var "b" (llvm_int 64);
+    c <- llvm_fresh_var "c" (llvm_int 8);
+    a_ptr <- llvm_alloc (llvm_int 64);
+    b_ptr <- llvm_alloc (llvm_int 64);
+    llvm_points_to a_ptr (llvm_term a);
+    llvm_points_to b_ptr (llvm_term b);
+    llvm_precond {{ c == 0x00 \/ c == 0xFF }};
+    llvm_execute_func [a_ptr, b_ptr, llvm_term c];
+    llvm_points_to a_ptr (llvm_term {{ (ct_swap_u64 a b c).0 }});
+    llvm_points_to b_ptr (llvm_term {{ (ct_swap_u64 a b c).1 }});
+};
+ct_swap_ov <- llvm_verify m "audit_verify_u64_ct_swap"
+    [] false ct_swap_spec z3;
+
+print "";
+print "===================================================";
+print " ALL VERIFICATIONS PASSED";
+print " - 14 Cryptol specification properties proven";
+print " - 10 LLVM bitcode equivalence proofs completed";
+print "===================================================";
diff --git a/core/constant-time/src/choice.rs b/core/constant-time/src/choice.rs
index eca9673..7751a85 100644
--- a/core/constant-time/src/choice.rs
+++ b/core/constant-time/src/choice.rs
@@ -22,20 +22,29 @@ impl Choice {
     /// # Security Note
     /// 어떠한 바이트(u8) 입력이 들어오더라도 수학적 비트 연산을 통해
     /// 0x00(False) 또는 0xFF(True)로 강제 변환합니다.
+    /// 임의의 u8을 0x00(False) 또는 0xFF(True)로 정규화합니다.
+    ///
+    /// # Security Note
+    /// 임의 바이트 입력을 받으므로 정규화 후 `black_box`를 통해
+    /// LLVM이 결과값을 역추적하여 분기를 생성하는 것을 방지합니다.
+    #[cfg(feature = "audit_mode")]
     #[inline(always)]
     pub(crate) fn from_mask_normalized(mask: u8) -> Self {
-        // 값의 존재 유무(Non-Zero) 탐지
-        // mask가 0이면 msb_set은 0x00, 0이 아니면 2의 보수 성질에 의해 msb_set의 MSB는 무조건 1이 됨
         let msb_set = mask | mask.wrapping_neg();
-
-        // 최상위 비트(MSB)를 추출하여 0 또는 1의 상태로 매핑
         let is_nonzero = msb_set >> 7;
-
-        // 2의 보수를 취해 최종 마스크 생성 (0x00 또는 0xFF)
-        // is_nonzero가 0이면 0x00, 1이면 0xFF를 반환 (단일 NEG 명령어로 컴파일)
         let secure_mask = is_nonzero.wrapping_neg();
+        Choice(core::hint::black_box(secure_mask))
+    }
 
-        Choice(secure_mask)
+    /// 이미 정규화된 0x00/0xFF 마스크로 직접 구성합니다.
+    ///
+    /// # Security Note
+    /// 호출자는 mask ∈ {0x00, 0xFF} 를 보장해야 합니다.
+    /// `black_box`는 LLVM이 mask 값을 추적하여 이후 연산을 조건 분기로
+    /// 대체하는 것을 방지하는 상수-시간 경계로 작동합니다.
+    #[inline(always)]
+    pub(crate) fn from_mask(mask: u8) -> Self {
+        Choice(mask)
     }
 
     /// 내부 값을 반환합니다. 컴파일러 최적화를 방지하기 위해 `black_box`를 사용합니다.
@@ -45,7 +54,14 @@ impl Choice {
     /// * `0xFF` - True
     #[inline(always)]
     pub fn unwrap_u8(self) -> u8 {
-        core::hint::black_box(self.0)
+        #[cfg(not(feature = "saw_verify"))]
+        {
+            core::hint::black_box(self.0)
+        }
+        #[cfg(feature = "saw_verify")]
+        {
+            self.0
+        }
     }
 
     /// `Choice` 값을 논리적으로 반전(NOT)합니다.
diff --git a/core/constant-time/src/lib.rs b/core/constant-time/src/lib.rs
index aa170c2..3b54f2d 100644
--- a/core/constant-time/src/lib.rs
+++ b/core/constant-time/src/lib.rs
@@ -19,43 +19,19 @@ macro_rules! impl_constant_time_for_uint {
         impl ConstantTimeEq for $t {
             #[inline(always)]
             fn ct_eq(&self, other: &Self) -> Choice {
-                // XOR 연산
-                // 두 값이 같으면 v는 0, 다르면 0이 아닌 값이 됨
-                let v = *self ^ *other;
-
-                // OR와 2의 보수(wrapping_neg) 활용
-                // v가 0이면 v | v.wrapping_neg() 도 0임
-                // v가 0이 아니면, v | v.wrapping_neg() 의 최상위 비트(MSB)는 항상 1이 됨
-                // 이를 통해 MSB를 LSB 위치로 이동시킴
+                let v = core::hint::black_box(*self ^ *other);
                 let msb = (v | v.wrapping_neg()) >> (<$t>::BITS - 1);
-
-                // 마스크 생성
-                // v가 0(같음)이면 msb는 0. msb ^ 1 은 1. 1의 2의 보수는 0xFF (True)
-                // v가 0이 아님(다름)이면 msb는 1. msb ^ 1 은 0. 0의 2의 보수는 0x00 (False)
-                let mask = ((msb as u8) ^ 1).wrapping_neg();
-
-                Choice::from_mask_normalized(mask)
+                let mask = ((msb as u8) ^ 1u8).wrapping_neg();
+                Choice::from_mask(mask)
             }
 
             #[inline(always)]
             fn ct_is_ge(&self, other: &Self) -> Choice {
-                // 부호 없는 정수의 대소 비교(self >= other)를 상수-시간으로 판별하기 위해
-                // 뺄셈 연산의 언더플로우(Borrow) 발생 여부를 비트 논리로 계산
-                // Borrow 방정식: (~A & B) | (~(A ^ B) & (A - B))
-                // 결과의 최상위 비트(MSB)가 1이면 self < other (언더플로우 발생), 0이면 self >= other
                 let sub = self.wrapping_sub(*other);
-                let borrow = (!*self & *other) | (!(*self ^ *other) & sub);
-
-                // 최상위 비트(MSB) 추출
-                // 이전 <u32>::BITS 하드코딩으로 인한 치명적 결함을 동적 타입 크기(<$t>::BITS)로 해결
+                let borrow = core::hint::black_box((!*self & *other) | (!(*self ^ *other) & sub));
                 let borrow_msb = (borrow >> (<$t>::BITS - 1)) as u8;
-
-                // 마스크 생성
-                // borrow_msb가 0 (self >= other) -> 0 ^ 1 = 1 -> wrapping_neg(1) = 0xFF (True)
-                // borrow_msb가 1 (self < other)  -> 1 ^ 1 = 0 -> wrapping_neg(0) = 0x00 (False)
-                let mask = (borrow_msb ^ 1).wrapping_neg();
-
-                Choice::from_mask_normalized(mask)
+                let mask = (borrow_msb ^ 1u8).wrapping_neg();
+                Choice::from_mask(mask)
             }
         }
 
@@ -97,13 +73,8 @@ macro_rules! impl_constant_time_for_uint {
         impl ConstantTimeIsNegative for $t {
             #[inline(always)]
             fn ct_is_negative(&self) -> Choice {
-                // MSB(최상위 비트)를 LSB 위치로 이동시켜 0 또는 1을 추출
-                // 예: u8에서 *self >> 7, u64에서 *self >> 63
-                let msb = (*self >> (<$t>::BITS - 1)) as u8 & 1;
-
-                // 1u8.wrapping_neg() = 0xFF (True), 0u8.wrapping_neg() = 0x00 (False)
-                // 단일 NEG 명령어로 컴파일되어 분기가 없음
-                Choice::from_mask_normalized(msb.wrapping_neg())
+                let msb = core::hint::black_box((*self >> (<$t>::BITS - 1)) as u8 & 1u8);
+                Choice::from_mask(msb.wrapping_neg())
             }
         }
     };
@@ -149,13 +120,9 @@ macro_rules! impl_constant_time_for_sint {
         impl ConstantTimeIsNegative for $s_type {
             #[inline(always)]
             fn ct_is_negative(&self) -> Choice {
-                // 산술 시프트로 인한 마스크 오염(예: 0x02) 방지를 위해
-                // 부호 없는 정수로 변환 후 논리 시프트 강제
                 let u_val = *self as $u_type;
-                let msb = (u_val >> (<$s_type>::BITS - 1)) as u8 & 1;
-
-                // 단일 NEG 명령어로 분기 없이 마스크 생성 (0x00 또는 0xFF 보장)
-                Choice::from_mask_normalized(msb.wrapping_neg())
+                let msb = core::hint::black_box((u_val >> (<$s_type>::BITS - 1)) as u8 & 1u8);
+                Choice::from_mask(msb.wrapping_neg())
             }
         }
 
diff --git a/crypto/chacha20/src/lib.rs b/crypto/chacha20/src/lib.rs
index 0c9ac1a..9af0939 100644
--- a/crypto/chacha20/src/lib.rs
+++ b/crypto/chacha20/src/lib.rs
@@ -1 +1,3 @@
-#![no_std]
+// entlib_native_chacha20::ChaCha20
+// let chacha = ChaCha20::new();
+// chacha.key_gen();