connections 0.1.0 – Galois‑connection 기반 숫자 캐스트 for Rust

connections 0.1.0 – Galois‑connection 기반 숫자 캐스트 for Rust

TL;DR – 크레이트가 하는 일과 중요한 이유

connections 0.1.0은 Galois 법칙을 만족하는 단조 함수 쌍을 패키징하는 Conn 타입을 제공합니다. Conn을 사용하면 명확한 왕복 의미론(예: 포화, 반올림)과 컴파일 타임 단계별 변환 조합을 얻을 수 있으며, 속성 테스트된 불변식과 선택적인 SMT 증명을 제공합니다.

Galois 연결을 일급 Rust 값으로

전순서 A와 B 사이의 Galois 연결은 단조 사상 f : A → B와 g : B → A의 쌍으로, 다음을 만족합니다.

f(a) ≤ b  ⇔  a ≤ g(b)

connections은 이 쌍을 다음 구조체에 인코딩합니다.

pub struct Conn<A, B, K: Kind = L> {
    f: fn(A) -> B,   // L‑kind: ceil; R‑kind: floor
    g: fn(B) -> A,   // L‑kind: upper; R‑kind: lower
    _kind: PhantomData<K>,
}
  • L‑kind (ConnL) 은 .ceil() 과 .upper() 를 노출합니다.
  • R‑kind (ConnR) 은 .floor() 와 .lower() 를 노출합니다.
  • ConnK 는 양쪽을 모두 구현하는 제로 사이즈 마커로, round, truncate, interval 같은 양면 헬퍼를 가능하게 합니다.

이 크레이트는 unsafe 코드를 금지하고, 모든 Conn을 Copy 및 const‑생성 가능하게 하며, 최소 지원 버전(MSRV)은 Rust 1.88 입니다.

왜 표준 캐스트만으로는 부족한가

  • 내장 as 캐스트는 단일 방향만 제공하고 라운딩/포화 정책을 조용히 선택합니다. 예를 들어 u32::MAX as i32는 -1 로 래핑됩니다.
  • From/Into 역시 한 방향만 제공하고 역연산을 노출하지 않습니다.
  • 따라서 여러 캐스트를 체인하면 전체 왕복 동작을 추론하기 어렵습니다.

connections는 인접 함수 쌍을 명시적으로 만들고 속성 테스트를 수행함으로써 이를 해결합니다:

  • 명확한 의미론 – 각 Conn은 왼쪽 Galois 부등식 ceil(a) ≤ b ⇔ a ≤ upper(b) 또는 오른쪽 Galois 부등식 lower(b) ≤ a ⇔ b ≤ floor(a) 를 보장합니다.
  • 안전한 조합 – compose! 매크로는 Conn 체인을 컴파일 타임에 하나의 Conn 으로 접어들어 Galois 법칙을 자동으로 유지합니다.

간단한 예시

use connections::conn::ConnR;
use connections::core::u032::U032I032;

// Rust의 `as`는 낮은 비트를 유지하고 래핑합니다:
assert_eq!(u32::MAX as i32, -1);

// 같은 변환을 Conn으로 하면 포화가 명시적으로 적용됩니다:
assert_eq!(U032I032.floor(u32::MAX), i32::MAX);

// 역 adjoint는 `lower` 입니다:
assert_eq!(U032I032.lower(-1), 0_u32);

이 예시는 Conn이 포화 정책을 가시화하고 수학적으로 대등한 연산과 짝을 이루게 함을 보여줍니다.

Composition API

매크로 compose!(및 변형 compose_l, compose_r, compose_k)는 일련의 쌍별 연결로부터 복합 Conn을 구축합니다. 결과 Conn은 구성에 의해 동일한 Galois 부등식을 만족하므로 런타임 검사가 필요 없습니다.

