Coverage report: /home/runner/work/geb/geb/src/specs/seqn.lisp

Kind	Covered	All	%
expression	51	150	34.0
branch	0	0	nil

Key

Not instrumented

Conditionalized out

Executed

Not executed

Both branches taken

One branch taken

Neither branch taken

1

(in-package #:geb.seqn.spec)

2

3

(deftype seqn ()

4

'(or composition id fork-seq drop-nil remove-right remove-left drop-width

5

inj-length-left inj-length-right inj-size branch-seq shift-front zero-bit

6

one-bit parallel-seq seqn-add seqn-subtract seqn-multiply seqn-divide

7

seqn-nat seqn-concat seqn-decompose seqn-lt seqn-eq seqn-mod))

8

9

(defclass <seqn> (geb.mixins:direct-pointwise-mixin cat-morph) ()

10

(:documentation "Seqn is a category whose objects are finite sequences of natural numbers.

11

The n-th natural number in the sequence represents the bitwidth of the n-th

12

entry of the corresponding polynomial circuit

13

14

Entries are to be read as (x_1,..., x_n) and x_i is the ith entry

15

So car of a such a list will be the first entry, this is the dissimilarity

16

with the bit notation where newer entries come first in the list

17

18

We interpret pairs as actual pairs if entry is of width above 0

19

and drop it otherwise in the Vamp-Ir setup so that

20

ident bool x bool goes to

21

name x1 = x1

22

as (seqwidth bool) = (1, max(0, 0)) "))

23

24

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

25

;; Constructor Morphisms for Seqn

26

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

27

28

(defclass composition (<seqn>)

29

((mcar :initarg :mcar

30

:accessor mcar

31

:documentation "")

32

(mcadr :initarg :mcadr

33

:accessor mcadr

34

:documentation ""))

35

(:documentation "composes the MCAR and MCADR morphisms

36

f : (a1,...,an) -> (b1,..., bm), g : (b1,...,bm) -> (c1, ..., ck)

37

compose g f : (a1,...,an) -> (c1,...,cn)"))

38

39

(defclass fork-seq (<seqn>)

40

((mcar :initarg :mcar

41

:accessor mcar

42

:documentation ""))

43

(:documentation "Copies the MCAR of length n onto length 2*n by copying its

44

inputs (MCAR). fork (a1, ...., an) -> (a1,...,an, a1,..., an)"))

45

46

(defclass parallel-seq (<seqn>)

47

((mcar :initarg :mcar

48

:accessor mcar

49

:documentation "")

50

(mcadr :initarg :mcadr

51

:accessor mcadr

52

:documentation ""))

53

(:documentation "For f : (a1,..., an) -> (x1,...,xk), g : (b1,..., bm) -> (y1,...,yl)

54

parallel f g : (a1,...,an, b1,...bm) -> (x1,...,xk,y1,...,yl)"))

55

56

(defclass id (<seqn>)

57

((mcar :initarg :mcar

58

:accessor mcar

59

:documentation ""))

60

(:documentation "For (x1,...,xn),

61

id (x1,...,xn) : (x1,....,xn) -> (x1,...,xn)"))

62

63

(defclass drop-nil (<seqn>)

64

((mcar :initarg :mcar

65

:accessor mcar

66

:documentation ""))

67

(:documentation "Drops everything onto a 0 vector,

68

the terminal object drop-nil (x1, ..., xn) : (x1,...,xn) -> (0)"))

69

70

(defclass remove-right (<seqn>)

71

((mcar :initarg :mcar

72

:accessor mcar

73

:documentation ""))

74

(:documentation "Removes an extra 0 entry from MCAR on the right

75

remove (x1,...,xn) : (x1,...,xn, 0) -> (x1,...,xn)"))

76

77

(defclass remove-left (<seqn>)

78

((mcar :initarg :mcar

79

:accessor mcar

80

:documentation ""))

81

(:documentation "Removes an extra 0 entry from MCAR on the left

82

remove (x1,...,xn) : (0, x1,...,xn) -> (x1,...,xn)"))

83

84

(defclass drop-width (<seqn>)

85

((mcar :initarg :mcar

86

:accessor mcar

87

:documentation "")

88

(mcadr :initarg :mcadr

89

:accessor mcadr

90

:documentation ""))

91

(:documentation "Given two vectors of same length

92

but with the first ones of padded width, simply project the

93

core bits without worrying about extra zeroes at the end if they

94

are not doing any work

95

drop-width (x1,...,xn) (y1,...,yn) : (x1,...,xn) -> (y1,...,yn)

96

where xi > yi for each i and entries need to be in the image of the

97

evident injection map

98

99

In other words the constraints here are that on the enput ei corresponding to

100

xi bit entry the constraint is that range yi ei is true alongside

101

the usual (isrange xi ei) constraint

102

103

Another implementation goes through manual removal of extra bits (specifically

104

xi-yi bits) to the left after the decomposition by range xi"))

105

106

(defclass inj-length-left (<seqn>)

107

((mcar :initarg :mcar

108

:accessor mcar

109

:documentation "")

110

(mcadr :initarg :mcadr

111

:accessor mcadr

112

:documentation ""))

113

(:documentation "Taken an MCAR vector appends to it

114

MCADR list of vectors with arbitrary bit length by doing

115

nothing on the extra entries, i.e. just putting 0es there.

116

inj-lengh-left (x1,...,xn) (y1,...,ym): (x1,...,xn) -> (x1,...,xn, y1,...,yn)

117

Where 0es go in the place of ys or nothing if the injection is into

118

0-bits

119

120

So what gets injected is the left part"))

121

122

(defclass inj-length-right (<seqn>)

123

((mcar :initarg :mcar

124

:accessor mcar

125

:documentation "")

126

(mcadr :initarg :mcadr

127

:accessor mcadr

128

:documentation ""))

129

(:documentation "Taken an MCADR vector appends to it

130

MCAR list of vectors with arbitrary bit length by doing

131

nothing on the extra entries, i.e. just putting 0es there.

132

inj-lengh-right (x1,...,xn) (y1,...,ym): (y1,...,ym) -> (x1,...,xn, y1,...,yn)

133

Where 0es go in the place of xs. If any of yi's are 0-bit vectors, the injection

134

goes to nil entry on those parts

135

136

What gets injected is the right part"))

137

138

139

(defclass inj-size (<seqn>)

140

((mcar :initarg :mcar

141

:accessor mcar

142

:documentation "")

143

(mcadr :initarg :mcadr

144

:accessor mcadr

145

:documentation ""))

146

(:documentation "Taken an MCAR 1-long and injects it to

147

MCADR-wide slot wider than the original one by padding it with

148

0es on the left.

149

inj-size x1 m: (x1) -> (m)

150

151

Just a special case of drop-width"))

152

153

(defclass branch-seq (<seqn>)

154

((mcar :initarg :mcar

155

:accessor mcar

156

:documentation "")

157

(mcadr :initarg :mcadr

158

:accessor mcadr

159

:documentation ""))

160

(:documentation "Takes an

161

f: (x1,...,xn) -> c, g : (x1,...,xn) ->c and

162

produces branch-seq f g (1, x1,...,xn) -> c acting as

163

f on 0 entry and g on 1"))

164

165

(defclass zero-bit (<seqn>)

166

()

167

(:documentation "Zero choice of a bit

168

zero: (0) -> (1)"))

169

170

171

(defclass one-bit (<seqn>)

172

()

173

(:documentation "1 choice of a bit

174

one: (0) -> (1)"))

175

176

(defclass shift-front (<seqn>)

177

((mcar :initarg :mcar

178

:accessor mcar

179

:documentation "")

180

(mcadr :initarg :mcadr

181

:accessor mcadr

182

:documentation ""))

183

(:documentation "Takes an MCAR sequence of length at least

184

MCADR and shifts the MCADR-entry to the front

185

shift-front (x1,...,xn) k : (x1,...,xk,...,xn) -> (xk, x1,..., x_k-1, x_k+1,...,xn)"))

186

187

(defclass seqn-add (<seqn>)

188

((mcar :initarg :mcar

189

:accessor mcar

190

:documentation ""))

191

(:documentation "Compiles to range-checked addition of natural numbers

192

of MCAR width. seqn-add n : (n, n) -> (n)"))

193

194

(defclass seqn-subtract (<seqn>)

195

((mcar :initarg :mcar

196

:accessor mcar

197

:documentation ""))

198

(:documentation "Compiles to negative-checked subtraction of natural numbers

199

of MCAR width. seqn-subtract n : (n, n) -> (n)"))

200

201

(defclass seqn-multiply (<seqn>)

202

((mcar :initarg :mcar

203

:accessor mcar

204

:documentation ""))

205

(:documentation "Compiles to range-checked multiplication of natural numbers

206

of MCAR width. seqn-multiply n : (n, n) -> (n)"))

207

208

(defclass seqn-divide (<seqn>)

209

((mcar :initarg :mcar

210

:accessor mcar

211

:documentation ""))

212

(:documentation "Compiles to usual Vamp-IR floored multiplication of natural

213

numbers of MCAR width. seqn-divide n : (n, n) -> (n)"))

214

215

(defclass seqn-nat (<seqn>)

216

((mcar :initarg :mcar

217

:accessor mcar

218

:documentation "")

219

(mcadr :initarg :mcadr

220

:accessor mcadr

221

:documentation ""))

222

(:documentation "Produces a MCAR-wide representation of MCADR natural number

223

seqn-nat n m = (0) -> (n)"))

224

225

(defclass seqn-concat (<seqn>)

226

((mcar :initarg :mcar

227

:accessor mcar

228

:documentation "")

229

(mcadr :initarg :mcadr

230

:accessor mcadr

231

:documentation ""))

232

(:documentation "Takes a number of MCAR and MCADR width and produces a number

233

of MCAR + MCADR width by concatenating the bit representations. Using field

234

elements, this translates to multiplying the first input by 2 to the power of

235

MCADR and summing with the second entry

236

seqn-concat n m = (n, m) -> (n+m)"))

237

238

(defclass seqn-decompose (<seqn>)

239

((mcar :initarg :mcar

240

:accessor mcar

241

:documentation ""))

242

(:documentation " The type signature of the morphism is

243

seqn-docompose n : (n) -> (1, (n - 1)) with the intended semantics being

244

that the morphism takes an n-bit integer and splits it, taking the leftmost

245

bit to the left part of the codomain and the rest of the bits to the righ"))

246

247

(defclass seqn-eq (<seqn>)

248

((mcar :initarg :mcar

249

:accessor mcar

250

:documentation ""))

251

(:documentation " The type signature of the morphism is

252

seqn-eq n : (n, n) -> (1, 0) with the intended semantics being

253

that the morphism takes two n-bit integers and produces 1 iff they are

254

equal"))

255

256

(defclass seqn-lt (<seqn>)

257

((mcar :initarg :mcar

258

:accessor mcar

259

:documentation ""))

260

(:documentation " The type signature of the morphism is

261

seqn-eq n : (n, n) -> (1, 0) with the intended semantics being

262

that the morphism takes two n-bit integers and produces 1 iff the first

263

one is less than the second"))

264

265

(defclass seqn-mod (<seqn>)

266

((mcar :initarg :mcar

267

:accessor mcar

268

:documentation ""))

269

(:documentation " The type signature of the morphism is

270

seqn-mod n : (n, n) -> (n) with the intended semantics being

271

that the morphism takes two n-bit integers and produces the

272

modulo of the first integer by the second"))

273

274

(serapeum:-> composition (<seqn> <seqn>) composition)

275

(defun composition (mcar mcadr)

276

(values

277

(make-instance 'composition :mcar mcar :mcadr mcadr)))

278

279

(serapeum:-> fork-seq (list) fork-seq)

280

(defun fork-seq (mcar)

281

(values

282

(make-instance 'fork-seq :mcar mcar)))

283

284

(serapeum:-> parallel-seq (<seqn> <seqn>) parallel-seq)

285

(defun parallel-seq (mcar mcadr)

286

(values

287

(make-instance 'parallel-seq :mcar mcar :mcadr mcadr)))

288

289

(serapeum:-> id (list) id)

290

(defun id (mcar)

291

(values

292

(make-instance 'id :mcar mcar)))

293

294

(serapeum:-> drop-nil (list) drop-nil)

295

(defun drop-nil (mcar)

296

(values

297

(make-instance 'drop-nil :mcar mcar)))

298

299

(serapeum:-> remove-right (list) remove-right)

300

(defun remove-right (mcar)

301

(values

302

(make-instance 'remove-right :mcar mcar)))

303

304

(serapeum:-> remove-left (list) remove-left)

305

(defun remove-left (mcar)

306

(values

307

(make-instance 'remove-left :mcar mcar)))

308

309

(serapeum:-> drop-width (list list) drop-width)

310

(defun drop-width (mcar mcadr)

311

(values

312

(make-instance 'drop-width :mcar mcar :mcadr mcadr)))

313

314

(serapeum:-> inj-length-left (list list) inj-length-left)

315

(defun inj-length-left (mcar mcadr)

316

(values

317

(make-instance 'inj-length-left :mcar mcar :mcadr mcadr)))

318

319

(serapeum:-> inj-length-right (list list) inj-length-right)

320

(defun inj-length-right (mcar mcadr)

321

(values

322

(make-instance 'inj-length-right :mcar mcar :mcadr mcadr)))

323

324

(serapeum:-> inj-size (fixnum fixnum) inj-size)

325

(defun inj-size (mcar mcadr)

326

(values

327

(make-instance 'inj-size :mcar mcar :mcadr mcadr)))

328

329

(serapeum:-> branch-seq (<seqn> <seqn>) branch-seq)

330

(defun branch-seq (mcar mcadr)

331

(values

332

(make-instance 'branch-seq :mcar mcar :mcadr mcadr)))

333

334

(serapeum:-> shift-front (list fixnum) shift-front)

335

(defun shift-front (mcar mcadr)

336

(values

337

(make-instance 'shift-front :mcar mcar :mcadr mcadr)))

338

339

(serapeum:def zero-bit

340

(make-instance 'zero-bit))

341

342

(serapeum:def one-bit

343

(make-instance 'one-bit))

344

345

(serapeum:-> seqn-add (fixnum) seqn-add)

346

(defun seqn-add (mcar)

347

(values

348

(make-instance 'seqn-add :mcar mcar)))

349

350

(serapeum:-> seqn-subtract (fixnum) seqn-subtract)

351

(defun seqn-subtract (mcar)

352

(values

353

(make-instance 'seqn-subtract :mcar mcar)))

354

355

(serapeum:-> seqn-multiply (fixnum) seqn-multiply)

356

(defun seqn-multiply (mcar)

357

(values

358

(make-instance 'seqn-multiply :mcar mcar)))

359

360

(serapeum:-> seqn-divide (fixnum) seqn-divide)

361

(defun seqn-divide (mcar)

362

(values

363

(make-instance 'seqn-divide :mcar mcar)))

364

365

(serapeum:-> seqn-nat (fixnum fixnum) seqn-nat)

366

(defun seqn-nat (mcar mcadr)

367

(values

368

(make-instance 'seqn-nat :mcar mcar :mcadr mcadr)))

369

370

(serapeum:-> seqn-concat (fixnum fixnum) seqn-concat)

371

(defun seqn-concat (mcar mcadr)

372

(values

373

(make-instance 'seqn-concat :mcar mcar :mcadr mcadr)))

374

375

(serapeum:-> seqn-decompose (fixnum) seqn-decompose)

376

(defun seqn-decompose (mcar)

377

(values

378

(make-instance 'seqn-decompose :mcar mcar)))

379

380

(serapeum:-> seqn-eq (fixnum) seqn-eq)

381

(defun seqn-eq (mcar)

382

(values

383

(make-instance 'seqn-eq :mcar mcar)))

384

385

(serapeum:-> seqn-lt (fixnum) seqn-lt)

386

(defun seqn-lt (mcar)

387

(values

388

(make-instance 'seqn-lt :mcar mcar)))

389

390

(serapeum:-> seqn-mod (fixnum) seqn-mod)

391

(defun seqn-mod (mcar)

392

(values

393

(make-instance 'seqn-mod :mcar mcar)))

394

395

(make-pattern composition mcar mcadr)

396

(make-pattern id mcar)

397

(make-pattern fork-seq mcar)

398

(make-pattern drop-nil mcar)

399

(make-pattern parallel-seq mcar mcadr)

400

(make-pattern remove-right mcar)

401

(make-pattern remove-left mcar)

402

(make-pattern drop-width mcar mcadr)

403

(make-pattern inj-length-left mcar mcadr)

404

(make-pattern inj-length-right mcar mcadr)

405

(make-pattern inj-size mcar mcadr)

406

(make-pattern branch-seq mcar mcadr)

407

(make-pattern shift-front mcar mcadr)

408

(make-pattern zero-bit)

409

(make-pattern one-bit)

410

(make-pattern seqn-add)

411

(make-pattern seqn-subtract)

412

(make-pattern seqn-multiply)

413

(make-pattern seqn-divide)

414

(make-pattern seqn-nat)

415

(make-pattern seqn-concat)

416

(make-pattern seqn-decompose)

417

(make-pattern seqn-eq)

418

(make-pattern seqn-lt)

419

(make-pattern seqn-mod)

420