(*
Copyright 2008-2018 Microsoft Research
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
*)
module Part2.MerkleTreeUpdate
open FStar.String
module L = FStar.List.Tot
//Length-indexed strings
let lstring (n:nat) = s:string{String.length s == n}
//Concatenating strings sums their lengths
let concat #n #m (s0:lstring n) (s1:lstring m)
: lstring (m + n)
= FStar.String.concat_length s0 s1;
s0 ^ s1
//A parameter, lenght of the hash in characters,
//e.g., this would be 32, if a character is 1 byte
//and we're using SHA-256
assume
val hash_size:nat
//The type of a hashed value
let hash_t = lstring hash_size
//The hash function itself
assume
val hash (m:string) : hash_t
//The type of resources stored in the tree
let resource = string
//SNIPPET_END: preliminaries
// Merkle tree, indexed by the depth of the tree and hash for the
// node. All data is stored in leaves, trees are complete.
type mtree: nat -> hash_t -> Type =
| L:
res:resource ->
mtree 0 (hash res)
| N:
#n:nat ->
#hl:hash_t ->
#hr:hash_t ->
left:mtree n hl ->
right:mtree n hr ->
mtree (n + 1) (hash (concat hl hr))
// get takes a path in the tree, true goes left, false goes right
let resource_id = list bool
let rec get #h
(ri:resource_id)
(tree:mtree (L.length ri) h)
: Tot resource (decreases ri)
= match ri with
| [] -> L?.res tree
| b::ri' ->
if b then
get ri' (N?.left tree)
else
get ri' (N?.right tree)
let rec update #h
(rid:resource_id)
(res:resource)
(tree:mtree (L.length rid) h)
: Tot (h':hash_t & mtree (L.length rid) h')
= admit()