베스트 프랙티스 – 라이브러리에서 Conn 값을 내보내고, 호출자는 매크로를 사용해 호출 지점에서 이를 조합합니다. 이렇게 하면 변환 정책과 정적 캐스트가 함께 유지되어 코드 감시와 테스트가 쉬워집니다.

라이브러리 제공 범위

connections는 요구되는 부등식을 만족하는 단조 함수들로부터 자동 생성된 방대한 연결군을 제공합니다:

도메인 모듈 예시 연결
IEEE‑754 부동소수점 float F064F032 (f64 → f32)
고정소수점 Q‑포맷 fixed (feature) Q008Q000 등
표준 정수 core 확대/축소 쌍 예: U032I032
NonZero 래퍼 core NonZeroU32 ↔ u32
바이트 순서 core U008BE01, U008LE01
IP 주소 변환 addr U032IPV4, U128IPV6
char 코드포인트 core::char U032CHAR
std::time::Duration 계열 time (feature) SDURU064, F064SDUR
고정밀 시간 (hifitime) hifi (feature) HDURNANO, ETAINANO
하이브리드 논리 시계 uhlc (feature) NDURU064, HLIDLX16

모든 핵심 연결은 힙 없이, Copy이며 const입니다. 선택적 기능(fixed, time, hifi, uhlc, f16, try_trait)은 추가 패밀리를 제공하지만 런타임 의존성을 끌어오지 않습니다.

형식 검증

  • Proptest 법칙 스위트 – 모든 연결은 Galois 법칙, 폐쇄성, 커널, 단조성, 멱등성을 포괄하는 속성 테스트를 수행합니다. 부동소수점 제너레이터는 NaN, 무한대, 비정규수, ULP 경계에 편향됩니다.
  • Kani SMT 증명 – 정수, Q‑포맷, NonZero, iso 계열에 대해 크레이트는 전체 비트폭 도메인에 대한 Galois 술어를 증명하는 Kani 하네스를 제공합니다. 부동소수점 증명은 f64 → f32 축소 경로에 한정되며, 모든 유한 입력에 대해 ≤ 2 회 반복으로 수렴함을 보입니다.
  • 증명 코드는 #[cfg(kani)] 로 조건부이며 일반 빌드에 영향을 주지 않습니다.

샌드위치 부등식과 adjoint 삼중항

단일 내부 함수가 upper와 lower 양쪽 역할을 할 수 있을 때, 크레이트는 세 함수 ceil, inner, floor 로 ConnK 마커를 구성합니다. 양면 헬퍼가 올바르게 동작하려면 샌드위치 부등식 floor(a) ≤ ceil(a) 가 모든 a에 대해 성립해야 합니다. 문서에서는 이 부등식과 inner 가 order‑reflecting 이어야 함을 동등하게 증명합니다.

각 측면 Galois 법칙은 만족하지만 샌드위치 부등식이 깨지는 반례를 제시하여 round/truncate 가 오동작하는 사례를 보여줍니다. 이는 ConnK 연결에 대해 부등식을 강제하는 이유를 설명합니다.

설치 및 사용법

cargo add connections
  • MSRV – Rust 1.88 (edition 2024).
  • 라이선스 – MIT.
  • 선택적 패밀리는 Cargo 기능으로 활성화합니다. 예: cargo add connections --features fixed,time.

커뮤니티 피드백

작성자의 HN 댓글에서는 connections가 TryFrom 의 대체가 아니라는 점을 강조합니다. 런타임 파라미터화된 변환과 사용자 정의 정책은 일반 함수에 남겨두고, 변환 정책이 정적이며 안전하게 조합될 필요가 있을 때 connections가 빛을 발합니다.

정리

connections는 수학적으로 근거 있는, 컴파일 타임에 조합 가능한 숫자 캐스트를 Rust에 도입합니다. Galois 연결을 일급 값으로 다룸으로써 반올림, 포화, 왕복 보장을 명시적이고 증명 가능하게 만들며, 다양한 숫자 및 시간 도메인에 걸쳐 재사용할 수 있습니다.

Sources