Working with fixed buffers

Stream: general

[Andrii Kurdiumov]

I do try to implement symmetric encryption algorithm in Lean4 and struggle to write code which modify fixed buffer. Here is how I do it now. I need to update things in specific places, accoring do algorithm, and Lean cannot infer Fin r0.size when working with literal.

let mut r0: Array UInt8 := mkArray 17 0
let i15 : Fin 17  := 15 -- Fin r0.size
r0 := Array.set r0 i15 key[30]!

I see 2 issues here,

• I have to introduce variable to be able put literal into Array.set
• • and I have to specify Fin 17 instead of Fin r0.size which make it less obvious to see that 17 here and in r0 are connected.

I may try to utilize

Array.set! r0 (r0.size - 2) key[30]!

but set! seems to be last resort. Maybe there libraries which try to provide nice primitives for array indexes, or fixed size arrays. I maybe was despearate enough to write my own, but I really don't enough knowledgeable for that.

[Daniel Weber]

There is docs#Batteries.Vector for fixed size arrays (as well as docs#Mathlib.Vector)

[Andrii Kurdiumov]

I would say both of the will have same issues as Array, because Vector.get use Fin n as an index. That type I would say a bit problematic for general purpose programming.

I understand that maybe I should try to reformulate algorithm in more mathy way, but I hope that maybe somebody also notice these economic issues and it was somehow solved, even in narrow cases.

[Shreyas Srinivas]

There are programming versions like get! for all these data structures

[Chris Bailey]

Andrii Kurdiumov said:

I would say both of the will have same issues as Array, because Vector.get use Fin n as an index. That type I would say a bit problematic for general purpose programming.

I understand that maybe I should try to reformulate algorithm in more mathy way, but I hope that maybe somebody also notice these economic issues and it was somehow solved, even in narrow cases.

I think the implementation of Vector in batteries does actually have the things you're asking for, here's an example in which the bounds proofs are synthesized and no local variables or explicit Fin elements are needed (and you'll get a compile-time error if the index is OOB):

import Batteries.Data.Vector.Basic
open Batteries (Vector)

abbrev BufSize : Nat := 17

def q : Vector UInt8 BufSize := Id.run do
  let mut key : Vector UInt8 BufSize := Vector.mkVector BufSize 1
  let mut r0: Vector UInt8 BufSize := Vector.mkVector BufSize 0
  r0 := r0.setN 11 key[3]
  r0 := r0.setN 15 key[4]
  let x := r0[15]
  r0 := r0.setN 1 x
  -- Will produce an error since 19 is OOB: `could not synthesize default value for parameter 'h' using tactics`
  --r0 := r0.setN 19 x
  return r0

#eval q

The APIs provided for data structures/collections frequently have more than one means of getting and setting values that do different things depending on how much proof you have or want to provide. For example, Vector has get, getN, and getD. In this case what you want is getN, which tries to synthesize the bounds check proof using get_elem_tactic.

This kind of integer indexing and bounds proof synthesis stuff got much better with get_elem_tactic. The indexing operations with xs[i] are handled by typeclasses GetElem and GetElem? that are quite smart.

[Andrii Kurdiumov]

Thank you. Now I lm enlightened. At least I see why suggestion to use batteries working. I somehow miss setN. Will try it then.