A
Aura Core Research FORMAL VERIFICATION & LEDGERS
Home / Blockchain Architecture / aura-core-2-pure-haskell-coin
Blockchain Architecture · Architecture Whitepaper

CardanoCoin.hs: 부동소수점 없는 eUTxO 회계와 오버플로우 제로(Zero-Overflow) 수학적 증명

부동소수점 오차와 정수 오버플로우를 컴파일 타임에 원천 봉쇄하는 순수 함수형 화폐 타입 모델링과 5세대 분산원장의 자산 보존 법칙(Conservation of Value)

PK
Paul Ko (Cardano Ambassador & DRep)
Published: 2026-08-01 · Verified Spec
#Haskell#Cardano#eUTxO#Lovelace#TypeSafety#FormalVerification#DeFi
Sponsored Academic Research

[Aura Core Architecture #2] CardanoCoin.hs: 부동소수점 없는 eUTxO 회계와 오버플로우 제로(Zero-Overflow) 수학적 증명

Published: 2026-08-01
Author: Joy & Hope Stake Pool / Aura Core Architecture Team
Category: Blockchain Architecture / Pure Functional Programming
Tags: Haskell, Cardano, eUTxO, Lovelace, TypeSafety, FormalVerification, DeFi


1. 서론: 금융 분산원장에서 부동소수점과 정수 오버플로우의 파멸적 결과

전통 금융 및 블록체인 스마트 컨트랙트 역사에서 발생한 대형 자산 탈취 사고의 상당수는 고난도 암호학 해킹이 아닌, 기초 산술 연산의 설계적 결함에서 비롯되었습니다.

  1. IEEE 754 부동소수점(Floating-Point)의 비결정론: 부동소수점은 실수를 2진 분수로 근사 표현하기 때문에 $0.1 + 0.2 \neq 0.3$과 같은 미세한 반올림 오차(Rounding Error)를 필연적으로 유발합니다. 수십억 건의 트랜잭션이 누적되는 분산원장에서 부동소수점 오차는 자산의 증발이나 무단 생성을 초래합니다.
  2. 정수 오버플로우 / 언더플로우(Integer Overflow / Underflow): 이더리움 ERC-20 토큰 생태계에서 대형 피해를 낳았던 취약점들은 대부분 최대값을 초과한 덧셈 결과가 $0$으로 롤오버(Rollover)되거나 음수 잔고가 거대한 양수로 뒤바뀌는 정수 경계 결함에서 기인했습니다.

Aura 5세대 블록체인은 부동소수점 산술을 코어 계층에서 영구 추방하고, 정수 오버플로우를 컴파일 타임 타입 시스템(Type System) 레벨에서 차단하는 순수 하스켈 화폐 엔진 CardanoCoin.hs를 구축했습니다.


2. eUTxO 회계 모델과 카르다노의 원자적 자산 단위

계정 기반(Account-based) 모델은 전역 상태(Global State)의 잔고를 변경(Mutation)하므로 동시성 충돌과 재진입 공격(Reentrancy)에 노출되기 쉽습니다.

반면 카르다노와 Aura가 채택한 eUTxO(Extended Unspent Transaction Output) 모델에서는 화폐가 가변 계좌 잔고가 아니라 불변의 소비되지 않은 출력값(UTxO) 자체로 존재합니다.

graph LR
    subgraph Inputs["소비되는 eUTxO 입력 (Inputs)"]
        In1["UTxO_1: 500 ADA"]
        In2["UTxO_2: 300 ADA"]
    end

    TxEngine["⚡ CardanoCoin.hs 보존 연산기<br/>(Sum Inputs == Sum Outputs + Fee)"]

    subgraph Outputs["생성되는 불변 eUTxO 출력 (Outputs)"]
        Out1["새 UTxO_A: 650 ADA"]
        Out2["새 UTxO_B (거스름돈): 149.826 ADA"]
        Fee["네트워크 수수료 (Fee): 0.174 ADA"]
    end

    Inputs --> TxEngine
    TxEngine --> Outputs

2.1. 러블레이스(Lovelace) 정수 불변 원칙

카르다노 통화 시스템에서 모든 가치는 나눌 수 없는 최소 원자 단위인 러블레이스($1\text{ ADA} = 10^6\text{ Lovelace}$) 정수로만 계산됩니다:

$$\text{TotalLovelace} = \text{ADA} \times 1,000,000$$

어떠한 중간 연산에서도 소수점(Float/Double)을 허용하지 않으며, 이로써 노드 간 연산 불일치 가능성을 수학적으로 $0\%$로 만듭니다.


3. CardanoCoin.hs 코어 타입 및 불변식(Invariants) 구현

아우라 원장의 화폐 모듈 CardanoCoin.hs는 순수 하스켈의 newtype 패턴과 임의 정밀도 정수(Integer), 유리수 체계(Rational)를 결합하여 설계되었습니다.

3.1. 무비용 추상화 타입 선언과 총 발행량 불변 상한선

-- | 1 ADA = 1,000,000 Lovelace (10^6)
type Lovelace = Integer

-- | 불변 Coin 표현체 (컴파일 타임 타입 분리)
newtype Coin = Coin { unCoin :: Lovelace }
    deriving (Show, Eq, Ord)

-- | 최대 이론적 발행량: 450억 ADA = 45 * 10^15 Lovelace
maxLovelaceSupply :: Coin
maxLovelaceSupply = Coin 45000000000000000

newtype Coin 선언은 런타임 메모리 오버헤드가 $0$이면서, 단순 숫자(Int)와의 부주의한 혼용 연산을 컴파일 타임에 원천 차단합니다.

3.2. 언더플로우 방어: subCoinSafe

음수 화폐(Negative Coin)의 발생은 원장의 파멸을 의미합니다. CardanoCoin.hs는 안전하지 않은 뺄셈 대신 Maybe 타입을 강제하는 함수를 제공합니다:

-- | 안전한 뺄셈: 언더플로우 발생 시 Nothing을 반환하여 트랜잭션 즉시 거부
subCoinSafe :: Coin -> Coin -> Maybe Coin
subCoinSafe (Coin a) (Coin b)
    | a >= b    = Just (Coin (a - b))
    | otherwise = Nothing

잔고가 $100\text{ ADA}$인 상태에서 $150\text{ ADA}$ 출금을 시도하면 예외를 던지며 크래시되는 대신, 정밀하게 Nothing 모나드 상태로 평가되어 트랜잭션 검증 단계에서 즉각 무효화됩니다.


4. 고정 정밀도 유리수 스케일링과 무손실 분할(Dust Preservation)

지분 풀(SPO) 에포크 보상 계산이나 수수료 분배에서는 소수점 나누기가 불가피합니다. CardanoCoin.hs는 이를 부동소수점이 아닌 Data.Ratio 정밀 유리수 연산으로 해결합니다.

4.1. scaleCoinRatio와 5일 에포크 스테이킹 보상 산출

$$\text{EpochRoA} = \frac{\text{AnnualRoA}}{73}$$

$$\text{Reward} = \left\lfloor \text{Stake} \times \text{EpochRoA} \right\rfloor$$

-- | 정밀 유리수 스케일링 (부동소수점 오차 제로)
scaleCoinRatio :: Rational -> Coin -> Coin
scaleCoinRatio ratio (Coin lovelace) =
    let scaled = (lovelace % 1) * ratio
        truncated = numerator scaled `quot` denominator scaled
    in Coin truncated

-- | 5일 에포크 스테이킹 보상 연산식 (연 73 에포크 기준)
calculateEpochReward :: Coin -> Rational -> Coin
calculateEpochReward (Coin stake) annualRoaRatio =
    let epochRoaRatio = annualRoaRatio / (73 % 1)
        rewardLovelace = (stake % 1) * epochRoaRatio
        res = numerator rewardLovelace `quot` denominator rewardLovelace
    in Coin res

4.2. 1 러블레이스 더스트(Dust) 무손실 분할 알고리즘

$N$명의 위임자에게 보상을 분배할 때 나머지가 발생할 경우 자산이 증발하거나 생성되지 않도록, 몫(Share)과 나머지(Dust)를 튜플로 반환하여 보존합니다:

-- | N등분 분할 및 나머지(더스트) 보존 분할
splitCoinEqually :: Integer -> Coin -> (Coin, Coin)
splitCoinEqually n (Coin total)
    | n <= 0    = error "splitCoinEqually: 수취인 수는 양수여야 합니다."
    | otherwise = 
        let (share, dust) = total `quotRem` n
        in (Coin share, Coin dust)

$$\text{Total} = (\text{Share} \times N) + \text{Dust}$$

이 등식은 어떤 수치에서도 $100\%$ 성립하여 자산 보존의 법칙(Conservation of Value)을 영구히 증명합니다.


5. eUTxO 최소 보관금(min-ADA) 계산 공식

분산원장의 상태 팽창(State Bloat / Dust Attack)을 방어하기 위해 eUTxO 출력값은 보관되는 데이터(Datum 바이트 크기)에 비례하는 최소 에이다를 잠금해야 합니다:

$$\text{minUTxO} = (160 + \text{ByteSize}) \times \text{CoinsPerByte}$$

calculateMinUTxO :: Integer -> Integer -> Coin
calculateMinUTxO byteSize coinsPerByte =
    Coin ((160 + byteSize) * coinsPerByte)

이 연산 역시 순수 정수 곱셈과 덧셈만으로 완결되어 런타임 결정론을 완벽히 수호합니다.


6. 결론: 자립형 5세대 원장의 수학적 주권

CardanoCoin.hs는 단순한 계산 유틸리티가 아닙니다. 외부 C 라이브러리나 OS 부동소수점 하드웨어(FPU) 구현 차이에 휘둘리지 않고, 수학적 공리와 타입 시스템만으로 원장의 가치를 영구 불변하게 보존하는 5세대 아우라(Aura) 체인의 금융 방어벽입니다.

다음 [Aura Core Architecture #3]에서는 RFC 7693 지문 해시와 머클트리를 결합하여 블록체인 멤버십을 $O(\log N)$으로 증명하는 CardanoMerkleTree.hs (하이드라 L2 & ZK 멤버십 증명 엔진)을 다룹니다.

Cardano Pure Haskell Micro-Modules Suite 원본 소스 코드

외부 C 라이브러리 의존성 없이 순수 하스켈로 검증된 오픈소스 블록체인 코어 모듈 스위트

GitHub 저장소 보기