21f0db3 · Idris-dev · git.iko.soy

28bitsUsed n = 8 * (2 `power` n)

29

30%assert_total

31−natToBits' : machineTy n -> Nat -> machineTy n

31+natToBits' : [static] {n : Nat} -> machineTy n -> Nat -> machineTy n

32natToBits' a Z = a

33natToBits' {n=n} a x with (n)

34 -- it seems I have to manually recover the value of n here, instead of being able to reference it

37 natToBits' a (S x') | S (S Z) = natToBits' {n=2} (prim__addB32 a (prim__truncInt_B32 1)) x'

38 natToBits' a (S x') | S (S (S _)) = natToBits' {n=3} (prim__addB64 a (prim__truncInt_B64 1)) x'

39

40−natToBits : Nat -> machineTy n

40+natToBits : [static] {n : Nat} -> Nat -> machineTy n

41natToBits {n=n} x with (n)

42 | Z = natToBits' {n=0} (prim__truncInt_B8 0) x

43 | S Z = natToBits' {n=1} (prim__truncInt_B16 0) x

44 | S (S Z) = natToBits' {n=2} (prim__truncInt_B32 0) x

45 | S (S (S _)) = natToBits' {n=3} (prim__truncInt_B64 0) x

46

47−getPad : Nat -> machineTy n

47+getPad : [static] {n : Nat} -> Nat -> machineTy n

48getPad n = natToBits (minus (bitsUsed (nextBytes n)) n)

49

50public

92 where

93 pad = getPad {n=3} n

94

95−shiftLeft' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

95+shiftLeft' : [static] {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

96shiftLeft' {n=n} x c with (nextBytes n)

97 | Z = pad8' n prim__shlB8 x c

98 | S Z = pad16' n prim__shlB16 x c

100 | S (S (S _)) = pad64' n prim__shlB64 x c

101

102public

103−shiftLeft : Bits n -> Bits n -> Bits n

103+shiftLeft : [static] {n : Nat} -> Bits n -> Bits n -> Bits n

104shiftLeft (MkBits x) (MkBits y) = MkBits (shiftLeft' x y)

105

106−shiftRightLogical' : machineTy n -> machineTy n -> machineTy n

106+shiftRightLogical' : [static] {n : Nat} -> machineTy n -> machineTy n -> machineTy n

107shiftRightLogical' {n=n} x c with (n)

108 | Z = prim__lshrB8 x c

109 | S Z = prim__lshrB16 x c

111 | S (S (S _)) = prim__lshrB64 x c

112

113public

114−shiftRightLogical : Bits n -> Bits n -> Bits n

114+shiftRightLogical : [static] {n : Nat} -> Bits n -> Bits n -> Bits n

115shiftRightLogical {n} (MkBits x) (MkBits y)

116 = MkBits {n} (shiftRightLogical' {n=nextBytes n} x y)

117

118−shiftRightArithmetic' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

118+shiftRightArithmetic' : [static] {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

119shiftRightArithmetic' {n=n} x c with (nextBytes n)

120 | Z = pad8' n prim__ashrB8 x c

121 | S Z = pad16' n prim__ashrB16 x c

123 | S (S (S _)) = pad64' n prim__ashrB64 x c

124

125public

126−shiftRightArithmetic : Bits n -> Bits n -> Bits n

126+shiftRightArithmetic : [static] {n : Nat} -> Bits n -> Bits n -> Bits n

127shiftRightArithmetic (MkBits x) (MkBits y) = MkBits (shiftRightArithmetic' x y)

128

129−and' : machineTy n -> machineTy n -> machineTy n

129+and' : [static] {n : Nat} -> machineTy n -> machineTy n -> machineTy n

130and' {n=n} x y with (n)

131 | Z = prim__andB8 x y

132 | S Z = prim__andB16 x y

134 | S (S (S _)) = prim__andB64 x y

135

136public

137−and : Bits n -> Bits n -> Bits n

137+and : [static] {n : Nat} -> Bits n -> Bits n -> Bits n

138and {n} (MkBits x) (MkBits y) = MkBits (and' {n=nextBytes n} x y)

139

140−or' : machineTy n -> machineTy n -> machineTy n

140+or' : [static] {n : Nat} -> machineTy n -> machineTy n -> machineTy n

141or' {n=n} x y with (n)

142 | Z = prim__orB8 x y

143 | S Z = prim__orB16 x y

145 | S (S (S _)) = prim__orB64 x y

146

147public

148−or : Bits n -> Bits n -> Bits n

148+or : [static] {n : Nat} -> Bits n -> Bits n -> Bits n

149or {n} (MkBits x) (MkBits y) = MkBits (or' {n=nextBytes n} x y)

150

151−xor' : machineTy n -> machineTy n -> machineTy n

151+xor' : [static] {n : Nat} -> machineTy n -> machineTy n -> machineTy n

152xor' {n=n} x y with (n)

153 | Z = prim__xorB8 x y

154 | S Z = prim__xorB16 x y

156 | S (S (S _)) = prim__xorB64 x y

157

158public

159−xor : Bits n -> Bits n -> Bits n

159+xor : [static] {n : Nat} -> Bits n -> Bits n -> Bits n

160xor {n} (MkBits x) (MkBits y) = MkBits {n} (xor' {n=nextBytes n} x y)

161

162plus' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

167 | S (S (S _)) = pad64 n prim__addB64 x y

168

169public

170−plus : Bits n -> Bits n -> Bits n

170+plus : [static] {n : Nat} -> Bits n -> Bits n -> Bits n

171plus (MkBits x) (MkBits y) = MkBits (plus' x y)

172

173minus' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

178 | S (S (S _)) = pad64 n prim__subB64 x y

179

180public

181−minus : Bits n -> Bits n -> Bits n

181+minus : [static] {n : Nat} -> Bits n -> Bits n -> Bits n

182minus (MkBits x) (MkBits y) = MkBits (minus' x y)

183

184times' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

189 | S (S (S _)) = pad64 n prim__mulB64 x y

190

191public

192−times : Bits n -> Bits n -> Bits n

192+times : [static] {n : Nat} -> Bits n -> Bits n -> Bits n

193times (MkBits x) (MkBits y) = MkBits (times' x y)

194

195partial

201 | S (S (S _)) = prim__sdivB64 x y

202

203public partial

204−sdiv : Bits n -> Bits n -> Bits n

204+sdiv : [static] {n : Nat} -> Bits n -> Bits n -> Bits n

205sdiv (MkBits x) (MkBits y) = MkBits (sdiv' x y)

206

207partial

213 | S (S (S _)) = prim__udivB64 x y

214

215public partial

216−udiv : Bits n -> Bits n -> Bits n

216+udiv : [static] {n : Nat} -> Bits n -> Bits n -> Bits n

217udiv (MkBits x) (MkBits y) = MkBits (udiv' x y)

218

219partial

220−srem' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

220+srem' : [static] {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

221srem' {n=n} x y with (nextBytes n)

222 | Z = prim__sremB8 x y

223 | S Z = prim__sremB16 x y

225 | S (S (S _)) = prim__sremB64 x y

226

227public partial

228−srem : Bits n -> Bits n -> Bits n

228+srem : [static] {n : Nat} -> Bits n -> Bits n -> Bits n

229srem (MkBits x) (MkBits y) = MkBits (srem' x y)

230

231partial

232−urem' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

232+urem' : [static] {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

233urem' {n=n} x y with (nextBytes n)

234 | Z = prim__uremB8 x y

235 | S Z = prim__uremB16 x y

237 | S (S (S _)) = prim__uremB64 x y

238

239public partial

240−urem : Bits n -> Bits n -> Bits n

240+urem : [static] {n : Nat} -> Bits n -> Bits n -> Bits n

241urem (MkBits x) (MkBits y) = MkBits (urem' x y)

242

243-- TODO: Proofy comparisons via postulates

244−lt : machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int

244+lt : [static] {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int

245lt {n=n} x y with (nextBytes n)

246 | Z = prim__ltB8 x y

247 | S Z = prim__ltB16 x y

248 | S (S Z) = prim__ltB32 x y

249 | S (S (S _)) = prim__ltB64 x y

250

251−lte : machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int

251+lte : [static] {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int

252lte {n=n} x y with (nextBytes n)

253 | Z = prim__lteB8 x y

254 | S Z = prim__lteB16 x y

255 | S (S Z) = prim__lteB32 x y

256 | S (S (S _)) = prim__lteB64 x y

257

258−eq : machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int

258+eq : [static] {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int

259eq {n=n} x y with (nextBytes n)

260 | Z = prim__eqB8 x y

261 | S Z = prim__eqB16 x y

262 | S (S Z) = prim__eqB32 x y

263 | S (S (S _)) = prim__eqB64 x y

264

265−gte : machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int

265+gte : [static] {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int

266gte {n=n} x y with (nextBytes n)

267 | Z = prim__gteB8 x y

268 | S Z = prim__gteB16 x y

269 | S (S Z) = prim__gteB32 x y

270 | S (S (S _)) = prim__gteB64 x y

271

272−gt : machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int

272+gt : [static] {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int

273gt {n=n} x y with (nextBytes n)

274 | Z = prim__gtB8 x y

275 | S Z = prim__gtB16 x y

291 then EQ

292 else GT

293

294−complement' : machineTy (nextBytes n) -> machineTy (nextBytes n)

294+complement' : [static] {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n)

295complement' {n=n} x with (nextBytes n)

296 | Z = let pad = getPad {n=0} n in

297 prim__complB8 (x `prim__shlB8` pad) `prim__lshrB8` pad

303 prim__complB64 (x `prim__shlB64` pad) `prim__lshrB64` pad

304

305public

306−complement : Bits n -> Bits n

306+complement : [static] {n : Nat} -> Bits n -> Bits n

307complement (MkBits x) = MkBits (complement' x)

308

309-- TODO: Prove

310%assert_total -- can't verify coverage of with block

311−zext' : machineTy (nextBytes n) -> machineTy (nextBytes (n+m))

311+zext' : [static] {n : Nat} -> [static] {m : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes (n+m))

312zext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))

313 | (Z, Z) = believe_me x

314 | (Z, S Z) = believe_me (prim__zextB8_B16 (believe_me x))

322 | (S (S (S _)), S (S (S _))) = believe_me x

323

324public

325−zeroExtend : Bits n -> Bits (n+m)

325+zeroExtend : [static] {n : Nat} -> [static] {m : Nat} -> Bits n -> Bits (n+m)

326zeroExtend (MkBits x) = MkBits (zext' x)

327

328%assert_total

329−intToBits' : Integer -> machineTy (nextBytes n)

329+intToBits' : [static] {n : Nat} -> Integer -> machineTy (nextBytes n)

330intToBits' {n=n} x with (nextBytes n)

331 | Z = let pad = getPad {n=0} n in

332 prim__lshrB8 (prim__shlB8 (prim__truncBigInt_B8 x) pad) pad

338 prim__lshrB64 (prim__shlB64 (prim__truncBigInt_B64 x) pad) pad

339

340public

341−intToBits : Integer -> Bits n

341+intToBits : [static] {n : Nat} -> Integer -> Bits n

342intToBits n = MkBits (intToBits' n)

343

344implementation Cast Integer (Bits n) where

345 cast = intToBits

346

347−bitsToInt' : machineTy (nextBytes n) -> Integer

347+bitsToInt' : [static] {n : Nat} -> machineTy (nextBytes n) -> Integer

348bitsToInt' {n=n} x with (nextBytes n)

349 | Z = prim__zextB8_BigInt x

350 | S Z = prim__zextB16_BigInt x

352 | S (S (S _)) = prim__zextB64_BigInt x

353

354public

355−bitsToInt : Bits n -> Integer

355+bitsToInt : [static] {n : Nat} -> Bits n -> Integer

356bitsToInt (MkBits x) = bitsToInt' x

357

358-- Zero out the high bits of a truncated bitstring

359−zeroUnused : machineTy (nextBytes n) -> machineTy (nextBytes n)

359+zeroUnused : [static] {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n)

360zeroUnused {n} x = x `and'` complement' (intToBits' {n=n} 0)

361

362--implementation Cast Nat (Bits n) where

364

365-- TODO: Prove

366%assert_total -- can't verify coverage of with block

367−sext' : machineTy (nextBytes n) -> machineTy (nextBytes (n+m))

367+sext' : [static] {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes (n+m))

368sext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))

369 | (Z, Z) = let pad = getPad {n=0} n in

370 believe_me (prim__ashrB8 (prim__shlB8 (believe_me x) pad) pad)

399

400-- TODO: Prove

401%assert_total -- can't verify coverage of with block

402−trunc' : machineTy (nextBytes (m+n)) -> machineTy (nextBytes n)

402+trunc' : [static] {m : Nat} -> [static] {n : Nat} -> machineTy (nextBytes (m+n)) -> machineTy (nextBytes n)

403trunc' {m=m} {n=n} x with (nextBytes n, nextBytes (m+n))

404 | (Z, Z) = believe_me x

405 | (Z, S Z) = believe_me (prim__truncB16_B8 (believe_me x))

413 | (S (S (S _)), S (S (S _))) = believe_me x

414

415public

416−truncate : Bits (m+n) -> Bits n

416+truncate : [static] {m : Nat} -> [static] {n : Nat} -> Bits (m+n) -> Bits n

417truncate (MkBits x) = MkBits (zeroUnused (trunc' x))

418

419public

420−bitAt : Fin n -> Bits n

420+bitAt : [static] {n : Nat} -> Fin n -> Bits n

421bitAt n = intToBits 1 `shiftLeft` intToBits (cast n)

422

423public

424−getBit : Fin n -> Bits n -> Bool

424+getBit : [static] {n : Nat} -> Fin n -> Bits n -> Bool

425getBit n x = (x `and` (bitAt n)) /= intToBits 0

426

427public

428−setBit : Fin n -> Bits n -> Bits n

428+setBit : [static] {n : Nat} -> Fin n -> Bits n -> Bits n

429setBit n x = x `or` (bitAt n)

430

431public

432−unsetBit : Fin n -> Bits n -> Bits n

432+unsetBit : [static] {n : Nat} -> Fin n -> Bits n -> Bits n

433unsetBit n x = x `and` complement (bitAt n)

434

435−bitsToStr : Bits n -> String

435+bitsToStr : [static] {n : Nat} -> Bits n -> String

436bitsToStr x = pack (helper last x)

437 where

438 %assert_total

439− helper : Fin (S n) -> Bits n -> List Char

439+ helper : [static] {n : Nat} -> Fin (S n) -> Bits n -> List Char

440 helper FZ _ = []

441 helper (FS x) b = (if getBit x b then '1' else '0') :: helper (weaken x) b

442